filter_upwards [cindex_eventually_eq_order hp] with r h4
case intro
ι : 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 : ℝ) in 𝓝[>] 0, cindex z₀ r f ≠ 0
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