Theorem: IMOSL.IMO2021A3.iota_map_add_append_iota_eq_iota (IMOSLLean4/IMO2021/A3/A3.lean)

State before:
n k : ℕ
⊢ map n.add (iota (k + 1)) ++ iota n = iota (n + (k + 1))
Tactic:
rw [iota_succ, map_cons, cons_append]
State after:
n k : ℕ
⊢ n.add (k + 1) :: (map n.add (iota k) ++ iota n) = iota (n + (k + 1))

State before:
n k : ℕ
⊢ n.add (k + 1) :: (map n.add (iota k) ++ iota n) = iota (n + (k + 1))
Tactic:
exact congr_arg₂ _ rfl (iota_map_add_append_iota_eq_iota n k)
State after:
no goals