awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
s : Set α
a' : α
ha' : a' ∈ s
ha : IsLUB s a'
h : ∀ᶠ (x : α) in 𝓝[≤] a', ¬(fun (x : α) ↦ x ∈ s) x
⊢ False

Tactic:
exact h.self_of_nhdsWithin le_rfl ha'

Premises used: Filter.Eventually.self_of_nhdsWithin, le_rfl
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
a' : α
ha' : a' ∈ s
h : ∀ᶠ (x : α) in 𝓝[≤] a, ¬(fun (x : α) ↦ x ∈ s) x
ha'a : a' < a
inr : ∀ (b : α) (hba : b ∈ Iio a) (hb : Ioc b a ⊆ {x : α | (fun (x : α) ↦ ¬(fun (x : α) ↦ x ∈ s) x) x}), False
⊢ False

Tactic:
rcases (mem_nhdsLE_iff_exists_Ioc_subset' ha'a).1 h with ⟨b, hba, hb⟩

Premises used: mem_nhdsLE_iff_exists_Ioc_subset', Iff.mp
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
a' : α
ha' : a' ∈ s
h : ∀ᶠ (x : α) in 𝓝[≤] a, ¬(fun (x : α) ↦ x ∈ s) x
ha'a : a' < a
b : α
hba : b ∈ Iio a
hb : Ioc b a ⊆ {x : α | (fun (x : α) ↦ ¬(fun (x : α) ↦ x ∈ s) x) x}
inr : ∀ (b' : α) (hb's : b' ∈ s) (hb' : b < b' ∧ b' ≤ a), False
⊢ False

Tactic:
rcases ha.exists_between hba with ⟨b', hb's, hb'⟩

Premises used: IsLUB.exists_between
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
a' : α
ha' : a' ∈ s
h : ∀ᶠ (x : α) in 𝓝[≤] a, ¬(fun (x : α) ↦ x ∈ s) x
ha'a : a' < a
b : α
hba : b ∈ Iio a
hb : Ioc b a ⊆ {x : α | (fun (x : α) ↦ ¬(fun (x : α) ↦ x ∈ s) x) x}
b' : α
hb's : b' ∈ s
hb' : b < b' ∧ b' ≤ a
⊢ False

Tactic:
hb hb' hb's
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
a' : α
ha' : a' ∈ s
h : ∀ᶠ (x : α) in 𝓝[≤] a, ¬(fun (x : α) ↦ x ∈ s) x
ha'a : a' < a
b : α
hba : b ∈ Iio a
hb : Ioc b a ⊆ {x : α | (fun (x : α) ↦ ¬(fun (x : α) ↦ x ∈ s) x) x}
b' : α
hb's : b' ∈ s
hb' : b < b' ∧ b' ≤ a
⊢ False

Tactic:
exact hb hb' hb's
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
hs : s.Nonempty
⊢ ∃ᶠ (x : α) in 𝓝 a, x ∈ s

Tactic:
(ha.frequently_mem hs).filter_mono inf_le_left

Premises used: Filter.Frequently.filter_mono, inf_le_left, IsLUB.frequently_mem
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
ha : IsGLB s a
hs : s.Nonempty
⊢ ∃ᶠ (x : α) in 𝓝[≥] a, x ∈ s

Tactic:
IsLUB.frequently_mem (α := αᵒᵈ) ha hs

Premises used: Set.Ici, Set.Mem, setOf, OrderDual, IsLUB.frequently_mem
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
ha : IsGLB s a
hs : s.Nonempty
⊢ ∃ᶠ (x : α) in 𝓝 a, x ∈ s

Tactic:
(ha.frequently_mem hs).filter_mono inf_le_left

Premises used: Filter.Frequently.filter_mono, IsGLB.frequently_mem, inf_le_left
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
hs : s.Nonempty
⊢ a ∈ closure[inst] s

Tactic:
(ha.frequently_nhds_mem hs).mem_closure

