have gU_nhd : g '' U ∈ 𝓝 (g z₀) := by
  have e1 : U ∈ 𝓝 z₀ := good_domain.is_open.mem_nhds hz₀
  have e2 := g_hol.analyticAt e1
  have f_eq_comp := (good_domain.is_open.eventually_mem hz₀).mono g_sqf
  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
  refine e2.eventually_constant_or_nhds_le_map_nhds.resolve_left (λ h => ?_) (image_mem_map e1)
  simp [EventuallyEq.deriv_eq h] at dg_nonzero
case intro.intro.intro.intro
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
⊢ Set.Nonempty (𝓘 U)
case intro.intro.intro.intro
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₀)
⊢ Set.Nonempty (𝓘 U)