awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Category.BddLat
Goal:
⊢ BddLat.dual ⋙
      forget₂ BddLat (FC := fun (x1 x2 : BddLat.{u_1}) ↦
        BoundedLatticeHom (↑x1.toLat : Type u_1) (↑x2.toLat : Type u_1)) (CC := fun (X : BddLat.{u_1}) ↦
        (↑X.toLat : Type u_1)) SemilatSupCat (FD := fun (x1 x2 : SemilatSupCat.{u_1}) ↦ SupBotHom x1.X x2.X) (CD :=
        SemilatSupCat.X) =
    forget₂ BddLat (FC := fun (x1 x2 : BddLat.{u_1}) ↦ BoundedLatticeHom (↑x1.toLat : Type u_1) (↑x2.toLat : Type u_1))
        (CC := fun (X : BddLat.{u_1}) ↦ (↑X.toLat : Type u_1)) SemilatInfCat (FD := fun (x1 x2 : SemilatInfCat.{u_1}) ↦
        InfTopHom x1.X x2.X) (CD := SemilatInfCat.X) ⋙
      SemilatInfCat.dual

Tactic:
rfl

Premises used: BddLat.dual, CategoryTheory.Functor.comp, OrderDual, rfl
-- Module: Mathlib.Order.Category.BddLat
Goal:
⊢ BddLat.dual ⋙
      forget₂ BddLat (FC := fun (x1 x2 : BddLat.{u_1}) ↦
        BoundedLatticeHom (↑x1.toLat : Type u_1) (↑x2.toLat : Type u_1)) (CC := fun (X : BddLat.{u_1}) ↦
        (↑X.toLat : Type u_1)) SemilatInfCat (FD := fun (x1 x2 : SemilatInfCat.{u_1}) ↦ InfTopHom x1.X x2.X) (CD :=
        SemilatInfCat.X) =
    forget₂ BddLat (FC := fun (x1 x2 : BddLat.{u_1}) ↦ BoundedLatticeHom (↑x1.toLat : Type u_1) (↑x2.toLat : Type u_1))
        (CC := fun (X : BddLat.{u_1}) ↦ (↑X.toLat : Type u_1)) SemilatSupCat (FD := fun (x1 x2 : SemilatSupCat.{u_1}) ↦
        SupBotHom x1.X x2.X) (CD := SemilatSupCat.X) ⋙
      SemilatSupCat.dual

Tactic:
rfl

Premises used: BddLat.dual, CategoryTheory.Functor.comp, OrderDual, rfl
-- Module: Mathlib.Order.Category.BddLat
Goal:
X : Lat
x : BddLat
f : latToBddLat.obj X ⟶ x
a b : (↑X : Type u)
⊢ (some ∘ some) (a ⊔ b) = (some ∘ some) a ⊔ (some ∘ some) b

Tactic:
rfl
-- Module: Mathlib.Order.Category.BddLat
Goal:
X : Lat
x : BddLat
f : latToBddLat.obj X ⟶ x
a b : (↑X : Type u)
⊢ (some ∘ some) (a ⊓ b) = (some ∘ some) a ⊓ (some ∘ some) b

Tactic:
rfl
-- Module: Mathlib.Order.Category.BddOrd
Goal:
X : BddOrd
⊢ Eq (α :=
    (a : (fun (X : BddOrd.{u_1}) ↦ (↑X.toPartOrd : Type u_1)) X) →
      (fun (X : BddOrd.{u_1}) ↦ (↑X.toPartOrd : Type u_1)) X)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : BddOrd.{u_1}) ↦
          BoundedOrderHom (↑x1.toPartOrd : Type u_1) (↑x2.toPartOrd : Type u_1)) (CC := fun (X : BddOrd.{u_1}) ↦
          (↑X.toPartOrd : Type u_1)) (𝟙 X)) :
      (a : (fun (X : BddOrd) ↦ (↑X.toPartOrd : Type u_1)) X) → (fun (X : BddOrd) ↦ (↑X.toPartOrd : Type u_1)) X)
    id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.BddOrd
