exact ⟨g.to_fun, 𝓘_subset_𝓙 ⟨⟨g.is_diff, g.maps_to.mono_right ball_subset_closedBall⟩, g.is_inj⟩, hg⟩
case intro.intro.intro.intro
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
z₀ : ℂ
hz₀ : z₀ ∈ U
hU : IsOpen U
hU' : IsPreconnected U
h1 : ContinuousOn (obs z₀) (𝓙 U)
f : 𝓒 U
hf : f ∈ 𝓙 U
h7 : ¬∃ w, EqOn f (fun x => w) U
h5 : f ∈ 𝓘 U
h10 : f '' U ⊆ ball 0 1
hfg : f '' U ⊂ ball 0 1
g : embedding U 𝔻
hg : ‖deriv { to_fun := f, is_diff := ⋯, is_inj := ⋯, maps_to := ⋯ }.to_fun z₀‖ < ‖deriv g.to_fun z₀‖
⊢ ∃ y ∈ 𝓙 U, obs z₀ f < obs z₀ y
no goals