Theorem: Hungary1998P6.sum_range_square_mul_six (Compfiles/Hungary1998P6.lean)

State before:
n : ℕ
⊢ (∑ i ∈ Finset.range n, (i + 1) ^ 2) * 6 = n * (n + 1) * (2 * n + 1)
Tactic:
induction n with
| zero => rfl
| succ n ih =>
  rw [Finset.sum_range_succ, add_mul, ih]
  ring
State after:
no goals

State before:
case zero

⊢ (∑ i ∈ Finset.range 0, (i + 1) ^ 2) * 6 = 0 * (0 + 1) * (2 * 0 + 1)
Tactic:
rfl
State after:
no goals

State before:
case succ
n : ℕ
ih : (∑ i ∈ Finset.range n, (i + 1) ^ 2) * 6 = n * (n + 1) * (2 * n + 1)
⊢ (∑ i ∈ Finset.range (n + 1), (i + 1) ^ 2) * 6 = (n + 1) * (n + 1 + 1) * (2 * (n + 1) + 1)
Tactic:
rw [Finset.sum_range_succ, add_mul, ih]
State after:
case succ
n : ℕ
ih : (∑ i ∈ Finset.range n, (i + 1) ^ 2) * 6 = n * (n + 1) * (2 * n + 1)
⊢ n * (n + 1) * (2 * n + 1) + (n + 1) ^ 2 * 6 = (n + 1) * (n + 1 + 1) * (2 * (n + 1) + 1)

State before:
case succ
n : ℕ
ih : (∑ i ∈ Finset.range n, (i + 1) ^ 2) * 6 = n * (n + 1) * (2 * n + 1)
⊢ n * (n + 1) * (2 * n + 1) + (n + 1) ^ 2 * 6 = (n + 1) * (n + 1 + 1) * (2 * (n + 1) + 1)
Tactic:
ring
State after:
no goals