Goal:
X Y Z : BddOrd
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α :=
    (a : (fun (X : BddOrd.{u_1}) ↦ (↑X.toPartOrd : Type u_1)) X) →
      (fun (X : BddOrd.{u_1}) ↦ (↑X.toPartOrd : Type u_1)) Z)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : BddOrd.{u_1}) ↦
          BoundedOrderHom (↑x1.toPartOrd : Type u_1) (↑x2.toPartOrd : Type u_1)) (CC := fun (X : BddOrd.{u_1}) ↦
          (↑X.toPartOrd : Type u_1)) (f ≫ g)) :
      (a : (fun (X : BddOrd) ↦ (↑X.toPartOrd : Type u_1)) X) → (fun (X : BddOrd) ↦ (↑X.toPartOrd : Type u_1)) Z)
    (Function.comp (β := (fun (X : BddOrd.{u_1}) ↦ (↑X.toPartOrd : Type u_1)) Y)
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : BddOrd.{u_1}) ↦
            BoundedOrderHom (↑x1.toPartOrd : Type u_1) (↑x2.toPartOrd : Type u_1)) (CC := fun (X : BddOrd.{u_1}) ↦
            (↑X.toPartOrd : Type u_1)) g) :
        (a : (fun (X : BddOrd) ↦ (↑X.toPartOrd : Type u_1)) Y) → (fun (X : BddOrd) ↦ (↑X.toPartOrd : Type u_1)) Z)
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : BddOrd.{u_1}) ↦
            BoundedOrderHom (↑x1.toPartOrd : Type u_1) (↑x2.toPartOrd : Type u_1)) (CC := fun (X : BddOrd.{u_1}) ↦
            (↑X.toPartOrd : Type u_1)) f) :
        (a : (fun (X : BddOrd) ↦ (↑X.toPartOrd : Type u_1)) X) → (fun (X : BddOrd) ↦ (↑X.toPartOrd : Type u_1)) Y))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.BddOrd
Goal:
X Y : BddOrd
f : X ⟶ Y
⊢ Eq (α :=
    (a :
        (fun (X : Type u_1) ↦ X)
          (Functor.obj
            (forget BddOrd (FC := fun (x1 x2 : BddOrd.{u_1}) ↦
              BoundedOrderHom (↑x1.toPartOrd : Type u_1) (↑x2.toPartOrd : Type u_1)) (CC := fun (X : BddOrd.{u_1}) ↦
              (↑X.toPartOrd : Type u_1)))
            X)) →
      (fun (X : Type u_1) ↦ X)
        (Functor.obj
          (forget BddOrd (FC := fun (x1 x2 : BddOrd.{u_1}) ↦
            BoundedOrderHom (↑x1.toPartOrd : Type u_1) (↑x2.toPartOrd : Type u_1)) (CC := fun (X : BddOrd.{u_1}) ↦
            (↑X.toPartOrd : Type u_1)))
          Y))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map
            (forget BddOrd (FC := fun (x1 x2 : BddOrd.{u_1}) ↦
              BoundedOrderHom (↑x1.toPartOrd : Type u_1) (↑x2.toPartOrd : Type u_1)) (CC := fun (X : BddOrd.{u_1}) ↦
              (↑X.toPartOrd : Type u_1)))
            f)) :
      (a : (fun (X : Type u_1) ↦ X) ((forget BddOrd).obj X)) → (fun (X : Type u_1) ↦ X) ((forget BddOrd).obj Y))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : BddOrd.{u_1}) ↦
          BoundedOrderHom (↑x1.toPartOrd : Type u_1) (↑x2.toPartOrd : Type u_1)) (CC := fun (X : BddOrd.{u_1}) ↦
          (↑X.toPartOrd : Type u_1)) f) :
      (a : (fun (X : BddOrd) ↦ (↑X.toPartOrd : Type u_1)) X) → (fun (X : BddOrd) ↦ (↑X.toPartOrd : Type u_1)) Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.BddOrd
