rw [hring n, ih]
case succ
n : ℕ
S : ℕ := ∑ x in Finset.range (n + 1), x
hS : S = ∑ x in Finset.range (n + 1), x
bigger : ∀ (n : ℕ), 1 ≤ n + 1
hring : ∀ (n : ℤ), (n + 1) ^ 2 + 2 * (n + 1) * ((n + 1) * (n + 1 - 1) / 2) = (n + 1) ^ 3
ih : (∑ x in Finset.range (n + 1), ↑x) ^ 2 = ∑ x in Finset.range (n + 1), ↑x ^ 3
⊢ (↑n + 1) ^ 2 + 2 * (↑n + 1) * ((↑n + 1) * (↑n + 1 - 1) / 2) + (∑ x in Finset.range (n + 1), ↑x) ^ 2 =
    (↑n + 1) ^ 3 + ∑ x in Finset.range (n + 1), ↑x ^ 3
no goals