Lean4
/-- `congrm e` is a tactic for proving goals of the form `lhs = rhs`, `lhs ↔ rhs`, `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:
```lean
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.
-/
@[tactic_parser 1000]
public meta def congrM : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.congrM 1022
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "congrm " false✝) (ParserDescr.cat✝ `term 0))
