Theorem: RMT (RMT4/Main.lean)

State before:
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀ : ℂ
h1 : IsOpen U
h2 : IsConnected U
h3 : U ≠ univ
h4 : has_primitives U
⊢ ∃ f, DifferentiableOn ℂ f U ∧ InjOn f U ∧ f '' U = ball 0 1
Tactic:
have : good_domain U := ⟨h1, h2.1, h2.2, h3, (h4.has_logs h1 h2.isPreconnected).has_sqrt⟩
State after:
ι : 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

State before:
ι : 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
Tactic:
obtain ⟨f, hf : f ∈ 𝓘 U, hfU⟩ := main (U := U)
State after:
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

State before:
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
Tactic:
exact ⟨f, hf.1.1, hf.2, hfU⟩
State after:
no goals