Theorem: IMOSL.IMO2013A5.map_add_four (IMOSLLean4/IMO2013/A5/A5.lean)

State before:
f : ℕ → ℕ
h : good f
n : ℕ
⊢ f (n + 4) = f n + 4
Tactic:
have h1 := iter_four_eq_add_four h
State after:
f : ℕ → ℕ
h : good f
n : ℕ
h1 : ∀ (n : ℕ), f^[4] n = n + 4
⊢ f (n + 4) = f n + 4

State before:
f : ℕ → ℕ
h : good f
n : ℕ
h1 : ∀ (n : ℕ), f^[4] n = n + 4
⊢ f (n + 4) = f n + 4
Tactic:
rw [← h1, ← h1]
State after:
f : ℕ → ℕ
h : good f
n : ℕ
h1 : ∀ (n : ℕ), f^[4] n = n + 4
⊢ f (f^[4] n) = f^[4] (f n)

State before:
f : ℕ → ℕ
h : good f
n : ℕ
h1 : ∀ (n : ℕ), f^[4] n = n + 4
⊢ f (f^[4] n) = f^[4] (f n)
Tactic:
rfl
State after:
no goals