awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Order.Category.AlexDisc (goal)
Goal:
α β : AlexDisc
e : (↑α.toTopCat : Type u_1) ≃ₜ (↑β.toTopCat : Type u_1)
⊢ ConcreteCategory.ofHom (FC := fun (x1 x2 : AlexDisc.{u_1}) ↦ C((↑x1.toTopCat : Type u_1), (↑x2.toTopCat : Type u_1)))
        (CC := fun (X : AlexDisc.{u_1}) ↦ (↑X.toTopCat : Type u_1))
        (↑e : C((↑α.toTopCat : Type u_1), (↑β.toTopCat : Type u_1))) ≫
      ConcreteCategory.ofHom (FC := fun (x1 x2 : AlexDisc.{u_1}) ↦
        C((↑x1.toTopCat : Type u_1), (↑x2.toTopCat : Type u_1))) (CC := fun (X : AlexDisc.{u_1}) ↦
        (↑X.toTopCat : Type u_1)) (↑e.symm : C((↑β.toTopCat : Type u_1), (↑α.toTopCat : Type u_1))) =
    𝟙 α
have h : ∀ (a : (↑α.toTopCat : Type u_1)),
  Eq (α := (↑α.toTopCat : Type u_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AlexDisc.{u_1}) ↦
            C((↑x1.toTopCat : Type u_1), (↑x2.toTopCat : Type u_1))) (CC := fun (X : AlexDisc.{u_1}) ↦
            (↑X.toTopCat : Type u_1))
            (ConcreteCategory.ofHom (FC := fun (x1 x2 : AlexDisc.{u_1}) ↦
                C((↑x1.toTopCat : Type u_1), (↑x2.toTopCat : Type u_1))) (CC := fun (X : AlexDisc.{u_1}) ↦
                (↑X.toTopCat : Type u_1)) (↑e : C((↑α.toTopCat : Type u_1), (↑β.toTopCat : Type u_1))) ≫
              ConcreteCategory.ofHom (FC := fun (x1 x2 : AlexDisc.{u_1}) ↦
                C((↑x1.toTopCat : Type u_1), (↑x2.toTopCat : Type u_1))) (CC := fun (X : AlexDisc.{u_1}) ↦
                (↑X.toTopCat : Type u_1)) (↑e.symm : C((↑β.toTopCat : Type u_1), (↑α.toTopCat : Type u_1)))) :
          (a : (↑α.toTopCat : Type u_1)) → (↑α.toTopCat : Type u_1))
        a :
      (↑α.toTopCat : Type u_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AlexDisc.{u_1}) ↦
            C((↑x1.toTopCat : Type u_1), (↑x2.toTopCat : Type u_1))) (CC := fun (X : AlexDisc.{u_1}) ↦
            (↑X.toTopCat : Type u_1)) (𝟙 α) :
          (a : (↑α.toTopCat : Type u_1)) → (↑α.toTopCat : Type u_1))
        a :
      (↑α.toTopCat : Type u_1))
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Order.Category.AlexDisc (goal)
Goal:
α β : AlexDisc
e : (↑α.toTopCat : Type u_1) ≃ₜ (↑β.toTopCat : Type u_1)
⊢ ConcreteCategory.ofHom (FC := fun (x1 x2 : AlexDisc.{u_1}) ↦ C((↑x1.toTopCat : Type u_1), (↑x2.toTopCat : Type u_1)))
        (CC := fun (X : AlexDisc.{u_1}) ↦ (↑X.toTopCat : Type u_1))
        (↑e.symm : C((↑β.toTopCat : Type u_1), (↑α.toTopCat : Type u_1))) ≫
      ConcreteCategory.ofHom (FC := fun (x1 x2 : AlexDisc.{u_1}) ↦
        C((↑x1.toTopCat : Type u_1), (↑x2.toTopCat : Type u_1))) (CC := fun (X : AlexDisc.{u_1}) ↦
        (↑X.toTopCat : Type u_1)) (↑e : C((↑α.toTopCat : Type u_1), (↑β.toTopCat : Type u_1))) =
    𝟙 β
