exact h2.eqOn_zero_of_preconnected_of_eventuallyEq_zero hU' hz₀ this
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
inst✝ : NeBot p
hU : IsOpen U
hU' : IsPreconnected U
F_holo : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
F_noz : ∀ (n : ι), ∀ z ∈ U, F n z ≠ 0
F_conv : TendstoLocallyUniformlyOn F f p U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
this : ∀ᶠ (z : ℂ) in 𝓝 z₀, f z = 0
h1 : DifferentiableOn ℂ f U
h2 : AnalyticOn ℂ f U
⊢ ∀ z ∈ U, f z = 0
no goals