Theorem: IMOSL.IMO2020A6.exists_iter_add_large_eq (IMOSLLean4/IMO2020/A6/A6.lean)

State before:
f : ℤ → ℤ
h : good f
a : ℤ
k : ℕ
⊢ ∃ N, f^[N + (k + 1)] a = f^[N] (a + ↑(k + 1))
Tactic:
rcases exists_iter_add_large_eq a k with ⟨N, h0⟩
State after:
case intro
f : ℤ → ℤ
h : good f
a : ℤ
k N : ℕ
h0 : f^[N + k] a = f^[N] (a + ↑k)
⊢ ∃ N, f^[N + (k + 1)] a = f^[N] (a + ↑(k + 1))

State before:
case intro
f : ℤ → ℤ
h : good f
a : ℤ
k N : ℕ
h0 : f^[N + k] a = f^[N] (a + ↑k)
⊢ ∃ N, f^[N + (k + 1)] a = f^[N] (a + ↑(k + 1))
Tactic:
refine ⟨N + (a + k + 1).natAbs ^ 2, ?_⟩
State after:
case intro
f : ℤ → ℤ
h : good f
a : ℤ
k N : ℕ
h0 : f^[N + k] a = f^[N] (a + ↑k)
⊢ f^[N + (a + ↑k + 1).natAbs ^ 2 + (k + 1)] a = f^[N + (a + ↑k + 1).natAbs ^ 2] (a + ↑(k + 1))

State before:
case intro
f : ℤ → ℤ
h : good f
a : ℤ
k N : ℕ
h0 : f^[N + k] a = f^[N] (a + ↑k)
⊢ f^[N + (a + ↑k + 1).natAbs ^ 2 + (k + 1)] a = f^[N + (a + ↑k + 1).natAbs ^ 2] (a + ↑(k + 1))
Tactic:
rw [f.iterate_add_apply N, Nat.cast_succ, ← add_assoc a,
  ← map_iterate_sq_add_one h, Commute.iterate_iterate_self, ← h0,
  ← iterate_add_apply, add_comm _ (N + k), add_add_add_comm]
State after:
no goals