awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.Compact
Goal:
α_1 : Type u_1
ι : Type u_2
α : ι → Type u_3
inst : (i : ι) → Preorder (α i)
inst_1 : (i : ι) → TopologicalSpace (α i)
inst_2 : ∀ (i : ι), CompactIccSpace.{u_3} (α i)
⊢ CompactIccSpace ((i : ι) → α i)

Tactic:
⟨fun {a b} => (pi_univ_Icc a b ▸ isCompact_univ_pi) fun _ => isCompact_Icc⟩

Premises used: CompactIccSpace.mk
-- Module: Mathlib.Topology.Order.Compact
Goal:
α_1 : Type u_1
α : Type u_2
β : Type u_3
inst : Preorder β
inst_1 : TopologicalSpace β
inst_2 : CompactIccSpace β
⊢ CompactIccSpace (α → β)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Order.Compact
Goal:
α_1 : Type u_1
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : CompactIccSpace α
inst_3 : Preorder β
inst_4 : TopologicalSpace β
inst_5 : CompactIccSpace β
⊢ CompactIccSpace (α × β)

Tactic:
⟨fun {a b} => (Icc_prod_eq a b).symm ▸ isCompact_Icc.prod isCompact_Icc⟩

Premises used: IsCompact.prod, Eq.rec, CompactIccSpace.mk, CompactIccSpace.isCompact_Icc, Set.Icc_prod_eq, Eq.symm
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : CompactIccSpace α
a b : α
⊢ IsCompact (uIcc a b)

Tactic:
isCompact_Icc

Premises used: CompactIccSpace.isCompact_Icc, Set.uIcc
-- Module: Mathlib.Topology.Order.Compact
Goal:
α_1 : Type u_1
α : Type u_2
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
⊢ IsCompact.{u_2} (X := α) univ

Tactic:
simp only [← Icc_bot_top, isCompact_Icc]

Premises used: Set.Icc_bot_top, CompactIccSpace.isCompact_Icc
-- Module: Mathlib.Topology.Order.Compact
Goal:
α_1 : Type u_1
α : Type u_2
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : CompactIccSpace α
a b : α
⊢ CompactSpace.{u_2} (↑(Icc a b) : Type u_2)

Tactic:
isCompact_iff_compactSpace.mp isCompact_Icc

Premises used: isCompact_iff_compactSpace, CompactIccSpace.isCompact_Icc, Iff.mp
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
⊢ b ≤ a → IsCompact (Ico a b)

Tactic:
simp_all
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
⊢ b ≤ a → IsCompact (Ioc a b)

Tactic:
simp_all
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
⊢ b ≤ a → IsCompact (Ioo a b)

Tactic:
simp_all
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : ClosedIicTopology α
s : Set α
hs : IsCompact s
ne_s : s.Nonempty
⊢ Nonempty.{u_2 + 1} (↑s : Type u_2)

Tactic:
haveI : Nonempty s := ne_s.to_subtype
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : ClosedIicTopology α
s : Set α
hs : IsCompact s
ne_s : s.Nonempty
this : Nonempty.{u_2 + 1} (↑s : Type u_2)
suffices : (s ∩ ⋂ x ∈ s, Iic x).Nonempty
⊢ ∃ (x : α), IsLeast s x

Tactic:
suffices (s ∩ ⋂ x ∈ s, Iic x).Nonempty from
    ⟨this.choose, this.choose_spec.1, mem_iInter₂.mp this.choose_spec.2⟩
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : ClosedIicTopology α
s : Set α
hs : IsCompact s
ne_s : s.Nonempty
this : Nonempty.{u_2 + 1} (↑s : Type u_2)
rw : (s ∩ ⋂ (x : (↑s : Type u_2)), Iic (↑x : α)).Nonempty
⊢ (s ∩ ⋂ x ∈ s, Iic x).Nonempty

Tactic:
rw [biInter_eq_iInter]

