awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
γ : Type u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLattice α
inst_2 : ClosedIciTopology α
f : γ → α
inst_3 : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst_3, inst] f
h : BddBelow (range f)
⊢ Eq.{u_3 + 1} (α := α) (⨅ (s : (↑S : Type u_2)), f (↑s : γ)) (⨅ (i : γ), f i)

Tactic:
hS.ciSup (α := αᵒᵈ) hf h

Premises used: iInf, Dense.ciSup, OrderDual
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
γ : Type u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : ClosedIicTopology α
f : γ → α
inst_3 : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst_3, inst] f
pos :
  ∀ (h : BddAbove.{u_3} (α := α) (range fun (x : (↑S : Type u_2)) ↦ f (↑x : γ))),
    Eq.{u_3 + 1} (α := α) (⨆ (s : (↑S : Type u_2)), f (↑s : γ)) (⨆ (i : γ), f i)
neg :
  ∀ (h : ¬BddAbove.{u_3} (α := α) (range fun (x : (↑S : Type u_2)) ↦ f (↑x : γ))),
    Eq.{u_3 + 1} (α := α) (⨆ (s : (↑S : Type u_2)), f (↑s : γ)) (⨆ (i : γ), f i)
⊢ Eq.{u_3 + 1} (α := α) (⨆ (s : (↑S : Type u_2)), f (↑s : γ)) (⨆ (i : γ), f i)

Tactic:
by_cases h : BddAbove (range (fun x : S ↦ f x))

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

Tactic:
hS.ciSup hf <| h.closure.mono ?_

Premises used: Dense.ciSup, BddAbove.closure, BddAbove.mono
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
γ : Type u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : ClosedIicTopology α
f : γ → α
inst_3 : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst_3, inst] f
h : BddAbove.{u_3} (α := α) (range fun (x : (↑S : Type u_2)) ↦ f (↑x : γ))
pos : range f ⊆ closure[inst] (range fun (x : (↑S : Type u_2)) ↦ f (↑x : γ))
⊢ Eq.{u_3 + 1} (α := α) (⨆ (s : (↑S : Type u_2)), f (↑s : γ)) (⨆ (i : γ), f i)

Tactic:
refine hS.ciSup hf <| h.closure.mono ?_

Premises used: Dense.ciSup, BddAbove.closure, BddAbove.mono
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
γ : Type u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : ClosedIicTopology α
f : γ → α
inst_3 : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst_3, inst] f
h : BddAbove.{u_3} (α := α) (range fun (x : (↑S : Type u_2)) ↦ f (↑x : γ))
⊢ range f ⊆ closure[inst] (range fun (x : (↑S : Type u_2)) ↦ f (↑x : γ))

Tactic:
simpa [← Function.comp_def, range_comp] using hf.range_subset_closure_image_dense hS

Premises used: Set.range_comp, Continuous.range_subset_closure_image_dense, Function.comp_def
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
γ : Type u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : ClosedIicTopology α
f : γ → α
inst_3 : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst_3, inst] f
h : ¬BddAbove.{u_3} (α := α) (range fun (x : (↑S : Type u_2)) ↦ f (↑x : γ))
this : ¬BddAbove (range f)
⊢ Eq.{u_3 + 1} (α := α) (⨆ (s : (↑S : Type u_2)), f (↑s : γ)) (⨆ (i : γ), f i)

Tactic:
simp [ciSup_of_not_bddAbove, this, h]

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

Tactic:
suffices ¬ BddAbove (range f) by simp [ciSup_of_not_bddAbove, this, h]
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
γ : Type u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : ClosedIicTopology α
f : γ → α
inst_3 : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst_3, inst] f
h : ¬BddAbove.{u_3} (α := α) (range fun (x : (↑S : Type u_2)) ↦ f (↑x : γ))
neg : ∀ (h : BddAbove (range f)), BddAbove.{u_3} (α := α) (range fun (x : (↑S : Type u_2)) ↦ f (↑x : γ))
⊢ ¬BddAbove (range f)

Tactic:
contrapose h
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
γ : Type u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : ClosedIicTopology α
f : γ → α
inst_3 : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst_3, inst] f
h : BddAbove (range f)
⊢ BddAbove.{u_3} (α := α) (range fun (x : (↑S : Type u_2)) ↦ f (↑x : γ))

Tactic:
grind [h.mono]

