have h2 : EqOn (deriv (λ y => f y - g y)) 0 U := by
  rintro z hz
  have e1 : U ∈ 𝓝 z := hU.mem_nhds hz
  rw [deriv_sub (hf.differentiableAt e1) (hg.differentiableAt e1), hfg hz, sub_self]
  rfl
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
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
h2 : EqOn (deriv fun y => f y - g y) 0 U
⊢ f z - g z = 0