Premises used: Set.biInter_eq_iInter
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : ClosedIicTopology α
s : Set α
hs : IsCompact s
ne_s : s.Nonempty
this : Nonempty.{u_2 + 1} (↑s : Type u_2)
by_contra : ∀ (H : ¬(s ∩ ⋂ (x : (↑s : Type u_2)), Iic (↑x : α)).Nonempty), False
⊢ (s ∩ ⋂ (x : (↑s : Type u_2)), Iic (↑x : α)).Nonempty

Tactic:
by_contra H
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : ClosedIicTopology α
s : Set α
hs : IsCompact s
ne_s : s.Nonempty
this : Nonempty.{u_2 + 1} (↑s : Type u_2)
H : ¬(s ∩ ⋂ (x : (↑s : Type u_2)), Iic (↑x : α)).Nonempty
⊢ s ∩ ⋂ (x : (↑s : Type u_2)), Iic (↑x : α) = ∅

Tactic:
rw [not_nonempty_iff_eq_empty] at H

Premises used: Set.not_nonempty_iff_eq_empty
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : ClosedIicTopology α
s : Set α
hs : IsCompact s
ne_s : s.Nonempty
this : Nonempty.{u_2 + 1} (↑s : Type u_2)
H : s ∩ ⋂ (x : (↑s : Type u_2)), Iic (↑x : α) = ∅
rcases : ∀ (x : (↑s : Type u_2)) (hx : s ∩ Iic (↑x : α) = ∅), False
⊢ False

Tactic:
rcases hs.elim_directed_family_closed (fun x : s => Iic ↑x) (fun x => isClosed_Iic) H
      (Monotone.directed_ge fun _ _ h => Iic_subset_Iic.mpr h) with ⟨x, hx⟩

Premises used: Iff.mpr, Set.Iic_subset_Iic, isClosed_Iic, Monotone.directed_ge, IsCompact.elim_directed_family_closed, Set.Iic, Subtype.val
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : ClosedIicTopology α
s : Set α
hs : IsCompact s
ne_s : s.Nonempty
this : Nonempty.{u_2 + 1} (↑s : Type u_2)
H : s ∩ ⋂ (x : (↑s : Type u_2)), Iic (↑x : α) = ∅
x : (↑s : Type u_2)
hx : s ∩ Iic (↑x : α) = ∅
⊢ False

Tactic:
not_nonempty_iff_eq_empty.mpr hx ⟨x, x.2, le_rfl⟩

Premises used: Iff.mpr, le_rfl, Set.not_nonempty_iff_eq_empty, And.intro, Exists.intro, Subtype.val, Subtype.property
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : ClosedIicTopology α
s : Set α
hs : IsCompact s
ne_s : s.Nonempty
this : Nonempty.{u_2 + 1} (↑s : Type u_2)
H : s ∩ ⋂ (x : (↑s : Type u_2)), Iic (↑x : α) = ∅
x : (↑s : Type u_2)
hx : s ∩ Iic (↑x : α) = ∅
⊢ False

Tactic:
exact not_nonempty_iff_eq_empty.mpr hx ⟨x, x.2, le_rfl⟩

Premises used: Iff.mpr, le_rfl, Set.not_nonempty_iff_eq_empty, And.intro, Exists.intro, Subtype.val, Subtype.property
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : ClosedIciTopology α
s : Set α
hs : IsCompact s
ne_s : s.Nonempty
⊢ ∃ (x : α), IsGreatest s x

Tactic:
IsCompact.exists_isLeast (α := αᵒᵈ) hs ne_s

Premises used: IsCompact.exists_isLeast, Set.Mem, setOf, upperBounds, IsGreatest, OrderDual
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : ClosedIicTopology α
s : Set α
hs : IsCompact s
ne_s : s.Nonempty
⊢ ∃ x ∈ s, IsGLB s x

Tactic:
(hs.exists_isLeast ne_s).imp (fun x (hx : IsLeast s x) => ⟨hx.1, hx.isGLB⟩)

Premises used: IsCompact.exists_isLeast, IsLeast.isGLB, Exists.imp, And.left, And.intro
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : ClosedIciTopology α
s : Set α
hs : IsCompact s
ne_s : s.Nonempty
⊢ ∃ x ∈ s, IsLUB s x

