awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Category.Frm
Goal:
X Y : Frm
f : X ⟶ Y
⊢ Eq (α :=
    (a :
        (fun (X : Type u_1) ↦ X)
          (Functor.obj
            (forget Frm (FC := fun (x1 x2 : Frm.{u_1}) ↦ FrameHom (↑x1 : Type u_1) (↑x2 : Type u_1)) (CC := carrier))
            X)) →
      (fun (X : Type u_1) ↦ X)
        (Functor.obj
          (forget Frm (FC := fun (x1 x2 : Frm.{u_1}) ↦ FrameHom (↑x1 : Type u_1) (↑x2 : Type u_1)) (CC := carrier)) Y))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map
            (forget Frm (FC := fun (x1 x2 : Frm.{u_1}) ↦ FrameHom (↑x1 : Type u_1) (↑x2 : Type u_1)) (CC := carrier))
            f)) :
      (a : (fun (X : Type u_1) ↦ X) ((forget Frm).obj X)) → (fun (X : Type u_1) ↦ X) ((forget Frm).obj Y))
    (⇑(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
-- Module: Mathlib.Order.Category.Frm
Goal:
X Y : Frm
f g : X ⟶ Y
w :
  ∀ (x : (↑X : Type u_1)),
    Eq (α := (↑Y : 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))
          x :
        (↑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 : (↑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.Frm
Goal:
X : Type u
inst : Frame X
⊢ (↑{ carrier := X, str := inst : Frm.{u} } : Type u) = X

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl, FrameHom.id
-- Module: Mathlib.Order.Category.Frm
Goal:
X : Frm
x : (↑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))
      x =
    x

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

Tactic:
rfl

Premises used: FrameHom.comp, rfl
-- Module: Mathlib.Order.Category.Frm
Goal:
X Y Z : Frm
f : X ⟶ Y
g : Y ⟶ Z
x : (↑X : Type u_1)
⊢ Eq (α := (↑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))
        x :
      (↑Z : 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))
            x :
          (↑Y : Type u_1)) :
      (↑Z : Type u_1))

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