Premises used: IsLUB.frequently_nhds_mem, Filter.Frequently.mem_closure
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
ha : IsGLB s a
hs : s.Nonempty
⊢ a ∈ closure[inst] s

Tactic:
(ha.frequently_nhds_mem hs).mem_closure

Premises used: IsGLB.frequently_nhds_mem, Filter.Frequently.mem_closure
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
hs : s.Nonempty
⊢ (𝓝[s] a).NeBot

Tactic:
mem_closure_iff_nhdsWithin_neBot.1 (ha.mem_closure hs)

Premises used: mem_closure_iff_nhdsWithin_neBot, IsLUB.mem_closure, Iff.mp
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
ha : IsGLB s a
hs : s.Nonempty
⊢ (𝓝[s] a).NeBot

Tactic:
IsLUB.nhdsWithin_neBot (α := αᵒᵈ) ha hs

Premises used: IsLUB.nhdsWithin_neBot, OrderDual
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
s : Set α
a : α
f : Filter α
hsa : a ∈ upperBounds s
hsf : s ∈ f
inst_3 : (f ⊓ 𝓝 a).NeBot
⊢ IsLUB s a

Tactic:
⟨hsa, fun b hb =>
    not_lt.1 fun hba =>
      have : s ∩ { a | b < a } ∈ f ⊓ 𝓝 a := inter_mem_inf hsf (IsOpen.mem_nhds (isOpen_lt' _) hba)
      let ⟨_x, ⟨hxs, hxb⟩⟩ := Filter.nonempty_of_mem this
      have : b < b := lt_of_lt_of_le hxb <| hb hxs
      lt_irrefl b this⟩

Premises used: False, lt_irrefl, Filter.inter_mem_inf, _private.0.isLUB_of_mem_nhds.match_1, Filter.nonempty_of_mem, IsLeast, not_lt, And.intro, IsOpen.mem_nhds, IsLUB, Iff.mp, isOpen_lt', lt_of_lt_of_le
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
s : Set α
a : α
hsa : a ∈ upperBounds s
hsf : a ∈ closure[inst] s
⊢ (𝓟 s ⊓ 𝓝 a).NeBot

Tactic:
rw [mem_closure_iff_clusterPt, ClusterPt, inf_comm] at hsf

Premises used: mem_closure_iff_clusterPt, inf_comm, ClusterPt
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
s : Set α
a : α
hsa : a ∈ upperBounds s
hsf : (𝓟 s ⊓ 𝓝 a).NeBot
⊢ IsLUB s a

Tactic:
isLUB_of_mem_nhds hsa (mem_principal_self s)

Premises used: Filter.mem_principal_self, isLUB_of_mem_nhds
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
s : Set α
a : α
hsa : a ∈ upperBounds s
hsf : (𝓟 s ⊓ 𝓝 a).NeBot
⊢ IsLUB s a

Tactic:
exact isLUB_of_mem_nhds hsa (mem_principal_self s)

Premises used: Filter.mem_principal_self, isLUB_of_mem_nhds
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
s : Set α
a : α
f : Filter α
hsa : a ∈ lowerBounds s
hsf : s ∈ f
inst_3 : (f ⊓ 𝓝 a).NeBot
⊢ IsGLB s a

Tactic:
isLUB_of_mem_nhds (α := αᵒᵈ) hsa hsf

Premises used: lowerBounds, Set.Mem, setOf, upperBounds, isLUB_of_mem_nhds, IsGreatest, IsGLB, OrderDual
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
s : Set α
a : α
hsa : a ∈ lowerBounds s
hsf : a ∈ closure[inst] s
⊢ IsGLB s a

Tactic:
isLUB_of_mem_closure (α := αᵒᵈ) hsa hsf

Premises used: lowerBounds, Set.Mem, setOf, upperBounds, IsGreatest, IsGLB, OrderDual, isLUB_of_mem_closure
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : Preorder γ
inst_4 : TopologicalSpace γ
inst_5 : OrderClosedTopology γ
f : α → γ
s : Set α
a : α
b : γ
hf : MonotoneOn f s
ha : IsLUB s a
hb : Tendsto f (𝓝[s] a) (𝓝 b)
x : α
hx : x ∈ s
⊢ IsLUB (s ∩ Ici x) a

Tactic:
replace ha := ha.inter_Ici_of_mem hx
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : Preorder γ
inst_4 : TopologicalSpace γ
inst_5 : OrderClosedTopology γ
f : α → γ
s : Set α
a : α
b : γ
hf : MonotoneOn f s
hb : Tendsto f (𝓝[s] a) (𝓝 b)
x : α
hx : x ∈ s
ha : IsLUB (s ∩ Ici x) a
⊢ (𝓝[s ∩ Ici x] a).NeBot

Tactic:
haveI := ha.nhdsWithin_neBot ⟨x, hx, le_rfl⟩
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : Preorder γ
inst_4 : TopologicalSpace γ
inst_5 : OrderClosedTopology γ
f : α → γ
s : Set α
a : α
b : γ
hf : MonotoneOn f s
hb : Tendsto f (𝓝[s] a) (𝓝 b)
x : α
hx : x ∈ s
ha : IsLUB (s ∩ Ici x) a
this : (𝓝[s ∩ Ici x] a).NeBot
⊢ f x ≤ b

Tactic:
ge_of_tendsto (hb.mono_left (nhdsWithin_mono a (inter_subset_left (t := Ici x)))) ?_

Premises used: ge_of_tendsto, Set.inter_subset_left, Filter.Tendsto.mono_left, nhdsWithin_mono
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : Preorder γ
inst_4 : TopologicalSpace γ
inst_5 : OrderClosedTopology γ
f : α → γ
s : Set α
a : α
b : γ
hf : MonotoneOn f s
hb : Tendsto f (𝓝[s] a) (𝓝 b)
x : α
hx : x ∈ s
ha : IsLUB (s ∩ Ici x) a
this : (𝓝[s ∩ Ici x] a).NeBot
refine : ∀ᶠ (c : α) in 𝓝[s ∩ Ici x] a, f x ≤ f c
⊢ f x ≤ b

Tactic:
refine ge_of_tendsto (hb.mono_left (nhdsWithin_mono a (inter_subset_left (t := Ici x)))) ?_

Premises used: ge_of_tendsto, Set.inter_subset_left, Filter.Tendsto.mono_left, nhdsWithin_mono
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : Preorder γ
inst_4 : TopologicalSpace γ
inst_5 : OrderClosedTopology γ
f : α → γ
s : Set α
a : α
b : γ
hf : MonotoneOn f s
hb : Tendsto f (𝓝[s] a) (𝓝 b)
x : α
hx : x ∈ s
ha : IsLUB (s ∩ Ici x) a
this : (𝓝[s ∩ Ici x] a).NeBot
⊢ ∀ᶠ (c : α) in 𝓝[s ∩ Ici x] a, f x ≤ f c

Tactic:
mem_of_superset self_mem_nhdsWithin fun y hy => hf hx hy.1 hy.2

Premises used: Filter.Eventually, And.right, self_mem_nhdsWithin, And.left, Filter.mem_of_superset
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : Preorder γ
inst_4 : TopologicalSpace γ
inst_5 : OrderClosedTopology γ
f : α → γ
s : Set α
a : α
b : γ
hf : MonotoneOn f s
hb : Tendsto f (𝓝[s] a) (𝓝 b)
x : α
hx : x ∈ s
ha : IsLUB (s ∩ Ici x) a
this : (𝓝[s ∩ Ici x] a).NeBot
⊢ ∀ᶠ (c : α) in 𝓝[s ∩ Ici x] a, f x ≤ f c

Tactic:
exact mem_of_superset self_mem_nhdsWithin fun y hy => hf hx hy.1 hy.2

Premises used: self_mem_nhdsWithin, Filter.mem_of_superset
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : Preorder γ
inst_4 : TopologicalSpace γ
inst_5 : OrderClosedTopology γ
f : α → γ
s : Set α
a : α
b : γ
hf : MonotoneOn f s
ha : IsLUB s a
hs : s.Nonempty
hb : Tendsto f (𝓝[s] a) (𝓝 b)
⊢ IsLUB (f '' s) b

Tactic:
haveI := ha.nhdsWithin_neBot hs
  ⟨ha.mem_upperBounds_of_tendsto hf hb, fun _b' hb' =>
    le_of_tendsto hb (mem_of_superset self_mem_nhdsWithin fun _ hx => hb' <| mem_image_of_mem _ hx)⟩

Premises used: le_of_tendsto, IsLeast, self_mem_nhdsWithin, Set.mem_image_of_mem, And.intro, IsLUB, IsLUB.mem_upperBounds_of_tendsto, Filter.mem_of_superset
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : Preorder γ
inst_4 : TopologicalSpace γ
inst_5 : OrderClosedTopology γ
f : α → γ
s : Set α
a : α
b : γ
hf : MonotoneOn f s
ha : IsGLB s a
hb : Tendsto f (𝓝[s] a) (𝓝 b)
⊢ b ∈ lowerBounds (f '' s)

Tactic:
IsLUB.mem_upperBounds_of_tendsto (α := αᵒᵈ) (γ := γᵒᵈ) hf.dual ha hb

Premises used: lowerBounds, Set.Mem, setOf, MonotoneOn.dual, OrderDual, IsLUB.mem_upperBounds_of_tendsto
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : Preorder γ
inst_4 : TopologicalSpace γ
inst_5 : OrderClosedTopology γ
f : α → γ
s : Set α
a : α
b : γ
hf : MonotoneOn f s
⊢ IsGLB s a → s.Nonempty → Tendsto f (𝓝[s] a) (𝓝 b) → IsGLB (f '' s) b

Tactic:
IsLUB.isLUB_of_tendsto (α := αᵒᵈ) (γ := γᵒᵈ) hf.dual

Premises used: lowerBounds, Set.Mem, setOf, upperBounds, MonotoneOn.dual, IsGreatest, IsGLB, IsLUB.isLUB_of_tendsto, OrderDual
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : Preorder γ
inst_4 : TopologicalSpace γ
inst_5 : OrderClosedTopology γ
f : α → γ
s : Set α
a : α
b : γ
hf : AntitoneOn f s
ha : IsLUB s a
hb : Tendsto f (𝓝[s] a) (𝓝 b)
⊢ b ∈ lowerBounds (f '' s)

Tactic:
IsLUB.mem_upperBounds_of_tendsto (γ := γᵒᵈ) hf ha hb

Premises used: lowerBounds, Set.Mem, setOf, OrderDual, IsLUB.mem_upperBounds_of_tendsto
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : Preorder γ
inst_4 : TopologicalSpace γ
inst_5 : OrderClosedTopology γ
f : α → γ
s : Set α
a : α
b : γ
hf : AntitoneOn f s
ha : IsLUB s a
hs : s.Nonempty
hb : Tendsto f (𝓝[s] a) (𝓝 b)
⊢ IsGLB (f '' s) b

Tactic:
IsLUB.isLUB_of_tendsto (γ := γᵒᵈ) hf ha hs hb

Premises used: lowerBounds, Set.Mem, setOf, upperBounds, IsGreatest, IsGLB, IsLUB.isLUB_of_tendsto, OrderDual
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : Preorder γ
inst_4 : TopologicalSpace γ
inst_5 : OrderClosedTopology γ
f : α → γ
s : Set α
a : α
b : γ
hf : AntitoneOn f s
ha : IsGLB s a
hb : Tendsto f (𝓝[s] a) (𝓝 b)
⊢ b ∈ upperBounds (f '' s)

Tactic:
IsGLB.mem_lowerBounds_of_tendsto (γ := γᵒᵈ) hf ha hb

Premises used: IsGLB.mem_lowerBounds_of_tendsto, Set.Mem, setOf, upperBounds, OrderDual
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : Preorder γ
inst_4 : TopologicalSpace γ
inst_5 : OrderClosedTopology γ
f : α → γ
s : Set α
a : α
b : γ
hf : AntitoneOn f s
ha : IsGLB s a
hs : s.Nonempty
hb : Tendsto f (𝓝[s] a) (𝓝 b)
⊢ IsLUB (f '' s) b

Tactic:
IsGLB.isGLB_of_tendsto (γ := γᵒᵈ) hf ha hs hb

Premises used: lowerBounds, Set.Mem, setOf, upperBounds, IsGLB.isGLB_of_tendsto, IsLeast, IsLUB, OrderDual
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
hs : s.Nonempty
sc : IsClosed[inst] s
⊢ a ∈ s

Tactic:
sc.closure_subset <| ha.mem_closure hs

Premises used: IsLUB.mem_closure, IsClosed.closure_subset
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
ha : IsGLB s a
hs : s.Nonempty
sc : IsClosed[inst] s
⊢ a ∈ s

Tactic:
sc.closure_subset <| ha.mem_closure hs

Premises used: IsGLB.mem_closure, IsClosed.closure_subset
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : ClosedIicTopology α
s t : Set α
hst : s ⊆ t
hts : t ⊆ closure[inst] s
x : α
⊢ IsLUB s x ↔ IsLUB t x

Tactic:
isLUB_congr <| (upperBounds_closure (s := s) ▸ upperBounds_mono_set hts).antisymm <|
    upperBounds_mono_set hst

Premises used: isLUB_congr
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : ClosedIciTopology α
s t : Set α
hst : s ⊆ t
hts : t ⊆ closure[inst] s
x : α
⊢ IsGLB s x ↔ IsGLB t x

Tactic:
isLUB_iff_of_subset_of_subset_closure (α := αᵒᵈ) hst hts

Premises used: lowerBounds, Set.Mem, setOf, isLUB_iff_of_subset_of_subset_closure, upperBounds, IsGreatest, IsGLB, OrderDual
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : ClosedIicTopology α
s t : Set α
hs : Dense s
ht : IsOpen[inst] t
x : α
⊢ t ∩ s ⊆ t

Tactic:
simp
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : ClosedIciTopology α
s t : Set α
hs : Dense s
ht : IsOpen[inst] t
x : α
⊢ IsGLB (t ∩ s) x ↔ IsGLB t x

Tactic:
hs.isLUB_inter_iff (α := αᵒᵈ) ht

Premises used: lowerBounds, Set.Mem, setOf, upperBounds, IsGreatest, IsGLB, OrderDual, Dense.isLUB_inter_iff
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
γ : Type u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : ClosedIicTopology α
f : γ → α
inst_3 : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst_3, inst] f
⊢ upperBounds (f '' S) = upperBounds (range f)

Tactic:
subset_antisymm ?_ fun _ => upperBounds_mono (Set.image_subset_range f S) le_rfl

Premises used: le_rfl, upperBounds_mono, Set.image_subset_range, subset_antisymm
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
γ : Type u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : ClosedIicTopology α
f : γ → α
inst_3 : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst_3, inst] f
refine : upperBounds (f '' S) ⊆ upperBounds (range f)
⊢ upperBounds (f '' S) = upperBounds (range f)

Tactic:
refine subset_antisymm ?_ fun _ => upperBounds_mono (Set.image_subset_range f S) le_rfl

Premises used: subset_antisymm
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
γ : Type u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : ClosedIicTopology α
f : γ → α
inst_3 : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst_3, inst] f
⊢ upperBounds (f '' S) ⊆ upperBounds (range f)

