congr tactic

Stream: general

[Sean Leather]

How do I know when to use the congr tactic? It's not in the Lean reference. Are there any good examples? I should've learned already, but I'm slow. :simple_smile:

[Gabriel Ebner]

As a motivating example you could try it on a + b + c = a + c + b and see what subgoals you get.

[Sean Leather]

state:
2 goals
a b c : ℕ
⊢ b = c

a b c : ℕ
⊢ c = b

[Gabriel Ebner]

With regards to the other thread: congr (and all other uses of congruence lemmas in lean such as cc and simp) skips all arguments that are have a subsingleton instance. For congr and cc this means you don't need to explicitly show that they're equal. For simp this means you can't rewrite there.

[Gabriel Ebner]

Looking back, this may have been a bad example. The point is: if you have an equality, then congr stubbornly reduces it to equalities of subterms (the topmost positions where the two sides differ, that is).