have h : ∀ (a : (↑β.toTopCat : Type u_1)),
  Eq (α := (↑β.toTopCat : Type u_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AlexDisc.{u_1}) ↦
            C((↑x1.toTopCat : Type u_1), (↑x2.toTopCat : Type u_1))) (CC := fun (X : AlexDisc.{u_1}) ↦
            (↑X.toTopCat : Type u_1))
            (ConcreteCategory.ofHom (FC := fun (x1 x2 : AlexDisc.{u_1}) ↦
                C((↑x1.toTopCat : Type u_1), (↑x2.toTopCat : Type u_1))) (CC := fun (X : AlexDisc.{u_1}) ↦
                (↑X.toTopCat : Type u_1)) (↑e.symm : C((↑β.toTopCat : Type u_1), (↑α.toTopCat : Type u_1))) ≫
              ConcreteCategory.ofHom (FC := fun (x1 x2 : AlexDisc.{u_1}) ↦
                C((↑x1.toTopCat : Type u_1), (↑x2.toTopCat : Type u_1))) (CC := fun (X : AlexDisc.{u_1}) ↦
                (↑X.toTopCat : Type u_1)) (↑e : C((↑α.toTopCat : Type u_1), (↑β.toTopCat : Type u_1)))) :
          (a : (↑β.toTopCat : Type u_1)) → (↑β.toTopCat : Type u_1))
        a :
      (↑β.toTopCat : Type u_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AlexDisc.{u_1}) ↦
            C((↑x1.toTopCat : Type u_1), (↑x2.toTopCat : Type u_1))) (CC := fun (X : AlexDisc.{u_1}) ↦
            (↑X.toTopCat : Type u_1)) (𝟙 β) :
          (a : (↑β.toTopCat : Type u_1)) → (↑β.toTopCat : Type u_1))
        a :
      (↑β.toTopCat : Type u_1))
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Order.Category.AlexDisc (goal)
Goal:
X : AlexDisc
⊢ (↑(Functor.obj (𝟭 AlexDisc) X).toTopCat : Type u_1) ≃ₜ
    (↑(AlexDisc.toTopCat
          (Functor.obj
            ((forget₂ AlexDisc (FC := fun (x1 x2 : AlexDisc.{u_1}) ↦
                  C((↑x1.toTopCat : Type u_1), (↑x2.toTopCat : Type u_1))) (CC := fun (X : AlexDisc.{u_1}) ↦
                  (↑X.toTopCat : Type u_1)) TopCat (FD := fun (X Y : TopCat.{u_1}) ↦
                  C((↑X : Type u_1), (↑Y : Type u_1))) (CD := TopCat.carrier) ⋙
                topToPreord) ⋙
              { obj := fun (X : Preord.{u_1}) ↦ AlexDisc.of (WithUpperSet (↑X : Type u_1)),
                map := fun {X Y : Preord.{u_1}} (f : X ⟶ Y) ↦
                  ConcreteCategory.ofHom (FC := fun (x1 x2 : AlexDisc.{u_1}) ↦
                    C((↑x1.toTopCat : Type u_1), (↑x2.toTopCat : Type u_1))) (CC := fun (X : AlexDisc.{u_1}) ↦
                    (↑X.toTopCat : Type u_1)) (WithUpperSet.map (Preord.Hom.hom f)),
                map_id := alexDiscEquivPreord._proof_1, map_comp := @alexDiscEquivPreord._proof_2 })
            X)) :
      Type u_1)
