apply Nat.div_eq_of_eq_mul_right (by norm_num : 0 < 6)
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
⊢ n * (n + 1) * (2 * n + 1) / 6 = ∑ i ∈ range (n + 1), i ^ 2
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
⊢ n * (n + 1) * (2 * n + 1) = 6 * ∑ i ∈ range (n + 1), i ^ 2