cases' n with n
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)
h5 : 2 * ∑ x ∈ Finset.range n, x = (∑ x ∈ Finset.range n, x) * 2
⊢ n ^ 3 = n * (n - 1) * n + n ^ 2
case zero
ih : ∑ i ∈ Finset.range 0, i ^ 3 = (∑ i ∈ Finset.range 0, i) ^ 2
h1 : (∑ x ∈ Finset.range 0, x + 0) ^ 2 = (∑ x ∈ Finset.range 0, x) ^ 2 + ((2 * ∑ x ∈ Finset.range 0, x) * 0 + 0 ^ 2)
h5 : 2 * ∑ x ∈ Finset.range 0, x = (∑ x ∈ Finset.range 0, x) * 2
⊢ 0 ^ 3 = 0 * (0 - 1) * 0 + 0 ^ 2

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 + 1 - 1) * (n + 1) + (n + 1) ^ 2