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

State before:
a b : ℤ
⊢ (fun x => x + 1)^[a.natAbs ^ 2 + b.natAbs ^ 2] (a + b) = a * (fun x => x + 1) a + b * (fun x => x + 1) b
Tactic:
have h (c : ℤ) : c + ((c.natAbs ^ 2 : ℕ) : ℤ) = c * (c + 1) := by
  rw [Int.natCast_pow, Int.natAbs_sq, sq, ← mul_one_add, add_comm]
State after:
a b : ℤ
h : ∀ (c : ℤ), c + ↑(c.natAbs ^ 2) = c * (c + 1)
⊢ (fun x => x + 1)^[a.natAbs ^ 2 + b.natAbs ^ 2] (a + b) = a * (fun x => x + 1) a + b * (fun x => x + 1) b

State before:
a b : ℤ
h : ∀ (c : ℤ), c + ↑(c.natAbs ^ 2) = c * (c + 1)
⊢ (fun x => x + 1)^[a.natAbs ^ 2 + b.natAbs ^ 2] (a + b) = a * (fun x => x + 1) a + b * (fun x => x + 1) b
Tactic:
rw [add_one_iterate, Int.ofNat_add, add_add_add_comm, h, h]
State after:
no goals

State before:
a b c : ℤ
⊢ c + ↑(c.natAbs ^ 2) = c * (c + 1)
Tactic:
rw [Int.natCast_pow, Int.natAbs_sq, sq, ← mul_one_add, add_comm]
State after:
no goals