Theorem: sum_sqr (LeanCourse/MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean)

State before:
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
⊢ ∑ i in range (n + 1), i ^ 2 = n * (n + 1) * (2 * n + 1) / 6
Tactic:
sorry
State after:
no goals