awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Category.FinBddDistLat
Goal:
X Y : FinBddDistLat
f g : X ⟶ Y
w :
  ∀ (x : (↑X.toDistLat : Type u_1)),
    Eq (α := (fun (X : FinBddDistLat.{u_1}) ↦ (↑X.toDistLat : Type u_1)) Y)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : FinBddDistLat.{u_1}) ↦
              BoundedLatticeHom (↑x1.toDistLat : Type u_1) (↑x2.toDistLat : Type u_1)) (CC :=
              fun (X : FinBddDistLat.{u_1}) ↦ (↑X.toDistLat : Type u_1)) f :
            (a : (fun (X : FinBddDistLat) ↦ (↑X.toDistLat : Type u_1)) X) →
              (fun (X : FinBddDistLat) ↦ (↑X.toDistLat : Type u_1)) Y)
          x :
        (fun (X : FinBddDistLat.{u_1}) ↦ (↑X.toDistLat : Type u_1)) Y)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : FinBddDistLat.{u_1}) ↦
              BoundedLatticeHom (↑x1.toDistLat : Type u_1) (↑x2.toDistLat : Type u_1)) (CC :=
              fun (X : FinBddDistLat.{u_1}) ↦ (↑X.toDistLat : Type u_1)) g :
            (a : (fun (X : FinBddDistLat) ↦ (↑X.toDistLat : Type u_1)) X) →
              (fun (X : FinBddDistLat) ↦ (↑X.toDistLat : Type u_1)) Y)
          x :
        (fun (X : FinBddDistLat.{u_1}) ↦ (↑X.toDistLat : Type u_1)) Y)
⊢ f = g

Tactic:
ConcreteCategory.hom_ext _ _ w

Premises used: CategoryTheory.ConcreteCategory.hom_ext
-- Module: Mathlib.Order.Category.FinBddDistLat
Goal:
X : FinBddDistLat
⊢ Hom.hom (𝟙 X) = BoundedLatticeHom.id (↑X.toDistLat : Type u_1)

Tactic:
rfl

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

Tactic:
simp
-- Module: Mathlib.Order.Category.FinBddDistLat
Goal:
X Y Z : FinBddDistLat
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.FinBddDistLat
Goal:
X Y Z : FinBddDistLat
f : X ⟶ Y
g : Y ⟶ Z
x : (↑X.toDistLat : Type u_1)
⊢ Eq (α := (fun (X : FinBddDistLat.{u_1}) ↦ (↑X.toDistLat : Type u_1)) Z)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : FinBddDistLat.{u_1}) ↦
            BoundedLatticeHom (↑x1.toDistLat : Type u_1) (↑x2.toDistLat : Type u_1)) (CC :=
            fun (X : FinBddDistLat.{u_1}) ↦ (↑X.toDistLat : Type u_1)) (f ≫ g) :
          (a : (fun (X : FinBddDistLat) ↦ (↑X.toDistLat : Type u_1)) X) →
            (fun (X : FinBddDistLat) ↦ (↑X.toDistLat : Type u_1)) Z)
        x :
      (fun (X : FinBddDistLat.{u_1}) ↦ (↑X.toDistLat : Type u_1)) Z)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : FinBddDistLat.{u_1}) ↦
            BoundedLatticeHom (↑x1.toDistLat : Type u_1) (↑x2.toDistLat : Type u_1)) (CC :=
            fun (X : FinBddDistLat.{u_1}) ↦ (↑X.toDistLat : Type u_1)) g :
          (a : (fun (X : FinBddDistLat) ↦ (↑X.toDistLat : Type u_1)) Y) →
            (fun (X : FinBddDistLat) ↦ (↑X.toDistLat : Type u_1)) Z)
        ((ConcreteCategory.hom (FC := fun (x1 x2 : FinBddDistLat.{u_1}) ↦
                BoundedLatticeHom (↑x1.toDistLat : Type u_1) (↑x2.toDistLat : Type u_1)) (CC :=
                fun (X : FinBddDistLat.{u_1}) ↦ (↑X.toDistLat : Type u_1)) f :
              (a : (fun (X : FinBddDistLat) ↦ (↑X.toDistLat : Type u_1)) X) →
                (fun (X : FinBddDistLat) ↦ (↑X.toDistLat : Type u_1)) Y)
            x :
          (fun (X : FinBddDistLat.{u_1}) ↦ (↑X.toDistLat : Type u_1)) Y) :
      (fun (X : FinBddDistLat.{u_1}) ↦ (↑X.toDistLat : Type u_1)) Z)

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

Tactic:
Hom.ext hf

