induction' n with n ih
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
⊢ n * (n + 1) * (2 * n + 1) = 6 * ∑ i ∈ range (n + 1), i ^ 2
case zero
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n : ℕ
⊢ 0 * (0 + 1) * (2 * 0 + 1) = 6 * ∑ i ∈ range (0 + 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) = 6 * ∑ i ∈ range (n + 1 + 1), i ^ 2