awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.Category.AlexDisc
Goal:
α β : AlexDisc
e : (↑α.toTopCat : Type u_1) ≃ₜ (↑β.toTopCat : Type u_1)
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))
⊢ 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))) =
    𝟙 α

Tactic:
ext
-- Module: Mathlib.Topology.Order.Category.AlexDisc
Goal:
α β : AlexDisc
e : (↑α.toTopCat : Type u_1) ≃ₜ (↑β.toTopCat : Type u_1)
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:
apply e.symm_apply_apply

Premises used: Homeomorph.symm_apply_apply
-- Module: Mathlib.Topology.Order.Category.AlexDisc
Goal:
α β : AlexDisc
e : (↑α.toTopCat : Type u_1) ≃ₜ (↑β.toTopCat : Type u_1)
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))
⊢ 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))) =
    𝟙 β

Tactic:
ext
-- Module: Mathlib.Topology.Order.Category.AlexDisc
Goal:
α β : AlexDisc
e : (↑α.toTopCat : Type u_1) ≃ₜ (↑β.toTopCat : Type u_1)
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:
apply e.apply_symm_apply

Premises used: Homeomorph.apply_symm_apply
-- Module: Mathlib.Topology.Order.Category.AlexDisc
Goal:
X : AlexDisc
dsimp : (↑X.toTopCat : Type u_1) ≃ₜ WithUpperSet (Specialization (↑X.toTopCat : Type u_1))
⊢ (↑(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)

Tactic:
dsimp
-- Module: Mathlib.Topology.Order.Category.AlexDisc
Goal:
X : AlexDisc
⊢ (↑X.toTopCat : Type u_1) ≃ₜ WithUpperSet (Specialization (↑X.toTopCat : Type u_1))

Tactic:
exact homeoWithUpperSetTopologyorderIso X

Premises used: homeoWithUpperSetTopologyorderIso, AlexDisc.toTopCat, TopCat.carrier
-- Module: Mathlib.Topology.Order.Category.AlexDisc
Goal:
X : Preord
dsimp : Specialization (WithUpperSet (↑X : Type u_1)) ≃o (↑X : Type u_1)
⊢ (↑(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)

Tactic:
dsimp
-- Module: Mathlib.Topology.Order.Category.AlexDisc
Goal:
X : Preord
⊢ Specialization (WithUpperSet (↑X : Type u_1)) ≃o (↑X : Type u_1)

Tactic:
exact (orderIsoSpecializationWithUpperSetTopology X).symm

Premises used: OrderIso.symm, orderIsoSpecializationWithUpperSetTopology, Preord.carrier
-- Module: Mathlib.Topology.Order.Category.FrameAdjunction
Goal:
L : Type u_1
inst : CompleteLattice L
a b : L
⊢ Eq.{u_1 + 1} (α := Set (PT L)) {x : PT L | (x : (a : L) → Prop) (a ⊓ b)}
    ({x : PT L | (x : (a : L) → Prop) a} ⊓ {x : PT L | (x : (a : L) → Prop) b})

Tactic:
simp [Set.setOf_and]

Premises used: Set.setOf_and
-- Module: Mathlib.Topology.Order.Category.FrameAdjunction
Goal:
L : Type u_1
inst : CompleteLattice L
⊢ Eq.{u_1 + 1} (α := Set (PT L)) {x : PT L | (x : (a : L) → Prop) ⊤} ⊤

Tactic:
simp
-- Module: Mathlib.Topology.Order.Category.FrameAdjunction
Goal:
L : Type u_1
inst : CompleteLattice L
S : Set L
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
⊢ 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))

Tactic:
ext
-- Module: Mathlib.Topology.Order.Category.FrameAdjunction
Goal:
L : Type u_1
inst : CompleteLattice L
S : Set L
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:
simp [Prop.exists_iff]

Premises used: Prop.exists_iff
-- Module: Mathlib.Topology.Order.Category.FrameAdjunction
Goal:
L : Type u_1
inst : CompleteLattice L
⊢ Eq.{u_1 + 1} (α := Set (PT L)) {x : PT L | (x : (a : L) → Prop) ⊤} univ

Tactic:
simp
-- Module: Mathlib.Topology.Order.Category.FrameAdjunction
Goal:
L : Type u_1
inst : CompleteLattice L
u v : L
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})
⊢ ∃ (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})

