awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Category.BddDistLat
Goal:
X Y : BddDistLat
e : X ≅ Y
x : (↑X.toDistLat : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : BddDistLat.{u_1}) ↦
          BoundedLatticeHom (↑x1.toDistLat : Type u_1) (↑x2.toDistLat : Type u_1)) (CC := fun (X : BddDistLat.{u_1}) ↦
          (↑X.toDistLat : Type u_1)) e.inv :
        (a : (fun (X : BddDistLat) ↦ (↑X.toDistLat : Type u_1)) Y) →
          (fun (X : BddDistLat) ↦ (↑X.toDistLat : Type u_1)) X)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : BddDistLat.{u_1}) ↦
              BoundedLatticeHom (↑x1.toDistLat : Type u_1) (↑x2.toDistLat : Type u_1)) (CC :=
              fun (X : BddDistLat.{u_1}) ↦ (↑X.toDistLat : Type u_1)) e.hom :
            (a : (fun (X : BddDistLat) ↦ (↑X.toDistLat : Type u_1)) X) →
              (fun (X : BddDistLat) ↦ (↑X.toDistLat : Type u_1)) Y)
          x :
        (fun (X : BddDistLat.{u_1}) ↦ (↑X.toDistLat : Type u_1)) Y) =
    x

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

Tactic:
simp
-- Module: Mathlib.Order.Category.BddDistLat
Goal:
X : BddDistLat
⊢ (↑X.toBddLat.toLat : Type u_1) = (↑X.toDistLat : Type u_1)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.BddDistLat
Goal:
⊢ Eq (α := BddDistLat ⥤ Lat)
    (forget₂ BddDistLat (FC := fun (x1 x2 : BddDistLat.{u_1}) ↦
        BoundedLatticeHom (↑x1.toDistLat : Type u_1) (↑x2.toDistLat : Type u_1)) (CC := fun (X : BddDistLat.{u_1}) ↦
        (↑X.toDistLat : Type u_1)) BddLat (FD := fun (x1 x2 : BddLat.{u_1}) ↦
        BoundedLatticeHom (↑x1.toLat : Type u_1) (↑x2.toLat : Type u_1)) (CD := fun (X : BddLat.{u_1}) ↦
        (↑X.toLat : Type u_1)) ⋙
      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)) Lat (FD := fun (x1 x2 : Lat.{u_1}) ↦ LatticeHom (↑x1 : Type u_1) (↑x2 : Type u_1)) (CD :=
        Lat.carrier))
    (forget₂ BddDistLat (FC := fun (x1 x2 : BddDistLat.{u_1}) ↦
        BoundedLatticeHom (↑x1.toDistLat : Type u_1) (↑x2.toDistLat : Type u_1)) (CC := fun (X : BddDistLat.{u_1}) ↦
        (↑X.toDistLat : Type u_1)) DistLat (FD := fun (x1 x2 : DistLat.{u_1}) ↦
        LatticeHom (↑x1 : Type u_1) (↑x2 : Type u_1)) (CD := DistLat.carrier) ⋙
      forget₂ DistLat (FC := fun (x1 x2 : DistLat.{u_1}) ↦ LatticeHom (↑x1 : Type u_1) (↑x2 : Type u_1)) (CC :=
        DistLat.carrier) Lat (FD := fun (x1 x2 : Lat.{u_1}) ↦ LatticeHom (↑x1 : Type u_1) (↑x2 : Type u_1)) (CD :=
        Lat.carrier))

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, rfl
-- Module: Mathlib.Order.Category.BddDistLat
Goal:
⊢ BddDistLat.dual ⋙
      forget₂ BddDistLat (FC := fun (x1 x2 : BddDistLat.{u_1}) ↦
        BoundedLatticeHom (↑x1.toDistLat : Type u_1) (↑x2.toDistLat : Type u_1)) (CC := fun (X : BddDistLat.{u_1}) ↦
        (↑X.toDistLat : Type u_1)) DistLat (FD := fun (x1 x2 : DistLat.{u_1}) ↦
        LatticeHom (↑x1 : Type u_1) (↑x2 : Type u_1)) (CD := DistLat.carrier) =
    forget₂ BddDistLat (FC := fun (x1 x2 : BddDistLat.{u_1}) ↦
        BoundedLatticeHom (↑x1.toDistLat : Type u_1) (↑x2.toDistLat : Type u_1)) (CC := fun (X : BddDistLat.{u_1}) ↦
        (↑X.toDistLat : Type u_1)) DistLat (FD := fun (x1 x2 : DistLat.{u_1}) ↦
        LatticeHom (↑x1 : Type u_1) (↑x2 : Type u_1)) (CD := DistLat.carrier) ⋙
      DistLat.dual

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, BddDistLat.dual, OrderDual, rfl
-- Module: Mathlib.Order.Category.BddLat
Goal:
α : Type u_1
inst : Lattice α
inst_1 : BoundedOrder α
⊢ (↑(of α).toLat : Type u_1) = α

