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

State before:
f : ℤ → ℤ
h : good f
a : ℤ
⊢ f^[a.natAbs ^ 2] a = a * f a
Tactic:
have h := h a 0
State after:
f : ℤ → ℤ
h✝ : good f
a : ℤ
h : f^[a.natAbs ^ 2 + Int.natAbs 0 ^ 2] (a + 0) = a * f a + 0 * f 0
⊢ f^[a.natAbs ^ 2] a = a * f a

State before:
f : ℤ → ℤ
h✝ : good f
a : ℤ
h : f^[a.natAbs ^ 2 + Int.natAbs 0 ^ 2] (a + 0) = a * f a + 0 * f 0
⊢ f^[a.natAbs ^ 2] a = a * f a
Tactic:
rwa [zero_mul, add_zero, add_zero] at h
State after:
no goals