induction' i with i ih
case h
i : ℕ
⊢ sum (fun n => n) i = i * (i + 1) / 2
case h.zero

⊢ sum (fun n => n) Nat.zero = Nat.zero * (Nat.zero + 1) / 2

case h.succ
i : ℕ
ih : sum (fun n => n) i = i * (i + 1) / 2
⊢ sum (fun n => n) (Nat.succ i) = Nat.succ i * (Nat.succ i + 1) / 2