Tactic:
IsCompact.exists_isGLB (α := αᵒᵈ) hs ne_s

Premises used: lowerBounds, Set.Mem, setOf, upperBounds, IsLeast, IsLUB, IsCompact.exists_isGLB, OrderDual
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : CompactIccSpace α
⊢ cocompact α ≤ atBot ⊔ atTop

Tactic:
fun s hs ↦ mem_cocompact.mpr <| (isEmpty_or_nonempty α).casesOn ?_ ?_

Premises used: Iff.mpr, isEmpty_or_nonempty, Or.casesOn, Filter.mem_cocompact
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : CompactIccSpace α
refine_1 :
  ∀ (s : Set α) (hs : Membership.mem (γ := Filter α) (atBot ⊔ atTop) s) (h : IsEmpty α),
    ∃ (t : Set α), IsCompact t ∧ tᶜ ⊆ s
refine_2 :
  ∀ (s : Set α) (hs : Membership.mem (γ := Filter α) (atBot ⊔ atTop) s) (h : Nonempty α),
    ∃ (t : Set α), IsCompact t ∧ tᶜ ⊆ s
⊢ cocompact α ≤ atBot ⊔ atTop

Tactic:
refine fun s hs ↦ mem_cocompact.mpr <| (isEmpty_or_nonempty α).casesOn ?_ ?_

Premises used: Iff.mpr, isEmpty_or_nonempty, Or.casesOn, Filter.mem_cocompact
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : CompactIccSpace α
s : Set α
hs : Membership.mem (γ := Filter α) (atBot ⊔ atTop) s
h : IsEmpty α
⊢ ∃ (t : Set α), IsCompact t ∧ tᶜ ⊆ s

Tactic:
⟨∅, isCompact_empty, fun x _ ↦ (IsEmpty.false x).elim⟩

Premises used: False.elim, And.intro, Exists.intro, IsEmpty.false, EmptyCollection.emptyCollection, isCompact_empty
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : CompactIccSpace α
s : Set α
hs : Membership.mem (γ := Filter α) (atBot ⊔ atTop) s
h : IsEmpty α
⊢ ∃ (t : Set α), IsCompact t ∧ tᶜ ⊆ s

Tactic:
exact ⟨∅, isCompact_empty, fun x _ ↦ (IsEmpty.false x).elim⟩
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : CompactIccSpace α
s : Set α
hs : Membership.mem (γ := Filter α) (atBot ⊔ atTop) s
h : Nonempty α
refine_2 : ∀ (t : α) (ht : ∀ b ≤ t, b ∈ s), ∃ (t : Set α), IsCompact t ∧ tᶜ ⊆ s
⊢ ∃ (t : Set α), IsCompact t ∧ tᶜ ⊆ s

Tactic:
obtain ⟨t, ht⟩ := mem_atBot_sets.mp hs.1

Premises used: And.left, Iff.mp, Filter.mem_atBot_sets
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : CompactIccSpace α
s : Set α
hs : Membership.mem (γ := Filter α) (atBot ⊔ atTop) s
h : Nonempty α
t : α
ht : ∀ b ≤ t, b ∈ s
refine_2 : ∀ (u : α) (hu : ∀ b ≥ u, b ∈ s), ∃ (t : Set α), IsCompact t ∧ tᶜ ⊆ s
⊢ ∃ (t : Set α), IsCompact t ∧ tᶜ ⊆ s

Tactic:
obtain ⟨u, hu⟩ := mem_atTop_sets.mp hs.2

Premises used: Filter.mem_atTop_sets, And.right, Iff.mp
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : CompactIccSpace α
s : Set α
hs : Membership.mem (γ := Filter α) (atBot ⊔ atTop) s
h : Nonempty α
t : α
ht : ∀ b ≤ t, b ∈ s
u : α
hu : ∀ b ≥ u, b ∈ s
⊢ ∃ (t : Set α), IsCompact t ∧ tᶜ ⊆ s

Tactic:
⟨Icc t u, isCompact_Icc, fun x hx ↦ ?_⟩

