awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Category.PartOrdEmb
Goal:
J : Type u
inst : SmallCategory J
inst_1 : IsFiltered J
F : J ⥤ PartOrdEmb
c :
  Cocone (F ⋙ forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier))
hc : IsColimit c
s : Cocone F
j : J
x' y' :
  (F ⋙ forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)).obj j
⊢ Eq (α :=
    Cocone.pt (F :=
      F ⋙ forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier))
      (Functor.mapCocone
        (forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)) s))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (c.ι.app j ≫
              hc.desc
                (Functor.mapCocone
                  (forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                    carrier))
                  s)) :
          (a : (F ⋙ forget PartOrdEmb).obj j) → ((forget PartOrdEmb).mapCocone s).pt)
        x' :
      Cocone.pt (F :=
        F ⋙ forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier))
        (Functor.mapCocone
          (forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier))
          s))
    (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (NatTrans.app
                (Cocone.ι
                  (Functor.mapCocone
                    (forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                      carrier))
                    s))
                j) :
            TypeCat.Fun
              ((F ⋙
                    forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                      carrier)).obj
                j)
              (Cocone.pt (F :=
                F ⋙
                  forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                    carrier))
                (Functor.mapCocone
                  (forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                    carrier))
                  s))) :
          (a : (F ⋙ forget PartOrdEmb).obj j) → ((forget PartOrdEmb).mapCocone s).pt)
        x' :
      Cocone.pt (F :=
        F ⋙ forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier))
        (Functor.mapCocone
          (forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier))
          s))

Tactic:
have hx := ConcreteCategory.congr_hom (hc.fac ((forget _).mapCocone s) j) x'
-- Module: Mathlib.Order.Category.PartOrdEmb
Goal:
J : Type u
inst : SmallCategory J
inst_1 : IsFiltered J
F : J ⥤ PartOrdEmb
c :
  Cocone (F ⋙ forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier))
hc : IsColimit c
s : Cocone F
j : J
x' y' :
  (F ⋙ forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)).obj j
hx :
  Eq (α := ToType (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier) s.pt)
    (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (hc.desc
                (Functor.mapCocone
                  (forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                    carrier))
                  s)) :
            TypeCat.Fun c.pt
              (ToType (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier) s.pt)) :
          (a : c.pt) → ToType s.pt)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j) : (a : ToType (F.obj j)) → c.pt) x' : c.pt) :
      ToType (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier) s.pt)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
            (s.ι.app j) :
          (a : (↑(F.obj j) : Type u)) → (↑s.pt : Type u))
        x' :
      (↑s.pt : Type u))
hy :
  Eq (α := ToType (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier) s.pt)
    (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (hc.desc
                (Functor.mapCocone
                  (forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                    carrier))
                  s)) :
            TypeCat.Fun c.pt
              (ToType (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier) s.pt)) :
          (a : c.pt) → ToType s.pt)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j) : (a : ToType (F.obj j)) → c.pt) y' : c.pt) :
      ToType (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier) s.pt)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
            (s.ι.app j) :
          (a : (↑(F.obj j) : Type u)) → (↑s.pt : Type u))
        y' :
      (↑s.pt : Type u))
⊢ x' ≤ y' ↔
    LE.le (α := CoconePt hc)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j) : (a : ToType (F.obj j)) → c.pt) x' : c.pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j) : (a : ToType (F.obj j)) → c.pt) y' : c.pt)

Tactic:
⟨fun h ↦ ⟨j, _, _, rfl, rfl, h⟩, fun ⟨k, x, y, hx', hy', h⟩ ↦ ?_⟩

Premises used: LE.le, _private.0.PartOrdEmb.Limits.CoconePt.desc.match_1, Iff.intro, Exists.intro, rfl
-- Module: Mathlib.Order.Category.PartOrdEmb
Goal:
J : Type u
inst : SmallCategory J
inst_1 : IsFiltered J
F : J ⥤ PartOrdEmb
c :
  Cocone (F ⋙ forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier))
