Theorem: IsCompact_𝓙 (RMT4/Main.lean)

State before:
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
⊢ IsCompact (𝓙 U)
Tactic:
have hU : IsOpen U := good_domain.is_open
State after:
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
⊢ IsCompact (𝓙 U)

State before:
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
⊢ IsCompact (𝓙 U)
Tactic:
refine (isCompact_𝓜 hU).of_isClosed_subset ?_ (λ _ hf => hf.1)
State after:
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
⊢ IsClosed (𝓙 U)

State before:
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
⊢ IsClosed (𝓙 U)
Tactic:
refine isClosed_iff_clusterPt.2 (λ f hf => ?_)
State after:
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
⊢ f ∈ 𝓙 U

State before:
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
⊢ f ∈ 𝓙 U
Tactic:
set l := 𝓝 f ⊓ 𝓟 (𝓙 U)
State after:
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
⊢ f ∈ 𝓙 U

State before:
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
⊢ f ∈ 𝓙 U
Tactic:
haveI : l.NeBot := hf
State after:
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this : NeBot l
⊢ f ∈ 𝓙 U

State before:
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this : NeBot l
⊢ f ∈ 𝓙 U
Tactic:
obtain ⟨h1, h2⟩ := tendsto_inf.1 (@tendsto_id _ l)
State after:
case intro
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this : NeBot l
h1 : Tendsto id l (𝓝 f)
h2 : Tendsto id l (𝓟 (𝓙 U))
⊢ f ∈ 𝓙 U

State before:
case intro
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this : NeBot l
h1 : Tendsto id l (𝓝 f)
h2 : Tendsto id l (𝓟 (𝓙 U))
⊢ f ∈ 𝓙 U
Tactic:
rw [tendsto_principal] at h2
State after:
case intro
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this : NeBot l
h1 : Tendsto id l (𝓝 f)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
⊢ f ∈ 𝓙 U

State before:
case intro
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this : NeBot l
h1 : Tendsto id l (𝓝 f)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
⊢ f ∈ 𝓙 U
Tactic:
refine ⟨(IsClosed_𝓜 hU).mem_of_tendsto h1 (h2.mono (λ _ h => h.1)), ?_⟩
State after:
case intro
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this : NeBot l
h1 : Tendsto id l (𝓝 f)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
⊢ InjOn f U ∨ ∃ w, EqOn f (fun x => w) U

State before:
case intro
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this : NeBot l
h1 : Tendsto id l (𝓝 f)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
⊢ InjOn f U ∨ ∃ w, EqOn f (fun x => w) U
Tactic:
by_cases h : ∃ᶠ f in l, InjOn f U
State after:
case pos
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this : NeBot l
h1 : Tendsto id l (𝓝 f)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
h : ∃ᶠ (f : ℂ → ℂ) in l, InjOn f U
⊢ InjOn f U ∨ ∃ w, EqOn f (fun x => w) U

case neg
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this : NeBot l
h1 : Tendsto id l (𝓝 f)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
h : ¬∃ᶠ (f : ℂ → ℂ) in l, InjOn f U
⊢ InjOn f U ∨ ∃ w, EqOn f (fun x => w) U

State before:
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this : NeBot l
h1 : Tendsto id l (𝓝 f)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
h : ∃ᶠ (f : ℂ → ℂ) in l, InjOn f U
⊢ InjOn f U ∨ ∃ w, EqOn f (fun x => w) U
Tactic:
case pos =>
  refine (hurwitz_inj hU good_domain.is_preconnected ?_ ((tendsto_𝓒_iff hU).1 h1) h).symm
  filter_upwards [h2] with g hg using hg.1.1
State after:
no goals

