rw [add_sq]
case succ
n : ℕ
ih : (∑ x in Finset.range (n + 1), x) ^ 2 = ∑ x in Finset.range (n + 1), x ^ 3
⊢ (n + 1 + ∑ x in Finset.range (n + 1), x) ^ 2 = (n + 1) ^ 3 + ∑ x in Finset.range (n + 1), x ^ 3
case succ
n : ℕ
ih : (∑ x in Finset.range (n + 1), x) ^ 2 = ∑ x in Finset.range (n + 1), x ^ 3
⊢ (n + 1) ^ 2 + 2 * (n + 1) * ∑ x in Finset.range (n + 1), x + (∑ x in Finset.range (n + 1), x) ^ 2 =
    (n + 1) ^ 3 + ∑ x in Finset.range (n + 1), x ^ 3