rw [Finset.range_succ,
    Finset.sum_insert Finset.not_mem_range_self,
    Finset.sum_insert Finset.not_mem_range_self]
case succ
n : ℕ
ih : (∑ x in Finset.range (n + 1), x) ^ 2 = ∑ x in Finset.range (n + 1), x ^ 3
⊢ (∑ x in Finset.range (Nat.succ n + 1), x) ^ 2 = ∑ x in Finset.range (Nat.succ 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 + ∑ x in Finset.range (n + 1), x) ^ 2 = (n + 1) ^ 3 + ∑ x in Finset.range (n + 1), x ^ 3