Premises used: BddAbove.mono
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
γ : Type u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : ClosedIciTopology α
f : γ → α
inst_3 : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst_3, inst] f
⊢ Eq.{u_3 + 1} (α := α) (⨅ (s : (↑S : Type u_2)), f (↑s : γ)) (⨅ (i : γ), f i)

Tactic:
hS.ciSup' (α := αᵒᵈ) hf

Premises used: iInf, OrderDual, Dense.ciSup'
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b : α
simp : ∀ (f : Ultrafilter α), Icc a b ∈ (↑f : Filter α) → ∃ x ∈ Icc a b, (↑f : Filter α) ≤ 𝓝 x
⊢ IsCompact (Icc a b)

Tactic:
simp only [isCompact_iff_ultrafilter_le_nhds, le_principal_iff]

Premises used: Filter.le_principal_iff, isCompact_iff_ultrafilter_le_nhds
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b : α
refine : a ≤ b → ∀ (f : Ultrafilter α) (hfab : Icc a b ∈ (↑f : Filter α)), ∃ x ∈ Icc a b, (↑f : Filter α) ≤ 𝓝 x
⊢ ∀ (f : Ultrafilter α), Icc a b ∈ (↑f : Filter α) → ∃ x ∈ Icc a b, (↑f : Filter α) ≤ 𝓝 x

Tactic:
refine (le_or_gt a b).elim (fun _ f hfab ↦ ?_) (by simp [·])

Premises used: le_or_gt, Or.elim
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b : α
h : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ (↑f : Filter α)
by_contra! : ∀ (hf : ∀ (x : α) (_ : x ∈ Icc a b), ¬(↑f : Filter α) ≤ 𝓝 x), False
⊢ ∃ x ∈ Icc a b, (↑f : Filter α) ≤ 𝓝 x

Tactic:
by_contra! hf
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b : α
h : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ (↑f : Filter α)
hf : ∀ (x : α) (_ : x ∈ Icc a b), ¬(↑f : Filter α) ≤ 𝓝 x
x : α
hx : x ∈ Icc a b
h_1 : {x} ∈ f
⊢ (↑f : Filter α) ≤ pure x

Tactic:
simpa
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b : α
h : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ (↑f : Filter α)
hf : ∀ (x : α) (_ : x ∈ Icc a b), ¬(↑f : Filter α) ≤ 𝓝 x
⊢ ∀ x ∈ Icc a b, {x} ∉ f

Tactic:
have hpt : ∀ x ∈ Icc a b, {x} ∉ f := fun x hx _ ↦ hf x hx (le_trans (by simpa) (pure_le_nhds x))
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b : α
h : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ (↑f : Filter α)
hf : ∀ (x : α) (_ : x ∈ Icc a b), ¬(↑f : Filter α) ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x : α | x ∈ Icc a b ∧ Icc a x ∉ f}
⊢ b ∈ upperBounds s

Tactic:
have hsb : b ∈ upperBounds s := fun x hx ↦ hx.1.2
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b : α
h : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ (↑f : Filter α)
hf : ∀ (x : α) (_ : x ∈ Icc a b), ¬(↑f : Filter α) ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x : α | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
⊢ a ∈ s

Tactic:
simp [s, *]
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b : α
h : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ (↑f : Filter α)
hf : ∀ (x : α) (_ : x ∈ Icc a b), ¬(↑f : Filter α) ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x : α | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
⊢ a ∈ s

Tactic:
have ha : a ∈ s := by simp [s, *]
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b : α
h : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ (↑f : Filter α)
hf : ∀ (x : α) (_ : x ∈ Icc a b), ¬(↑f : Filter α) ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x : α | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
ha : a ∈ s
c : α := sSup s
⊢ IsLUB s c

Tactic:
have hsc : IsLUB s c := isLUB_csSup ⟨a, ha⟩ ⟨b, hsb⟩
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b : α
h : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ (↑f : Filter α)
hf : ∀ (x : α) (_ : x ∈ Icc a b), ¬(↑f : Filter α) ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x : α | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
ha : a ∈ s
c : α := sSup s
hsc : IsLUB s c
⊢ c ∈ Icc a b

Tactic:
have hc : c ∈ Icc a b := ⟨hsc.1 ha, hsc.2 hsb⟩
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b : α
h : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ (↑f : Filter α)
hf : ∀ (x : α) (_ : x ∈ Icc a b), ¬(↑f : Filter α) ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x : α | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
ha : a ∈ s
c : α := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
i : α
hic : i < c
have : ∀ (j : α) (hj : j ∈ s) (hij : i < j) (hjc : j ≤ c), Ioi i ∈ f
⊢ Ioi i ∈ f

