refine u_not_in_f_U ⟨z, z_in_U, ?_⟩
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
z : ℂ
z_in_U : z ∈ U
hz : φᵤf.to_fun z = 0
⊢ False
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
z : ℂ
z_in_U : z ∈ U
hz : φᵤf.to_fun z = 0
⊢ f.to_fun z = u