awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Category.BoolAlg
Goal:
X Y : Type u
inst : BooleanAlgebra X
inst_1 : BooleanAlgebra Y
f : BoundedLatticeHom X Y
x : X
⊢ Eq (α := (↑{ carrier := Y, str := inst_1 } : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : BoolAlg.{u}) ↦ BoundedLatticeHom (↑x1 : Type u) (↑x2 : Type u)) (CC :=
            carrier) (ofHom f) :
          (a : (↑{ carrier := X, str := inst } : Type u)) → (↑{ carrier := Y, str := inst_1 } : Type u))
        x :
      (↑{ carrier := Y, str := inst_1 } : Type u))
    ((f : (a : X) → Y) x : Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.BoolAlg
Goal:
X Y : BoolAlg
e : X ≅ Y
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) e.inv :
        (a : (↑Y : 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) e.hom :
            (a : (↑X : Type u_1)) → (↑Y : Type u_1))
          x :
        (↑Y : Type u_1)) =
    x

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

Tactic:
simp
-- Module: Mathlib.Order.Category.BoolAlg
Goal:
X : BoolAlg
⊢ (↑X.toBddDistLat.toDistLat : Type u_1) = (↑X : Type u_1)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.BoolAlg
Goal:
⊢ BoolAlg.dual ⋙
      forget₂ BoolAlg (FC := fun (x1 x2 : BoolAlg.{u_1}) ↦ BoundedLatticeHom (↑x1 : Type u_1) (↑x2 : Type u_1)) (CC :=
        BoolAlg.carrier) 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₂ BoolAlg (FC := fun (x1 x2 : BoolAlg.{u_1}) ↦ BoundedLatticeHom (↑x1 : Type u_1) (↑x2 : Type u_1)) (CC :=
        BoolAlg.carrier) 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: BoolAlg.dual, CategoryTheory.Functor.comp, OrderDual, rfl
-- Module: Mathlib.Order.Category.CompleteLat
Goal:
α : Type u_1
inst : CompleteLattice α
⊢ (↑{ carrier := α, str := inst : CompleteLat.{u_1} } : Type u_1) = α

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.CompleteLat
Goal:
α β : CompleteLat
e : (↑α : Type u) ≃o (↑β : Type u)
h :
  ∀ (a : (↑α : Type u)),
    Eq (α := (↑α : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : CompleteLat.{u}) ↦ CompleteLatticeHom (↑x1 : Type u) (↑x2 : Type u))
              (CC := carrier) (X := α) (Y := α)
              (CategoryStruct.comp (Y := β)
                (ConcreteCategory.ofHom (FC := fun (x1 x2 : CompleteLat.{u}) ↦
                  CompleteLatticeHom (↑x1 : Type u) (↑x2 : Type u)) (CC := carrier)
                  { toFun := (⇑e : (a : (↑α : Type u)) → (↑β : Type u)), map_sInf' := ⋯, map_sSup' := ⋯ })
                (ConcreteCategory.ofHom (FC := fun (x1 x2 : CompleteLat.{u}) ↦
                  CompleteLatticeHom (↑x1 : Type u) (↑x2 : Type u)) (CC := carrier)
                  { toFun := (⇑e.symm : (a : (↑β : Type u)) → (↑α : Type u)), map_sInf' := ⋯, map_sSup' := ⋯ })) :
            (a : (↑α : Type u)) → (↑α : Type u))
          a :
        (↑α : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : CompleteLat.{u}) ↦ CompleteLatticeHom (↑x1 : Type u) (↑x2 : Type u))
              (CC := carrier) (𝟙 α) :
            (a : (↑α : Type u)) → (↑α : Type u))
          a :
        (↑α : Type u))