Premises used: CompactIccSpace.isCompact_Icc, Set.Icc, And.intro, Exists.intro
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : CompactIccSpace α
s : Set α
hs : Membership.mem (γ := Filter α) (atBot ⊔ atTop) s
h : Nonempty α
t : α
ht : ∀ b ≤ t, b ∈ s
u : α
hu : ∀ b ≥ u, b ∈ s
refine_2 : ∀ (x : α) (hx : x ∈ (Icc t u)ᶜ), x ∈ s
⊢ ∃ (t : Set α), IsCompact t ∧ tᶜ ⊆ s

Tactic:
refine ⟨Icc t u, isCompact_Icc, fun x hx ↦ ?_⟩
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : CompactIccSpace α
s : Set α
hs : Membership.mem (γ := Filter α) (atBot ⊔ atTop) s
h : Nonempty α
t : α
ht : ∀ b ≤ t, b ∈ s
u : α
hu : ∀ b ≥ u, b ∈ s
x : α
hx : x ∈ (Icc t u)ᶜ
⊢ x ∈ s

Tactic:
(not_and_or.mp hx).casesOn (fun h ↦ ht x (le_of_not_ge h)) fun h ↦ hu x (le_of_not_ge h)

Premises used: Or.casesOn, not_and_or, Iff.mp
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : CompactIccSpace α
s : Set α
hs : Membership.mem (γ := Filter α) (atBot ⊔ atTop) s
h : Nonempty α
t : α
ht : ∀ b ≤ t, b ∈ s
u : α
hu : ∀ b ≥ u, b ∈ s
x : α
hx : x ∈ (Icc t u)ᶜ
⊢ x ∈ s

Tactic:
exact (not_and_or.mp hx).casesOn (fun h ↦ ht x (le_of_not_ge h)) fun h ↦ hu x (le_of_not_ge h)
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTop α
inst_3 : CompactIccSpace α
⊢ cocompact α ≤ atBot

Tactic:
fun _ hs ↦ mem_cocompact.mpr <| (isEmpty_or_nonempty α).casesOn ?_ ?_

Premises used: Iff.mpr, isEmpty_or_nonempty, Or.casesOn, Filter.mem_cocompact
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTop α
inst_3 : CompactIccSpace α
refine_1 :
  ∀ (x : Set α) (hs : Membership.mem (γ := Filter α) atBot x) (h : IsEmpty α), ∃ (t : Set α), IsCompact t ∧ tᶜ ⊆ x
refine_2 :
  ∀ (x : Set α) (hs : Membership.mem (γ := Filter α) atBot x) (h : Nonempty α), ∃ (t : Set α), IsCompact t ∧ tᶜ ⊆ x
⊢ cocompact α ≤ atBot

Tactic:
refine fun _ hs ↦ mem_cocompact.mpr <| (isEmpty_or_nonempty α).casesOn ?_ ?_

Premises used: Iff.mpr, isEmpty_or_nonempty, Or.casesOn, Filter.mem_cocompact
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTop α
inst_3 : CompactIccSpace α
x : Set α
hs : Membership.mem (γ := Filter α) atBot x
h : IsEmpty α
⊢ ∃ (t : Set α), IsCompact t ∧ tᶜ ⊆ x

Tactic:
⟨∅, isCompact_empty, fun x _ ↦ (IsEmpty.false x).elim⟩

Premises used: False.elim, And.intro, Exists.intro, IsEmpty.false, EmptyCollection.emptyCollection, isCompact_empty
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTop α
inst_3 : CompactIccSpace α
x : Set α
hs : Membership.mem (γ := Filter α) atBot x
h : IsEmpty α
⊢ ∃ (t : Set α), IsCompact t ∧ tᶜ ⊆ x

Tactic:
exact ⟨∅, isCompact_empty, fun x _ ↦ (IsEmpty.false x).elim⟩
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTop α
inst_3 : CompactIccSpace α
x : Set α
hs : Membership.mem (γ := Filter α) atBot x
h : Nonempty α
refine_2 : ∀ (t : α) (ht : ∀ b ≤ t, b ∈ x), ∃ (t : Set α), IsCompact t ∧ tᶜ ⊆ x
⊢ ∃ (t : Set α), IsCompact t ∧ tᶜ ⊆ x

