case neg => simp at h; simp [h]
ι : 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