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

⊢ sum (fun i => i * 2 + 1) Nat.zero = (Nat.zero + 1) ^ 2

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