Goal:
X Y : BddOrd
f g : X ⟶ Y
w :
  ∀ (x : (↑X.toPartOrd : Type u_1)),
    Eq (α := (fun (X : BddOrd.{u_1}) ↦ (↑X.toPartOrd : Type u_1)) Y)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : BddOrd.{u_1}) ↦
              BoundedOrderHom (↑x1.toPartOrd : Type u_1) (↑x2.toPartOrd : Type u_1)) (CC := fun (X : BddOrd.{u_1}) ↦
              (↑X.toPartOrd : Type u_1)) f :
            (a : (fun (X : BddOrd) ↦ (↑X.toPartOrd : Type u_1)) X) → (fun (X : BddOrd) ↦ (↑X.toPartOrd : Type u_1)) Y)
          x :
        (fun (X : BddOrd.{u_1}) ↦ (↑X.toPartOrd : Type u_1)) Y)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : BddOrd.{u_1}) ↦
              BoundedOrderHom (↑x1.toPartOrd : Type u_1) (↑x2.toPartOrd : Type u_1)) (CC := fun (X : BddOrd.{u_1}) ↦
              (↑X.toPartOrd : Type u_1)) g :
            (a : (fun (X : BddOrd) ↦ (↑X.toPartOrd : Type u_1)) X) → (fun (X : BddOrd) ↦ (↑X.toPartOrd : Type u_1)) Y)
          x :
        (fun (X : BddOrd.{u_1}) ↦ (↑X.toPartOrd : Type u_1)) Y)
⊢ f = g

Tactic:
ConcreteCategory.hom_ext _ _ w

Premises used: CategoryTheory.ConcreteCategory.hom_ext
-- Module: Mathlib.Order.Category.BddOrd
Goal:
X : Type u
inst : PartialOrder X
inst_1 : BoundedOrder X
⊢ (↑(of X).toPartOrd : Type u) = X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.BddOrd
Goal:
X : BddOrd
⊢ Hom.hom (𝟙 X) = BoundedOrderHom.id (↑X.toPartOrd : Type u_1)

Tactic:
rfl

Premises used: BoundedOrderHom.id, rfl
-- Module: Mathlib.Order.Category.BddOrd
Goal:
X : BddOrd
x : (↑X.toPartOrd : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : BddOrd.{u_1}) ↦
          BoundedOrderHom (↑x1.toPartOrd : Type u_1) (↑x2.toPartOrd : Type u_1)) (CC := fun (X : BddOrd.{u_1}) ↦
          (↑X.toPartOrd : Type u_1)) (𝟙 X) :
        (a : (fun (X : BddOrd) ↦ (↑X.toPartOrd : Type u_1)) X) → (fun (X : BddOrd) ↦ (↑X.toPartOrd : Type u_1)) X)
      x =
    x

Tactic:
simp
-- Module: Mathlib.Order.Category.BddOrd
Goal:
X Y Z : BddOrd
f : X ⟶ Y
g : Y ⟶ Z
⊢ Hom.hom (f ≫ g) = (Hom.hom g).comp (Hom.hom f)

Tactic:
rfl

Premises used: BoundedOrderHom.comp, rfl
-- Module: Mathlib.Order.Category.BddOrd
Goal:
X Y Z : BddOrd
f : X ⟶ Y
g : Y ⟶ Z
x : (↑X.toPartOrd : Type u_1)
⊢ Eq (α := (fun (X : BddOrd.{u_1}) ↦ (↑X.toPartOrd : Type u_1)) Z)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : BddOrd.{u_1}) ↦
            BoundedOrderHom (↑x1.toPartOrd : Type u_1) (↑x2.toPartOrd : Type u_1)) (CC := fun (X : BddOrd.{u_1}) ↦
            (↑X.toPartOrd : Type u_1)) (f ≫ g) :
          (a : (fun (X : BddOrd) ↦ (↑X.toPartOrd : Type u_1)) X) → (fun (X : BddOrd) ↦ (↑X.toPartOrd : Type u_1)) Z)
        x :
      (fun (X : BddOrd.{u_1}) ↦ (↑X.toPartOrd : Type u_1)) Z)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : BddOrd.{u_1}) ↦
            BoundedOrderHom (↑x1.toPartOrd : Type u_1) (↑x2.toPartOrd : Type u_1)) (CC := fun (X : BddOrd.{u_1}) ↦
            (↑X.toPartOrd : Type u_1)) g :
          (a : (fun (X : BddOrd) ↦ (↑X.toPartOrd : Type u_1)) Y) → (fun (X : BddOrd) ↦ (↑X.toPartOrd : Type u_1)) Z)
        ((ConcreteCategory.hom (FC := fun (x1 x2 : BddOrd.{u_1}) ↦
                BoundedOrderHom (↑x1.toPartOrd : Type u_1) (↑x2.toPartOrd : Type u_1)) (CC := fun (X : BddOrd.{u_1}) ↦
                (↑X.toPartOrd : Type u_1)) f :
              (a : (fun (X : BddOrd) ↦ (↑X.toPartOrd : Type u_1)) X) → (fun (X : BddOrd) ↦ (↑X.toPartOrd : Type u_1)) Y)
            x :
          (fun (X : BddOrd.{u_1}) ↦ (↑X.toPartOrd : Type u_1)) Y) :
      (fun (X : BddOrd.{u_1}) ↦ (↑X.toPartOrd : Type u_1)) Z)

