induction' n with n ih
n : ℕ
⊢ (∑ x in Finset.range (n + 1), x) ^ 2 = ∑ x in Finset.range (n + 1), x ^ 3
case zero

⊢ (∑ x in Finset.range (Nat.zero + 1), x) ^ 2 = ∑ x in Finset.range (Nat.zero + 1), x ^ 3

case succ
n : ℕ
ih : (∑ x in Finset.range (n + 1), x) ^ 2 = ∑ x in Finset.range (n + 1), x ^ 3
⊢ (∑ x in Finset.range (Nat.succ n + 1), x) ^ 2 = ∑ x in Finset.range (Nat.succ n + 1), x ^ 3