Tactic:
subset_trans ?_ fun _ => upperBounds_mono (hf.range_subset_closure_image_dense hS) le_rfl

Premises used: Continuous.range_subset_closure_image_dense, le_rfl, subset_trans, upperBounds_mono
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
γ : Type u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : ClosedIicTopology α
f : γ → α
inst_3 : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst_3, inst] f
refine : upperBounds (f '' S) ⊆ upperBounds (closure[inst] (f '' S))
⊢ upperBounds (f '' S) ⊆ upperBounds (range f)

Tactic:
refine subset_trans ?_ fun _ => upperBounds_mono (hf.range_subset_closure_image_dense hS) le_rfl

Premises used: subset_trans
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
γ : Type u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : ClosedIicTopology α
f : γ → α
inst_3 : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst_3, inst] f
x : α
hx : x ∈ upperBounds (f '' S)
i : α
hi : i ∈ closure[inst] (f '' S)
⊢ ∃ᶠ (x : α) in 𝓝 i, x ∈ f '' S

Tactic:
rw [mem_closure_iff_frequently] at hi

Premises used: mem_closure_iff_frequently
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
γ : Type u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : ClosedIicTopology α
f : γ → α
inst_3 : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst_3, inst] f
x : α
hx : x ∈ upperBounds (f '' S)
i : α
hi : ∃ᶠ (x : α) in 𝓝 i, x ∈ f '' S
⊢ i ≤ x