Tactic:
rfl

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

Tactic:
rfl

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

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

Tactic:
rfl

Premises used: LatticeHom.comp, rfl
-- Module: Mathlib.Order.Category.BddLat
Goal:
X Y Z : Lat
f : X ⟶ Y
g : Y ⟶ Z
x : (↑X : Type u_1)
⊢ Eq (α := (↑Z : Type u_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : Lat.{u_1}) ↦ LatticeHom (↑x1 : Type u_1) (↑x2 : Type u_1)) (CC :=
            Lat.carrier) (f ≫ g) :
          (a : (↑X : Type u_1)) → (↑Z : Type u_1))
        x :
      (↑Z : Type u_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : Lat.{u_1}) ↦ LatticeHom (↑x1 : Type u_1) (↑x2 : Type u_1)) (CC :=
            Lat.carrier) g :
          (a : (↑Y : Type u_1)) → (↑Z : Type u_1))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : Lat.{u_1}) ↦ LatticeHom (↑x1 : Type u_1) (↑x2 : Type u_1)) (CC :=
                Lat.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.BddLat
Goal:
X Y : BddLat
f g : X ⟶ Y
w :
  ∀ (x : (↑X.toLat : Type u_1)),
    Eq (α := (fun (X : BddLat.{u_1}) ↦ (↑X.toLat : Type u_1)) Y)
      ((ConcreteCategory.hom (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)) f :
            (a : (fun (X : BddLat) ↦ (↑X.toLat : Type u_1)) X) → (fun (X : BddLat) ↦ (↑X.toLat : Type u_1)) Y)
          x :
        (fun (X : BddLat.{u_1}) ↦ (↑X.toLat : Type u_1)) Y)
      ((ConcreteCategory.hom (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)) g :
            (a : (fun (X : BddLat) ↦ (↑X.toLat : Type u_1)) X) → (fun (X : BddLat) ↦ (↑X.toLat : Type u_1)) Y)
          x :
        (fun (X : BddLat.{u_1}) ↦ (↑X.toLat : Type u_1)) Y)
⊢ f = g

Tactic:
ConcreteCategory.hom_ext _ _ w

Premises used: CategoryTheory.ConcreteCategory.hom_ext
-- Module: Mathlib.Order.Category.BddLat
Goal:
X Y : BddLat
f g : X ⟶ Y
hf : Hom.hom f = Hom.hom g
⊢ f = g

Tactic:
Hom.ext hf

Premises used: BddLat.Hom.ext
-- Module: Mathlib.Order.Category.BddLat
Goal:
X : BddLat
⊢ (↑(Functor.obj
            (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)) BddOrd (FD := fun (x1 x2 : BddOrd.{u_1}) ↦
              BoundedOrderHom (↑x1.toPartOrd : Type u_1) (↑x2.toPartOrd : Type u_1)) (CD := fun (X : BddOrd.{u_1}) ↦
              (↑X.toPartOrd : Type u_1)))
            X).toPartOrd :
      Type u_1) =
    (↑X.toLat : Type u_1)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.BddLat
Goal:
X : BddLat
⊢ (↑(Functor.obj
          (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)) Lat (FD := fun (x1 x2 : Lat.{u_1}) ↦ LatticeHom (↑x1 : Type u_1) (↑x2 : Type u_1))
            (CD := Lat.carrier))
          X) :
      Type u_1) =
    (↑X.toLat : Type u_1)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.BddLat
Goal:
X : BddLat
⊢ (Functor.obj
        (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))
        X).X =
    (↑X.toLat : Type u_1)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.BddLat
Goal:
X : BddLat
⊢ (Functor.obj
        (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))
        X).X =
    (↑X.toLat : Type u_1)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.BddLat
