have dg_nonzero : deriv g z₀ ≠ 0 := by
  have e3 := e2.differentiableAt.deriv_eq_deriv_pow_div_pow zero_lt_two f_eq_comp (f_noz hz₀)
  simp [e3, deriv_sub_const, f]
  intro h
  have := g_sqf hz₀
  rw [Pi.pow_apply, h, zero_pow two_ne_zero] at this
  cases f_noz hz₀ this
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
e1 : U ∈ 𝓝 z₀
e2 : AnalyticAt ℂ g z₀
f_eq_comp : ∀ᶠ (x : ℂ) in 𝓝 z₀, f x = (g ^ 2) x
⊢ g '' U ∈ 𝓝 (g z₀)
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
e1 : U ∈ 𝓝 z₀
e2 : AnalyticAt ℂ g z₀
f_eq_comp : ∀ᶠ (x : ℂ) in 𝓝 z₀, f x = (g ^ 2) x
dg_nonzero : deriv g z₀ ≠ 0
⊢ g '' U ∈ 𝓝 (g z₀)