induction' n with n ih
n : ℕ
⊢ ∑ i ∈ Finset.range n, i ^ 3 = (∑ i ∈ Finset.range n, i) ^ 2
case zero

⊢ ∑ i ∈ Finset.range 0, i ^ 3 = (∑ i ∈ Finset.range 0, i) ^ 2

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