Tactic:
(hi.mono hx).mem_of_closed isClosed_Iic

Premises used: Set.Mem, Filter.Frequently.mono, isClosed_Iic, Filter.Frequently.mem_of_closed
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
γ : Type u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : ClosedIicTopology α
f : γ → α
inst_3 : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst_3, inst] f
x : α
hx : x ∈ upperBounds (f '' S)
i : α
hi : ∃ᶠ (x : α) in 𝓝 i, x ∈ f '' S
⊢ i ≤ x

Tactic:
exact (hi.mono hx).mem_of_closed isClosed_Iic

Premises used: Filter.Frequently.mono, isClosed_Iic, Filter.Frequently.mem_of_closed
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
γ : Type u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : ClosedIciTopology α
f : γ → α
inst_3 : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst_3, inst] f
⊢ lowerBounds (f '' S) = lowerBounds (range f)

Tactic:
hS.upperBounds_image (α := αᵒᵈ) hf

Premises used: lowerBounds, Set.Mem, setOf, OrderDual, Dense.upperBounds_image
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
γ : Type u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLattice α
inst_2 : ClosedIicTopology α
f : γ → α
inst_3 : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst_3, inst] f
h : BddAbove (range f)
rw : Eq.{u_3 + 1} (α := α) (sSup (range fun (s : (↑S : Type u_2)) ↦ f (↑s : γ))) (sSup (range fun (i : γ) ↦ f i))
⊢ Eq.{u_3 + 1} (α := α) (⨆ (s : (↑S : Type u_2)), f (↑s : γ)) (⨆ (i : γ), f i)

