obtain ⟨r, hr, hrU⟩ := nhds_basis_ball.mem_iff.1 (hU.mem_nhds hz₀)
z z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
⊢ f =ᶠ[𝓝 z₀] 0
case intro.intro
z z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
r : ℝ
hr : 0 < r
hrU : ball z₀ r ⊆ U
⊢ f =ᶠ[𝓝 z₀] 0