case t => exact 𝔻
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hz₀ : z₀ ∈ U
f : embedding U 𝔻
hf : f.to_fun '' U ⊂ 𝔻
u : ℂ
u_in_𝔻 : u ∈ 𝔻
u_not_in_f_U : u ∉ f.to_fun '' U
φᵤ : embedding 𝔻 𝔻 := φ u_in_𝔻
φᵤf : embedding U 𝔻 := embedding.comp φᵤ f
φᵤf_ne_zero : ∀ z ∈ U, φᵤf.to_fun z ≠ 0
g : embedding U 𝔻
hg : EqOn φᵤf.to_fun (g.to_fun ^ 2) U
v : ℂ := g.to_fun z₀
v_in_𝔻 : v ∈ 𝔻
h : embedding U 𝔻 := embedding.comp (φ v_in_𝔻) g
h_z₀_eq_0 : h.to_fun z₀ = 0
σ : ℂ → ℂ := fun z => z ^ 2
ψ : ℂ → ℂ := (φ ⋯).to_fun ∘ σ ∘ (φ ⋯).to_fun
f_eq_ψ_h : EqOn f.to_fun (ψ ∘ h.to_fun) U
⊢ Set ℂ
no goals