by_cases h : NeBot p
ι : 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 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))
case pos
ι : 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 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))

case neg
ι : 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 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : ¬NeBot p
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))