simp only [Nat.zero_eq, add_zero, Finset.range_one, Finset.sum_singleton, ne_eq,
  OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow']
case zero

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