Tactic:
rw [← sSup_range, ← sSup_range]

Premises used: sSup_range
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
γ : Type u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLattice α
inst_2 : ClosedIicTopology α
f : γ → α
inst_3 : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst_3, inst] f
h : BddAbove (range f)
inl :
  IsEmpty γ →
    Eq.{u_3 + 1} (α := α) (sSup (range fun (s : (↑S : Type u_2)) ↦ f (↑s : γ))) (sSup (range fun (i : γ) ↦ f i))
inr :
  Nonempty γ →
    Eq.{u_3 + 1} (α := α) (sSup (range fun (s : (↑S : Type u_2)) ↦ f (↑s : γ))) (sSup (range fun (i : γ) ↦ f i))
⊢ Eq.{u_3 + 1} (α := α) (sSup (range fun (s : (↑S : Type u_2)) ↦ f (↑s : γ))) (sSup (range fun (i : γ) ↦ f i))

Tactic:
obtain (_ | _) := isEmpty_or_nonempty γ

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
γ : Type u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLattice α
inst_2 : ClosedIicTopology α
f : γ → α
inst_3 : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst_3, inst] f
h : BddAbove (range f)
h_1 : IsEmpty γ
⊢ Eq.{u_3 + 1} (α := α) (sSup (range fun (s : (↑S : Type u_2)) ↦ f (↑s : γ))) (sSup (range fun (i : γ) ↦ f i))