Premises used: FinBddDistLat.Hom.ext
-- Module: Mathlib.Order.Category.FinBddDistLat
Goal:
X Y : Type u
inst : DistribLattice X
inst_1 : BoundedOrder X
inst_2 : Fintype X
inst_3 : DistribLattice Y
inst_4 : BoundedOrder Y
inst_5 : Fintype Y
f : BoundedLatticeHom X Y
⊢ Hom.hom (ofHom f) = f

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.FinBddDistLat
Goal:
X : Type u
inst : DistribLattice X
inst_1 : BoundedOrder X
inst_2 : Fintype X
⊢ ofHom (BoundedLatticeHom.id X) = 𝟙 (of X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.FinBddDistLat
Goal:
X Y Z : Type u
inst : DistribLattice X
inst_1 : BoundedOrder X
inst_2 : Fintype X
inst_3 : DistribLattice Y
inst_4 : BoundedOrder Y
inst_5 : Fintype Y
inst_6 : DistribLattice Z
inst_7 : BoundedOrder Z
inst_8 : Fintype Z
f : BoundedLatticeHom X Y
g : BoundedLatticeHom Y Z
⊢ Eq (α := of X ⟶ of Z) (ofHom (g.comp f)) (CategoryStruct.comp (Y := of Y) (ofHom f) (ofHom g))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.FinBddDistLat
Goal:
X Y : Type u
inst : DistribLattice X
inst_1 : BoundedOrder X
inst_2 : Fintype X
inst_3 : DistribLattice Y
inst_4 : BoundedOrder Y
inst_5 : Fintype Y
f : BoundedLatticeHom X Y
x : X
⊢ Eq (α := (fun (X : FinBddDistLat.{u}) ↦ (↑X.toDistLat : Type u)) (of Y))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : FinBddDistLat.{u}) ↦
            BoundedLatticeHom (↑x1.toDistLat : Type u) (↑x2.toDistLat : Type u)) (CC := fun (X : FinBddDistLat.{u}) ↦
            (↑X.toDistLat : Type u)) (X := of X) (Y := of Y) (ofHom f) :
          (a : (fun (X : FinBddDistLat) ↦ (↑X.toDistLat : Type u)) (of X)) →
            (fun (X : FinBddDistLat) ↦ (↑X.toDistLat : Type u)) (of Y))
        x :
      (fun (X : FinBddDistLat.{u}) ↦ (↑X.toDistLat : Type u)) (of Y))
    ((f : (a : X) → Y) x : Y)

Tactic:
rfl

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

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

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

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

Tactic:
e.symm_apply_apply _

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

Tactic:
exact e.symm_apply_apply _

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

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

Tactic:
e.apply_symm_apply _

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

Tactic:
exact e.apply_symm_apply _

Premises used: OrderIso.apply_symm_apply
-- Module: Mathlib.Order.Category.FinBddDistLat
Goal:
⊢ FinBddDistLat.dual ⋙
      forget₂ FinBddDistLat (FC := fun (x1 x2 : FinBddDistLat.{u_1}) ↦
        BoundedLatticeHom (↑x1.toDistLat : Type u_1) (↑x2.toDistLat : Type u_1)) (CC := fun (X : FinBddDistLat.{u_1}) ↦
        (↑X.toDistLat : Type u_1)) BddDistLat (FD := fun (x1 x2 : BddDistLat.{u_1}) ↦
        BoundedLatticeHom (↑x1.toDistLat : Type u_1) (↑x2.toDistLat : Type u_1)) (CD := fun (X : BddDistLat.{u_1}) ↦
        (↑X.toDistLat : Type u_1)) =
    forget₂ FinBddDistLat (FC := fun (x1 x2 : FinBddDistLat.{u_1}) ↦
        BoundedLatticeHom (↑x1.toDistLat : Type u_1) (↑x2.toDistLat : Type u_1)) (CC := fun (X : FinBddDistLat.{u_1}) ↦
        (↑X.toDistLat : Type u_1)) BddDistLat (FD := fun (x1 x2 : BddDistLat.{u_1}) ↦
        BoundedLatticeHom (↑x1.toDistLat : Type u_1) (↑x2.toDistLat : Type u_1)) (CD := fun (X : BddDistLat.{u_1}) ↦
        (↑X.toDistLat : Type u_1)) ⋙
      BddDistLat.dual

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, FinBddDistLat.dual, OrderDual, rfl
-- Module: Mathlib.Order.Category.FinBoolAlg
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Fintype α
⊢ (↑(of α).toBoolAlg : Type u_1) = α

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.FinBoolAlg
Goal:
⊢ Functor.Full
    (forget₂ FinBoolAlg (FC := fun (x1 x2 : FinBoolAlg.{u_1}) ↦
      BoundedLatticeHom (↑x1.toBoolAlg : Type u_1) (↑x2.toBoolAlg : Type u_1)) (CC := fun (X : FinBoolAlg.{u_1}) ↦
      (↑X.toBoolAlg : Type u_1)) BoolAlg (FD := fun (x1 x2 : BoolAlg.{u_1}) ↦
      BoundedLatticeHom (↑x1 : Type u_1) (↑x2 : Type u_1)) (CD := BoolAlg.carrier))

Tactic:
InducedCategory.full _