Tactic:
simp
-- Module: Mathlib.Order.Category.BddOrd
Goal:
X Y : BddOrd
f g : X ⟶ Y
hf : Hom.hom f = Hom.hom g
⊢ f = g

Tactic:
Hom.ext hf

Premises used: BddOrd.Hom.ext
-- Module: Mathlib.Order.Category.BddOrd
Goal:
X Y : Type u
inst : PartialOrder X
inst_1 : BoundedOrder X
inst_2 : PartialOrder Y
inst_3 : BoundedOrder Y
f : BoundedOrderHom X Y
⊢ Hom.hom (ofHom f) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.BddOrd
Goal:
X Y : BddOrd
f : X ⟶ Y
⊢ ofHom (Hom.hom f) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.BddOrd
Goal:
X : Type u
inst : PartialOrder X
inst_1 : BoundedOrder X
⊢ ofHom (BoundedOrderHom.id X) = 𝟙 (of X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.BddOrd
Goal:
X Y Z : Type u
inst : PartialOrder X
inst_1 : BoundedOrder X
inst_2 : PartialOrder Y
inst_3 : BoundedOrder Y
inst_4 : PartialOrder Z
inst_5 : BoundedOrder Z
f : BoundedOrderHom X Y
g : BoundedOrderHom Y Z
⊢ ofHom (g.comp f) = ofHom f ≫ ofHom g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.BddOrd
Goal:
X Y : Type u
inst : PartialOrder X
inst_1 : BoundedOrder X
inst_2 : PartialOrder Y
inst_3 : BoundedOrder Y
f : BoundedOrderHom X Y
x : X
⊢ Eq (α := (fun (X : BddOrd.{u}) ↦ (↑X.toPartOrd : Type u)) (of Y))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : BddOrd.{u}) ↦
            BoundedOrderHom (↑x1.toPartOrd : Type u) (↑x2.toPartOrd : Type u)) (CC := fun (X : BddOrd.{u}) ↦
            (↑X.toPartOrd : Type u)) (ofHom f) :
          (a : (fun (X : BddOrd) ↦ (↑X.toPartOrd : Type u)) (of X)) →
            (fun (X : BddOrd) ↦ (↑X.toPartOrd : Type u)) (of Y))
        x :
      (fun (X : BddOrd.{u}) ↦ (↑X.toPartOrd : Type u)) (of Y))
    ((f : (a : X) → Y) x : Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.BddOrd
Goal:
X Y : BddOrd
e : X ≅ Y
x : (↑X.toPartOrd : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : BddOrd.{u_1}) ↦
          BoundedOrderHom (↑x1.toPartOrd : Type u_1) (↑x2.toPartOrd : Type u_1)) (CC := fun (X : BddOrd.{u_1}) ↦
          (↑X.toPartOrd : Type u_1)) e.inv :
        (a : (fun (X : BddOrd) ↦ (↑X.toPartOrd : Type u_1)) Y) → (fun (X : BddOrd) ↦ (↑X.toPartOrd : Type u_1)) X)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : BddOrd.{u_1}) ↦
              BoundedOrderHom (↑x1.toPartOrd : Type u_1) (↑x2.toPartOrd : Type u_1)) (CC := fun (X : BddOrd.{u_1}) ↦
              (↑X.toPartOrd : Type u_1)) e.hom :
            (a : (fun (X : BddOrd) ↦ (↑X.toPartOrd : Type u_1)) X) → (fun (X : BddOrd) ↦ (↑X.toPartOrd : Type u_1)) Y)
          x :
        (fun (X : BddOrd.{u_1}) ↦ (↑X.toPartOrd : Type u_1)) Y) =
    x

