simpa [h4, order_eq_zero_iff hp h2] using h3.frequently.filter_mono nhdsWithin_le_nhds
case h
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p✝ : Filter ι
r✝ : ℝ
U : Set ℂ
h2 : f z₀ = 0
h3 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ 0
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f p z₀
r : ℝ
h4 : cindex z₀ r f = ↑(FormalMultilinearSeries.order p)
⊢ cindex z₀ r f ≠ 0
no goals