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