Tactic:
use u ⊓ v
-- Module: Mathlib.Topology.Order.Category.FrameAdjunction
Goal:
L : Type u_1
inst : CompleteLattice L
u v : L
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})
⊢ 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:
simp_rw [map_inf]

Premises used: InfHomClass.map_inf
-- Module: Mathlib.Topology.Order.Category.FrameAdjunction
Goal:
L : Type u_1
inst : CompleteLattice L
u v : L
⊢ 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:
rfl
-- Module: Mathlib.Topology.Order.Category.FrameAdjunction
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
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
⊢ ∃ (u : L), {x : PT L | (x : (a : L) → Prop) u} = ⋃₀ S

Tactic:
choose f hf using hS
-- Module: Mathlib.Topology.Order.Category.FrameAdjunction
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 | (x : (a : L) → Prop) (⨆ (t : Set (PT L)), ⨆ (ht : t ∈ S), f t ht)} = ⋃₀ S
⊢ ∃ (u : L), {x : PT L | (x : (a : L) → Prop) u} = ⋃₀ S

Tactic:
use ⨆ t, ⨆ ht, f t ht
-- Module: Mathlib.Topology.Order.Category.FrameAdjunction
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
h₃ : ⋃ i ∈ S, i = ⋃₀ S
⊢ {x : PT L | (x : (a : L) → Prop) (⨆ (t : Set (PT L)), ⨆ (ht : t ∈ S), f t ht)} = ⋃₀ S

Tactic:
simp_rw [map_iSup, iSup_Prop_eq, setOf_exists, hf, sUnion_eq_biUnion]

Premises used: Set.setOf_exists, Set.sUnion_eq_biUnion, iSup_Prop_eq, map_iSup
-- Module: Mathlib.Topology.Order.Category.FrameAdjunction
Goal:
L : Type u_1
inst : CompleteLattice L
U : Set (PT L)
⊢ IsOpen U ↔ ∃ (u : L), {x : PT L | (x : (a : L) → Prop) u} = U

Tactic:
Iff.rfl

Premises used: Iff.rfl, IsOpen
-- Module: Mathlib.Topology.Order.Category.FrameAdjunction
Goal:
L : Type u_1
inst : CompleteLattice L
X Y : Locale
f : X ⟶ Y
u : (↑(Opposite.unop Y) : Type u_2)
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})
⊢ 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})

Tactic:
use f.unop u

Premises used: CategoryTheory.ConcreteCategory.hom, Quiver.Hom.unop, DFunLike.coe
-- Module: Mathlib.Topology.Order.Category.FrameAdjunction
Goal:
L : Type u_1
inst : CompleteLattice L
X Y : Locale
f : X ⟶ Y
u : (↑(Opposite.unop Y) : Type u_2)
⊢ 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:
rfl
-- Module: Mathlib.Topology.Order.Category.FrameAdjunction
Goal:
X : Type u_1
inst : TopologicalSpace X
L : Locale
x : X
S : Set (Opens X)
⊢ (x ∈ sSup S) = sSup ((fun (x_1 : Opens X) ↦ x ∈ x_1) '' S)

Tactic:
simp [Prop.exists_iff]

Premises used: Prop.exists_iff
-- Module: Mathlib.Topology.Order.Category.FrameAdjunction
Goal:
X : Type u_1
inst : TopologicalSpace X
L : Locale
a b : (↑(Opposite.unop L) : Type u_2)
⊢ Eq.{u_2 + 1} (α := 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)))
          (a ⊓ b),
      is_open' := ⋯ }
    ({
        carrier :=
          (openOfElementHom (↑(Opposite.unop L) : Type u_2) :
              (a : (↑(Opposite.unop L) : Type u_2)) → Set (PT (↑(Opposite.unop L) : Type u_2)))
            a,
        is_open' := ⋯ } ⊓
      {
        carrier :=
          (openOfElementHom (↑(Opposite.unop L) : Type u_2) :
              (a : (↑(Opposite.unop L) : Type u_2)) → Set (PT (↑(Opposite.unop L) : Type u_2)))
            b,
        is_open' := ⋯ })

Tactic:
simp
-- Module: Mathlib.Topology.Order.Category.FrameAdjunction
Goal:
X : Type u_1
inst : TopologicalSpace X
L : Locale
⊢ Eq.{u_2 + 1} (α := 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)))
          ⊤,
      is_open' := ⋯ }
    ⊤

Tactic:
simp
-- Module: Mathlib.Topology.Order.Category.FrameAdjunction
Goal:
X : Type u_1
inst : TopologicalSpace X
L : Locale
S : Set (↑(Opposite.unop L) : Type u_2)
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' := ⋯ : 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' := ⋯ : Opens (PT (↑(Opposite.unop L) : Type u_2)) }) ''
                S)) :
          Set (PT (↑(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))

Tactic:
ext
-- Module: Mathlib.Topology.Order.Category.FrameAdjunction
Goal:
X : Type u_1
inst : TopologicalSpace X
L : Locale
S : Set (↑(Opposite.unop L) : Type u_2)
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' := ⋯ : 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' := ⋯ : Opens (PT (↑(Opposite.unop L) : Type u_2)) }) ''
              S)) :
        Set (PT (↑(Opposite.unop L) : Type u_2)))

