# 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)`

.

`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.