Theorem: IMOSL.IMO2010A6.lem4 (IMOSLLean4/IMO2010/A6/A6.lean)

State before:
f g : ℕ → ℕ
h : good f g
h0 : good g f
k m : ℕ
h1 : ∃ x, f x = k
h2 : ∃ y, f y = m
h3 : f k = f m
⊢ k = m
Tactic:
rcases h1 with ⟨x, rfl⟩
State after:
case intro
f g : ℕ → ℕ
h : good f g
h0 : good g f
m : ℕ
h2 : ∃ y, f y = m
x : ℕ
h3 : f (f x) = f m
⊢ f x = m

State before:
case intro
f g : ℕ → ℕ
h : good f g
h0 : good g f
m : ℕ
h2 : ∃ y, f y = m
x : ℕ
h3 : f (f x) = f m
⊢ f x = m
Tactic:
rcases h2 with ⟨y, rfl⟩
State after:
case intro.intro
f g : ℕ → ℕ
h : good f g
h0 : good g f
x y : ℕ
h3 : f (f x) = f (f y)
⊢ f x = f y

State before:
case intro.intro
f g : ℕ → ℕ
h : good f g
h0 : good g f
x y : ℕ
h3 : f (f x) = f (f y)
⊢ f x = f y
Tactic:
replace h3 := lem2 h0 h3
State after:
case intro.intro
f g : ℕ → ℕ
h : good f g
h0 : good g f
x y : ℕ
h3 : g (f x) = g (f y)
⊢ f x = f y

State before:
case intro.intro
f g : ℕ → ℕ
h : good f g
h0 : good g f
x y : ℕ
h3 : g (f x) = g (f y)
⊢ f x = f y
Tactic:
rw [h0, h0, Nat.succ_inj'] at h3
State after:
case intro.intro
f g : ℕ → ℕ
h : good f g
h0 : good g f
x y : ℕ
h3 : g x = g y
⊢ f x = f y

State before:
case intro.intro
f g : ℕ → ℕ
h : good f g
h0 : good g f
x y : ℕ
h3 : g x = g y
⊢ f x = f y
Tactic:
exact lem2 h h3
State after:
no goals