Tactic:
simp
-- Module: Mathlib.Order.Category.BddOrd
Goal:
X Y : BddOrd
e : X ≅ Y
s : (↑Y.toPartOrd : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : BddOrd.{u_1}) ↦
          BoundedOrderHom (↑x1.toPartOrd : Type u_1) (↑x2.toPartOrd : Type u_1)) (CC := fun (X : BddOrd.{u_1}) ↦
          (↑X.toPartOrd : Type u_1)) e.hom :
        (a : (fun (X : BddOrd) ↦ (↑X.toPartOrd : Type u_1)) X) → (fun (X : BddOrd) ↦ (↑X.toPartOrd : Type u_1)) Y)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : BddOrd.{u_1}) ↦
              BoundedOrderHom (↑x1.toPartOrd : Type u_1) (↑x2.toPartOrd : Type u_1)) (CC := fun (X : BddOrd.{u_1}) ↦
              (↑X.toPartOrd : Type u_1)) e.inv :
            (a : (fun (X : BddOrd) ↦ (↑X.toPartOrd : Type u_1)) Y) → (fun (X : BddOrd) ↦ (↑X.toPartOrd : Type u_1)) X)
          s :
        (fun (X : BddOrd.{u_1}) ↦ (↑X.toPartOrd : Type u_1)) X) =
    s

Tactic:
simp
-- Module: Mathlib.Order.Category.BddOrd
Goal:
α β : BddOrd
e : (↑α.toPartOrd : Type u) ≃o (↑β.toPartOrd : Type u)
hf :
  ∀ (a : (↑α.toPartOrd : Type u)),
    Eq (α := (↑α.toPartOrd : Type u))
      ((Hom.hom
              (CategoryStruct.comp (Y := β) (ofHom (↑e : BoundedOrderHom (↑α.1 : Type u) (↑β.1 : Type u)))
                (ofHom (↑e.symm : BoundedOrderHom (↑β.1 : Type u) (↑α.1 : Type u)))) :
            (a : (↑α.toPartOrd : Type u)) → (↑α.toPartOrd : Type u))
          a :
        (↑α.toPartOrd : Type u))
      ((Hom.hom (𝟙 α) : (a : (↑α.toPartOrd : Type u)) → (↑α.toPartOrd : Type u)) a : (↑α.toPartOrd : Type u))
⊢ CategoryStruct.comp (Y := β) (ofHom (↑e : BoundedOrderHom (↑α.1 : Type u) (↑β.1 : Type u)))
      (ofHom (↑e.symm : BoundedOrderHom (↑β.1 : Type u) (↑α.1 : Type u))) =
    𝟙 α

Tactic:
ext
-- Module: Mathlib.Order.Category.BddOrd
Goal:
α β : BddOrd
e : (↑α.toPartOrd : Type u) ≃o (↑β.toPartOrd : Type u)
a : (↑α.toPartOrd : Type u)
⊢ Eq (α := (↑α.toPartOrd : Type u))
    ((Hom.hom
            (CategoryStruct.comp (Y := β) (ofHom (↑e : BoundedOrderHom (↑α.1 : Type u) (↑β.1 : Type u)))
              (ofHom (↑e.symm : BoundedOrderHom (↑β.1 : Type u) (↑α.1 : Type u)))) :
          (a : (↑α.toPartOrd : Type u)) → (↑α.toPartOrd : Type u))
        a :
      (↑α.toPartOrd : Type u))
    ((Hom.hom (𝟙 α) : (a : (↑α.toPartOrd : Type u)) → (↑α.toPartOrd : Type u)) a : (↑α.toPartOrd : Type u))

Tactic:
e.symm_apply_apply _

Premises used: OrderIso.symm_apply_apply
-- Module: Mathlib.Order.Category.BddOrd
Goal:
α β : BddOrd
e : (↑α.toPartOrd : Type u) ≃o (↑β.toPartOrd : Type u)
a : (↑α.toPartOrd : Type u)
⊢ Eq (α := (↑α.toPartOrd : Type u))
    ((Hom.hom
            (CategoryStruct.comp (Y := β) (ofHom (↑e : BoundedOrderHom (↑α.1 : Type u) (↑β.1 : Type u)))
              (ofHom (↑e.symm : BoundedOrderHom (↑β.1 : Type u) (↑α.1 : Type u)))) :
          (a : (↑α.toPartOrd : Type u)) → (↑α.toPartOrd : Type u))
        a :
      (↑α.toPartOrd : Type u))
    ((Hom.hom (𝟙 α) : (a : (↑α.toPartOrd : Type u)) → (↑α.toPartOrd : Type u)) a : (↑α.toPartOrd : Type u))

Tactic:
exact e.symm_apply_apply _