Tactic:
have ⟨j, hj, hij, hjc⟩ := hsc.exists_between hic
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b : α
h_1 : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ (↑f : Filter α)
hf : ∀ (x : α) (_ : x ∈ Icc a b), ¬(↑f : Filter α) ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x : α | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
ha : a ∈ s
c : α := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
i : α
hic : i < c
j : α
hj : j ∈ s
hij : i < j
hjc : j ≤ c
h : ∀ a_1 ∈ (Icc a j)ᶜ, a_1 ∈ Icc a b → a_1 ∈ Ioi i
⊢ Ioi i ∈ f

Tactic:
filter_upwards [f.compl_mem_iff_notMem.mpr hj.2, hfab]

Premises used: Iff.mpr, And.right, Ultrafilter.compl_mem_iff_notMem
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b : α
h : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ (↑f : Filter α)
hf : ∀ (x : α) (_ : x ∈ Icc a b), ¬(↑f : Filter α) ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x : α | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
ha : a ∈ s
c : α := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
i : α
hic : i < c
j : α
hj : j ∈ s
hij : i < j
hjc : j ≤ c
⊢ ∀ a_1 ∈ (Icc a j)ᶜ, a_1 ∈ Icc a b → a_1 ∈ Ioi i

Tactic:
grind
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b : α
h : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ (↑f : Filter α)
hf : ∀ (x : α) (_ : x ∈ Icc a b), ¬(↑f : Filter α) ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x : α | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
ha : a ∈ s
c : α := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
⊢ ∀ (i : α) (hic : i < c), Ioi i ∈ f

Tactic:
have (i : _) (hic : i < c) : Ioi i ∈ f := by
    have ⟨j, hj, hij, hjc⟩ := hsc.exists_between hic
    filter_upwards [f.compl_mem_iff_notMem.mpr hj.2, hfab]; grind
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b : α
h : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ (↑f : Filter α)
hf : ∀ (x : α) (_ : x ∈ Icc a b), ¬(↑f : Filter α) ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x : α | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
ha : a ∈ s
c : α := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
this : ∀ (i : α) (hic : i < c), Ioi i ∈ f
⊢ ∃ (x : α), c < x ∧ Iio x ∉ f

Tactic:
simpa [nhds_eq_order, eq_true this] using hf c hc

Premises used: nhds_eq_order, eq_true
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b : α
h : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ (↑f : Filter α)
hf : ∀ (x : α) (_ : x ∈ Icc a b), ¬(↑f : Filter α) ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x : α | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
ha : a ∈ s
c : α := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
this : ∀ (i : α) (hic : i < c), Ioi i ∈ f
have : ∀ (x : α) (hx : c < x) (hxf : Iio x ∉ f), False
⊢ False

Tactic:
have ⟨x, hx, hxf⟩ : ∃ x, c < x ∧ Iio x ∉ f := by simpa [nhds_eq_order, eq_true this] using hf c hc
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b : α
h : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ (↑f : Filter α)
hf : ∀ (x : α) (_ : x ∈ Icc a b), ¬(↑f : Filter α) ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x : α | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
ha : a ∈ s
c : α := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
this : ∀ (i : α) (hic : i < c), Ioi i ∈ f
x : α
hx : c < x
hxf : Iio x ∉ f
h_1 : Icc a c ∈ f
⊢ Icc a c ⊆ Iio x

Tactic:
grind
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b : α
h : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ (↑f : Filter α)
hf : ∀ (x : α) (_ : x ∈ Icc a b), ¬(↑f : Filter α) ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x : α | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
ha : a ∈ s
c : α := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
this : ∀ (i : α) (hic : i < c), Ioi i ∈ f
x : α
hx : c < x
hxf : Iio x ∉ f
⊢ Icc a c ∉ f

Tactic:
have : Icc a c ∉ f := mt (mem_of_superset · (by grind)) hxf
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b : α
h : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ (↑f : Filter α)
hf : ∀ (x : α) (_ : x ∈ Icc a b), ¬(↑f : Filter α) ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x : α | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
ha : a ∈ s
c : α := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
this_1 : ∀ (i : α) (hic : i < c), Ioi i ∈ f
x : α
hx : c < x
hxf : Iio x ∉ f
this : Icc a c ∉ f
⊢ a ≤ x

