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

State before:
n : ℕ
l : List ℕ
h : l.length = n.succ
k : ℕ
⊢ targetSum (map n.add (iota (k + 1)) ++ l) = targetSum l
Tactic:
rw [iota_succ, map_cons, cons_append, targetSum, length_cons,
  targetSum_map_add_iota_length_succ h k, Nat.add_eq_right]
State after:
n : ℕ
l : List ℕ
h : l.length = n.succ
k : ℕ
⊢ n.add (k + 1) / (map n.add (iota k) ++ l).length.succ = 0

State before:
n : ℕ
l : List ℕ
h : l.length = n.succ
k : ℕ
⊢ n.add (k + 1) / (map n.add (iota k) ++ l).length.succ = 0
Tactic:
refine Nat.div_eq_of_lt ?_
State after:
n : ℕ
l : List ℕ
h : l.length = n.succ
k : ℕ
⊢ n.add (k + 1) < (map n.add (iota k) ++ l).length.succ

State before:
n : ℕ
l : List ℕ
h : l.length = n.succ
k : ℕ
⊢ n.add (k + 1) < (map n.add (iota k) ++ l).length.succ
Tactic:
rw [length_append, length_map, length_iota, h]
State after:
n : ℕ
l : List ℕ
h : l.length = n.succ
k : ℕ
⊢ n.add (k + 1) < (k + n.succ).succ