have h3 : g z₀ = 0 := by simp [g]
z z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
g : ℂ → ℂ := fun z => f z - f z₀
h2 : EqOn (deriv g) 0 U
⊢ EqOn f (fun x => f z₀) U
z z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
g : ℂ → ℂ := fun z => f z - f z₀
h2 : EqOn (deriv g) 0 U
h3 : g z₀ = 0
⊢ EqOn f (fun x => f z₀) U