rw [Pi.zero_apply, ← hfz₀]
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 = 0 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
⊢ f z = f z₀