obtain ⟨f, hf : f ∈ 𝓘 U, hfU⟩ := main (U := U)
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀ : ℂ
h1 : IsOpen U
h2 : IsConnected U
h3 : U ≠ univ
h4 : has_primitives U
this : good_domain U
⊢ ∃ f, DifferentiableOn ℂ f U ∧ InjOn f U ∧ f '' U = ball 0 1
case intro.intro
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀ : ℂ
h1 : IsOpen U
h2 : IsConnected U
h3 : U ≠ univ
h4 : has_primitives U
this : good_domain U
f : 𝓒 U
hf : f ∈ 𝓘 U
hfU : f '' U = ball 0 1
⊢ ∃ f, DifferentiableOn ℂ f U ∧ InjOn f U ∧ f '' U = ball 0 1