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

State before:
n : ℕ
a : ℤ
⊢ (fun x => x + 1)^[n + 1] a = a + ↑(n + 1)
Tactic:
rw [iterate_succ_apply', add_one_iterate n a, add_assoc]
State after:
n : ℕ
a : ℤ
⊢ a + (↑n + 1) = a + ↑(n + 1)

State before:
n : ℕ
a : ℤ
⊢ a + (↑n + 1) = a + ↑(n + 1)
Tactic:
rfl
State after:
no goals