omega
case succ
n : ℕ
ih : ∑ i ∈ Finset.range n, i ^ 3 = (∑ i ∈ Finset.range n, i) ^ 2
h1 : (∑ x ∈ Finset.range n, x + n) ^ 2 = (∑ x ∈ Finset.range n, x) ^ 2 + ((2 * ∑ x ∈ Finset.range n, x) * n + n ^ 2)
h2 : n ^ 3 = (2 * ∑ x ∈ Finset.range n, x) * n + n ^ 2
⊢ (∑ i ∈ Finset.range n, i) ^ 2 + n ^ 3 = (∑ x ∈ Finset.range n, x) ^ 2 + ((2 * ∑ x ∈ Finset.range n, x) * n + n ^ 2)
no goals