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

State before:
n : ℕ
⊢ ∑ i ∈ Finset.range n, (↑i + 1) ^ 2 = ↑(∑ i ∈ Finset.range n, (i + 1) ^ 2)
Tactic:
norm_cast
State after:
no goals