⊢ CategoryStruct.comp (Y := β)
      (ConcreteCategory.ofHom (FC := fun (x1 x2 : CompleteLat.{u}) ↦ CompleteLatticeHom (↑x1 : Type u) (↑x2 : Type u))
        (CC := carrier) { toFun := (⇑e : (a : (↑α : Type u)) → (↑β : Type u)), map_sInf' := ⋯, map_sSup' := ⋯ })
      (ConcreteCategory.ofHom (FC := fun (x1 x2 : CompleteLat.{u}) ↦ CompleteLatticeHom (↑x1 : Type u) (↑x2 : Type u))
        (CC := carrier) { toFun := (⇑e.symm : (a : (↑β : Type u)) → (↑α : Type u)), map_sInf' := ⋯, map_sSup' := ⋯ }) =
    𝟙 α

Tactic:
ext
-- Module: Mathlib.Order.Category.CompleteLat
Goal:
α β : CompleteLat
e : (↑α : Type u) ≃o (↑β : Type u)
a : (↑α : Type u)
⊢ Eq (α := (↑α : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompleteLat.{u}) ↦ CompleteLatticeHom (↑x1 : Type u) (↑x2 : Type u))
            (CC := carrier) (X := α) (Y := α)
            (CategoryStruct.comp (Y := β)
              (ConcreteCategory.ofHom (FC := fun (x1 x2 : CompleteLat.{u}) ↦
                CompleteLatticeHom (↑x1 : Type u) (↑x2 : Type u)) (CC := carrier)
                { toFun := (⇑e : (a : (↑α : Type u)) → (↑β : Type u)), map_sInf' := ⋯, map_sSup' := ⋯ })
              (ConcreteCategory.ofHom (FC := fun (x1 x2 : CompleteLat.{u}) ↦
                CompleteLatticeHom (↑x1 : Type u) (↑x2 : Type u)) (CC := carrier)
                { toFun := (⇑e.symm : (a : (↑β : Type u)) → (↑α : Type u)), map_sInf' := ⋯, map_sSup' := ⋯ })) :
          (a : (↑α : Type u)) → (↑α : Type u))
        a :
      (↑α : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompleteLat.{u}) ↦ CompleteLatticeHom (↑x1 : Type u) (↑x2 : Type u))
            (CC := carrier) (𝟙 α) :
          (a : (↑α : Type u)) → (↑α : Type u))
        a :
      (↑α : Type u))

Tactic:
e.symm_apply_apply _

Premises used: OrderIso.symm_apply_apply
-- Module: Mathlib.Order.Category.CompleteLat
Goal:
α β : CompleteLat
e : (↑α : Type u) ≃o (↑β : Type u)
a : (↑α : Type u)
⊢ Eq (α := (↑α : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompleteLat.{u}) ↦ CompleteLatticeHom (↑x1 : Type u) (↑x2 : Type u))
            (CC := carrier) (X := α) (Y := α)
            (CategoryStruct.comp (Y := β)
              (ConcreteCategory.ofHom (FC := fun (x1 x2 : CompleteLat.{u}) ↦
                CompleteLatticeHom (↑x1 : Type u) (↑x2 : Type u)) (CC := carrier)
                { toFun := (⇑e : (a : (↑α : Type u)) → (↑β : Type u)), map_sInf' := ⋯, map_sSup' := ⋯ })
              (ConcreteCategory.ofHom (FC := fun (x1 x2 : CompleteLat.{u}) ↦
                CompleteLatticeHom (↑x1 : Type u) (↑x2 : Type u)) (CC := carrier)
                { toFun := (⇑e.symm : (a : (↑β : Type u)) → (↑α : Type u)), map_sInf' := ⋯, map_sSup' := ⋯ })) :
          (a : (↑α : Type u)) → (↑α : Type u))
        a :
      (↑α : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompleteLat.{u}) ↦ CompleteLatticeHom (↑x1 : Type u) (↑x2 : Type u))
            (CC := carrier) (𝟙 α) :
          (a : (↑α : Type u)) → (↑α : Type u))
        a :
      (↑α : Type u))

Tactic:
exact e.symm_apply_apply _