Tactic:
simp
-- Module: Mathlib.Topology.Order.Category.FrameAdjunction
Goal:
X_1 : Type u_1
inst : TopologicalSpace X_1
L : Locale
X : TopCat
u : (↑(Opposite.unop (topToLocale.obj X)) : Type u_2)
⊢ IsOpen.{u_2} (X := (↑X : Type u_2))
    (preimage (β := PT (↑(Opposite.unop (topToLocale.obj X)) : Type u_2)) (localePointOfSpacePoint (↑X : Type u_2))
      {x : PT (↑(Opposite.unop (topToLocale.obj X)) : Type u_2) |
        (x : (a : (↑(Opposite.unop (topToLocale.obj X)) : Type u_2)) → Prop) u})

Tactic:
simpa using u.2

Premises used: TopologicalSpace.Opens.is_open'
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Preorder α
h : ∀ {a b : α}, a ≤ b → IsCompact (Icc a b)
a b : α
hab : ¬a ≤ b
rw : IsCompact.{u_1} (X := α) ∅
⊢ IsCompact (Icc a b)

Tactic:
rw [Icc_eq_empty hab]

Premises used: Set.Icc_eq_empty
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Preorder α
h : ∀ {a b : α}, a ≤ b → IsCompact (Icc a b)
a b : α
hab : ¬a ≤ b
⊢ IsCompact.{u_1} (X := α) ∅

Tactic:
isCompact_empty

Premises used: isCompact_empty
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Preorder α
h : ∀ {a b : α}, a ≤ b → IsCompact (Icc a b)
a b : α
hab : ¬a ≤ b
⊢ IsCompact.{u_1} (X := α) ∅

Tactic:
exact isCompact_empty

Premises used: isCompact_empty
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PartialOrder α
h : ∀ {a b : α}, a < b → IsCompact (Icc a b)
a : α
hab : a ≤ a
⊢ IsCompact (Icc a a)

Tactic:
simp
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : CompactIccSpace α
a b : αᵒᵈ
⊢ IsCompact (Icc b a)

Tactic:
isCompact_Icc (α := α) (a := b) (b := a)

Premises used: CompactIccSpace.isCompact_Icc
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : CompactIccSpace α
a b : αᵒᵈ
h : αᵒᵈ = α → Icc a b = Icc b a
⊢ IsCompact (Icc a b)

Tactic:
convert! isCompact_Icc (α := α) (a := b) (b := a) using 1

Premises used: CompactIccSpace.isCompact_Icc
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : CompactIccSpace α
a b : αᵒᵈ
e_1 : αᵒᵈ = α
⊢ Icc a b = Icc b a

Tactic:
Icc_toDual (α := α)

Premises used: Set.Mem, setOf, Set.Icc, Set.preimage, OrderDual, Set.Icc_toDual
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : CompactIccSpace α
a b : αᵒᵈ
e_1 : αᵒᵈ = α
⊢ Icc a b = Icc b a

Tactic:
exact Icc_toDual (α := α)

Premises used: Set.Icc_toDual
-- Module: Mathlib.Topology.Order.Compact
Goal:
α_1 : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
⊢ CompactIccSpace α

Tactic:
⟨fun {_ _} ↦ ConditionallyCompleteLinearOrder.isCompact_Icc _ _⟩

Premises used: CompactIccSpace.mk, ConditionallyCompleteLinearOrder.isCompact_Icc