Premises used: OrderIso.symm_apply_apply
-- Module: Mathlib.Order.Category.BddOrd
Goal:
α β : BddOrd
e : (↑α.toPartOrd : Type u) ≃o (↑β.toPartOrd : Type u)
hf :
  ∀ (a : (↑β.toPartOrd : Type u)),
    Eq (α := (↑β.toPartOrd : Type u))
      ((Hom.hom
              (CategoryStruct.comp (Y := α) (ofHom (↑e.symm : BoundedOrderHom (↑β.1 : Type u) (↑α.1 : Type u)))
                (ofHom (↑e : BoundedOrderHom (↑α.1 : Type u) (↑β.1 : Type u)))) :
            (a : (↑β.toPartOrd : Type u)) → (↑β.toPartOrd : Type u))
          a :
        (↑β.toPartOrd : Type u))
      ((Hom.hom (𝟙 β) : (a : (↑β.toPartOrd : Type u)) → (↑β.toPartOrd : Type u)) a : (↑β.toPartOrd : Type u))
⊢ CategoryStruct.comp (Y := α) (ofHom (↑e.symm : BoundedOrderHom (↑β.1 : Type u) (↑α.1 : Type u)))
      (ofHom (↑e : BoundedOrderHom (↑α.1 : Type u) (↑β.1 : Type u))) =
    𝟙 β

Tactic:
ext
-- Module: Mathlib.Order.Category.BddOrd
Goal:
α β : BddOrd
e : (↑α.toPartOrd : Type u) ≃o (↑β.toPartOrd : Type u)
a : (↑β.toPartOrd : Type u)
⊢ Eq (α := (↑β.toPartOrd : Type u))
    ((Hom.hom
            (CategoryStruct.comp (Y := α) (ofHom (↑e.symm : BoundedOrderHom (↑β.1 : Type u) (↑α.1 : Type u)))
              (ofHom (↑e : BoundedOrderHom (↑α.1 : Type u) (↑β.1 : Type u)))) :
          (a : (↑β.toPartOrd : Type u)) → (↑β.toPartOrd : Type u))
        a :
      (↑β.toPartOrd : Type u))
    ((Hom.hom (𝟙 β) : (a : (↑β.toPartOrd : Type u)) → (↑β.toPartOrd : Type u)) a : (↑β.toPartOrd : Type u))

Tactic:
e.apply_symm_apply _

Premises used: OrderIso.apply_symm_apply
-- Module: Mathlib.Order.Category.BddOrd
Goal:
α β : BddOrd
e : (↑α.toPartOrd : Type u) ≃o (↑β.toPartOrd : Type u)
a : (↑β.toPartOrd : Type u)
⊢ Eq (α := (↑β.toPartOrd : Type u))
    ((Hom.hom
            (CategoryStruct.comp (Y := α) (ofHom (↑e.symm : BoundedOrderHom (↑β.1 : Type u) (↑α.1 : Type u)))
              (ofHom (↑e : BoundedOrderHom (↑α.1 : Type u) (↑β.1 : Type u)))) :
          (a : (↑β.toPartOrd : Type u)) → (↑β.toPartOrd : Type u))
        a :
      (↑β.toPartOrd : Type u))
    ((Hom.hom (𝟙 β) : (a : (↑β.toPartOrd : Type u)) → (↑β.toPartOrd : Type u)) a : (↑β.toPartOrd : Type u))

Tactic:
exact e.apply_symm_apply _

Premises used: OrderIso.apply_symm_apply
-- Module: Mathlib.Order.Category.BddOrd
Goal:
⊢ BddOrd.dual ⋙
      forget₂ BddOrd (FC := fun (x1 x2 : BddOrd.{u_1}) ↦
        BoundedOrderHom (↑x1.toPartOrd : Type u_1) (↑x2.toPartOrd : Type u_1)) (CC := fun (X : BddOrd.{u_1}) ↦
        (↑X.toPartOrd : Type u_1)) PartOrd (FD := fun (x1 x2 : PartOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1))
        (CD := PartOrd.carrier) =
    forget₂ BddOrd (FC := fun (x1 x2 : BddOrd.{u_1}) ↦
        BoundedOrderHom (↑x1.toPartOrd : Type u_1) (↑x2.toPartOrd : Type u_1)) (CC := fun (X : BddOrd.{u_1}) ↦
        (↑X.toPartOrd : Type u_1)) PartOrd (FD := fun (x1 x2 : PartOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1))
        (CD := PartOrd.carrier) ⋙
      PartOrd.dual