Premises used: OrderIso.symm_apply_apply
-- Module: Mathlib.Order.Category.CompleteLat
Goal:
α β : CompleteLat
e : (↑α : Type u) ≃o (↑β : Type u)
h :
  ∀ (a : (↑β : Type u)),
    Eq (α := (↑β : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : CompleteLat.{u}) ↦ CompleteLatticeHom (↑x1 : Type u) (↑x2 : Type u))
              (CC := carrier) (X := β) (Y := β)
              (CategoryStruct.comp (Y := α)
                (ConcreteCategory.ofHom (FC := fun (x1 x2 : CompleteLat.{u}) ↦
                  CompleteLatticeHom (↑x1 : Type u) (↑x2 : Type u)) (CC := carrier)
                  { toFun := (⇑e.symm : (a : (↑β : Type u)) → (↑α : Type u)), map_sInf' := ⋯, map_sSup' := ⋯ })
                (ConcreteCategory.ofHom (FC := fun (x1 x2 : CompleteLat.{u}) ↦
                  CompleteLatticeHom (↑x1 : Type u) (↑x2 : Type u)) (CC := carrier)
                  { toFun := (⇑e : (a : (↑α : Type u)) → (↑β : Type u)), map_sInf' := ⋯, map_sSup' := ⋯ })) :
            (a : (↑β : Type u)) → (↑β : Type u))
          a :
        (↑β : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : CompleteLat.{u}) ↦ CompleteLatticeHom (↑x1 : Type u) (↑x2 : Type u))
              (CC := carrier) (𝟙 β) :
            (a : (↑β : Type u)) → (↑β : Type u))
          a :
        (↑β : Type u))
⊢ CategoryStruct.comp (Y := α)
      (ConcreteCategory.ofHom (FC := fun (x1 x2 : CompleteLat.{u}) ↦ CompleteLatticeHom (↑x1 : Type u) (↑x2 : Type u))
        (CC := carrier) { toFun := (⇑e.symm : (a : (↑β : Type u)) → (↑α : Type u)), map_sInf' := ⋯, map_sSup' := ⋯ })
      (ConcreteCategory.ofHom (FC := fun (x1 x2 : CompleteLat.{u}) ↦ CompleteLatticeHom (↑x1 : Type u) (↑x2 : Type u))
        (CC := carrier) { toFun := (⇑e : (a : (↑α : Type u)) → (↑β : Type u)), map_sInf' := ⋯, map_sSup' := ⋯ }) =
    𝟙 β

Tactic:
ext
-- Module: Mathlib.Order.Category.CompleteLat
Goal:
α β : CompleteLat
e : (↑α : Type u) ≃o (↑β : Type u)
a : (↑β : Type u)
⊢ Eq (α := (↑β : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompleteLat.{u}) ↦ CompleteLatticeHom (↑x1 : Type u) (↑x2 : Type u))
            (CC := carrier) (X := β) (Y := β)
            (CategoryStruct.comp (Y := α)
              (ConcreteCategory.ofHom (FC := fun (x1 x2 : CompleteLat.{u}) ↦
                CompleteLatticeHom (↑x1 : Type u) (↑x2 : Type u)) (CC := carrier)
                { toFun := (⇑e.symm : (a : (↑β : Type u)) → (↑α : Type u)), map_sInf' := ⋯, map_sSup' := ⋯ })
              (ConcreteCategory.ofHom (FC := fun (x1 x2 : CompleteLat.{u}) ↦
                CompleteLatticeHom (↑x1 : Type u) (↑x2 : Type u)) (CC := carrier)
                { toFun := (⇑e : (a : (↑α : Type u)) → (↑β : Type u)), map_sInf' := ⋯, map_sSup' := ⋯ })) :
          (a : (↑β : Type u)) → (↑β : Type u))
        a :
      (↑β : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompleteLat.{u}) ↦ CompleteLatticeHom (↑x1 : Type u) (↑x2 : Type u))
            (CC := carrier) (𝟙 β) :
          (a : (↑β : Type u)) → (↑β : Type u))
        a :
      (↑β : Type u))

Tactic:
e.apply_symm_apply _

