ring
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))
no goals