Local avgOver congruence tactic

This opt-in proof helper peels equality goals headed by the project-local MIPStarRE.LDT.avgOver by first trying avgOver_congr, introducing the averaged variable, and recursing through nested averages. When a using tactic asks it to close the leaf and the plain route cannot do so, it backtracks to the support-restricted theorem avgOver_congr_on_support, introduces both the averaged variable and its support membership hypothesis, and retries the same leaf logic. At non-average leaves it tries an optional user-supplied tactic first, then rfl and simp, and finally leaves an unclosed leaf goal for the following tactic only after at least one average has been peeled.

Usage patterns:

• avg_congr recursively descends through avgOver goals and closes definitional or simplifiable leaves.
• avg_congr with x, u names the introduced average variables before leaving the final leaf goal; the comma-separated with list is variadic.
• avg_congr using tac additionally tries tac at every leaf before the default closers; placeholders such as _ are often enough when the introduced variables need not be named. If the plain pointwise route does not close, the tactic retries with avgOver_congr_on_support, so tac may use the introduced support membership hypothesis; with x it is named hx when that name is available, and it can always be found by type with by assumption or ‹_›.

The tactic is intentionally conservative: it registers no global simp rules and first tries the existing avgOver_congr theorem. With a using tactic, the support-restricted theorem avgOver_congr_on_support is used only as a backtracking fallback when the plain route cannot close the resulting leaf.

def avgCongr : Lean.ParserDescr

Recursively peel avgOver equality goals with optional leaf tactics.

Equations

• One or more equations did not get rendered due to their size.

def evalAvgCongr : Lean.Elab.Tactic.Tactic

Elaborator for the avg_congr tactic syntax.

Equations

• One or more equations did not get rendered due to their size.