Tactic:
Hom.ext hf

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.Frm
Goal:
X Y : Type u
inst : Frame X
inst_1 : Frame Y
f : FrameHom X Y
x : X
⊢ Eq (α := (↑{ carrier := Y, str := inst_1 } : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : Frm.{u}) ↦ FrameHom (↑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.Frm
Goal:
X Y : Frm
e : X ≅ Y
x : (↑X : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : Frm.{u_1}) ↦ FrameHom (↑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 : Frm.{u_1}) ↦ FrameHom (↑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.Frm
Goal:
X Y : Frm
e : X ≅ Y
s : (↑Y : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : Frm.{u_1}) ↦ FrameHom (↑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 : Frm.{u_1}) ↦ FrameHom (↑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.HeytAlg
Goal:
X : HeytAlg
⊢ Eq (α := (a : (↑X : Type u_1)) → (↑X : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : HeytAlg.{u_1}) ↦ HeytingHom (↑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.HeytAlg
Goal:
X Y Z : HeytAlg
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := (a : (↑X : Type u_1)) → (↑Z : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : HeytAlg.{u_1}) ↦ HeytingHom (↑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 : HeytAlg.{u_1}) ↦ HeytingHom (↑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 : HeytAlg.{u_1}) ↦ HeytingHom (↑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.HeytAlg
Goal:
X Y : HeytAlg
f : X ⟶ Y
⊢ Eq (α :=
    (a :
        (fun (X : Type u_1) ↦ X)
          (Functor.obj
            (forget HeytAlg (FC := fun (x1 x2 : HeytAlg.{u_1}) ↦ HeytingHom (↑x1 : Type u_1) (↑x2 : Type u_1)) (CC :=
              carrier))
            X)) →
      (fun (X : Type u_1) ↦ X)
        (Functor.obj
          (forget HeytAlg (FC := fun (x1 x2 : HeytAlg.{u_1}) ↦ HeytingHom (↑x1 : Type u_1) (↑x2 : Type u_1)) (CC :=
            carrier))
          Y))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map
            (forget HeytAlg (FC := fun (x1 x2 : HeytAlg.{u_1}) ↦ HeytingHom (↑x1 : Type u_1) (↑x2 : Type u_1)) (CC :=
              carrier))
            f)) :
      (a : (fun (X : Type u_1) ↦ X) ((forget HeytAlg).obj X)) → (fun (X : Type u_1) ↦ X) ((forget HeytAlg).obj Y))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : HeytAlg.{u_1}) ↦ HeytingHom (↑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.HeytAlg
Goal:
X Y : HeytAlg
f g : X ⟶ Y
w :
  ∀ (x : (↑X : Type u_1)),
    Eq (α := (↑Y : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : HeytAlg.{u_1}) ↦ HeytingHom (↑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 : HeytAlg.{u_1}) ↦ HeytingHom (↑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.HeytAlg
Goal:
X : Type u
inst : HeytingAlgebra X
⊢ (↑(of X) : Type u) = X

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
Hom.ext hf

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

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.HeytAlg
Goal:
X : Type u
inst : HeytingAlgebra X
⊢ ofHom (HeytingHom.id X) = 𝟙 (of X)

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.HeytAlg
Goal:
X Y : Type u
inst : HeytingAlgebra X
inst_1 : HeytingAlgebra Y
f : HeytingHom X Y
x : X
⊢ Eq (α := (↑(of Y) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : HeytAlg.{u}) ↦ HeytingHom (↑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.HeytAlg
Goal:
X Y : HeytAlg
e : X ≅ Y
x : (↑X : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : HeytAlg.{u_1}) ↦ HeytingHom (↑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 : HeytAlg.{u_1}) ↦ HeytingHom (↑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.HeytAlg
Goal:
X Y : HeytAlg
e : X ≅ Y
s : (↑Y : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : HeytAlg.{u_1}) ↦ HeytingHom (↑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 : HeytAlg.{u_1}) ↦ HeytingHom (↑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.HeytAlg
Goal:
α β : HeytAlg
e : (↑α : Type u) ≃o (↑β : Type u)
hf :
  ∀ (a : (↑α : Type u)),
    Eq (α := (↑α : Type u))
      ((Hom.hom
              (CategoryStruct.comp (Y := β)
                (ofHom
                  { toFun := (⇑e : (a : (↑α : Type u)) → (↑β : Type u)), map_sup' := ⋯, map_inf' := ⋯, map_bot' := ⋯,
                    map_himp' := ⋯ })
                (ofHom
                  { toFun := (⇑e.symm : (a : (↑β : Type u)) → (↑α : Type u)), map_sup' := ⋯, map_inf' := ⋯,
                    map_bot' := ⋯, map_himp' := ⋯ })) :
            (a : (↑α : Type u)) → (↑α : Type u))
          a :
        (↑α : Type u))
      ((Hom.hom (𝟙 α) : (a : (↑α : Type u)) → (↑α : Type u)) a : (↑α : Type u))
⊢ CategoryStruct.comp (Y := β)
      (ofHom
        { toFun := (⇑e : (a : (↑α : Type u)) → (↑β : Type u)), map_sup' := ⋯, map_inf' := ⋯, map_bot' := ⋯,
          map_himp' := ⋯ })
      (ofHom
        { toFun := (⇑e.symm : (a : (↑β : Type u)) → (↑α : Type u)), map_sup' := ⋯, map_inf' := ⋯, map_bot' := ⋯,
          map_himp' := ⋯ }) =
    𝟙 α

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

Tactic:
e.symm_apply_apply _

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

Tactic:
exact e.symm_apply_apply _

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

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

Tactic:
e.apply_symm_apply _

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

Tactic:
exact e.apply_symm_apply _

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

Tactic:
rfl

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

Tactic:
rfl

Premises used: LatticeHom.id, rfl
-- Module: Mathlib.Order.Category.Lat
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 := carrier)
          (𝟙 X) :
        (a : (↑X : Type u_1)) → (↑X : Type u_1))
      x =
    x

Tactic:
simp
-- Module: Mathlib.Order.Category.Lat
Goal:
X Y Z : Lat
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.Lat
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 :=
            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 :=
            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 :=
                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.Lat
Goal:
X Y : Lat
f g : X ⟶ Y
hf : Hom.hom f = Hom.hom g
⊢ f = g

Tactic:
Hom.ext hf

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.Lat
Goal:
X Y Z : Type u
inst : Lattice X
inst_1 : Lattice Y
inst_2 : Lattice 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.Lat
Goal:
X Y : Type u
inst : Lattice X
inst_1 : Lattice Y
f : LatticeHom X Y
x : X
⊢ Eq (α := (↑(of Y) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : Lat.{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.Lat
Goal:
X Y : Lat
e : X ≅ Y
x : (↑X : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : Lat.{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 : Lat.{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