Theorem: IMOSL.IMO2011A4.final_solution (IMOSLLean4/IMO2011/A4/A4.lean)

State before:
f g : ℕ → ℕ
⊢ (∀ (k : ℕ), f^[g k + 2] k + (g^[f k + 1] k + g (k + 1)) + 1 = f (k + 1)) ↔ f = id ∧ g = fun x => 0
Tactic:
refine Iff.symm ⟨λ h k ↦ ?_, λ h ↦ ?_⟩
State after:
case refine_1
f g : ℕ → ℕ
h : f = id ∧ g = fun x => 0
k : ℕ
⊢ f^[g k + 2] k + (g^[f k + 1] k + g (k + 1)) + 1 = f (k + 1)

case refine_2
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k + (g^[f k + 1] k + g (k + 1)) + 1 = f (k + 1)
⊢ f = id ∧ g = fun x => 0

State before:
case refine_1
f g : ℕ → ℕ
h : f = id ∧ g = fun x => 0
k : ℕ
⊢ f^[g k + 2] k + (g^[f k + 1] k + g (k + 1)) + 1 = f (k + 1)
Tactic:
rcases h with ⟨rfl, rfl⟩
State after:
case refine_1.intro
k : ℕ
⊢ id^[(fun x => 0) k + 2] k + ((fun x => 0)^[id k + 1] k + (fun x => 0) (k + 1)) + 1 = id (k + 1)

State before:
case refine_1.intro
k : ℕ
⊢ id^[(fun x => 0) k + 2] k + ((fun x => 0)^[id k + 1] k + (fun x => 0) (k + 1)) + 1 = id (k + 1)
Tactic:
rw [iterate_id, iterate_succ_apply']
State after:
case refine_1.intro
k : ℕ
⊢ id k + (0 + (fun x => 0) (k + 1)) + 1 = id (k + 1)

State before:
case refine_1.intro
k : ℕ
⊢ id k + (0 + (fun x => 0) (k + 1)) + 1 = id (k + 1)
Tactic:
rfl
State after:
no goals

State before:
case refine_2
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k + (g^[f k + 1] k + g (k + 1)) + 1 = f (k + 1)
⊢ f = id ∧ g = fun x => 0
Tactic:
obtain rfl : f = id := by
  refine main_step (g := g) (λ k ↦ ?_)
  rw [← h, Nat.lt_succ_iff]
  exact Nat.le_add_right _ _
State after:
case refine_2
g : ℕ → ℕ
h : ∀ (k : ℕ), id^[g k + 2] k + (g^[id k + 1] k + g (k + 1)) + 1 = id (k + 1)
⊢ id = id ∧ g = fun x => 0

State before:
case refine_2
g : ℕ → ℕ
h : ∀ (k : ℕ), id^[g k + 2] k + (g^[id k + 1] k + g (k + 1)) + 1 = id (k + 1)
⊢ id = id ∧ g = fun x => 0
Tactic:
refine ⟨rfl, funext λ n ↦ ?_⟩
State after:
case refine_2
g : ℕ → ℕ
h : ∀ (k : ℕ), id^[g k + 2] k + (g^[id k + 1] k + g (k + 1)) + 1 = id (k + 1)
n : ℕ
⊢ g n = 0

State before:
case refine_2
g : ℕ → ℕ
h : ∀ (k : ℕ), id^[g k + 2] k + (g^[id k + 1] k + g (k + 1)) + 1 = id (k + 1)
n : ℕ
⊢ g n = 0
Tactic:
simp_rw [iterate_id, Function.id_def, Nat.succ_inj',
  add_right_eq_self, add_eq_zero_iff] at h
State after:
case refine_2
g : ℕ → ℕ
n : ℕ
h : ∀ (k : ℕ), g^[k + 1] k = 0 ∧ g (k + 1) = 0
⊢ g n = 0

State before:
case refine_2
g : ℕ → ℕ
n : ℕ
h : ∀ (k : ℕ), g^[k + 1] k = 0 ∧ g (k + 1) = 0
⊢ g n = 0
Tactic:
rcases n with _ | n
State after:
case refine_2.zero
g : ℕ → ℕ
h : ∀ (k : ℕ), g^[k + 1] k = 0 ∧ g (k + 1) = 0
⊢ g 0 = 0

case refine_2.succ
g : ℕ → ℕ
h : ∀ (k : ℕ), g^[k + 1] k = 0 ∧ g (k + 1) = 0
n : ℕ
⊢ g (n + 1) = 0

State before:
case refine_2.zero
g : ℕ → ℕ
h : ∀ (k : ℕ), g^[k + 1] k = 0 ∧ g (k + 1) = 0
⊢ g 0 = 0

case refine_2.succ
g : ℕ → ℕ
h : ∀ (k : ℕ), g^[k + 1] k = 0 ∧ g (k + 1) = 0
n : ℕ
⊢ g (n + 1) = 0
Tactic:
exacts [(h 0).1, (h n).2]
State after:
no goals

State before:
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k + (g^[f k + 1] k + g (k + 1)) + 1 = f (k + 1)
⊢ f = id
Tactic:
refine main_step (g := g) (λ k ↦ ?_)
State after:
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k + (g^[f k + 1] k + g (k + 1)) + 1 = f (k + 1)
k : ℕ
⊢ f^[g k + 2] k < f (k + 1)

State before:
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k + (g^[f k + 1] k + g (k + 1)) + 1 = f (k + 1)
k : ℕ
⊢ f^[g k + 2] k < f (k + 1)
Tactic:
rw [← h, Nat.lt_succ_iff]
State after:
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k + (g^[f k + 1] k + g (k + 1)) + 1 = f (k + 1)
k : ℕ
⊢ f^[g k + 2] k ≤ f^[g k + 2] k + (g^[f k + 1] k + g (k + 1))

State before:
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k + (g^[f k + 1] k + g (k + 1)) + 1 = f (k + 1)
k : ℕ
⊢ f^[g k + 2] k ≤ f^[g k + 2] k + (g^[f k + 1] k + g (k + 1))
Tactic:
exact Nat.le_add_right _ _
State after:
no goals