Theorem: main (RMT4/Main.lean)

State before:
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
⊢ ∃ f ∈ 𝓘 U, f '' U = ball 0 1
Tactic:
obtain ⟨z₀, hz₀⟩ : U.Nonempty := good_domain.is_nonempty
State after:
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

State before:
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
Tactic:
have hU : IsOpen U := good_domain.is_open
State after:
case intro
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
z₀ : ℂ
hz₀ : z₀ ∈ U
hU : IsOpen U
⊢ ∃ f ∈ 𝓘 U, f '' U = ball 0 1

State before:
case intro
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
z₀ : ℂ
hz₀ : z₀ ∈ U
hU : IsOpen U
⊢ ∃ f ∈ 𝓘 U, f '' U = ball 0 1
Tactic:
have hU' : IsPreconnected U := good_domain.is_preconnected
State after:
case intro
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
z₀ : ℂ
hz₀ : z₀ ∈ U
hU : IsOpen U
hU' : IsPreconnected U
⊢ ∃ f ∈ 𝓘 U, f '' U = ball 0 1

State before:
case intro
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
z₀ : ℂ
hz₀ : z₀ ∈ U
hU : IsOpen U
hU' : IsPreconnected U
⊢ ∃ f ∈ 𝓘 U, f '' U = ball 0 1
Tactic:
have h1 : ContinuousOn (obs z₀) (𝓙 U) := ((ContinuousOn_obs hU hz₀).mono (λ f hf => hf.1.1))
State after:
case 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, f '' U = ball 0 1

State before:
case 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, f '' U = ball 0 1
Tactic:
obtain ⟨f, hf, hfg⟩ := IsCompact_𝓙.exists_forall_ge (𝓘_nonempty.mono 𝓘_subset_𝓙) h1
State after:
case 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
hfg : ∀ y ∈ 𝓙 U, obs z₀ y ≤ obs z₀ f
⊢ ∃ f ∈ 𝓘 U, f '' U = ball 0 1