Tactic:
grind
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b : α
h_1 : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ (↑f : Filter α)
hf : ∀ (x : α) (_ : x ∈ Icc a b), ¬(↑f : Filter α) ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x : α | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
ha : a ∈ s
c : α := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
this_1 : ∀ (i : α) (hic : i < c), Ioi i ∈ f
x : α
hx : c < x
hxf : Iio x ∉ f
this : Icc a c ∉ f
h : b < x
⊢ Icc a b ⊆ Iio x

Tactic:
grind
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b : α
h : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ (↑f : Filter α)
hf : ∀ (x : α) (_ : x ∈ Icc a b), ¬(↑f : Filter α) ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x : α | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
ha : a ∈ s
c : α := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
this_1 : ∀ (i : α) (hic : i < c), Ioi i ∈ f
x : α
hx : c < x
hxf : Iio x ∉ f
this : Icc a c ∉ f
⊢ x ∈ Icc a b

Tactic:
have : x ∈ Icc a b := ⟨by grind, le_of_not_gt fun h ↦ hxf (mem_of_superset hfab (by grind))⟩
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b : α
h : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ (↑f : Filter α)
hf : ∀ (x : α) (_ : x ∈ Icc a b), ¬(↑f : Filter α) ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x : α | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
ha : a ∈ s
c : α := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
this_1 : ∀ (i : α) (hic : i < c), Ioi i ∈ f
x : α
hx : c < x
hxf : Iio x ∉ f
this_2 : Icc a c ∉ f
this : x ∈ Icc a b
⊢ Icc a x ∈ f

Tactic:
simpa [s, this.1, this.2] using notMem_of_csSup_lt hx ⟨b, hsb⟩

Premises used: notMem_of_csSup_lt, And.right, And.left, Exists.intro
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b : α
h : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ (↑f : Filter α)
hf : ∀ (x : α) (_ : x ∈ Icc a b), ¬(↑f : Filter α) ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x : α | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
ha : a ∈ s
c : α := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
this_1 : ∀ (i : α) (hic : i < c), Ioi i ∈ f
x : α
hx : c < x
hxf : Iio x ∉ f
this_2 : Icc a c ∉ f
this : x ∈ Icc a b
⊢ Icc a x ∈ f

Tactic:
have : Icc a x ∈ f := by simpa [s, this.1, this.2] using notMem_of_csSup_lt hx ⟨b, hsb⟩
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b : α
h_1 : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ (↑f : Filter α)
hf : ∀ (x : α) (_ : x ∈ Icc a b), ¬(↑f : Filter α) ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x : α | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
ha : a ∈ s
c : α := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
this_1 : ∀ (i : α) (hic : i < c), Ioi i ∈ f
x : α
hx : c < x
hxf : Iio x ∉ f
this_2 : Icc a c ∉ f
this_3 : x ∈ Icc a b
this : Icc a x ∈ f
h : ∀ a_1 ∈ (Iio x)ᶜ, a_1 ∈ Icc a x → Membership.mem (γ := Set α) {x} a_1
⊢ {x} ∈ f

Tactic:
filter_upwards [f.compl_mem_iff_notMem.mpr hxf, this]

Premises used: Iff.mpr, Ultrafilter.compl_mem_iff_notMem
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b : α
h : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ (↑f : Filter α)
hf : ∀ (x : α) (_ : x ∈ Icc a b), ¬(↑f : Filter α) ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x : α | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
ha : a ∈ s
c : α := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
this_1 : ∀ (i : α) (hic : i < c), Ioi i ∈ f
x : α
hx : c < x
hxf : Iio x ∉ f
this_2 : Icc a c ∉ f
this_3 : x ∈ Icc a b
this : Icc a x ∈ f
⊢ ∀ a_1 ∈ (Iio x)ᶜ, a_1 ∈ Icc a x → Membership.mem (γ := Set α) {x} a_1

Tactic:
grind
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b : α
h : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ (↑f : Filter α)
hf : ∀ (x : α) (_ : x ∈ Icc a b), ¬(↑f : Filter α) ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x : α | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
ha : a ∈ s
c : α := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
this_1 : ∀ (i : α) (hic : i < c), Ioi i ∈ f
x : α
hx : c < x
hxf : Iio x ∉ f
this_2 : Icc a c ∉ f
this_3 : x ∈ Icc a b
this : Icc a x ∈ f
⊢ False