Tactic:
rfl

Premises used: BddOrd.dual, CategoryTheory.Functor.comp, OrderDual, rfl
-- Module: Mathlib.Order.Category.BddOrd
Goal:
⊢ BddOrd.dual ⋙
      forget₂ BddOrd (FC := fun (x1 x2 : BddOrd.{u_1}) ↦
        BoundedOrderHom (↑x1.toPartOrd : Type u_1) (↑x2.toPartOrd : Type u_1)) (CC := fun (X : BddOrd.{u_1}) ↦
        (↑X.toPartOrd : Type u_1)) Bipointed (FD := Bipointed.HomSubtype) (CD := Bipointed.X) =
    forget₂ BddOrd (FC := fun (x1 x2 : BddOrd.{u_1}) ↦
        BoundedOrderHom (↑x1.toPartOrd : Type u_1) (↑x2.toPartOrd : Type u_1)) (CC := fun (X : BddOrd.{u_1}) ↦
        (↑X.toPartOrd : Type u_1)) Bipointed (FD := Bipointed.HomSubtype) (CD := Bipointed.X) ⋙
      Bipointed.swap

Tactic:
rfl

Premises used: BddOrd.dual, CategoryTheory.Functor.comp, Prod.swap, OrderDual, rfl
-- Module: Mathlib.Order.Category.BoolAlg
Goal:
X : BoolAlg
⊢ Eq (α := (a : (↑X : Type u_1)) → (↑X : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : BoolAlg.{u_1}) ↦ BoundedLatticeHom (↑x1 : Type u_1) (↑x2 : Type u_1))
          (CC := carrier) (𝟙 X)) :
      (a : (↑X : Type u_1)) → (↑X : Type u_1))
    id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.BoolAlg
Goal:
X Y Z : BoolAlg
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := (a : (↑X : Type u_1)) → (↑Z : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : BoolAlg.{u_1}) ↦ BoundedLatticeHom (↑x1 : Type u_1) (↑x2 : Type u_1))
          (CC := carrier) (f ≫ g)) :
      (a : (↑X : Type u_1)) → (↑Z : Type u_1))
    (Function.comp (β := (↑Y : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : BoolAlg.{u_1}) ↦ BoundedLatticeHom (↑x1 : Type u_1) (↑x2 : Type u_1))
            (CC := carrier) g) :
        (a : (↑Y : Type u_1)) → (↑Z : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : BoolAlg.{u_1}) ↦ BoundedLatticeHom (↑x1 : Type u_1) (↑x2 : Type u_1))
            (CC := carrier) f) :
        (a : (↑X : Type u_1)) → (↑Y : Type u_1)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.BoolAlg
Goal:
X Y : BoolAlg
f : X ⟶ Y
⊢ Eq (α :=
    (a :
        (fun (X : Type u_1) ↦ X)
          (Functor.obj
            (forget BoolAlg (FC := fun (x1 x2 : BoolAlg.{u_1}) ↦ BoundedLatticeHom (↑x1 : Type u_1) (↑x2 : Type u_1))
              (CC := carrier))
            X)) →
      (fun (X : Type u_1) ↦ X)
        (Functor.obj
          (forget BoolAlg (FC := fun (x1 x2 : BoolAlg.{u_1}) ↦ BoundedLatticeHom (↑x1 : Type u_1) (↑x2 : Type u_1))
            (CC := carrier))
          Y))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map
            (forget BoolAlg (FC := fun (x1 x2 : BoolAlg.{u_1}) ↦ BoundedLatticeHom (↑x1 : Type u_1) (↑x2 : Type u_1))
              (CC := carrier))
            f)) :
      (a : (fun (X : Type u_1) ↦ X) ((forget BoolAlg).obj X)) → (fun (X : Type u_1) ↦ X) ((forget BoolAlg).obj Y))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : BoolAlg.{u_1}) ↦ BoundedLatticeHom (↑x1 : Type u_1) (↑x2 : Type u_1))
          (CC := carrier) f) :
      (a : (↑X : Type u_1)) → (↑Y : Type u_1))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.BoolAlg
