obtain ⟨z₀, h1, h2⟩ : ∃ z₀ ∈ U, ∃ᶠ z in 𝓝[≠] z₀, f z = 0 := by 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
⊢ EqOn f 0 U
case intro.intro
ι : 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₀ : ℂ
h1 : z₀ ∈ U
h2 : ∃ᶠ (z : ℂ) in 𝓝[≠] z₀, f z = 0
⊢ EqOn f 0 U