obtain ⟨g, g_hol, g_sqf⟩ := good_domain.has_sqrt f f_noz f_hol
case 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
⊢ Set.Nonempty (𝓘 U)
case 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
⊢ Set.Nonempty (𝓘 U)