simp [ih, show Nat.succ i = i + 1 from rfl]
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))
case h.succ
i : ℕ
ih : sum (fun i => 3 * (i ^ 2 + i) + 1) i = (i + 1) * ((i + 1) * (i + 1))
⊢ (i + 1) * ((i + 1) * (i + 1)) + (3 * ((i + 1) ^ 2 + (i + 1)) + 1) = (i + 1 + 1) * ((i + 1 + 1) * (i + 1 + 1))