awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₂)
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))

Tactic:
CategoryTheory.congr_fun h x

Premises used: CategoryTheory.congr_fun
-- 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₂)
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))

Tactic:
exact CategoryTheory.congr_fun h x

Premises used: CategoryTheory.congr_fun
-- Module: Mathlib.Order.Category.FinBoolAlg
Goal:
α β : FinBoolAlg
e : (↑α.toBoolAlg : Type u) ≃o (↑β.toBoolAlg : Type u)
h :
  ∀ (a : (↑α.toBoolAlg : Type u)),
    Eq (α := (↑α.toBoolAlg : Type u))
      ((@ConcreteCategory.hom FinBoolAlg largeCategory
              (fun (x1 x2 : FinBoolAlg.{u}) ↦ BoundedLatticeHom (↑x1.toBoolAlg : Type u) (↑x2.toBoolAlg : Type u))
              (fun (X : FinBoolAlg.{u}) ↦ (↑X.toBoolAlg : Type u)) _ _ α α
              (CategoryStruct.comp (Y := β)
                (InducedCategory.homMk
                  (BoolAlg.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' := ⋯ })))
                (InducedCategory.homMk
                  (BoolAlg.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 : (↑α.toBoolAlg : Type u)) → (↑α.toBoolAlg : Type u))
          a :
        (↑α.toBoolAlg : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : FinBoolAlg.{u}) ↦
              BoundedLatticeHom (↑x1.toBoolAlg : Type u) (↑x2.toBoolAlg : Type u)) (CC := fun (X : FinBoolAlg.{u}) ↦
              (↑X.toBoolAlg : Type u)) (𝟙 α) :
            (a : (↑α.toBoolAlg : Type u)) → (↑α.toBoolAlg : Type u))
          a :
        (↑α.toBoolAlg : Type u))
⊢ CategoryStruct.comp (Y := β)
      (InducedCategory.homMk
        (BoolAlg.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' := ⋯ })))
      (InducedCategory.homMk
        (BoolAlg.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.FinBoolAlg
Goal:
α β : FinBoolAlg
e : (↑α.toBoolAlg : Type u) ≃o (↑β.toBoolAlg : Type u)
a : (↑α.toBoolAlg : Type u)
⊢ Eq (α := (↑α.toBoolAlg : Type u))
    ((@ConcreteCategory.hom FinBoolAlg largeCategory
            (fun (x1 x2 : FinBoolAlg.{u}) ↦ BoundedLatticeHom (↑x1.toBoolAlg : Type u) (↑x2.toBoolAlg : Type u))
            (fun (X : FinBoolAlg.{u}) ↦ (↑X.toBoolAlg : Type u)) _ _ α α
            (CategoryStruct.comp (Y := β)
              (InducedCategory.homMk
                (BoolAlg.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' := ⋯ })))
              (InducedCategory.homMk
                (BoolAlg.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 : (↑α.toBoolAlg : Type u)) → (↑α.toBoolAlg : Type u))
        a :
      (↑α.toBoolAlg : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : FinBoolAlg.{u}) ↦
            BoundedLatticeHom (↑x1.toBoolAlg : Type u) (↑x2.toBoolAlg : Type u)) (CC := fun (X : FinBoolAlg.{u}) ↦
            (↑X.toBoolAlg : Type u)) (𝟙 α) :
          (a : (↑α.toBoolAlg : Type u)) → (↑α.toBoolAlg : Type u))
        a :
      (↑α.toBoolAlg : Type u))

Tactic:
e.symm_apply_apply _

Premises used: OrderIso.symm_apply_apply
-- Module: Mathlib.Order.Category.FinBoolAlg
Goal:
α β : FinBoolAlg
e : (↑α.toBoolAlg : Type u) ≃o (↑β.toBoolAlg : Type u)
a : (↑α.toBoolAlg : Type u)
⊢ Eq (α := (↑α.toBoolAlg : Type u))
    ((@ConcreteCategory.hom FinBoolAlg largeCategory
            (fun (x1 x2 : FinBoolAlg.{u}) ↦ BoundedLatticeHom (↑x1.toBoolAlg : Type u) (↑x2.toBoolAlg : Type u))
            (fun (X : FinBoolAlg.{u}) ↦ (↑X.toBoolAlg : Type u)) _ _ α α
            (CategoryStruct.comp (Y := β)
              (InducedCategory.homMk
                (BoolAlg.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' := ⋯ })))
              (InducedCategory.homMk
                (BoolAlg.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 : (↑α.toBoolAlg : Type u)) → (↑α.toBoolAlg : Type u))
        a :
      (↑α.toBoolAlg : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : FinBoolAlg.{u}) ↦
            BoundedLatticeHom (↑x1.toBoolAlg : Type u) (↑x2.toBoolAlg : Type u)) (CC := fun (X : FinBoolAlg.{u}) ↦
            (↑X.toBoolAlg : Type u)) (𝟙 α) :
          (a : (↑α.toBoolAlg : Type u)) → (↑α.toBoolAlg : Type u))
        a :
      (↑α.toBoolAlg : Type u))

Tactic:
exact e.symm_apply_apply _

Premises used: OrderIso.symm_apply_apply
-- Module: Mathlib.Order.Category.FinBoolAlg
Goal:
α β : FinBoolAlg
e : (↑α.toBoolAlg : Type u) ≃o (↑β.toBoolAlg : Type u)
h :
  ∀ (a : (↑β.toBoolAlg : Type u)),
    Eq (α := (↑β.toBoolAlg : Type u))
      ((@ConcreteCategory.hom FinBoolAlg largeCategory
              (fun (x1 x2 : FinBoolAlg.{u}) ↦ BoundedLatticeHom (↑x1.toBoolAlg : Type u) (↑x2.toBoolAlg : Type u))
              (fun (X : FinBoolAlg.{u}) ↦ (↑X.toBoolAlg : Type u)) _ _ β β
              (CategoryStruct.comp (Y := α)
                (InducedCategory.homMk
                  (BoolAlg.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' := ⋯ })))
                (InducedCategory.homMk
                  (BoolAlg.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 : (↑β.toBoolAlg : Type u)) → (↑β.toBoolAlg : Type u))
          a :
        (↑β.toBoolAlg : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : FinBoolAlg.{u}) ↦
              BoundedLatticeHom (↑x1.toBoolAlg : Type u) (↑x2.toBoolAlg : Type u)) (CC := fun (X : FinBoolAlg.{u}) ↦
              (↑X.toBoolAlg : Type u)) (𝟙 β) :
            (a : (↑β.toBoolAlg : Type u)) → (↑β.toBoolAlg : Type u))
          a :
        (↑β.toBoolAlg : Type u))
⊢ CategoryStruct.comp (Y := α)
      (InducedCategory.homMk
        (BoolAlg.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' := ⋯ })))
      (InducedCategory.homMk
        (BoolAlg.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.FinBoolAlg
Goal:
α β : FinBoolAlg
e : (↑α.toBoolAlg : Type u) ≃o (↑β.toBoolAlg : Type u)
a : (↑β.toBoolAlg : Type u)
⊢ Eq (α := (↑β.toBoolAlg : Type u))
    ((@ConcreteCategory.hom FinBoolAlg largeCategory
            (fun (x1 x2 : FinBoolAlg.{u}) ↦ BoundedLatticeHom (↑x1.toBoolAlg : Type u) (↑x2.toBoolAlg : Type u))
            (fun (X : FinBoolAlg.{u}) ↦ (↑X.toBoolAlg : Type u)) _ _ β β
            (CategoryStruct.comp (Y := α)
              (InducedCategory.homMk
                (BoolAlg.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' := ⋯ })))
              (InducedCategory.homMk
                (BoolAlg.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 : (↑β.toBoolAlg : Type u)) → (↑β.toBoolAlg : Type u))
        a :
      (↑β.toBoolAlg : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : FinBoolAlg.{u}) ↦
            BoundedLatticeHom (↑x1.toBoolAlg : Type u) (↑x2.toBoolAlg : Type u)) (CC := fun (X : FinBoolAlg.{u}) ↦
            (↑X.toBoolAlg : Type u)) (𝟙 β) :
          (a : (↑β.toBoolAlg : Type u)) → (↑β.toBoolAlg : Type u))
        a :
      (↑β.toBoolAlg : Type u))

Tactic:
e.apply_symm_apply _

Premises used: OrderIso.apply_symm_apply
-- Module: Mathlib.Order.Category.FinBoolAlg
Goal:
α β : FinBoolAlg
e : (↑α.toBoolAlg : Type u) ≃o (↑β.toBoolAlg : Type u)
a : (↑β.toBoolAlg : Type u)
⊢ Eq (α := (↑β.toBoolAlg : Type u))
    ((@ConcreteCategory.hom FinBoolAlg largeCategory
            (fun (x1 x2 : FinBoolAlg.{u}) ↦ BoundedLatticeHom (↑x1.toBoolAlg : Type u) (↑x2.toBoolAlg : Type u))
            (fun (X : FinBoolAlg.{u}) ↦ (↑X.toBoolAlg : Type u)) _ _ β β
            (CategoryStruct.comp (Y := α)
              (InducedCategory.homMk
                (BoolAlg.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' := ⋯ })))
              (InducedCategory.homMk
                (BoolAlg.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 : (↑β.toBoolAlg : Type u)) → (↑β.toBoolAlg : Type u))
        a :
      (↑β.toBoolAlg : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : FinBoolAlg.{u}) ↦
            BoundedLatticeHom (↑x1.toBoolAlg : Type u) (↑x2.toBoolAlg : Type u)) (CC := fun (X : FinBoolAlg.{u}) ↦
            (↑X.toBoolAlg : Type u)) (𝟙 β) :
          (a : (↑β.toBoolAlg : Type u)) → (↑β.toBoolAlg : Type u))
        a :
      (↑β.toBoolAlg : Type u))

Tactic:
exact e.apply_symm_apply _

Premises used: OrderIso.apply_symm_apply
-- Module: Mathlib.Order.Category.FinBoolAlg
Goal:
⊢ FinBoolAlg.dual ⋙
      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)) FinBddDistLat (FD := fun (x1 x2 : FinBddDistLat.{u_1}) ↦
        BoundedLatticeHom (↑x1.toDistLat : Type u_1) (↑x2.toDistLat : Type u_1)) (CD := fun (X : FinBddDistLat.{u_1}) ↦
        (↑X.toDistLat : Type u_1)) =
    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)) FinBddDistLat (FD := fun (x1 x2 : FinBddDistLat.{u_1}) ↦
        BoundedLatticeHom (↑x1.toDistLat : Type u_1) (↑x2.toDistLat : Type u_1)) (CD := fun (X : FinBddDistLat.{u_1}) ↦
        (↑X.toDistLat : Type u_1)) ⋙
      FinBddDistLat.dual

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, FinBoolAlg.dual, OrderDual, rfl
-- Module: Mathlib.Order.Category.FinPartOrd
Goal:
X : FinPartOrd
⊢ PartOrd.Hom.hom (InducedCategory.Hom.hom (𝟙 X)) = OrderHom.id

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
InducedCategory.hom_ext (ConcreteCategory.ext hf)

Premises used: CategoryTheory.InducedCategory.hom_ext, CategoryTheory.ConcreteCategory.ext
-- Module: Mathlib.Order.Category.FinPartOrd
Goal:
X Y : Type u
inst : PartialOrder X
inst_1 : Fintype X
inst_2 : PartialOrder Y
inst_3 : Fintype Y
f : X →o Y
⊢ PartOrd.Hom.hom (InducedCategory.Hom.hom (ofHom f)) = f

Tactic:
rfl

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

Tactic:
rfl

Premises used: CategoryTheory.InducedCategory.homMk, rfl
-- Module: Mathlib.Order.Category.FinPartOrd
Goal:
⊢ FinPartOrd.dual ⋙
      forget₂ FinPartOrd (FC := fun (x1 x2 : FinPartOrd.{u_1}) ↦
        (↑x1.toPartOrd : Type u_1) →o (↑x2.toPartOrd : Type u_1)) (CC := fun (X : FinPartOrd.{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₂ FinPartOrd (FC := fun (x1 x2 : FinPartOrd.{u_1}) ↦ (↑x1.toPartOrd : Type u_1) →o (↑x2.toPartOrd : Type u_1))
        (CC := fun (X : FinPartOrd.{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: FinPartOrd.dual, CategoryTheory.Functor.comp, CategoryTheory.inducedFunctor, OrderDual, rfl
-- Module: Mathlib.Order.Category.Frm
Goal:
X : Frm
⊢ Eq (α := (a : (↑X : Type u_1)) → (↑X : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : Frm.{u_1}) ↦ FrameHom (↑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.Frm
Goal:
X Y Z : Frm
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := (a : (↑X : Type u_1)) → (↑Z : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : Frm.{u_1}) ↦ FrameHom (↑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 : Frm.{u_1}) ↦ FrameHom (↑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 : Frm.{u_1}) ↦ FrameHom (↑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