hc : IsColimit c
s : Cocone F
j : J
x : (↑(F.obj j) : Type u)
⊢ Eq (α := (↑s.pt : Type u))
    ((desc hc s : (a : CoconePt hc) → (↑s.pt : Type u))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j) : (a : ToType (F.obj j)) → c.pt) x : c.pt) :
      (↑s.pt : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
            (s.ι.app j) :
          (a : (↑(F.obj j) : Type u)) → (↑s.pt : Type u))
        x :
      (↑s.pt : Type u))

Tactic:
ConcreteCategory.congr_hom (hc.fac ((forget _).mapCocone s) j) x

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Functor.mapCocone, CategoryTheory.forget, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.Order.Category.PartOrdEmb
Goal:
J : Type u
inst : SmallCategory J
inst_1 : IsFiltered J
F : J ⥤ PartOrdEmb
c :
  Cocone (F ⋙ forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier))
hc : IsColimit c
s : Cocone F
j : J
hf :
  ∀ (x : (↑(F.obj j) : Type u)),
    Eq (α := (↑s.pt : Type u))
      ((Hom.hom ((cocone hc).ι.app j ≫ ofHom (CoconePt.desc hc s)) : (a : (↑(F.obj j) : Type u)) → (↑s.pt : Type u)) x :
        (↑s.pt : Type u))
      ((Hom.hom (s.ι.app j) : (a : (↑(F.obj j) : Type u)) → (↑s.pt : Type u)) x : (↑s.pt : Type u))
⊢ (cocone hc).ι.app j ≫ ofHom (CoconePt.desc hc s) = s.ι.app j

Tactic:
ext x
-- Module: Mathlib.Order.Category.PartOrdEmb
Goal:
J : Type u
inst : SmallCategory J
inst_1 : IsFiltered J
F : J ⥤ PartOrdEmb
c :
  Cocone (F ⋙ forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier))
hc : IsColimit c
s : Cocone F
j : J
x : (↑(F.obj j) : Type u)
⊢ Eq (α := (↑s.pt : Type u))
    ((Hom.hom ((cocone hc).ι.app j ≫ ofHom (CoconePt.desc hc s)) : (a : (↑(F.obj j) : Type u)) → (↑s.pt : Type u)) x :
      (↑s.pt : Type u))
    ((Hom.hom (s.ι.app j) : (a : (↑(F.obj j) : Type u)) → (↑s.pt : Type u)) x : (↑s.pt : Type u))

Tactic:
ConcreteCategory.congr_hom (hc.fac ((forget _).mapCocone s) j) x

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Functor.mapCocone, CategoryTheory.forget, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.Order.Category.PartOrdEmb
Goal:
J : Type u
inst : SmallCategory J
inst_1 : IsFiltered J
F : J ⥤ PartOrdEmb
c :
  Cocone (F ⋙ forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier))
hc : IsColimit c
s : Cocone F
j : J
x : (↑(F.obj j) : Type u)
⊢ Eq (α := (↑s.pt : Type u))
    ((Hom.hom ((cocone hc).ι.app j ≫ ofHom (CoconePt.desc hc s)) : (a : (↑(F.obj j) : Type u)) → (↑s.pt : Type u)) x :
      (↑s.pt : Type u))
    ((Hom.hom (s.ι.app j) : (a : (↑(F.obj j) : Type u)) → (↑s.pt : Type u)) x : (↑s.pt : Type u))

Tactic:
exact ConcreteCategory.congr_hom (hc.fac ((forget _).mapCocone s) j) x

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Functor.mapCocone, CategoryTheory.forget, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.Order.Category.PartOrdEmb
Goal:
J : Type u
inst : SmallCategory J
inst_1 : IsFiltered J
F : J ⥤ PartOrdEmb
c :
  Cocone (F ⋙ forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier))
hc : IsColimit c
s : Cocone F
m : (cocone hc).pt ⟶ s.pt
hm : ∀ (j : J), (cocone hc).ι.app j ≫ m = s.ι.app j
hf :
  ∀ (x : (↑(cocone hc).pt : Type u)),
    Eq (α := (↑s.pt : Type u)) ((Hom.hom m : (a : (↑(cocone hc).pt : Type u)) → (↑s.pt : Type u)) x : (↑s.pt : Type u))
      ((Hom.hom (ofHom (CoconePt.desc hc s)) : (a : (↑(cocone hc).pt : Type u)) → (↑s.pt : Type u)) x :
        (↑s.pt : Type u))