Tactic:
obtain ⟨t, ht⟩ := mem_atBot_sets.mp hs

Premises used: Iff.mp, Filter.mem_atBot_sets
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTop α
inst_3 : CompactIccSpace α
x : Set α
hs : Membership.mem (γ := Filter α) atBot x
h : Nonempty α
t : α
ht : ∀ b ≤ t, b ∈ x
⊢ ∃ (t : Set α), IsCompact t ∧ tᶜ ⊆ x

Tactic:
⟨Icc t ⊤, isCompact_Icc, fun _ hx ↦ ?_⟩

Premises used: CompactIccSpace.isCompact_Icc, Set.Icc, And.intro, Exists.intro, Top.top
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTop α
inst_3 : CompactIccSpace α
x : Set α
hs : Membership.mem (γ := Filter α) atBot x
h : Nonempty α
t : α
ht : ∀ b ≤ t, b ∈ x
refine_2 : ∀ (x_1 : α) (hx : x_1 ∈ (Icc t ⊤)ᶜ), x_1 ∈ x
⊢ ∃ (t : Set α), IsCompact t ∧ tᶜ ⊆ x

Tactic:
refine ⟨Icc t ⊤, isCompact_Icc, fun _ hx ↦ ?_⟩
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTop α
inst_3 : CompactIccSpace α
x : Set α
hs : Membership.mem (γ := Filter α) atBot x
h : Nonempty α
t : α
ht : ∀ b ≤ t, b ∈ x
x_1 : α
hx : x_1 ∈ (Icc t ⊤)ᶜ
⊢ x_1 ∈ x

Tactic:
(not_and_or.mp hx).casesOn (fun h ↦ ht _ (le_of_not_ge h)) (fun h ↦ (h le_top).elim)

Premises used: Or.casesOn, not_and_or, Iff.mp
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTop α
inst_3 : CompactIccSpace α
x : Set α
hs : Membership.mem (γ := Filter α) atBot x
h : Nonempty α
t : α
ht : ∀ b ≤ t, b ∈ x
x_1 : α
hx : x_1 ∈ (Icc t ⊤)ᶜ
⊢ x_1 ∈ x

Tactic:
exact (not_and_or.mp hx).casesOn (fun h ↦ ht _ (le_of_not_ge h)) (fun h ↦ (h le_top).elim)
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderBot α
inst_3 : CompactIccSpace α
⊢ cocompact α ≤ atTop

Tactic:
cocompact_le_atBot (α := αᵒᵈ)

Premises used: cocompact_le_atBot, Set.Ici, Set.Mem, setOf, OrderDual
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : NoMinOrder α
inst_3 : ClosedIicTopology α
⊢ atBot ≤ cocompact α

Tactic:
fun s hs ↦ ?_
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : NoMinOrder α
inst_3 : ClosedIicTopology α
refine : ∀ (s : Set α) (hs : s ∈ cocompact α), Membership.mem (γ := Filter α) atBot s
⊢ atBot ≤ cocompact α

Tactic:
refine fun s hs ↦ ?_
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : NoMinOrder α
inst_3 : ClosedIicTopology α
s : Set α
hs : s ∈ cocompact α
obtain : ∀ (t : Set α) (ht : IsCompact t) (hts : tᶜ ⊆ s), Membership.mem (γ := Filter α) atBot s
⊢ Membership.mem (γ := Filter α) atBot s

Tactic:
obtain ⟨t, ht, hts⟩ := mem_cocompact.mp hs

Premises used: Iff.mp, Filter.mem_cocompact
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : NoMinOrder α
inst_3 : ClosedIicTopology α
s : Set α
hs : s ∈ cocompact α
t : Set α
ht : IsCompact t
hts : tᶜ ⊆ s
⊢ Membership.mem (γ := Filter α) atBot s

Tactic:
(Set.eq_empty_or_nonempty t).casesOn (fun h_empty ↦ ?_) (fun h_nonempty ↦ ?_)

