rintro z hz
ι : 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₀ ε
⊢ ∀ z ∈ ball z₀ ε, fderivWithin ℂ f (ball z₀ ε) z = 0
ι : 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₀ ε
z : ℂ
hz : z ∈ ball z₀ ε
⊢ fderivWithin ℂ f (ball z₀ ε) z = 0