rw [Finset.sum_range_id]
case succ
n : ℕ
ih : (∑ x in Finset.range (n + 1), x) ^ 2 = ∑ x in Finset.range (n + 1), x ^ 3
S : ℕ := ∑ x in Finset.range (n + 1), x
hS : S = ∑ x in Finset.range (n + 1), x
bigger : ∀ (n : ℕ), 1 ≤ n + 1
⊢ (n + 1) ^ 2 + 2 * (n + 1) * ∑ x in Finset.range (n + 1), x + S ^ 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
S : ℕ := ∑ x in Finset.range (n + 1), x
hS : S = ∑ x in Finset.range (n + 1), x
bigger : ∀ (n : ℕ), 1 ≤ n + 1
⊢ (n + 1) ^ 2 + 2 * (n + 1) * ((n + 1) * (n + 1 - 1) / 2) + S ^ 2 = (n + 1) ^ 3 + ∑ x in Finset.range (n + 1), x ^ 3