suffices h : ∀ z ∈ ball z₀ r, fderivWithin ℂ f (ball z₀ r) z = 0
  by exact (convex_ball z₀ r).is_const_of_fderivWithin_eq_zero (hf.mono hrU) h hz (mem_ball_self hr)
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
z : ℂ
hz : dist z z₀ < r
⊢ f z = f z₀
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
z : ℂ
hz : dist z z₀ < r
⊢ ∀ z ∈ ball z₀ r, fderivWithin ℂ f (ball z₀ r) z = 0