Tactic:
exact hpt _ ‹_› (by filter_upwards [f.compl_mem_iff_notMem.mpr hxf, this]; grind)
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
s : Set α
h₁ : s.Nonempty
h₂ : BddBelow s
hs : IsClosed[inst_1] s
⊢ (↑(upperClosure s) : Set α) = Ici (sInf s)

Tactic:
Set.ext fun _ ↦ ⟨fun ⟨_, h, h'⟩ ↦ csInf_le_of_le h₂ h h',
    (⟨_, (isGLB_csInf h₁ h₂).mem_of_isClosed h₁ hs, ·⟩)⟩

Premises used: IsGLB.mem_of_isClosed, Set.ext, Set.Ici, _private.0.upperClosure_eq_Ici_csInf.match_1, csInf_le_of_le, Membership.mem, isGLB_csInf, And.intro, Iff.intro, Exists.intro, InfSet.sInf
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
s : Set α
h₁ : s.Nonempty
h₂ : BddAbove s
hs : IsClosed[inst_1] s
⊢ (↑(lowerClosure s) : Set α) = Iic (sSup s)

Tactic:
upperClosure_eq_Ici_csInf (α := αᵒᵈ) h₁ h₂ hs

Premises used: Set.Mem, setOf, Set.Iic, OrderDual, upperClosure_eq_Ici_csInf
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
s : Set α
hs : IsClosed[inst_1] s
inl : ∀ (hs : IsClosed[inst_1] ∅), IsClosed[inst_1] (↑(upperClosure ∅) : Set α)
inr : ∀ (h₁ : s.Nonempty), IsClosed[inst_1] (↑(upperClosure s) : Set α)
⊢ IsClosed[inst_1] (↑(upperClosure s) : Set α)

Tactic:
obtain rfl | h₁ := s.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
hs : IsClosed[inst_1] ∅
⊢ IsClosed[inst_1] (↑(upperClosure ∅) : Set α)

Tactic:
simp
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
s : Set α
hs : IsClosed[inst_1] s
h₁ : s.Nonempty
pos : ∀ (h₂ : BddBelow s), IsClosed[inst_1] (↑(upperClosure s) : Set α)
neg : ∀ (h₂ : ¬BddBelow s), IsClosed[inst_1] (↑(upperClosure s) : Set α)
⊢ IsClosed[inst_1] (↑(upperClosure s) : Set α)

Tactic:
by_cases h₂ : BddBelow s

Premises used: BddBelow
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
s : Set α
hs : IsClosed[inst_1] s
h₁ : s.Nonempty
h₂ : BddBelow s
⊢ IsClosed[inst_1] (↑(upperClosure s) : Set α)

Tactic:
upperClosure_eq_Ici_csInf h₁ h₂ hs ▸ isClosed_Ici

Premises used: Eq.rec, Eq.symm, isClosed_Ici, upperClosure_eq_Ici_csInf
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
s : Set α
hs : IsClosed[inst_1] s
h₁ : s.Nonempty
h₂ : BddBelow s
⊢ IsClosed[inst_1] (↑(upperClosure s) : Set α)

Tactic:
exact upperClosure_eq_Ici_csInf h₁ h₂ hs ▸ isClosed_Ici
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
s : Set α
hs : IsClosed[inst_1] s
h₁ : s.Nonempty
h₂ : ¬BddBelow s
⊢ IsClosed[inst_1] (↑(upperClosure s) : Set α)

Tactic:
upperClosure_eq_bot h₂ ▸ isClosed_univ

Premises used: isClosed_univ, Eq.rec, Eq.symm, upperClosure_eq_bot
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
s : Set α
hs : IsClosed[inst_1] s
h₁ : s.Nonempty
h₂ : ¬BddBelow s
⊢ IsClosed[inst_1] (↑(upperClosure s) : Set α)

Tactic:
exact upperClosure_eq_bot h₂ ▸ isClosed_univ
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
s : Set α
hs : IsClosed[inst_1] s
⊢ IsClosed[inst_1] (LowerSet.carrier (lowerClosure s))

Tactic:
IsClosed.upperClosure (α := αᵒᵈ) hs

Premises used: IsClosed.upperClosure, Set.Mem, setOf, OrderDual