have : ∀ (z : ℂ), z ∈ ball z₀ r ∪ sphere z₀ r → F n z ≠ 0 := λ z hz => hz.casesOn (h z) (h' z)
case h
ι : 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
H1 : IsCompact (sphere z₀ r)
H2 : sphere z₀ r ⊆ U
H3 : TendstoUniformlyOn F f p (sphere z₀ r)
H4 : ContinuousOn f (sphere z₀ r)
H5 : ∀ᶠ (n : ι) in p, ∀ z ∈ sphere z₀ r, F n z ≠ 0
n : ι
h' : ∀ z ∈ sphere z₀ r, F n z ≠ 0
hF : DifferentiableOn ℂ (F n) U
h : ∀ z ∈ ball z₀ r, F n z ≠ 0
⊢ (cindex z₀ r ∘ fun n => F n) n = 0
case h
ι : 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
H1 : IsCompact (sphere z₀ r)
H2 : sphere z₀ r ⊆ U
H3 : TendstoUniformlyOn F f p (sphere z₀ r)
H4 : ContinuousOn f (sphere z₀ r)
H5 : ∀ᶠ (n : ι) in p, ∀ z ∈ sphere z₀ r, F n z ≠ 0
n : ι
h' : ∀ z ∈ sphere z₀ r, F n z ≠ 0
hF : DifferentiableOn ℂ (F n) U
h : ∀ z ∈ ball z₀ r, F n z ≠ 0
this : ∀ z ∈ ball z₀ r ∪ sphere z₀ r, F n z ≠ 0
⊢ (cindex z₀ r ∘ fun n => F n) n = 0