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

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

State before:
f : ℤ → ℤ
h : good f
a : ℤ
h0 : f^[(a + 1).natAbs ^ 2 + (-1).natAbs ^ 2] (a + 1 + -1) = (a + 1) * f (a + 1) + -1 * f (-1)
⊢ f^[(a + 1).natAbs ^ 2 + 1] a = f^[(a + 1).natAbs ^ 2] (a + 1)
Tactic:
rwa [add_neg_cancel_right, map_neg_one h,
  mul_zero, add_zero, ← map_iterate_sq h] at h0
State after:
no goals