Premises used: OrderIso.apply_symm_apply
-- Module: Mathlib.Order.Category.CompleteLat
Goal:
α β : CompleteLat
e : (↑α : Type u) ≃o (↑β : Type u)
a : (↑β : Type u)
⊢ Eq (α := (↑β : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompleteLat.{u}) ↦ CompleteLatticeHom (↑x1 : Type u) (↑x2 : Type u))
            (CC := carrier) (X := β) (Y := β)
            (CategoryStruct.comp (Y := α)
              (ConcreteCategory.ofHom (FC := fun (x1 x2 : CompleteLat.{u}) ↦
                CompleteLatticeHom (↑x1 : Type u) (↑x2 : Type u)) (CC := carrier)
                { toFun := (⇑e.symm : (a : (↑β : Type u)) → (↑α : Type u)), map_sInf' := ⋯, map_sSup' := ⋯ })
              (ConcreteCategory.ofHom (FC := fun (x1 x2 : CompleteLat.{u}) ↦
                CompleteLatticeHom (↑x1 : Type u) (↑x2 : Type u)) (CC := carrier)
                { toFun := (⇑e : (a : (↑α : Type u)) → (↑β : Type u)), map_sInf' := ⋯, map_sSup' := ⋯ })) :
          (a : (↑β : Type u)) → (↑β : Type u))
        a :
      (↑β : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompleteLat.{u}) ↦ CompleteLatticeHom (↑x1 : Type u) (↑x2 : Type u))
            (CC := carrier) (𝟙 β) :
          (a : (↑β : Type u)) → (↑β : Type u))
        a :
      (↑β : Type u))

Tactic:
exact e.apply_symm_apply _

