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