Premises used: Or.casesOn, Set.eq_empty_or_nonempty
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : NoMinOrder α
inst_3 : ClosedIicTopology α
s : Set α
hs : s ∈ cocompact α
t : Set α
ht : IsCompact t
hts : tᶜ ⊆ s
refine_1 : ∀ (h_empty : t = ∅), Membership.mem (γ := Filter α) atBot s
refine_2 : ∀ (h_nonempty : t.Nonempty), Membership.mem (γ := Filter α) atBot s
⊢ Membership.mem (γ := Filter α) atBot s

Tactic:
refine (Set.eq_empty_or_nonempty t).casesOn (fun h_empty ↦ ?_) (fun h_nonempty ↦ ?_)
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : NoMinOrder α
inst_3 : ClosedIicTopology α
s : Set α
hs : s ∈ cocompact α
t : Set α
ht : IsCompact t
hts : tᶜ ⊆ s
h_empty : t = ∅
⊢ s = univ

Tactic:
rewrite [compl_univ_iff.mpr h_empty, univ_subset_iff] at hts

Premises used: Iff.mpr, Set.univ_subset_iff, Set.compl_univ_iff
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : NoMinOrder α
inst_3 : ClosedIicTopology α
s : Set α
hs : s ∈ cocompact α
t : Set α
ht : IsCompact t
hts : tᶜ ⊆ s
h_empty : t = ∅
hts₁ : s = univ
⊢ t = ∅

Tactic:
rewrite [compl_univ_iff.mpr h_empty, univ_subset_iff] at hts

Premises used: Iff.mpr, Set.univ_subset_iff, Set.compl_univ_iff
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : NoMinOrder α
inst_3 : ClosedIicTopology α
s : Set α
hs : s ∈ cocompact α
t : Set α
ht : IsCompact t
hts : s = univ
h_empty : t = ∅
⊢ Membership.mem (γ := Filter α) atBot univ

Tactic:
univ_mem

Premises used: Filter.univ_mem
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : NoMinOrder α
inst_3 : ClosedIicTopology α
s : Set α
hs : s ∈ cocompact α
t : Set α
ht : IsCompact t
hts : s = univ
h_empty : t = ∅
⊢ Membership.mem (γ := Filter α) atBot s

Tactic:
convert! univ_mem

Premises used: Filter.univ_mem
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : NoMinOrder α
inst_3 : ClosedIicTopology α
s : Set α
hs : s ∈ cocompact α
t : Set α
ht : IsCompact t
hts : tᶜ ⊆ s
h_nonempty : t.Nonempty
⊢ Nonempty α

Tactic:
haveI := h_nonempty.nonempty
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : NoMinOrder α
inst_3 : ClosedIicTopology α
s : Set α
hs : s ∈ cocompact α
t : Set α
ht : IsCompact t
hts : tᶜ ⊆ s
h_nonempty : t.Nonempty
this : Nonempty α
refine_2 : ∀ (a : α) (ha : IsLeast t a), Membership.mem (γ := Filter α) atBot s
⊢ Membership.mem (γ := Filter α) atBot s

Tactic:
obtain ⟨a, ha⟩ := ht.exists_isLeast h_nonempty

Premises used: IsCompact.exists_isLeast
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : NoMinOrder α
inst_3 : ClosedIicTopology α
s : Set α
hs : s ∈ cocompact α
t : Set α
ht : IsCompact t
hts : tᶜ ⊆ s
h_nonempty : t.Nonempty
this : Nonempty α
a : α
ha : IsLeast t a
refine_2 : ∀ (b : α) (hb : b < a), Membership.mem (γ := Filter α) atBot s
⊢ Membership.mem (γ := Filter α) atBot s

Tactic:
obtain ⟨b, hb⟩ := exists_lt a

Premises used: NoMinOrder.exists_lt
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : NoMinOrder α
inst_3 : ClosedIicTopology α
s : Set α
hs : s ∈ cocompact α
t : Set α
ht : IsCompact t
hts : tᶜ ⊆ s
h_nonempty : t.Nonempty
this : Nonempty α
a : α
ha : IsLeast t a
b : α
hb : b < a
⊢ Membership.mem (γ := Filter α) atBot s

