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
z : ℂ
hz : z ∈ U
e1 : U ∈ 𝓝 z
⊢ 0 = 0 z
no goals