rw [deriv_sub_const, hf' hz]
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₀
z : ℂ
hz : z ∈ U
⊢ deriv g z = 0 z
no goals