Tactic:
simp [Set.range_eq_empty]

Premises used: Set.range_eq_empty
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
γ : Type u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLattice α
inst_2 : ClosedIicTopology α
f : γ → α
inst_3 : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst_3, inst] f
h : BddAbove (range f)
h_1 : Nonempty γ
⊢ Eq.{u_3 + 1} (α := α) (sSup (range fun (s : (↑S : Type u_2)) ↦ f (↑s : γ))) (sSup (range fun (i : γ) ↦ f i))

Tactic:
((isLUB_csSup (range_nonempty f) h).unique ?_).symm

Premises used: Set.range_nonempty, IsLUB.unique, isLUB_csSup, Eq.symm
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
γ : Type u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLattice α
inst_2 : ClosedIicTopology α
f : γ → α
inst_3 : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst_3, inst] f
h : BddAbove (range f)
h_1 : Nonempty γ
inr : IsLUB (range f) (sSup (range fun (s : (↑S : Type u_2)) ↦ f (↑s : γ)))
⊢ Eq.{u_3 + 1} (α := α) (sSup (range fun (s : (↑S : Type u_2)) ↦ f (↑s : γ))) (sSup (range fun (i : γ) ↦ f i))

Tactic:
refine ((isLUB_csSup (range_nonempty f) h).unique ?_).symm

