have h4 := cindex_eventually_eq_order hp
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
inst✝ : NeBot p
hU : IsOpen U
F_holo : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
F_noz : ∀ (n : ι), ∀ z ∈ U, F n z ≠ 0
F_conv : TendstoLocallyUniformlyOn F f p U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
h : ∀ᶠ (r : ℝ) in 𝓝[>] 0, ∀ z ∈ closedBall z₀ r, z ∈ {z₀}ᶜ → f z ≠ 0
pf : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f pf z₀
hh : ∃ᶠ (x : ℂ) in 𝓝 z₀, ¬f x = 0
h1 : 0 < FormalMultilinearSeries.order pf
⊢ ∃ r > 0, closedBall z₀ r ⊆ U ∧ (∀ z ∈ sphere z₀ r, f z ≠ 0) ∧ cindex z₀ r f ≠ 0
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
inst✝ : NeBot p
hU : IsOpen U
F_holo : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
F_noz : ∀ (n : ι), ∀ z ∈ U, F n z ≠ 0
F_conv : TendstoLocallyUniformlyOn F f p U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
h : ∀ᶠ (r : ℝ) in 𝓝[>] 0, ∀ z ∈ closedBall z₀ r, z ∈ {z₀}ᶜ → f z ≠ 0
pf : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f pf z₀
hh : ∃ᶠ (x : ℂ) in 𝓝 z₀, ¬f x = 0
h1 : 0 < FormalMultilinearSeries.order pf
h4 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, cindex z₀ r f = ↑(FormalMultilinearSeries.order pf)
⊢ ∃ r > 0, closedBall z₀ r ⊆ U ∧ (∀ z ∈ sphere z₀ r, f z ≠ 0) ∧ cindex z₀ r f ≠ 0