Theorem: sum_sqr (LeanCourse/MIL/C05_Elementary_Number_Theory/solutions/Solutions_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:
symm
State after:
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
⊢ n * (n + 1) * (2 * n + 1) / 6 = ∑ i in range (n + 1), i ^ 2

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

State before:
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
⊢ n * (n + 1) * (2 * n + 1) = 6 * ∑ i in range (n + 1), i ^ 2
Tactic:
induction' n with n ih
State after:
case zero
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n : ℕ
⊢ 0 * (0 + 1) * (2 * 0 + 1) = 6 * ∑ i in range (0 + 1), i ^ 2

case succ
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
ih : n * (n + 1) * (2 * n + 1) = 6 * ∑ i in range (n + 1), i ^ 2
⊢ (n + 1) * (n + 1 + 1) * (2 * (n + 1) + 1) = 6 * ∑ i in range (n + 1 + 1), i ^ 2

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

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

State before:
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
⊢ 0 < 6
Tactic:
norm_num
State after:
no goals

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