⊢ m = ofHom (CoconePt.desc hc s)

Tactic:
ext x
-- Module: Mathlib.Order.Category.PartOrdEmb
Goal:
J : Type u
inst : SmallCategory J
inst_1 : IsFiltered J
F : J ⥤ PartOrdEmb
c :
  Cocone (F ⋙ forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier))
hc : IsColimit c
s : Cocone F
m : (cocone hc).pt ⟶ s.pt
hm : ∀ (j : J), (cocone hc).ι.app j ≫ m = s.ι.app j
x : (↑(cocone hc).pt : Type u)
hf :
  ∀ (j : J)
    (x :
      (F ⋙
            forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
              carrier)).obj
        j),
    Eq (α := (↑s.pt : Type u))
      ((Hom.hom m : (a : (↑(cocone hc).pt : Type u)) → (↑s.pt : Type u))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j) :
                (a : (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj j)) →
                  (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj j))
              x :
            (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) j)) :
        (↑s.pt : Type u))
      ((Hom.hom (ofHom (CoconePt.desc hc s)) : (a : (↑(cocone hc).pt : Type u)) → (↑s.pt : Type u))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j) :
                (a : (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj j)) →
                  (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj j))
              x :
            (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) j)) :
        (↑s.pt : Type u))
⊢ Eq (α := (↑s.pt : Type u)) ((Hom.hom m : (a : (↑(cocone hc).pt : Type u)) → (↑s.pt : Type u)) x : (↑s.pt : Type u))
    ((Hom.hom (ofHom (CoconePt.desc hc s)) : (a : (↑(cocone hc).pt : Type u)) → (↑s.pt : Type u)) x : (↑s.pt : Type u))

Tactic:
obtain ⟨j, x, rfl⟩ := Types.jointly_surjective_of_isColimit hc x

Premises used: CategoryTheory.Limits.Types.jointly_surjective_of_isColimit, rfl
-- Module: Mathlib.Order.Category.PartOrdEmb
Goal:
J : Type u
inst : SmallCategory J
inst_1 : IsFiltered J
F : J ⥤ PartOrdEmb
c :
  Cocone (F ⋙ forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier))
hc : IsColimit c
s : Cocone F
m : (cocone hc).pt ⟶ s.pt
hm : ∀ (j : J), (cocone hc).ι.app j ≫ m = s.ι.app j
j : J
x :
  (F ⋙ forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)).obj j
⊢ Eq (α := (↑s.pt : Type u))
    ((Hom.hom m : (a : (↑(cocone hc).pt : Type u)) → (↑s.pt : Type u))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j) :
              (a : (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj j)) →
                (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj j))
            x :
          (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) j)) :
      (↑s.pt : Type u))
    ((Hom.hom (ofHom (CoconePt.desc hc s)) : (a : (↑(cocone hc).pt : Type u)) → (↑s.pt : Type u))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j) :
              (a : (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj j)) →
                (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj j))
            x :
          (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) j)) :
      (↑s.pt : Type u))

Tactic:
((ConcreteCategory.congr_hom (hm j)) x).trans (CoconePt.fac_apply hc s j x).symm

Premises used: PartOrdEmb.Limits.CoconePt.fac_apply, CategoryTheory.ConcreteCategory.congr_hom, Eq.symm, Eq.trans
-- Module: Mathlib.Order.Category.PartOrdEmb
Goal:
J : Type u
inst : SmallCategory J
inst_1 : IsFiltered J
F : J ⥤ PartOrdEmb
c :
  Cocone (F ⋙ forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier))
hc : IsColimit c
s : Cocone F
m : (cocone hc).pt ⟶ s.pt
hm : ∀ (j : J), (cocone hc).ι.app j ≫ m = s.ι.app j
j : J
x :
  (F ⋙ forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)).obj j
