simpa [not_forall] using h
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
hf : DifferentiableOn ℂ f U
h : ¬∀ z₀ ∈ U, ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ 0
⊢ ∃ z₀ ∈ U, ∃ᶠ (z : ℂ) in 𝓝[≠] z₀, f z = 0
no goals