Theorem: MvPowerSeries.degree_eq_zero_iff (DividedPowers/ForMathlib/MvPowerSeries/Order.lean)

State before:
σ : Type u_1
α : Type ?u.66556
inst✝ : Semiring α
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ degree d = 0 ↔ d = 0
Tactic:
simp only [degree, weight, one_mul, AddMonoidHom.coe_mk, Finsupp.sum, Finset.sum_eq_zero_iff,
  Finsupp.mem_support_iff, _root_.not_imp_self, DFunLike.ext_iff, Finsupp.coe_zero, Pi.zero_apply,
  ZeroHom.coe_mk, Finset.sum_eq_zero_iff, Finsupp.mem_support_iff, ne_eq]
State after:
no goals