case pos =>
  have H1 := (hf.differentiableOn hF hU).analyticAt (hU.mem_nhds hz₀)
  have H5 := cindex_pos H1 h1 h2
  rw [eventually_nhdsWithin_iff] at h2
  have h3 := eventually_nhds_iff_eventually_closed_ball.1 h2
  have h4 : ∀ᶠ r in 𝓝[>] 0, closedBall z₀ r ⊆ U :=
    (eventually_closedBall_subset (hU.mem_nhds hz₀)).filter_mono nhdsWithin_le_nhds
  have h4' : ∀ᶠ r in 𝓝[>] 0, closedBall z₀ r ⊆ s :=
    (eventually_closedBall_subset hs).filter_mono nhdsWithin_le_nhds
  obtain ⟨r, hr, h5, h6, h7, h9⟩ := (h3.and (h4.and (H5.and h4'))).exists'
  have h8 : ∀ z ∈ sphere z₀ r, f z ≠ 0 := by
    exact λ z hz => h5 z (sphere_subset_closedBall hz) (ne_of_mem_sphere hz hr.lt.ne.symm)
  refine (hurwitz2 hU hF hf hr h6 h8 h7).mono ?_
  rintro n ⟨z, hz, hFnz⟩
  refine ⟨z, h9 (ball_subset_closedBall hz), hFnz⟩
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U s : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hz₀ : z₀ ∈ U
h1 : f z₀ = 0
h2 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ 0
hs : s ∈ 𝓝 z₀
h : NeBot p
⊢ ∀ᶠ (n : ι) in p, ∃ z ∈ s, F n z = 0
no goals