have h1 : ((∑ x ∈ Finset.range n, x) + n) ^ 2 =
    ((∑ x ∈ Finset.range n, x))^2 +
       (2 * (∑ x ∈ Finset.range n, x) * n +
         n ^ 2) := by ring
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
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)
⊢ (∑ i ∈ Finset.range n, i) ^ 2 + n ^ 3 = (∑ x ∈ Finset.range n, x + n) ^ 2