Goal:
X Y : BoolAlg
f g : X ⟶ Y
w :
  ∀ (x : (↑X : Type u_1)),
    Eq (α := (↑Y : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : BoolAlg.{u_1}) ↦ BoundedLatticeHom (↑x1 : Type u_1) (↑x2 : Type u_1))
              (CC := carrier) f :
            (a : (↑X : Type u_1)) → (↑Y : Type u_1))
          x :
        (↑Y : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : BoolAlg.{u_1}) ↦ BoundedLatticeHom (↑x1 : Type u_1) (↑x2 : Type u_1))
              (CC := carrier) g :
            (a : (↑X : Type u_1)) → (↑Y : Type u_1))
          x :
        (↑Y : Type u_1))
⊢ f = g

Tactic:
ConcreteCategory.hom_ext _ _ w

Premises used: CategoryTheory.ConcreteCategory.hom_ext
-- Module: Mathlib.Order.Category.BoolAlg
Goal:
X : Type u
inst : BooleanAlgebra X
⊢ (↑{ carrier := X, str := inst : BoolAlg.{u} } : Type u) = X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.BoolAlg
Goal:
X : BoolAlg
⊢ Hom.hom (𝟙 X) = BoundedLatticeHom.id (↑X : Type u_1)

Tactic:
rfl

Premises used: BoundedLatticeHom.id, rfl
-- Module: Mathlib.Order.Category.BoolAlg
Goal:
X : BoolAlg
x : (↑X : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : BoolAlg.{u_1}) ↦ BoundedLatticeHom (↑x1 : Type u_1) (↑x2 : Type u_1)) (CC :=
          carrier) (𝟙 X) :
        (a : (↑X : Type u_1)) → (↑X : Type u_1))
      x =
    x

Tactic:
simp
-- Module: Mathlib.Order.Category.BoolAlg
Goal:
X Y Z : BoolAlg
f : X ⟶ Y
g : Y ⟶ Z
⊢ Hom.hom (f ≫ g) = (Hom.hom g).comp (Hom.hom f)

Tactic:
rfl

Premises used: BoundedLatticeHom.comp, rfl
-- Module: Mathlib.Order.Category.BoolAlg
Goal:
X Y Z : BoolAlg
f : X ⟶ Y
g : Y ⟶ Z
x : (↑X : Type u_1)
⊢ Eq (α := (↑Z : Type u_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : BoolAlg.{u_1}) ↦ BoundedLatticeHom (↑x1 : Type u_1) (↑x2 : Type u_1))
            (CC := carrier) (f ≫ g) :
          (a : (↑X : Type u_1)) → (↑Z : Type u_1))
        x :
      (↑Z : Type u_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : BoolAlg.{u_1}) ↦ BoundedLatticeHom (↑x1 : Type u_1) (↑x2 : Type u_1))
            (CC := carrier) g :
          (a : (↑Y : Type u_1)) → (↑Z : Type u_1))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : BoolAlg.{u_1}) ↦ BoundedLatticeHom (↑x1 : Type u_1) (↑x2 : Type u_1))
                (CC := carrier) f :
              (a : (↑X : Type u_1)) → (↑Y : Type u_1))
            x :
          (↑Y : Type u_1)) :
      (↑Z : Type u_1))

Tactic:
simp
-- Module: Mathlib.Order.Category.BoolAlg
Goal:
X Y : BoolAlg
f g : X ⟶ Y
hf : Hom.hom f = Hom.hom g
⊢ f = g

Tactic:
Hom.ext hf

Premises used: BoolAlg.Hom.ext
-- Module: Mathlib.Order.Category.BoolAlg
Goal:
X Y : Type u
inst : BooleanAlgebra X
inst_1 : BooleanAlgebra Y
f : BoundedLatticeHom X Y
⊢ Hom.hom (ofHom f) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.BoolAlg
Goal:
X Y : BoolAlg
f : X ⟶ Y
⊢ ofHom (Hom.hom f) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.BoolAlg
Goal:
X : Type u
inst : BooleanAlgebra X
⊢ ofHom (BoundedLatticeHom.id X) = 𝟙 { carrier := X, str := inst : BoolAlg.{u} }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.BoolAlg
Goal:
X Y Z : Type u
inst : BooleanAlgebra X
inst_1 : BooleanAlgebra Y
inst_2 : BooleanAlgebra Z
f : BoundedLatticeHom X Y
g : BoundedLatticeHom Y Z
⊢ ofHom (g.comp f) = ofHom f ≫ ofHom g

Tactic:
rfl

Premises used: rfl