rw [Finset.sum_range_succ, mul_add 6, ← ih]
case succ
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
ih : n * (n + 1) * (2 * n + 1) = 6 * ∑ i ∈ range (n + 1), i ^ 2
⊢ (n + 1) * (n + 1 + 1) * (2 * (n + 1) + 1) = 6 * ∑ i ∈ range (n + 1 + 1), i ^ 2
case succ
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
ih : n * (n + 1) * (2 * n + 1) = 6 * ∑ i ∈ range (n + 1), i ^ 2
⊢ (n + 1) * (n + 1 + 1) * (2 * (n + 1) + 1) = n * (n + 1) * (2 * n + 1) + 6 * (n + 1) ^ 2