Tactic:
Filter.mem_atBot_sets.mpr ⟨b, fun b' hb' ↦ hts <| Classical.byContradiction
      fun hc ↦ LT.lt.false <| hb'.trans_lt <| hb.trans_le <| ha.2 (not_notMem.mp hc)⟩

Premises used: Iff.mpr, Classical.byContradiction, Set.not_notMem, And.right, LT.lt.trans_le, Exists.intro, Iff.mp, LT.lt.false, LE.le.trans_lt, Filter.mem_atBot_sets
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : NoMinOrder α
inst_3 : ClosedIicTopology α
s : Set α
hs : s ∈ cocompact α
t : Set α
ht : IsCompact t
hts : tᶜ ⊆ s
h_nonempty : t.Nonempty
this : Nonempty α
a : α
ha : IsLeast t a
b : α
hb : b < a
⊢ Membership.mem (γ := Filter α) atBot s

Tactic:
exact Filter.mem_atBot_sets.mpr ⟨b, fun b' hb' ↦ hts <| Classical.byContradiction
      fun hc ↦ LT.lt.false <| hb'.trans_lt <| hb.trans_le <| ha.2 (not_notMem.mp hc)⟩

Premises used: Iff.mpr, Classical.byContradiction, Set.not_notMem, And.right, LT.lt.trans_le, Exists.intro, Iff.mp, LT.lt.false, LE.le.trans_lt, Filter.mem_atBot_sets
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : NoMaxOrder α
inst_3 : ClosedIciTopology α
⊢ atTop ≤ cocompact α

Tactic:
atBot_le_cocompact (α := αᵒᵈ)

Premises used: Set.Ici, Set.Mem, setOf, OrderDual, atBot_le_cocompact
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : NoMinOrder α
inst_3 : NoMaxOrder α
inst_4 : OrderClosedTopology α
⊢ atBot ⊔ atTop ≤ cocompact α

Tactic:
sup_le atBot_le_cocompact atTop_le_cocompact

Premises used: Set.Mem, sup_le, atTop_le_cocompact, atBot_le_cocompact
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : NoMaxOrder α
inst_3 : NoMinOrder α
inst_4 : OrderClosedTopology α
inst_5 : CompactIccSpace α
⊢ cocompact α = atBot ⊔ atTop

Tactic:
cocompact_le_atBot_atTop.antisymm atBot_atTop_le_cocompact

Premises used: atBot_atTop_le_cocompact, LE.le.antisymm, cocompact_le_atBot_atTop
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : NoMinOrder α
inst_3 : OrderTop α
inst_4 : ClosedIicTopology α
inst_5 : CompactIccSpace α
⊢ cocompact α = atBot

Tactic:
cocompact_le_atBot.antisymm atBot_le_cocompact

Premises used: cocompact_le_atBot, LE.le.antisymm, atBot_le_cocompact
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : NoMaxOrder α
inst_3 : OrderBot α
inst_4 : ClosedIciTopology α
inst_5 : CompactIccSpace α
⊢ cocompact α = atTop

Tactic:
cocompact_le_atTop.antisymm atTop_le_cocompact

Premises used: cocompact_le_atTop, LE.le.antisymm, atTop_le_cocompact
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
s : Set β
hs : IsCompact s
ne_s : s.Nonempty
f : β → α
hf : ContinuousOn f s
rcases : ∀ (x : β) (hxs : x ∈ s) (hx : f x ∈ lowerBounds (f '' s)), ∃ x ∈ s, IsMinOn f s x
⊢ ∃ x ∈ s, IsMinOn f s x

Tactic:
rcases (hs.image_of_continuousOn hf).exists_isLeast (ne_s.image f) with ⟨_, ⟨x, hxs, rfl⟩, hx⟩

Premises used: IsCompact.exists_isLeast, Set.Nonempty.image, IsCompact.image_of_continuousOn, rfl