Premises used: Set.range_nonempty, IsLUB.unique, isLUB_csSup, Eq.symm
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
γ : Type u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLattice α
inst_2 : ClosedIicTopology α
f : γ → α
inst_3 : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst_3, inst] f
h : BddAbove (range f)
h_1 : Nonempty γ
⊢ IsLUB (range f) (sSup (range fun (s : (↑S : Type u_2)) ↦ f (↑s : γ)))

Tactic:
(isLUB_congr (hS.upperBounds_image hf)).mp (isLUB_ciSup_set ?_ hS.nonempty)

Premises used: isLUB_congr, Dense.nonempty, isLUB_ciSup_set, Iff.mp, Dense.upperBounds_image
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
γ : Type u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLattice α
inst_2 : ClosedIicTopology α
f : γ → α
inst_3 : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst_3, inst] f
h : BddAbove (range f)
h_1 : Nonempty γ
inr : BddAbove (f '' S)
⊢ IsLUB (range f) (sSup (range fun (s : (↑S : Type u_2)) ↦ f (↑s : γ)))

Tactic:
refine (isLUB_congr (hS.upperBounds_image hf)).mp (isLUB_ciSup_set ?_ hS.nonempty)

Premises used: isLUB_congr, Dense.nonempty, isLUB_ciSup_set, Iff.mp, Dense.upperBounds_image
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
γ : Type u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLattice α
inst_2 : ClosedIicTopology α
f : γ → α
inst_3 : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst_3, inst] f
h : BddAbove (range f)
h_1 : Nonempty γ
⊢ f '' S ⊆ range f

Tactic:
grind
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
γ : Type u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLattice α
inst_2 : ClosedIicTopology α
f : γ → α
inst_3 : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst_3, inst] f
h : BddAbove (range f)
h_1 : Nonempty γ
⊢ BddAbove (f '' S)

Tactic:
exact h.mono (by grind)

Premises used: BddAbove.mono