Theorem: LSeries.pow_mul_term_eq (EulerProducts/LSeriesUnique.lean)

State before:
f : ℕ → ℂ
s : ℂ
n : ℕ
⊢ (↑n + 1) ^ s * term f s (n + 1) = f (n + 1)
Tactic:
simp only [term, add_eq_zero, one_ne_zero, and_false, ↓reduceIte, Nat.cast_add, Nat.cast_one,
  mul_div_assoc', ne_eq, cpow_natCast_add_one_ne_zero n _, not_false_eq_true, div_eq_iff,
  mul_comm (f _)]
State after:
no goals