congr

1import Mathlib.Tactic.Congr
2
3-- congr breaks down equality goals by congruence
4example (a b : Nat) (h : a = b) : a + 1 = b + 1 := by
5  congr
6  -- Reduces to: a = b
7  -- Automatically solved by exact h
8
9example (f : Nat → Nat) (a b : Nat) (h : a = b) : f a = f b := by
10  congr

1import Mathlib.Tactic.Congr
2
3-- congr handles multiple arguments
4example (a b c d : Nat) (h1 : a = c) (h2 : b = d) : a + b = c + d := by
5  congr
6  · exact h1  -- prove a = c
7  · exact h2  -- prove b = d
8
9-- With lists
10example (x y : Nat) (xs ys : List Nat) (hx : x = y) (hxs : xs = ys) : 
11    x :: xs = y :: ys := by
12  congr

1import Mathlib.Tactic.Congr
2
3-- congr n applies congruence n levels deep
4example (a b : Nat) (h : a = b) : (a + 1) * 2 = (b + 1) * 2 := by
5  congr 1
6  -- Only descends one level: a + 1 = b + 1
7
8example (a b : Nat) (h : a = b) : (a + 1) * 2 = (b + 1) * 2 := by
9  congr 2
10  -- Descends two levels: a = b

1import Mathlib.Tactic.Congr
2
3-- congr works with structure constructors
4example (a b c d : Nat) (h1 : a = c) (h2 : b = d) : (a, b) = (c, d) := by
5  congr
6
7-- Nested structures
8example (a b c d : Nat) (h1 : a = c) (h2 : b = d) : 
9    ((a, b), 0) = ((c, d), 0) := by
10  congr
11  congr

1import Mathlib.Tactic.GCongr
2
3-- gcongr handles inequalities and relations, not just equality
4example (a b c d : Nat) (h1 : a ≤ c) (h2 : b ≤ d) : a + b ≤ c + d := by
5  gcongr
6
7example (a b : Nat) (h : a ≤ b) : 2 * a ≤ 2 * b := by
8  gcongr

1import Mathlib.Tactic.Congr
2
3-- Sometimes congr creates subgoals you need to prove
4example (n m : Nat) (h : n = m) : n.succ = m.succ := by
5  congr
6
7-- congr might create impossible subgoals if misused
8-- example (a b c : Nat) : a + b = a + c := by
9--   congr  -- Creates goal b = c, which may not be provable!

1-- Core Lean has congrArg and congrFun lemmas
2
3-- congrArg: f a = f b from a = b
4example (f : Nat → Nat) (a b : Nat) (h : a = b) : f a = f b :=
5  congrArg f h
6
7-- congrFun: f x = g x from f = g
8example (f g : Nat → Nat) (h : f = g) (x : Nat) : f x = g x :=
9  congrFun h x
10
11-- These are the building blocks congr uses

1import Mathlib.Tactic.Congr
2
3-- Proving that mapped lists are equal
4example (f : Nat → Nat) (xs ys : List Nat) (h : xs = ys) : 
5    xs.map f = ys.map f := by
6  congr

1import Mathlib.Tactic.Congr
2
3-- Breaking down complex arithmetic
4example (a b c : Nat) (h : a = b) : a * c + a = b * c + b := by
5  congr 1
6  · congr 1
7    exact h
8  · exact h

1import Mathlib.Tactic.GCongr
2
3-- Monotonicity proofs
4example (a b c : Nat) (hab : a ≤ b) (hc : c > 0) : a * c ≤ b * c := by
5  gcongr
6
7example (a b : Nat) (h : a ≤ b) : a + 5 ≤ b + 5 := by
8  gcongr

1import Mathlib.Tactic.Congr
2
3-- simp rewrites using lemmas
4-- congr breaks down by structure
5
6-- congr is useful when:
7-- 1. You need to prove parts are equal separately
8-- 2. simp doesn't know the relevant lemmas
9-- 3. You want fine-grained control
10
11example (a b : Nat) (h : a = b) : [a, 1, 2] = [b, 1, 2] := by
12  congr  -- Immediately reduces to a = b

1import Mathlib.Tactic.Congr
2
3-- Pattern: Prove outer structure matches, then inner
4example (f g : Nat → Nat) (x y : Nat) 
5    (hf : f = g) (hx : x = y) : f x = g y := by
6  rw [hf, hx]
7
8-- Alternative with congr
9example (f : Nat → Nat) (x y : Nat) (h : x = y) : f x = f y := by
10  congr
11
12-- Pattern: Focus on the differing part
13example (a b c : Nat) (h : b = c) : a + b + 1 = a + c + 1 := by
14  congr 2  -- Descend to b = c