Premises used: OrderIso.apply_symm_apply
-- Module: Mathlib.Order.Category.CompleteLat
Goal:
⊢ CompleteLat.dual ⋙
      forget₂ CompleteLat (FC := fun (x1 x2 : CompleteLat.{u_1}) ↦ CompleteLatticeHom (↑x1 : Type u_1) (↑x2 : Type u_1))
        (CC := CompleteLat.carrier) 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₂ CompleteLat (FC := fun (x1 x2 : CompleteLat.{u_1}) ↦ CompleteLatticeHom (↑x1 : Type u_1) (↑x2 : Type u_1))
        (CC := CompleteLat.carrier) 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)) ⋙
      BddLat.dual

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, CompleteLat.dual, CompleteLatticeHom.toBoundedLatticeHom, OrderDual, rfl
-- Module: Mathlib.Order.Category.DistLat
Goal:
X : DistLat
⊢ Eq (α := (a : (↑X : Type u_1)) → (↑X : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : DistLat.{u_1}) ↦ LatticeHom (↑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.DistLat
Goal:
X Y Z : DistLat
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := (a : (↑X : Type u_1)) → (↑Z : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : DistLat.{u_1}) ↦ LatticeHom (↑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 : DistLat.{u_1}) ↦ LatticeHom (↑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 : DistLat.{u_1}) ↦ LatticeHom (↑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.DistLat
Goal:
X Y : DistLat
f : X ⟶ Y
⊢ Eq (α :=
    (a :
        (fun (X : Type u_1) ↦ X)
          (Functor.obj
            (forget DistLat (FC := fun (x1 x2 : DistLat.{u_1}) ↦ LatticeHom (↑x1 : Type u_1) (↑x2 : Type u_1)) (CC :=
              carrier))
            X)) →
      (fun (X : Type u_1) ↦ X)
        (Functor.obj
          (forget DistLat (FC := fun (x1 x2 : DistLat.{u_1}) ↦ LatticeHom (↑x1 : Type u_1) (↑x2 : Type u_1)) (CC :=
            carrier))
          Y))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map
            (forget DistLat (FC := fun (x1 x2 : DistLat.{u_1}) ↦ LatticeHom (↑x1 : Type u_1) (↑x2 : Type u_1)) (CC :=
              carrier))
            f)) :
      (a : (fun (X : Type u_1) ↦ X) ((forget DistLat).obj X)) → (fun (X : Type u_1) ↦ X) ((forget DistLat).obj Y))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : DistLat.{u_1}) ↦ LatticeHom (↑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.DistLat
Goal:
X Y : DistLat
f g : X ⟶ Y
w :
  ∀ (x : (↑X : Type u_1)),
    Eq (α := (↑Y : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : DistLat.{u_1}) ↦ LatticeHom (↑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 : DistLat.{u_1}) ↦ LatticeHom (↑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.DistLat
Goal:
X : Type u
inst : DistribLattice X
⊢ (↑(of X) : Type u) = X

Tactic:
rfl

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

Tactic:
rfl

Premises used: LatticeHom.id, rfl
-- Module: Mathlib.Order.Category.DistLat
Goal:
X : DistLat
x : (↑X : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : DistLat.{u_1}) ↦ LatticeHom (↑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.DistLat
Goal:
X Y Z : DistLat
f : X ⟶ Y
g : Y ⟶ Z
⊢ Hom.hom (f ≫ g) = (Hom.hom g).comp (Hom.hom f)

Tactic:
rfl

Premises used: LatticeHom.comp, rfl
-- Module: Mathlib.Order.Category.DistLat
Goal:
X Y Z : DistLat
f : X ⟶ Y
g : Y ⟶ Z
x : (↑X : Type u_1)
⊢ Eq (α := (↑Z : Type u_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : DistLat.{u_1}) ↦ LatticeHom (↑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 : DistLat.{u_1}) ↦ LatticeHom (↑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 : DistLat.{u_1}) ↦ LatticeHom (↑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.DistLat
Goal:
X Y : DistLat
f g : X ⟶ Y
hf : Hom.hom f = Hom.hom g
⊢ f = g

Tactic:
Hom.ext hf

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

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.DistLat
Goal:
X : Type u
inst : DistribLattice X
⊢ ofHom (LatticeHom.id X) = 𝟙 (of X)

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.DistLat
Goal:
X Y : Type u
inst : DistribLattice X
inst_1 : DistribLattice Y
f : LatticeHom X Y
x : X
⊢ Eq (α := (↑(of Y) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : DistLat.{u}) ↦ LatticeHom (↑x1 : Type u) (↑x2 : Type u)) (CC := carrier)
            (ofHom f) :
          (a : (↑(of X) : Type u)) → (↑(of Y) : Type u))
        x :
      (↑(of Y) : Type u))
    ((f : (a : X) → Y) x : Y)

Tactic:
rfl

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

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

Tactic:
simp
-- Module: Mathlib.Order.Category.DistLat
Goal:
⊢ DistLat.dual ⋙
      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) =
    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) ⋙
      Lat.dual

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, OrderDual, rfl, DistLat.dual
-- Module: Mathlib.Order.Category.FinBddDistLat
Goal:
X : FinBddDistLat
⊢ Eq (α :=
    (a : (fun (X : FinBddDistLat.{u_1}) ↦ (↑X.toDistLat : Type u_1)) X) →
      (fun (X : FinBddDistLat.{u_1}) ↦ (↑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)) (𝟙 X)) :
      (a : (fun (X : FinBddDistLat) ↦ (↑X.toDistLat : Type u_1)) X) →
        (fun (X : FinBddDistLat) ↦ (↑X.toDistLat : Type u_1)) X)
    id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.FinBddDistLat
Goal:
X Y Z : FinBddDistLat
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α :=
    (a : (fun (X : FinBddDistLat.{u_1}) ↦ (↑X.toDistLat : Type u_1)) 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)) (f ≫ g)) :
      (a : (fun (X : FinBddDistLat) ↦ (↑X.toDistLat : Type u_1)) X) →
        (fun (X : FinBddDistLat) ↦ (↑X.toDistLat : Type u_1)) Z)
    (Function.comp (β := (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)) 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))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.FinBddDistLat
Goal:
X Y : FinBddDistLat
f : X ⟶ Y
⊢ Eq (α :=
    (a :
        (fun (X : Type u_1) ↦ X)
          (Functor.obj
            (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)))
            X)) →
      (fun (X : Type u_1) ↦ X)
        (Functor.obj
          (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)))
          Y))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map
            (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)))
            f)) :
      (a : (fun (X : Type u_1) ↦ X) ((forget FinBddDistLat).obj X)) →
        (fun (X : Type u_1) ↦ X) ((forget FinBddDistLat).obj 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)

Tactic:
rfl

Premises used: rfl