obtain ⟨z₀, hz₀⟩ : U.Nonempty := good_domain.is_nonempty
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
⊢ ∃ f ∈ 𝓘 U, f '' U = ball 0 1
case intro
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
z₀ : ℂ
hz₀ : z₀ ∈ U
⊢ ∃ f ∈ 𝓘 U, f '' U = ball 0 1