exact (hf.analyticOn hU).eqOn_zero_of_preconnected_of_frequently_eq_zero hU' h1 h2
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
no goals