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

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

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