have dsimp : (↑X.toTopCat : Type u_1) ≃ₜ WithUpperSet (Specialization (↑X.toTopCat : Type u_1))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Topology.Order.Category.AlexDisc (goal)
Goal:
X : Preord
⊢ (↑(Functor.obj
          ({ obj := fun (X : Preord.{u_1}) ↦ AlexDisc.of (WithUpperSet (↑X : Type u_1)),
              map := fun {X Y : Preord.{u_1}} (f : X ⟶ Y) ↦
                ConcreteCategory.ofHom (FC := fun (x1 x2 : AlexDisc.{u_1}) ↦
                  C((↑x1.toTopCat : Type u_1), (↑x2.toTopCat : Type u_1))) (CC := fun (X : AlexDisc.{u_1}) ↦
                  (↑X.toTopCat : Type u_1)) (WithUpperSet.map (Preord.Hom.hom f)),
              map_id := alexDiscEquivPreord._proof_1, map_comp := @alexDiscEquivPreord._proof_2 } ⋙
            forget₂ AlexDisc (FC := fun (x1 x2 : AlexDisc.{u_1}) ↦
                C((↑x1.toTopCat : Type u_1), (↑x2.toTopCat : Type u_1))) (CC := fun (X : AlexDisc.{u_1}) ↦
                (↑X.toTopCat : Type u_1)) TopCat (FD := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1)))
                (CD := TopCat.carrier) ⋙
              topToPreord)
          X) :
      Type u_1) ≃o
    (↑(Functor.obj (𝟭 Preord) X) : Type u_1)
have dsimp : Specialization (WithUpperSet (↑X : Type u_1)) ≃o (↑X : Type u_1)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Topology.Order.Category.FrameAdjunction (goal)
Goal:
L : Type u_1
inst : CompleteLattice L
S : Set L
⊢ Eq (α := Set (PT L)) {x : PT L | (x : (a : L) → Prop) (sSup S)}
    (sSup ((fun (u : L) ↦ {x : PT L | (x : (a : L) → Prop) u}) '' S))
