have h4 : DifferentiableOn ℂ f (ball z₀ ε) := λ z hz => (h hz).1.differentiableWithinAt
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
hf : AnalyticAt ℂ f z₀
hf' : HasFPowerSeriesAt (deriv f) 0 z₀
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ε : ℝ
hε : ε > 0
h : ball z₀ ε ⊆ {x | (fun x => AnalyticAt ℂ f x ∧ deriv f x = 0) x}
z : ℂ
hz : z ∈ ball z₀ ε
h3 : ∀ z ∈ ball z₀ ε, fderivWithin ℂ f (ball z₀ ε) z = 0
⊢ z ∈ {x | (fun z => f z = f z₀) x}
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
hf : AnalyticAt ℂ f z₀
hf' : HasFPowerSeriesAt (deriv f) 0 z₀
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ε : ℝ
hε : ε > 0
h : ball z₀ ε ⊆ {x | (fun x => AnalyticAt ℂ f x ∧ deriv f x = 0) x}
z : ℂ
hz : z ∈ ball z₀ ε
h3 : ∀ z ∈ ball z₀ ε, fderivWithin ℂ f (ball z₀ ε) z = 0
h4 : DifferentiableOn ℂ f (ball z₀ ε)
⊢ z ∈ {x | (fun z => f z = f z₀) x}