refine λ z hz => sub_eq_zero.1 ?_
z z₀ : ℂ
U : Set ℂ
f g : ℂ → ℂ
hU : IsOpen U
hU' : IsPreconnected U
hf : DifferentiableOn ℂ f U
hg : DifferentiableOn ℂ g U
hfg : EqOn (deriv f) (deriv g) U
hz₀ : z₀ ∈ U
hfgz₀ : f z₀ = g z₀
⊢ EqOn f g U
z✝ z₀ : ℂ
U : Set ℂ
f g : ℂ → ℂ
hU : IsOpen U
hU' : IsPreconnected U
hf : DifferentiableOn ℂ f U
hg : DifferentiableOn ℂ g U
hfg : EqOn (deriv f) (deriv g) U
hz₀ : z₀ ∈ U
hfgz₀ : f z₀ = g z₀
z : ℂ
hz : z ∈ U
⊢ f z - g z = 0