State before:
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this : NeBot l
h1 : Tendsto id l (𝓝 f)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
h : ¬∃ᶠ (f : ℂ → ℂ) in l, InjOn f U
⊢ InjOn f U ∨ ∃ w, EqOn f (fun x => w) U
Tactic:
case neg =>
  obtain ⟨z₀, hz₀⟩ : U.Nonempty := good_domain.is_nonempty
  have : ∀ z ∈ U, Tendsto (eval z) l (𝓝 (f z)) := by
    refine λ z hz => (map_mono inf_le_left).trans ?_
    exact ((UniformOnFun.uniformContinuous_eval_of_mem ℂ (compacts U)
      (mem_singleton z) ⟨singleton_subset_iff.2 hz, isCompact_singleton⟩).continuous).tendsto f
  refine Or.inr ⟨f z₀, λ z hz => tendsto_nhds_unique ((this z hz).congr' ?_) (this z₀ hz₀)⟩
  filter_upwards [not_frequently.1 h, h2] with f hf1 hf2
  obtain ⟨w, hw⟩ := hf2.2.resolve_left hf1
  exact (hw hz).trans (hw hz₀).symm
State after:
no goals

State before:
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this : NeBot l
h1 : Tendsto id l (𝓝 f)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
h : ∃ᶠ (f : ℂ → ℂ) in l, InjOn f U
⊢ InjOn f U ∨ ∃ w, EqOn f (fun x => w) U
Tactic:
refine (hurwitz_inj hU good_domain.is_preconnected ?_ ((tendsto_𝓒_iff hU).1 h1) h).symm
State after:
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this : NeBot l
h1 : Tendsto id l (𝓝 f)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
h : ∃ᶠ (f : ℂ → ℂ) in l, InjOn f U
⊢ ∀ᶠ (n : 𝓒 U) in l, DifferentiableOn ℂ (id n) U

State before:
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this : NeBot l
h1 : Tendsto id l (𝓝 f)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
h : ∃ᶠ (f : ℂ → ℂ) in l, InjOn f U
⊢ ∀ᶠ (n : 𝓒 U) in l, DifferentiableOn ℂ (id n) U
Tactic:
filter_upwards [h2] with g hg using hg.1.1
State after:
no goals

State before:
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this : NeBot l
h1 : Tendsto id l (𝓝 f)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
h : ¬∃ᶠ (f : ℂ → ℂ) in l, InjOn f U
⊢ InjOn f U ∨ ∃ w, EqOn f (fun x => w) U
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
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this : NeBot l
h1 : Tendsto id l (𝓝 f)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
h : ¬∃ᶠ (f : ℂ → ℂ) in l, InjOn f U
z₀ : ℂ
hz₀ : z₀ ∈ U
⊢ InjOn f U ∨ ∃ w, EqOn f (fun x => w) U

State before:
case intro
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this : NeBot l
h1 : Tendsto id l (𝓝 f)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
h : ¬∃ᶠ (f : ℂ → ℂ) in l, InjOn f U
z₀ : ℂ
hz₀ : z₀ ∈ U
⊢ InjOn f U ∨ ∃ w, EqOn f (fun x => w) U
Tactic:
have : ∀ z ∈ U, Tendsto (eval z) l (𝓝 (f z)) := by
  refine λ z hz => (map_mono inf_le_left).trans ?_
  exact ((UniformOnFun.uniformContinuous_eval_of_mem ℂ (compacts U)
    (mem_singleton z) ⟨singleton_subset_iff.2 hz, isCompact_singleton⟩).continuous).tendsto f
State after:
case intro
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this✝ : NeBot l
h1 : Tendsto id l (𝓝 f)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
h : ¬∃ᶠ (f : ℂ → ℂ) in l, InjOn f U
z₀ : ℂ
hz₀ : z₀ ∈ U
this : ∀ z ∈ U, Tendsto (eval z) l (𝓝 (f z))
⊢ InjOn f U ∨ ∃ w, EqOn f (fun x => w) U

State before:
case intro
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this✝ : NeBot l
h1 : Tendsto id l (𝓝 f)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
h : ¬∃ᶠ (f : ℂ → ℂ) in l, InjOn f U
z₀ : ℂ
hz₀ : z₀ ∈ U
this : ∀ z ∈ U, Tendsto (eval z) l (𝓝 (f z))
⊢ InjOn f U ∨ ∃ w, EqOn f (fun x => w) U
Tactic:
refine Or.inr ⟨f z₀, λ z hz => tendsto_nhds_unique ((this z hz).congr' ?_) (this z₀ hz₀)⟩
State after:
case intro
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this✝ : NeBot l
h1 : Tendsto id l (𝓝 f)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
h : ¬∃ᶠ (f : ℂ → ℂ) in l, InjOn f U
z₀ : ℂ
hz₀ : z₀ ∈ U
this : ∀ z ∈ U, Tendsto (eval z) l (𝓝 (f z))
z : ℂ
hz : z ∈ U
⊢ eval z =ᶠ[l] eval z₀

State before:
case intro
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this✝ : NeBot l
h1 : Tendsto id l (𝓝 f)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
h : ¬∃ᶠ (f : ℂ → ℂ) in l, InjOn f U
z₀ : ℂ
hz₀ : z₀ ∈ U
this : ∀ z ∈ U, Tendsto (eval z) l (𝓝 (f z))
z : ℂ
hz : z ∈ U
⊢ eval z =ᶠ[l] eval z₀
Tactic:
filter_upwards [not_frequently.1 h, h2] with f hf1 hf2
State after:
case h
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f✝ : 𝓒 U
hf : ClusterPt f✝ (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f✝ ⊓ 𝓟 (𝓙 U)
this✝ : NeBot l
h1 : Tendsto id l (𝓝 f✝)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
h : ¬∃ᶠ (f : ℂ → ℂ) in l, InjOn f U
z₀ : ℂ
hz₀ : z₀ ∈ U
this : ∀ z ∈ U, Tendsto (eval z) l (𝓝 (f✝ z))
z : ℂ
hz : z ∈ U
f : ℂ → ℂ
hf1 : ¬InjOn f U
hf2 : f ∈ {x | id x ∈ 𝓙 U}
⊢ eval z f = eval z₀ f

State before:
case h
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f✝ : 𝓒 U
hf : ClusterPt f✝ (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f✝ ⊓ 𝓟 (𝓙 U)
this✝ : NeBot l
h1 : Tendsto id l (𝓝 f✝)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
h : ¬∃ᶠ (f : ℂ → ℂ) in l, InjOn f U
z₀ : ℂ
hz₀ : z₀ ∈ U
this : ∀ z ∈ U, Tendsto (eval z) l (𝓝 (f✝ z))
z : ℂ
hz : z ∈ U
f : ℂ → ℂ
hf1 : ¬InjOn f U
hf2 : f ∈ {x | id x ∈ 𝓙 U}
⊢ eval z f = eval z₀ f
Tactic:
obtain ⟨w, hw⟩ := hf2.2.resolve_left hf1
State after:
case h.intro
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f✝ : 𝓒 U
hf : ClusterPt f✝ (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f✝ ⊓ 𝓟 (𝓙 U)
this✝ : NeBot l
h1 : Tendsto id l (𝓝 f✝)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
h : ¬∃ᶠ (f : ℂ → ℂ) in l, InjOn f U
z₀ : ℂ
hz₀ : z₀ ∈ U
this : ∀ z ∈ U, Tendsto (eval z) l (𝓝 (f✝ z))
z : ℂ
hz : z ∈ U
f : ℂ → ℂ
hf1 : ¬InjOn f U
hf2 : f ∈ {x | id x ∈ 𝓙 U}
w : ℂ
hw : EqOn (id f) (fun x => w) U
⊢ eval z f = eval z₀ f

State before:
case h.intro
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f✝ : 𝓒 U
hf : ClusterPt f✝ (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f✝ ⊓ 𝓟 (𝓙 U)
this✝ : NeBot l
h1 : Tendsto id l (𝓝 f✝)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
h : ¬∃ᶠ (f : ℂ → ℂ) in l, InjOn f U
z₀ : ℂ
hz₀ : z₀ ∈ U
this : ∀ z ∈ U, Tendsto (eval z) l (𝓝 (f✝ z))
z : ℂ
hz : z ∈ U
f : ℂ → ℂ
hf1 : ¬InjOn f U
hf2 : f ∈ {x | id x ∈ 𝓙 U}
w : ℂ
hw : EqOn (id f) (fun x => w) U
⊢ eval z f = eval z₀ f
Tactic:
exact (hw hz).trans (hw hz₀).symm
State after:
no goals

State before:
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this : NeBot l
h1 : Tendsto id l (𝓝 f)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
h : ¬∃ᶠ (f : ℂ → ℂ) in l, InjOn f U
z₀ : ℂ
hz₀ : z₀ ∈ U
⊢ ∀ z ∈ U, Tendsto (eval z) l (𝓝 (f z))
Tactic:
refine λ z hz => (map_mono inf_le_left).trans ?_
State after:
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this : NeBot l
h1 : Tendsto id l (𝓝 f)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
h : ¬∃ᶠ (f : ℂ → ℂ) in l, InjOn f U
z₀ : ℂ
hz₀ : z₀ ∈ U
z : ℂ
hz : z ∈ U
⊢ map (eval z) (𝓝 f) ≤ 𝓝 (f z)

State before:
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this : NeBot l
h1 : Tendsto id l (𝓝 f)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
h : ¬∃ᶠ (f : ℂ → ℂ) in l, InjOn f U
z₀ : ℂ
hz₀ : z₀ ∈ U
z : ℂ
hz : z ∈ U
⊢ map (eval z) (𝓝 f) ≤ 𝓝 (f z)
Tactic:
exact ((UniformOnFun.uniformContinuous_eval_of_mem ℂ (compacts U)
  (mem_singleton z) ⟨singleton_subset_iff.2 hz, isCompact_singleton⟩).continuous).tendsto f
State after:
no goals