State before:
case 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
hfg : ∀ y ∈ 𝓙 U, obs z₀ y ≤ obs z₀ f
⊢ ∃ f ∈ 𝓘 U, f '' U = ball 0 1
Tactic:
have h7 : ¬ ∃ w, EqOn f (λ _ => w) U := by
  obtain ⟨g, hg⟩ : (𝓘 U).Nonempty := 𝓘_nonempty
  specialize hfg g (𝓘_subset_𝓙 hg)
  have := norm_pos_iff.1 ((norm_pos_iff.2 (deriv_ne_zero_of_inj hU hg.1.1 hg.2 hz₀)).trans_le hfg)
  contrapose! this
  obtain ⟨w, hw : EqOn f (λ _ => w) U⟩ := this
  simpa only [deriv_const'] using (hw.eventuallyEq_of_mem (hU.mem_nhds hz₀)).deriv_eq
State after:
case 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
hfg : ∀ y ∈ 𝓙 U, obs z₀ y ≤ obs z₀ f
h7 : ¬∃ w, EqOn f (fun x => w) U
⊢ ∃ f ∈ 𝓘 U, f '' U = ball 0 1

State before:
case 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
hfg : ∀ y ∈ 𝓙 U, obs z₀ y ≤ obs z₀ f
h7 : ¬∃ w, EqOn f (fun x => w) U
⊢ ∃ f ∈ 𝓘 U, f '' U = ball 0 1
Tactic:
have h5 : f ∈ 𝓘 U := ⟨hf.1, hf.2.resolve_right h7⟩
State after:
case 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
hfg : ∀ y ∈ 𝓙 U, obs z₀ y ≤ obs z₀ f
h7 : ¬∃ w, EqOn f (fun x => w) U
h5 : f ∈ 𝓘 U
⊢ ∃ f ∈ 𝓘 U, f '' U = ball 0 1

State before:
case 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
hfg : ∀ y ∈ 𝓙 U, obs z₀ y ≤ obs z₀ f
h7 : ¬∃ w, EqOn f (fun x => w) U
h5 : f ∈ 𝓘 U
⊢ ∃ f ∈ 𝓘 U, f '' U = ball 0 1
Tactic:
refine ⟨f, h5, ?_⟩
State after:
case 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
hfg : ∀ y ∈ 𝓙 U, obs z₀ y ≤ obs z₀ f
h7 : ¬∃ w, EqOn f (fun x => w) U
h5 : f ∈ 𝓘 U
⊢ f '' U = ball 0 1

State before:
case 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
hfg : ∀ y ∈ 𝓙 U, obs z₀ y ≤ obs z₀ f
h7 : ¬∃ w, EqOn f (fun x => w) U
h5 : f ∈ 𝓘 U
⊢ f '' U = ball 0 1
Tactic:
have h10 : f '' U ⊆ ball 0 1 := by
  have := ((hf.1.1.analyticOn hU).is_constant_or_isOpen hU').resolve_left h7 U subset_rfl hU
  simpa [interior_closedBall] using this.subset_interior_iff.2 (mapsTo'.1 hf.1.2)
State after:
case 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
hfg : ∀ y ∈ 𝓙 U, obs z₀ y ≤ obs z₀ f
h7 : ¬∃ w, EqOn f (fun x => w) U
h5 : f ∈ 𝓘 U
h10 : f '' U ⊆ ball 0 1
⊢ f '' U = ball 0 1

State before:
case 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
hfg : ∀ y ∈ 𝓙 U, obs z₀ y ≤ obs z₀ f
h7 : ¬∃ w, EqOn f (fun x => w) U
h5 : f ∈ 𝓘 U
h10 : f '' U ⊆ ball 0 1
⊢ f '' U = ball 0 1
Tactic:
refine (subset_iff_ssubset_or_eq.1 h10).resolve_left ?_
State after:
case 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
hfg : ∀ y ∈ 𝓙 U, obs z₀ y ≤ obs z₀ f
h7 : ¬∃ w, EqOn f (fun x => w) U
h5 : f ∈ 𝓘 U
h10 : f '' U ⊆ ball 0 1
⊢ ¬f '' U ⊂ ball 0 1

State before:
case 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
hfg : ∀ y ∈ 𝓙 U, obs z₀ y ≤ obs z₀ f
h7 : ¬∃ w, EqOn f (fun x => w) U
h5 : f ∈ 𝓘 U
h10 : f '' U ⊆ ball 0 1
⊢ ¬f '' U ⊂ ball 0 1
Tactic:
contrapose! hfg
State after:
case 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
⊢ ∃ y ∈ 𝓙 U, obs z₀ f < obs z₀ y

State before:
case 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
⊢ ∃ y ∈ 𝓙 U, obs z₀ f < obs z₀ y
Tactic:
obtain ⟨g, hg⟩ := step_2 U hz₀ ⟨f, hf.1.1, h5.2, mapsTo'.2 h10⟩ hfg
State after:
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

State before:
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
Tactic:
exact ⟨g.to_fun, 𝓘_subset_𝓙 ⟨⟨g.is_diff, g.maps_to.mono_right ball_subset_closedBall⟩, g.is_inj⟩, hg⟩
State after:
no goals

State before:
ι : 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
hfg : ∀ y ∈ 𝓙 U, obs z₀ y ≤ obs z₀ f
⊢ ¬∃ w, EqOn f (fun x => w) U
Tactic:
obtain ⟨g, hg⟩ : (𝓘 U).Nonempty := 𝓘_nonempty
State after:
case 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
hfg : ∀ y ∈ 𝓙 U, obs z₀ y ≤ obs z₀ f
g : 𝓒 U
hg : g ∈ 𝓘 U
⊢ ¬∃ w, EqOn f (fun x => w) U

State before:
case 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
hfg : ∀ y ∈ 𝓙 U, obs z₀ y ≤ obs z₀ f
g : 𝓒 U
hg : g ∈ 𝓘 U
⊢ ¬∃ w, EqOn f (fun x => w) U
Tactic:
specialize hfg g (𝓘_subset_𝓙 hg)
State after:
case 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
g : 𝓒 U
hg : g ∈ 𝓘 U
hfg : obs z₀ g ≤ obs z₀ f
⊢ ¬∃ w, EqOn f (fun x => w) U

State before:
case 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
g : 𝓒 U
hg : g ∈ 𝓘 U
hfg : obs z₀ g ≤ obs z₀ f
⊢ ¬∃ w, EqOn f (fun x => w) U
Tactic:
have := norm_pos_iff.1 ((norm_pos_iff.2 (deriv_ne_zero_of_inj hU hg.1.1 hg.2 hz₀)).trans_le hfg)
State after:
case 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
g : 𝓒 U
hg : g ∈ 𝓘 U
hfg : obs z₀ g ≤ obs z₀ f
this : deriv f z₀ ≠ 0
⊢ ¬∃ w, EqOn f (fun x => w) U

State before:
case 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
g : 𝓒 U
hg : g ∈ 𝓘 U
hfg : obs z₀ g ≤ obs z₀ f
this : deriv f z₀ ≠ 0
⊢ ¬∃ w, EqOn f (fun x => w) U
Tactic:
contrapose! this
State after:
case 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
g : 𝓒 U
hg : g ∈ 𝓘 U
hfg : obs z₀ g ≤ obs z₀ f
this : ∃ w, EqOn f (fun x => w) U
⊢ deriv f z₀ = 0

State before:
case 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
g : 𝓒 U
hg : g ∈ 𝓘 U
hfg : obs z₀ g ≤ obs z₀ f
this : ∃ w, EqOn f (fun x => w) U
⊢ deriv f z₀ = 0
Tactic:
obtain ⟨w, hw : EqOn f (λ _ => w) U⟩ := this
State after:
case 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
g : 𝓒 U
hg : g ∈ 𝓘 U
hfg : obs z₀ g ≤ obs z₀ f
w : ℂ
hw : EqOn f (fun x => w) U
⊢ deriv f z₀ = 0

State before:
case 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
g : 𝓒 U
hg : g ∈ 𝓘 U
hfg : obs z₀ g ≤ obs z₀ f
w : ℂ
hw : EqOn f (fun x => w) U
⊢ deriv f z₀ = 0
Tactic:
simpa only [deriv_const'] using (hw.eventuallyEq_of_mem (hU.mem_nhds hz₀)).deriv_eq
State after:
no goals

State before:
ι : 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
hfg : ∀ y ∈ 𝓙 U, obs z₀ y ≤ obs z₀ f
h7 : ¬∃ w, EqOn f (fun x => w) U
h5 : f ∈ 𝓘 U
⊢ f '' U ⊆ ball 0 1
Tactic:
have := ((hf.1.1.analyticOn hU).is_constant_or_isOpen hU').resolve_left h7 U subset_rfl hU
State after:
ι : 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
hfg : ∀ y ∈ 𝓙 U, obs z₀ y ≤ obs z₀ f
h7 : ¬∃ w, EqOn f (fun x => w) U
h5 : f ∈ 𝓘 U
this : IsOpen (f '' U)
⊢ f '' U ⊆ ball 0 1

State before:
ι : 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
hfg : ∀ y ∈ 𝓙 U, obs z₀ y ≤ obs z₀ f
h7 : ¬∃ w, EqOn f (fun x => w) U
h5 : f ∈ 𝓘 U
this : IsOpen (f '' U)
⊢ f '' U ⊆ ball 0 1
Tactic:
simpa [interior_closedBall] using this.subset_interior_iff.2 (mapsTo'.1 hf.1.2)
State after:
no goals