case pos =>
  have H1 : IsCompact (sphere z₀ r) := isCompact_sphere z₀ r
  have H2 : sphere z₀ r ⊆ U := sphere_subset_closedBall.trans hr2
  have H3 : TendstoUniformlyOn F f p (sphere z₀ r) :=
    (tendstoLocallyUniformlyOn_iff_forall_isCompact hU).1 hf _ H2 H1
  have H4 : ContinuousOn f (sphere z₀ r) :=
    (hf.differentiableOn hF hU).continuousOn.mono H2
  have H5 : ∀ᶠ n in p, ∀ z ∈ sphere z₀ r, F n z ≠ 0 := hurwitz2_1 H1 H3 H4 hf1
  filter_upwards [(hurwitz2_2 hU hF hf hr1 H2 hf1).eventually_ne hf2, H5, hF] with n h h' hF
  contrapose! h
  have : ∀ (z : ℂ), z ∈ ball z₀ r ∪ sphere z₀ r → F n z ≠ 0 := λ z hz => hz.casesOn (h z) (h' z)
  refine cindex_eq_zero hU hr1 hr2 hF (by rwa [← ball_union_sphere])
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : closedBall z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
hf2 : cindex z₀ r f ≠ 0
h : NeBot p
⊢ ∀ᶠ (n : ι) in p, ∃ z ∈ ball z₀ r, F n z = 0
no goals