have h : ∀ (x : PT L),
  Membership.mem (γ := Set (PT L)) {x : PT L | (x : (a : L) → Prop) (sSup S)} x ↔
    Membership.mem (γ := Set (PT L)) (sSup ((fun (u : L) ↦ {x : PT L | (x : (a : L) → Prop) u}) '' S)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Order.Category.FrameAdjunction (goal)
Goal:
L : Type u_1
inst : CompleteLattice L
u v : L
⊢ ∃ (u_1 : L),
    Eq.{u_1 + 1} (α := Set (PT L)) {x : PT L | (x : (a : L) → Prop) u_1}
      ({x : PT L | (x : (a : L) → Prop) u} ∩ {x : PT L | (x : (a : L) → Prop) v})
have h : Eq.{u_1 + 1} (α := Set (PT L)) {x : PT L | (x : (a : L) → Prop) (u ⊓ v)}
  ({x : PT L | (x : (a : L) → Prop) u} ∩ {x : PT L | (x : (a : L) → Prop) v})
Tactic: use u ⊓ v
-- Lean 4 proof step from Mathlib.Topology.Order.Category.FrameAdjunction (goal)
Goal:
L : Type u_1
inst : CompleteLattice L
u v : L
⊢ Eq.{u_1 + 1} (α := Set (PT L)) {x : PT L | (x : (a : L) → Prop) (u ⊓ v)}
    ({x : PT L | (x : (a : L) → Prop) u} ∩ {x : PT L | (x : (a : L) → Prop) v})
have h : Eq.{u_1 + 1} (α := Set (PT L)) {x : PT L | min ((x : (a : L) → Prop) u) ((x : (a : L) → Prop) v)}
  ({x : PT L | (x : (a : L) → Prop) u} ∩ {x : PT L | (x : (a : L) → Prop) v})
Tactic: simp_rw [map_inf]
-- Lean 4 proof step from Mathlib.Topology.Order.Category.FrameAdjunction (goal)
Goal:
L : Type u_1
inst : CompleteLattice L
S : Set (Set (PT L))
hS : ∀ t ∈ S, ∃ (u : L), {x : PT L | (x : (a : L) → Prop) u} = t
⊢ ∃ (u : L), {x : PT L | (x : (a : L) → Prop) u} = ⋃₀ S
have choose : ∀ (f : (t : Set (PT L)) → t ∈ S → L)
  (hf : ∀ (t : Set (PT L)) (a : t ∈ S), {x : PT L | (x : (a : L) → Prop) (f t a)} = t),
  ∃ (u : L), {x : PT L | (x : (a : L) → Prop) u} = ⋃₀ S
Tactic: choose f hf using hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.Topology.Order.Category.FrameAdjunction (goal)
Goal:
L : Type u_1
inst : CompleteLattice L
S : Set (Set (PT L))
f : (t : Set (PT L)) → t ∈ S → L
hf : ∀ (t : Set (PT L)) (a : t ∈ S), {x : PT L | (x : (a : L) → Prop) (f t a)} = t
⊢ ∃ (u : L), {x : PT L | (x : (a : L) → Prop) u} = ⋃₀ S
have h : {x : PT L | (x : (a : L) → Prop) (⨆ (t : Set (PT L)), ⨆ (ht : t ∈ S), f t ht)} = ⋃₀ S
Tactic: use ⨆ t, ⨆ ht, f t ht
-- Lean 4 proof step from Mathlib.Topology.Order.Category.FrameAdjunction (goal)
Goal:
L : Type u_1
inst : CompleteLattice L
S : Set (Set (PT L))
f : (t : Set (PT L)) → t ∈ S → L
hf : ∀ (t : Set (PT L)) (a : t ∈ S), {x : PT L | (x : (a : L) → Prop) (f t a)} = t
⊢ {x : PT L | (x : (a : L) → Prop) (⨆ (t : Set (PT L)), ⨆ (ht : t ∈ S), f t ht)} = ⋃₀ S
have h : {x : PT L | ⨆ (i : Set (PT L)), ⨆ (i_1 : i ∈ S), (x : (a : L) → Prop) (f i i_1)} = ⋃₀ S
Tactic: simp_rw [map_iSup, iSup_Prop_eq, setOf_exists, hf, sUnion_eq_biUnion]
-- Lean 4 proof step from Mathlib.Topology.Order.Category.FrameAdjunction (goal)
Goal:
L : Type u_1
inst : CompleteLattice L
S : Set (Set (PT L))
f : (t : Set (PT L)) → t ∈ S → L
hf : ∀ (t : Set (PT L)) (a : t ∈ S), {x : PT L | (x : (a : L) → Prop) (f t a)} = t
h : {x : PT L | ⨆ (i : Set (PT L)), ⨆ (i_1 : i ∈ S), (x : (a : L) → Prop) (f i i_1)} = ⋃₀ S
⊢ {x : PT L | (x : (a : L) → Prop) (⨆ (t : Set (PT L)), ⨆ (ht : t ∈ S), f t ht)} = ⋃₀ S
have h₁ : {x : PT L | ∃ (i : Set (PT L)) (i_1 : i ∈ S), (x : (a : L) → Prop) (f i i_1)} = ⋃₀ S
Tactic: simp_rw [map_iSup, iSup_Prop_eq, setOf_exists, hf, sUnion_eq_biUnion]
-- Lean 4 proof step from Mathlib.Topology.Order.Category.FrameAdjunction (goal)
Goal:
L : Type u_1
inst : CompleteLattice L
S : Set (Set (PT L))
f : (t : Set (PT L)) → t ∈ S → L
hf : ∀ (t : Set (PT L)) (a : t ∈ S), {x : PT L | (x : (a : L) → Prop) (f t a)} = t
h : {x : PT L | ⨆ (i : Set (PT L)), ⨆ (i_1 : i ∈ S), (x : (a : L) → Prop) (f i i_1)} = ⋃₀ S
h₁ : {x : PT L | ∃ (i : Set (PT L)) (i_1 : i ∈ S), (x : (a : L) → Prop) (f i i_1)} = ⋃₀ S
⊢ {x : PT L | (x : (a : L) → Prop) (⨆ (t : Set (PT L)), ⨆ (ht : t ∈ S), f t ht)} = ⋃₀ S
have h₂ : ⋃ (i : Set (PT L)), ⋃ (i_1 : i ∈ S), {x : PT L | (x : (a : L) → Prop) (f i i_1)} = ⋃₀ S
Tactic: simp_rw [map_iSup, iSup_Prop_eq, setOf_exists, hf, sUnion_eq_biUnion]
-- Lean 4 proof step from Mathlib.Topology.Order.Category.FrameAdjunction (goal)
Goal:
L : Type u_1
inst : CompleteLattice L
S : Set (Set (PT L))
f : (t : Set (PT L)) → t ∈ S → L
hf : ∀ (t : Set (PT L)) (a : t ∈ S), {x : PT L | (x : (a : L) → Prop) (f t a)} = t
h : {x : PT L | ⨆ (i : Set (PT L)), ⨆ (i_1 : i ∈ S), (x : (a : L) → Prop) (f i i_1)} = ⋃₀ S
h₁ : {x : PT L | ∃ (i : Set (PT L)) (i_1 : i ∈ S), (x : (a : L) → Prop) (f i i_1)} = ⋃₀ S
h₂ : ⋃ (i : Set (PT L)), ⋃ (i_1 : i ∈ S), {x : PT L | (x : (a : L) → Prop) (f i i_1)} = ⋃₀ S
⊢ {x : PT L | (x : (a : L) → Prop) (⨆ (t : Set (PT L)), ⨆ (ht : t ∈ S), f t ht)} = ⋃₀ S
have h₃ : ⋃ i ∈ S, i = ⋃₀ S
Tactic: simp_rw [map_iSup, iSup_Prop_eq, setOf_exists, hf, sUnion_eq_biUnion]
-- Lean 4 proof step from Mathlib.Topology.Order.Category.FrameAdjunction (goal)
Goal:
L : Type u_1
inst : CompleteLattice L
X Y : Locale
f : X ⟶ Y
u : (↑(Opposite.unop Y) : Type u_2)
⊢ IsOpen.{u_2} (X := PT (↑(Opposite.unop X) : Type u_2))
    (preimage (β := PT (↑(Opposite.unop Y) : Type u_2))
      (fun (p : PT (↑(Opposite.unop X) : Type u_2)) ↦ FrameHom.comp p (Frm.Hom.hom f.unop))
      {x : PT (↑(Opposite.unop Y) : Type u_2) | (x : (a : (↑(Opposite.unop Y) : Type u_2)) → Prop) u})
have h : Eq.{u_2 + 1} (α := Set (PT (↑(Opposite.unop X) : Type u_2)))
  {x : PT (↑(Opposite.unop X) : Type u_2) |
    (x : (a : (↑(Opposite.unop X) : Type u_2)) → Prop)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : Frm.{u_2}) ↦ FrameHom (↑x1 : Type u_2) (↑x2 : Type u_2)) (CC :=
              Frm.carrier) f.unop :
            (a : (↑(Opposite.unop Y) : Type u_2)) → (↑(Opposite.unop X) : Type u_2))
          u :
        (↑(Opposite.unop X) : Type u_2))}
  (preimage (β := PT (↑(Opposite.unop Y) : Type u_2))
    (fun (p : PT (↑(Opposite.unop X) : Type u_2)) ↦ FrameHom.comp p (Frm.Hom.hom f.unop))
    {x : PT (↑(Opposite.unop Y) : Type u_2) | (x : (a : (↑(Opposite.unop Y) : Type u_2)) → Prop) u})
