simp [g_sqf _, hz₁, hz₂, hgz]
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
gU_nhd : g '' U ∈ 𝓝 (g z₀)
r : ℝ
r_pos : r > 0
hr : ball (g z₀) r ⊆ g '' U
z₁ : ℂ
hz₁ : z₁ ∈ U
z₂ : ℂ
hz₂ : z₂ ∈ U
hgz : g z₁ = g z₂
⊢ f z₁ = f z₂
no goals