Premises used: CategoryTheory.inducedFunctor, CategoryTheory.InducedCategory, CategoryTheory.InducedCategory.full
-- Module: Mathlib.Order.Category.FinBoolAlg
Goal:
⊢ Functor.Faithful
    (forget₂ FinBoolAlg (FC := fun (x1 x2 : FinBoolAlg.{u_1}) ↦
      BoundedLatticeHom (↑x1.toBoolAlg : Type u_1) (↑x2.toBoolAlg : Type u_1)) (CC := fun (X : FinBoolAlg.{u_1}) ↦
      (↑X.toBoolAlg : Type u_1)) BoolAlg (FD := fun (x1 x2 : BoolAlg.{u_1}) ↦
      BoundedLatticeHom (↑x1 : Type u_1) (↑x2 : Type u_1)) (CD := BoolAlg.carrier))

Tactic:
InducedCategory.faithful _

Premises used: CategoryTheory.InducedCategory.faithful, CategoryTheory.inducedFunctor, CategoryTheory.InducedCategory
-- Module: Mathlib.Order.Category.FinBoolAlg
Goal:
X Y : FinBoolAlg
a₁ a₂ : X ⟶ Y
h :
  Eq (α :=
    Functor.obj
        (forget₂ FinBoolAlg (FC := fun (x1 x2 : FinBoolAlg.{u_1}) ↦
          BoundedLatticeHom (↑x1.toBoolAlg : Type u_1) (↑x2.toBoolAlg : Type u_1)) (CC := fun (X : FinBoolAlg.{u_1}) ↦
          (↑X.toBoolAlg : Type u_1)) FinPartOrd (FD := fun (x1 x2 : FinPartOrd.{u_1}) ↦
          (↑x1.toPartOrd : Type u_1) →o (↑x2.toPartOrd : Type u_1)) (CD := fun (X : FinPartOrd.{u_1}) ↦
          (↑X.toPartOrd : Type u_1)))
        X ⟶
      Functor.obj
        (forget₂ FinBoolAlg (FC := fun (x1 x2 : FinBoolAlg.{u_1}) ↦
          BoundedLatticeHom (↑x1.toBoolAlg : Type u_1) (↑x2.toBoolAlg : Type u_1)) (CC := fun (X : FinBoolAlg.{u_1}) ↦
          (↑X.toBoolAlg : Type u_1)) FinPartOrd (FD := fun (x1 x2 : FinPartOrd.{u_1}) ↦
          (↑x1.toPartOrd : Type u_1) →o (↑x2.toPartOrd : Type u_1)) (CD := fun (X : FinPartOrd.{u_1}) ↦
          (↑X.toPartOrd : Type u_1)))
        Y)
    (CategoryTheory.Functor.map
      (forget₂ FinBoolAlg (FC := fun (x1 x2 : FinBoolAlg.{u_1}) ↦
        BoundedLatticeHom (↑x1.toBoolAlg : Type u_1) (↑x2.toBoolAlg : Type u_1)) (CC := fun (X : FinBoolAlg.{u_1}) ↦
        (↑X.toBoolAlg : Type u_1)) FinPartOrd (FD := fun (x1 x2 : FinPartOrd.{u_1}) ↦
        (↑x1.toPartOrd : Type u_1) →o (↑x2.toPartOrd : Type u_1)) (CD := fun (X : FinPartOrd.{u_1}) ↦
        (↑X.toPartOrd : Type u_1)))
      a₁)
    (CategoryTheory.Functor.map
      (forget₂ FinBoolAlg (FC := fun (x1 x2 : FinBoolAlg.{u_1}) ↦
        BoundedLatticeHom (↑x1.toBoolAlg : Type u_1) (↑x2.toBoolAlg : Type u_1)) (CC := fun (X : FinBoolAlg.{u_1}) ↦
        (↑X.toBoolAlg : Type u_1)) FinPartOrd (FD := fun (x1 x2 : FinPartOrd.{u_1}) ↦
        (↑x1.toPartOrd : Type u_1) →o (↑x2.toPartOrd : Type u_1)) (CD := fun (X : FinPartOrd.{u_1}) ↦
        (↑X.toPartOrd : Type u_1)))
      a₂)
h₁ :
  ∀ (x : (↑X.toBoolAlg : Type u_1)),
    Eq (α := (↑Y.toBoolAlg : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : FinBoolAlg.{u_1}) ↦
              BoundedLatticeHom (↑x1.toBoolAlg : Type u_1) (↑x2.toBoolAlg : Type u_1)) (CC :=
              fun (X : FinBoolAlg.{u_1}) ↦ (↑X.toBoolAlg : Type u_1)) a₁ :
            (a : (↑X.toBoolAlg : Type u_1)) → (↑Y.toBoolAlg : Type u_1))
          x :
        (↑Y.toBoolAlg : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : FinBoolAlg.{u_1}) ↦
              BoundedLatticeHom (↑x1.toBoolAlg : Type u_1) (↑x2.toBoolAlg : Type u_1)) (CC :=
              fun (X : FinBoolAlg.{u_1}) ↦ (↑X.toBoolAlg : Type u_1)) a₂ :
            (a : (↑X.toBoolAlg : Type u_1)) → (↑Y.toBoolAlg : Type u_1))
          x :
        (↑Y.toBoolAlg : Type u_1))
⊢ a₁ = a₂

Tactic:
ext x