Theorem: MvPowerSeries.StronglySummable.not_mem_unionOfSupportOfCoeffLe_iff (DividedPowers/ForMathlib/MvPowerSeries/StronglySummable/Basic.lean)

State before:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : DecidableEq ι
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
i : ι
⊢ i ∉ hf.unionOfSupportOfCoeffLe d ↔ ∀ e ≤ d, (coeff α e) (f i) = 0
Tactic:
simp only [unionOfSupportOfCoeffLe, Finset.mem_biUnion, Finset.mem_Iic, Finite.mem_toFinset,
  mem_support, not_exists, ne_eq, not_and, not_not]
State after:
no goals