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

State before:
n : ℕ
⊢ ∑ i ∈ Finset.range n, (i + 1) ^ 2 = n * (n + 1) * (2 * n + 1) / 6
Tactic:
rw [← sum_range_square_mul_six n, Nat.mul_div_cancel]
State after:
case H
n : ℕ
⊢ 0 < 6

State before:
case H
n : ℕ
⊢ 0 < 6
Tactic:
norm_num
State after:
no goals