Tactic: use f.unop u
-- Lean 4 proof step from Mathlib.Topology.Order.Category.FrameAdjunction (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
L : Locale
S : Set (↑(Opposite.unop L) : Type u_2)
⊢ Eq (α := Opens (PT (↑(Opposite.unop L) : Type u_2)))
    {
      carrier :=
        (openOfElementHom (↑(Opposite.unop L) : Type u_2) :
            (a : (↑(Opposite.unop L) : Type u_2)) → Set (PT (↑(Opposite.unop L) : Type u_2)))
          (sSup S),
      is_open' := ⋯ }
    (sSup
      ((fun (u : (↑(Opposite.unop L) : Type u_2)) ↦
          {
            carrier :=
              (openOfElementHom (↑(Opposite.unop L) : Type u_2) :
                  (a : (↑(Opposite.unop L) : Type u_2)) → Set (PT (↑(Opposite.unop L) : Type u_2)))
                u,
            is_open' := ⋯ }) ''
        S))
have h : ∀ (x : PT (↑(Opposite.unop L) : Type u_2)),
  x ∈
      (↑{
            carrier :=
              (openOfElementHom (↑(Opposite.unop L) : Type u_2) :
                  (a : (↑(Opposite.unop L) : Type u_2)) → Set (PT (↑(Opposite.unop L) : Type u_2)))
                (sSup S),
            is_open' := sorry : Opens (PT (↑(Opposite.unop L) : Type u_2)) } :
        Set (PT (↑(Opposite.unop L) : Type u_2))) ↔
    x ∈
      (↑(sSup
            ((fun (u : (↑(Opposite.unop L) : Type u_2)) ↦
                {
                  carrier :=
                    (openOfElementHom (↑(Opposite.unop L) : Type u_2) :
                        (a : (↑(Opposite.unop L) : Type u_2)) → Set (PT (↑(Opposite.unop L) : Type u_2)))
                      u,
                  is_open' := sorry : Opens (PT (↑(Opposite.unop L) : Type u_2)) }) ''
              S)) :
        Set (PT (↑(Opposite.unop L) : Type u_2)))
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Preorder α
h : ∀ {a b : α}, a ≤ b → IsCompact (Icc a b)
a b : α
hab : ¬a ≤ b
⊢ IsCompact (Icc a b)
have rw : IsCompact.{u_1} (X := α) ∅
Tactic: rw [Icc_eq_empty hab]
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : CompactIccSpace α
a b : αᵒᵈ
⊢ IsCompact (Icc a b)
have h : αᵒᵈ = α → Icc a b = Icc b a
Tactic: convert! isCompact_Icc (α := α) (a := b) (b := a) using 1
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (hypothesis)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : ClosedIicTopology α
s : Set α
hs : IsCompact s
ne_s : s.Nonempty
⊢ ∃ (x : α), IsLeast s x
have this : Nonempty.{u_2 + 1} (↑s : Type u_2)
Tactic: haveI : Nonempty s := ne_s.to_subtype
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
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)
⊢ ∃ (x : α), IsLeast s x
have suffices : (s ∩ ⋂ x ∈ s, Iic x).Nonempty
Tactic: suffices (s ∩ ⋂ x ∈ s, Iic x).Nonempty from
    ⟨this.choose, this.choose_spec.1, mem_iInter₂.mp this.choose_spec.2⟩
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
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)
⊢ (s ∩ ⋂ x ∈ s, Iic x).Nonempty
have rw : (s ∩ ⋂ (x : (↑s : Type u_2)), Iic (↑x : α)).Nonempty
Tactic: rw [biInter_eq_iInter]
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
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)
⊢ (s ∩ ⋂ (x : (↑s : Type u_2)), Iic (↑x : α)).Nonempty
have by_contra : ∀ (H : ¬(s ∩ ⋂ (x : (↑s : Type u_2)), Iic (↑x : α)).Nonempty), False
Tactic: by_contra H
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (hypothesis)
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
⊢ False
have H₁ : s ∩ ⋂ (x : (↑s : Type u_2)), Iic (↑x : α) = ∅
Tactic: rw [not_nonempty_iff_eq_empty] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
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 : α) = ∅
⊢ False
have rcases : ∀ (x : (↑s : Type u_2)) (hx : s ∩ Iic (↑x : α) = ∅), 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⟩
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : CompactIccSpace α
⊢ cocompact α ≤ atBot ⊔ atTop
have refine_1 : ∀ (s : Set α) (hs : Membership.mem (γ := Filter α) (atBot ⊔ atTop) s) (h : IsEmpty α),
  ∃ (t : Set α), IsCompact t ∧ tᶜ ⊆ s
Tactic: refine fun s hs ↦ mem_cocompact.mpr <| (isEmpty_or_nonempty α).casesOn ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
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
⊢ cocompact α ≤ atBot ⊔ atTop
have refine_2 : ∀ (s : Set α) (hs : Membership.mem (γ := Filter α) (atBot ⊔ atTop) s) (h : Nonempty α),
  ∃ (t : Set α), IsCompact t ∧ tᶜ ⊆ s
Tactic: refine fun s hs ↦ mem_cocompact.mpr <| (isEmpty_or_nonempty α).casesOn ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : CompactIccSpace α
s : Set α
hs : Membership.mem (γ := Filter α) (atBot ⊔ atTop) s
h : Nonempty α
⊢ ∃ (t : Set α), IsCompact t ∧ tᶜ ⊆ s
have refine_2 : ∀ (t : α) (ht : ∀ b ≤ t, b ∈ s), ∃ (t : Set α), IsCompact t ∧ tᶜ ⊆ s
Tactic: obtain ⟨t, ht⟩ := mem_atBot_sets.mp hs.1
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
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
⊢ ∃ (t : Set α), IsCompact t ∧ tᶜ ⊆ s
have refine_2 : ∀ (u : α) (hu : ∀ b ≥ u, b ∈ s), ∃ (t : Set α), IsCompact t ∧ tᶜ ⊆ s
Tactic: obtain ⟨u, hu⟩ := mem_atTop_sets.mp hs.2
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
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
have refine_2 : ∀ (x : α) (hx : x ∈ (Icc t u)ᶜ), x ∈ s
Tactic: refine ⟨Icc t u, isCompact_Icc, fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTop α
inst_3 : CompactIccSpace α
⊢ cocompact α ≤ atBot
have refine_1 : ∀ (x : Set α) (hs : Membership.mem (γ := Filter α) atBot x) (h : IsEmpty α), ∃ (t : Set α), IsCompact t ∧ tᶜ ⊆ x
Tactic: refine fun _ hs ↦ mem_cocompact.mpr <| (isEmpty_or_nonempty α).casesOn ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
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
⊢ cocompact α ≤ atBot
have refine_2 : ∀ (x : Set α) (hs : Membership.mem (γ := Filter α) atBot x) (h : Nonempty α), ∃ (t : Set α), IsCompact t ∧ tᶜ ⊆ x
Tactic: refine fun _ hs ↦ mem_cocompact.mpr <| (isEmpty_or_nonempty α).casesOn ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
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 : Set α), IsCompact t ∧ tᶜ ⊆ x
have refine_2 : ∀ (t : α) (ht : ∀ b ≤ t, b ∈ x), ∃ (t : Set α), IsCompact t ∧ tᶜ ⊆ x
Tactic: obtain ⟨t, ht⟩ := mem_atBot_sets.mp hs
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
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
have refine_2 : ∀ (x_1 : α) (hx : x_1 ∈ (Icc t ⊤)ᶜ), x_1 ∈ x
Tactic: refine ⟨Icc t ⊤, isCompact_Icc, fun _ hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : NoMinOrder α
inst_3 : ClosedIicTopology α
⊢ atBot ≤ cocompact α
have refine : ∀ (s : Set α) (hs : s ∈ cocompact α), Membership.mem (γ := Filter α) atBot s
Tactic: refine fun s hs ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : NoMinOrder α
inst_3 : ClosedIicTopology α
s : Set α
hs : s ∈ cocompact α
⊢ Membership.mem (γ := Filter α) atBot s
have obtain : ∀ (t : Set α) (ht : IsCompact t) (hts : tᶜ ⊆ s), Membership.mem (γ := Filter α) atBot s
Tactic: obtain ⟨t, ht, hts⟩ := mem_cocompact.mp hs
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
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
have refine_1 : ∀ (h_empty : t = ∅), Membership.mem (γ := Filter α) atBot s
Tactic: refine (Set.eq_empty_or_nonempty t).casesOn (fun h_empty ↦ ?_) (fun h_nonempty ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
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
⊢ Membership.mem (γ := Filter α) atBot s
have refine_2 : ∀ (h_nonempty : t.Nonempty), Membership.mem (γ := Filter α) atBot s
Tactic: refine (Set.eq_empty_or_nonempty t).casesOn (fun h_empty ↦ ?_) (fun h_nonempty ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (hypothesis)
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 = ∅
⊢ Membership.mem (γ := Filter α) atBot s
have hts₁ : s = univ
Tactic: rewrite [compl_univ_iff.mpr h_empty, univ_subset_iff] at hts
Cleared hypotheses: hts, h_empty
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (hypothesis)
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
⊢ Membership.mem (γ := Filter α) atBot s
have this : Nonempty α
Tactic: haveI := h_nonempty.nonempty