The congrm tactic

The congrm tactic ("congr with matching") is a convenient frontend for congr(...) congruence quotations. Roughly, congrm e is refine congr(e'), where e' is e with every ?m placeholder replaced by $(?m).

def Mathlib.Tactic.congrM : Lean.ParserDescr

congrm e is a tactic for proving goals of the form lhs = rhs, lhs ↔ rhs, HEq lhs rhs, or R lhs rhs when R is a reflexive relation. The expression e is a pattern containing placeholders ?_, and this pattern is matched against lhs and rhs simultaneously. These placeholders generate new goals that state that corresponding subexpressions in lhs and rhs are equal. If the placeholders have names, such as ?m, then the new goals are given tags with those names.

Examples:

example {a b c d : ℕ} :
    Nat.pred a.succ * (d + (c + a.pred)) = Nat.pred b.succ * (b + (c + d.pred)) := by
  congrm Nat.pred (Nat.succ ?h1) * (?h2 + ?h3)
  /-  Goals left:
  case h1 ⊢ a = b
  case h2 ⊢ d = b
  case h3 ⊢ c + a.pred = c + d.pred
  -/
  sorry
  sorry
  sorry

example {a b : ℕ} (h : a = b) : (fun y : ℕ => ∀ z, a + a = z) = (fun x => ∀ z, b + a = z) := by
  congrm fun x => ∀ w, ?_ + a = w
  -- ⊢ a = b
  exact h

The congrm command is a convenient frontend to congr(...) congruence quotations. If the goal is an equality, congrm e is equivalent to refine congr(e') where e' is built from e by replacing each placeholder ?m by $(?m). The pattern e is allowed to contain $(...) expressions to immediately substitute equality proofs into the congruence, just like for congruence quotations.

Equations

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