⊢ Eq (α := (↑s.pt : Type u))
    ((Hom.hom m : (a : (↑(cocone hc).pt : Type u)) → (↑s.pt : Type u))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j) :
              (a : (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj j)) →
                (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj j))
            x :
          (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) j)) :
      (↑s.pt : Type u))
    ((Hom.hom (ofHom (CoconePt.desc hc s)) : (a : (↑(cocone hc).pt : Type u)) → (↑s.pt : Type u))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j) :
              (a : (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj j)) →
                (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj j))
            x :
          (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) j)) :
      (↑s.pt : Type u))

Tactic:
exact ((ConcreteCategory.congr_hom (hm j)) x).trans (CoconePt.fac_apply hc s j x).symm

Premises used: PartOrdEmb.Limits.CoconePt.fac_apply, CategoryTheory.ConcreteCategory.congr_hom, Eq.symm, Eq.trans
-- Module: Mathlib.Order.Category.Preord
Goal:
X : Preord
⊢ Eq (α := (a : (↑X : Type u_1)) → (↑X : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : Preord.{u_1}) ↦ (↑x1 : Type u_1) →o (↑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.Preord
Goal:
X Y Z : Preord
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := (a : (↑X : Type u_1)) → (↑Z : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : Preord.{u_1}) ↦ (↑x1 : Type u_1) →o (↑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 : Preord.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CC := carrier)
            g) :
        (a : (↑Y : Type u_1)) → (↑Z : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : Preord.{u_1}) ↦ (↑x1 : Type u_1) →o (↑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.Preord
Goal:
X Y : Preord
f g : X ⟶ Y
w :
  ∀ (x : (↑X : Type u_1)),
    Eq (α := (↑Y : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : Preord.{u_1}) ↦ (↑x1 : Type u_1) →o (↑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 : Preord.{u_1}) ↦ (↑x1 : Type u_1) →o (↑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.Preord
Goal:
X : Type u
inst : Preorder X
⊢ (↑{ carrier := X, str := inst : Preord.{u} } : Type u) = X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.Preord
Goal:
X : Preord
⊢ Hom.hom (𝟙 X) = OrderHom.id

Tactic:
rfl

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

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

Tactic:
rfl

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

Tactic:
Hom.ext hf

Premises used: Preord.Hom.ext
-- Module: Mathlib.Order.Category.Preord
Goal:
X Y : Type u
inst : Preorder X
inst_1 : Preorder Y
f : X →o Y
⊢ Hom.hom (ofHom f) = f

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.Preord
Goal:
X : Type u
inst : Preorder X
⊢ ofHom OrderHom.id = 𝟙 { carrier := X, str := inst : Preord.{u} }

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.Preord
Goal:
X Y : Type u
inst : Preorder X
inst_1 : Preorder Y
f : X →o Y
x : X
⊢ Eq (α := (↑{ carrier := Y, str := inst_1 } : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : Preord.{u}) ↦ (↑x1 : Type u) →o (↑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.Preord
Goal:
X Y : Preord
e : X ≅ Y
x : (↑X : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : Preord.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CC := carrier)
          e.inv :
        (a : (↑Y : Type u_1)) → (↑X : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : Preord.{u_1}) ↦ (↑x1 : Type u_1) →o (↑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.Preord
Goal:
X Y : Preord
e : X ≅ Y
s : (↑Y : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : Preord.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CC := carrier)
          e.hom :
        (a : (↑X : Type u_1)) → (↑Y : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : Preord.{u_1}) ↦ (↑x1 : Type u_1) →o (↑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.Preord
Goal:
X Y : Preord
a₁ a₂ : X ⟶ Y
h : preordToCat.map a₁ = preordToCat.map a₂
hf :
  ∀ (x : (↑X : Type u)),
    Eq (α := (↑Y : Type u)) ((Preord.Hom.hom a₁ : (a : (↑X : Type u)) → (↑Y : Type u)) x : (↑Y : Type u))
      ((Preord.Hom.hom a₂ : (a : (↑X : Type u)) → (↑Y : Type u)) x : (↑Y : Type u))
⊢ a₁ = a₂

Tactic:
ext x
-- Module: Mathlib.Order.Category.Preord
Goal:
X Y : Preord
a₁ a₂ : X ⟶ Y
h : preordToCat.map a₁ = preordToCat.map a₂
x : (↑X : Type u)
⊢ Eq (α := (↑Y : Type u)) ((Preord.Hom.hom a₁ : (a : (↑X : Type u)) → (↑Y : Type u)) x : (↑Y : Type u))
    ((Preord.Hom.hom a₂ : (a : (↑X : Type u)) → (↑Y : Type u)) x : (↑Y : Type u))

Tactic:
Functor.congr_obj congr(($h).toFunctor) x

Premises used: congrArg, CategoryTheory.Functor.congr_obj, id, CategoryTheory.Cat.Hom.toFunctor
-- Module: Mathlib.Order.Category.Preord
Goal:
X Y : Preord
a₁ a₂ : X ⟶ Y
h : preordToCat.map a₁ = preordToCat.map a₂
x : (↑X : Type u)
⊢ Eq (α := (↑Y : Type u)) ((Preord.Hom.hom a₁ : (a : (↑X : Type u)) → (↑Y : Type u)) x : (↑Y : Type u))
    ((Preord.Hom.hom a₂ : (a : (↑X : Type u)) → (↑Y : Type u)) x : (↑Y : Type u))

Tactic:
exact Functor.congr_obj congr(($h).toFunctor) x

Premises used: congrArg, CategoryTheory.Functor.congr_obj, id, CategoryTheory.Cat.Hom.toFunctor
-- Module: Mathlib.Order.Category.Semilat
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : OrderBot α
⊢ { X := α, isSemilatticeSup := inst, isOrderBot := inst_1 : SemilatSupCat.{u_1} }.X = α

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.Semilat
Goal:
X : SemilatSupCat
⊢ (↑(Functor.obj
          (forget₂ SemilatSupCat (FC := fun (x1 x2 : SemilatSupCat.{u_1}) ↦ SupBotHom x1.X x2.X) (CC := SemilatSupCat.X)
            PartOrd (FD := fun (x1 x2 : PartOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CD := PartOrd.carrier))
          X) :
      Type u_1) =
    X.X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.Semilat
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderTop α
⊢ { X := α, isSemilatticeInf := inst, isOrderTop := inst_1 : SemilatInfCat.{u_1} }.X = α

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.Semilat
Goal:
X : SemilatInfCat
⊢ (↑(Functor.obj
          (forget₂ SemilatInfCat (FC := fun (x1 x2 : SemilatInfCat.{u_1}) ↦ InfTopHom x1.X x2.X) (CC := SemilatInfCat.X)
            PartOrd (FD := fun (x1 x2 : PartOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CD := PartOrd.carrier))
          X) :
      Type u_1) =
    X.X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.Semilat
Goal:
α β : SemilatSupCat
e : α.X ≃o β.X
h :
  ∀ (a : α.X),
    Eq (α := α.X)
      ((@ConcreteCategory.hom _ instLargeCategory (fun (x1 x2 : SemilatSupCat.{u}) ↦ SupBotHom x1.X x2.X)
              SemilatSupCat.X _ _ α α
              (CategoryStruct.comp (Y := β) { toFun := (⇑e : (a : α.X) → β.X), map_sup' := ⋯, map_bot' := ⋯ }
                { toFun := (⇑e.symm : (a : β.X) → α.X), map_sup' := ⋯, map_bot' := ⋯ }) :
            (a : α.X) → α.X)
          a :
        α.X)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : SemilatSupCat.{u}) ↦ SupBotHom x1.X x2.X) (CC := SemilatSupCat.X)
              (𝟙 α) :
            (a : α.X) → α.X)
          a :
        α.X)
⊢ CategoryStruct.comp (Y := β) { toFun := (⇑e : (a : α.X) → β.X), map_sup' := ⋯, map_bot' := ⋯ }
      { toFun := (⇑e.symm : (a : β.X) → α.X), map_sup' := ⋯, map_bot' := ⋯ } =
    𝟙 α

Tactic:
ext