Goal:
⊢ Eq (α := BddLat ⥤ PartOrd)
    (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)) Lat (FD := fun (x1 x2 : Lat.{u_1}) ↦
        LatticeHom (↑x1 : Type u_1) (↑x2 : Type u_1)) (CD := Lat.carrier) ⋙
      forget₂ Lat (FC := fun (x1 x2 : Lat.{u_1}) ↦ LatticeHom (↑x1 : Type u_1) (↑x2 : Type u_1)) (CC := Lat.carrier)
        PartOrd (FD := fun (x1 x2 : PartOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CD := PartOrd.carrier))
    (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)) BddOrd (FD := fun (x1 x2 : BddOrd.{u_1}) ↦
        BoundedOrderHom (↑x1.toPartOrd : Type u_1) (↑x2.toPartOrd : Type u_1)) (CD := fun (X : BddOrd.{u_1}) ↦
        (↑X.toPartOrd : Type u_1)) ⋙
      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))

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, OrderHomClass.toOrderHom, rfl
-- Module: Mathlib.Order.Category.BddLat
Goal:
⊢ Eq (α := BddLat ⥤ PartOrd)
    (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₂ SemilatSupCat (FC := fun (x1 x2 : SemilatSupCat.{u_1}) ↦ SupBotHom x1.X x2.X) (CC := SemilatSupCat.X)
        PartOrd (FD := fun (x1 x2 : PartOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CD := PartOrd.carrier))
    (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)) BddOrd (FD := fun (x1 x2 : BddOrd.{u_1}) ↦
        BoundedOrderHom (↑x1.toPartOrd : Type u_1) (↑x2.toPartOrd : Type u_1)) (CD := fun (X : BddOrd.{u_1}) ↦
        (↑X.toPartOrd : Type u_1)) ⋙
      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))

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, rfl
-- Module: Mathlib.Order.Category.BddLat
Goal:
⊢ Eq (α := BddLat ⥤ PartOrd)
    (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₂ SemilatInfCat (FC := fun (x1 x2 : SemilatInfCat.{u_1}) ↦ InfTopHom x1.X x2.X) (CC := SemilatInfCat.X)
        PartOrd (FD := fun (x1 x2 : PartOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CD := PartOrd.carrier))
    (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)) BddOrd (FD := fun (x1 x2 : BddOrd.{u_1}) ↦
        BoundedOrderHom (↑x1.toPartOrd : Type u_1) (↑x2.toPartOrd : Type u_1)) (CD := fun (X : BddOrd.{u_1}) ↦
        (↑X.toPartOrd : Type u_1)) ⋙
      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))

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, rfl
-- Module: Mathlib.Order.Category.BddLat
Goal:
α β : BddLat
e : (↑α.toLat : Type u) ≃o (↑β.toLat : Type u)
hf :
  ∀ (a : (↑α.toLat : Type u)),
    Eq (α := (↑α.toLat : Type u))
      ((Hom.hom
              (CategoryStruct.comp (Y := β)
                (ofHom
                  (let __src : LatticeHom (↑α.1 : Type u) (↑β.1 : Type u) :=
                    { toFun := (⇑e : (a : (↑α.1 : Type u)) → (↑β.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯ };
                  { toFun := (⇑e : (a : (↑α.1 : Type u)) → (↑β.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯,
                    map_top' := ⋯, map_bot' := ⋯ }))
                (ofHom
                  (let __src : LatticeHom (↑β.1 : Type u) (↑α.1 : Type u) :=
                    { toFun := (⇑e.symm : (a : (↑β.1 : Type u)) → (↑α.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯ };
                  { toFun := (⇑e.symm : (a : (↑β.1 : Type u)) → (↑α.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯,
                    map_top' := ⋯, map_bot' := ⋯ }))) :
            (a : (↑α.toLat : Type u)) → (↑α.toLat : Type u))
          a :
        (↑α.toLat : Type u))
      ((Hom.hom (𝟙 α) : (a : (↑α.toLat : Type u)) → (↑α.toLat : Type u)) a : (↑α.toLat : Type u))
⊢ CategoryStruct.comp (Y := β)
      (ofHom
        (let __src : LatticeHom (↑α.1 : Type u) (↑β.1 : Type u) :=
          { toFun := (⇑e : (a : (↑α.1 : Type u)) → (↑β.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯ };
        { toFun := (⇑e : (a : (↑α.1 : Type u)) → (↑β.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯,
          map_bot' := ⋯ }))
      (ofHom
        (let __src : LatticeHom (↑β.1 : Type u) (↑α.1 : Type u) :=
          { toFun := (⇑e.symm : (a : (↑β.1 : Type u)) → (↑α.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯ };
        { toFun := (⇑e.symm : (a : (↑β.1 : Type u)) → (↑α.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯,
          map_bot' := ⋯ })) =
    𝟙 α

Tactic:
ext
-- Module: Mathlib.Order.Category.BddLat
Goal:
α β : BddLat
e : (↑α.toLat : Type u) ≃o (↑β.toLat : Type u)
a : (↑α.toLat : Type u)
⊢ Eq (α := (↑α.toLat : Type u))
    ((Hom.hom
            (CategoryStruct.comp (Y := β)
              (ofHom
                (let __src : LatticeHom (↑α.1 : Type u) (↑β.1 : Type u) :=
                  { toFun := (⇑e : (a : (↑α.1 : Type u)) → (↑β.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯ };
                { toFun := (⇑e : (a : (↑α.1 : Type u)) → (↑β.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯,
                  map_bot' := ⋯ }))
              (ofHom
                (let __src : LatticeHom (↑β.1 : Type u) (↑α.1 : Type u) :=
                  { toFun := (⇑e.symm : (a : (↑β.1 : Type u)) → (↑α.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯ };
                { toFun := (⇑e.symm : (a : (↑β.1 : Type u)) → (↑α.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯,
                  map_top' := ⋯, map_bot' := ⋯ }))) :
          (a : (↑α.toLat : Type u)) → (↑α.toLat : Type u))
        a :
      (↑α.toLat : Type u))
    ((Hom.hom (𝟙 α) : (a : (↑α.toLat : Type u)) → (↑α.toLat : Type u)) a : (↑α.toLat : Type u))

Tactic:
e.symm_apply_apply _

Premises used: OrderIso.symm_apply_apply
-- Module: Mathlib.Order.Category.BddLat
Goal:
α β : BddLat
e : (↑α.toLat : Type u) ≃o (↑β.toLat : Type u)
a : (↑α.toLat : Type u)
⊢ Eq (α := (↑α.toLat : Type u))
    ((Hom.hom
            (CategoryStruct.comp (Y := β)
              (ofHom
                (let __src : LatticeHom (↑α.1 : Type u) (↑β.1 : Type u) :=
                  { toFun := (⇑e : (a : (↑α.1 : Type u)) → (↑β.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯ };
                { toFun := (⇑e : (a : (↑α.1 : Type u)) → (↑β.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯,
                  map_bot' := ⋯ }))
              (ofHom
                (let __src : LatticeHom (↑β.1 : Type u) (↑α.1 : Type u) :=
                  { toFun := (⇑e.symm : (a : (↑β.1 : Type u)) → (↑α.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯ };
                { toFun := (⇑e.symm : (a : (↑β.1 : Type u)) → (↑α.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯,
                  map_top' := ⋯, map_bot' := ⋯ }))) :
          (a : (↑α.toLat : Type u)) → (↑α.toLat : Type u))
        a :
      (↑α.toLat : Type u))
    ((Hom.hom (𝟙 α) : (a : (↑α.toLat : Type u)) → (↑α.toLat : Type u)) a : (↑α.toLat : Type u))

Tactic:
exact e.symm_apply_apply _

Premises used: OrderIso.symm_apply_apply
-- Module: Mathlib.Order.Category.BddLat
Goal:
α β : BddLat
e : (↑α.toLat : Type u) ≃o (↑β.toLat : Type u)
hf :
  ∀ (a : (↑β.toLat : Type u)),
    Eq (α := (↑β.toLat : Type u))
      ((Hom.hom
              (CategoryStruct.comp (Y := α)
                (ofHom
                  (let __src : LatticeHom (↑β.1 : Type u) (↑α.1 : Type u) :=
                    { toFun := (⇑e.symm : (a : (↑β.1 : Type u)) → (↑α.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯ };
                  { toFun := (⇑e.symm : (a : (↑β.1 : Type u)) → (↑α.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯,
                    map_top' := ⋯, map_bot' := ⋯ }))
                (ofHom
                  (let __src : LatticeHom (↑α.1 : Type u) (↑β.1 : Type u) :=
                    { toFun := (⇑e : (a : (↑α.1 : Type u)) → (↑β.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯ };
                  { toFun := (⇑e : (a : (↑α.1 : Type u)) → (↑β.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯,
                    map_top' := ⋯, map_bot' := ⋯ }))) :
            (a : (↑β.toLat : Type u)) → (↑β.toLat : Type u))
          a :
        (↑β.toLat : Type u))
      ((Hom.hom (𝟙 β) : (a : (↑β.toLat : Type u)) → (↑β.toLat : Type u)) a : (↑β.toLat : Type u))
⊢ CategoryStruct.comp (Y := α)
      (ofHom
        (let __src : LatticeHom (↑β.1 : Type u) (↑α.1 : Type u) :=
          { toFun := (⇑e.symm : (a : (↑β.1 : Type u)) → (↑α.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯ };
        { toFun := (⇑e.symm : (a : (↑β.1 : Type u)) → (↑α.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯,
          map_bot' := ⋯ }))
      (ofHom
        (let __src : LatticeHom (↑α.1 : Type u) (↑β.1 : Type u) :=
          { toFun := (⇑e : (a : (↑α.1 : Type u)) → (↑β.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯ };
        { toFun := (⇑e : (a : (↑α.1 : Type u)) → (↑β.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯,
          map_bot' := ⋯ })) =
    𝟙 β

Tactic:
ext
-- Module: Mathlib.Order.Category.BddLat
Goal:
α β : BddLat
e : (↑α.toLat : Type u) ≃o (↑β.toLat : Type u)
a : (↑β.toLat : Type u)
⊢ Eq (α := (↑β.toLat : Type u))
    ((Hom.hom
            (CategoryStruct.comp (Y := α)
              (ofHom
                (let __src : LatticeHom (↑β.1 : Type u) (↑α.1 : Type u) :=
                  { toFun := (⇑e.symm : (a : (↑β.1 : Type u)) → (↑α.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯ };
                { toFun := (⇑e.symm : (a : (↑β.1 : Type u)) → (↑α.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯,
                  map_top' := ⋯, map_bot' := ⋯ }))
              (ofHom
                (let __src : LatticeHom (↑α.1 : Type u) (↑β.1 : Type u) :=
                  { toFun := (⇑e : (a : (↑α.1 : Type u)) → (↑β.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯ };
                { toFun := (⇑e : (a : (↑α.1 : Type u)) → (↑β.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯,
                  map_bot' := ⋯ }))) :
          (a : (↑β.toLat : Type u)) → (↑β.toLat : Type u))
        a :
      (↑β.toLat : Type u))
    ((Hom.hom (𝟙 β) : (a : (↑β.toLat : Type u)) → (↑β.toLat : Type u)) a : (↑β.toLat : Type u))

Tactic:
e.apply_symm_apply _

Premises used: OrderIso.apply_symm_apply
-- Module: Mathlib.Order.Category.BddLat
Goal:
α β : BddLat
e : (↑α.toLat : Type u) ≃o (↑β.toLat : Type u)
a : (↑β.toLat : Type u)
⊢ Eq (α := (↑β.toLat : Type u))
    ((Hom.hom
            (CategoryStruct.comp (Y := α)
              (ofHom
                (let __src : LatticeHom (↑β.1 : Type u) (↑α.1 : Type u) :=
                  { toFun := (⇑e.symm : (a : (↑β.1 : Type u)) → (↑α.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯ };
                { toFun := (⇑e.symm : (a : (↑β.1 : Type u)) → (↑α.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯,
                  map_top' := ⋯, map_bot' := ⋯ }))
              (ofHom
                (let __src : LatticeHom (↑α.1 : Type u) (↑β.1 : Type u) :=
                  { toFun := (⇑e : (a : (↑α.1 : Type u)) → (↑β.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯ };
                { toFun := (⇑e : (a : (↑α.1 : Type u)) → (↑β.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯,
                  map_bot' := ⋯ }))) :
          (a : (↑β.toLat : Type u)) → (↑β.toLat : Type u))
        a :
      (↑β.toLat : Type u))
    ((Hom.hom (𝟙 β) : (a : (↑β.toLat : Type u)) → (↑β.toLat : Type u)) a : (↑β.toLat : Type u))

Tactic:
exact e.apply_symm_apply _

Premises used: OrderIso.apply_symm_apply
-- 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)) BddOrd (FD := fun (x1 x2 : BddOrd.{u_1}) ↦
        BoundedOrderHom (↑x1.toPartOrd : Type u_1) (↑x2.toPartOrd : Type u_1)) (CD := fun (X : BddOrd.{u_1}) ↦
        (↑X.toPartOrd : Type u_1)) =
    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)) BddOrd (FD := fun (x1 x2 : BddOrd.{u_1}) ↦
        BoundedOrderHom (↑x1.toPartOrd : Type u_1) (↑x2.toPartOrd : Type u_1)) (CD := fun (X : BddOrd.{u_1}) ↦
        (↑X.toPartOrd : Type u_1)) ⋙
      BddOrd.dual

Tactic:
rfl

Premises used: BoundedLatticeHom.toBoundedOrderHom, 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)) Lat (FD := fun (x1 x2 : Lat.{u_1}) ↦ LatticeHom (↑x1 : Type u_1) (↑x2 : Type u_1)) (CD :=
        Lat.carrier) =
    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)) Lat (FD := fun (x1 x2 : Lat.{u_1}) ↦
        LatticeHom (↑x1 : Type u_1) (↑x2 : Type u_1)) (CD := Lat.carrier) ⋙
      Lat.dual

Tactic:
rfl

Premises used: BddLat.dual, CategoryTheory.Functor.comp, OrderDual, rfl