awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Category.PartOrd
Goal:
X : Preord
a : (↑X : Type u)
⊢ Eq (α :=
    (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
          str := instPartialOrderAntisymmetrization } :
      Type u))
    ((PartOrd.Hom.hom (PartOrd.ofHom (Preord.Hom.hom (𝟙 X)).antisymmetrization) :
          (a :
              (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
                    str := instPartialOrderAntisymmetrization } :
                Type u)) →
            (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
                  str := instPartialOrderAntisymmetrization } :
              Type u))
        (Quotient.mk'' a) :
      (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
            str := instPartialOrderAntisymmetrization } :
        Type u))
    ((PartOrd.Hom.hom
            (𝟙
              { carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
                str := instPartialOrderAntisymmetrization : PartOrd.{u} }) :
          (a :
              (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
                    str := instPartialOrderAntisymmetrization } :
                Type u)) →
            (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
                  str := instPartialOrderAntisymmetrization } :
              Type u))
        (Quotient.mk'' a) :
      (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
            str := instPartialOrderAntisymmetrization } :
        Type u))

Tactic:
Quotient.map'_mk'' _ (fun a b ↦ id) _

Premises used: id, Antisymmetrization, Quotient, Quot.map, Quotient.map', Quotient.map'_mk''
-- Module: Mathlib.Order.Category.PartOrd
Goal:
X : Preord
a : (↑X : Type u)
⊢ Eq (α :=
    (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
          str := instPartialOrderAntisymmetrization } :
      Type u))
    ((PartOrd.Hom.hom (PartOrd.ofHom (Preord.Hom.hom (𝟙 X)).antisymmetrization) :
          (a :
              (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
                    str := instPartialOrderAntisymmetrization } :
                Type u)) →
            (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
                  str := instPartialOrderAntisymmetrization } :
              Type u))
        (Quotient.mk'' a) :
      (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
            str := instPartialOrderAntisymmetrization } :
        Type u))
    ((PartOrd.Hom.hom
            (𝟙
              { carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
                str := instPartialOrderAntisymmetrization : PartOrd.{u} }) :
          (a :
              (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
                    str := instPartialOrderAntisymmetrization } :
                Type u)) →
            (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
                  str := instPartialOrderAntisymmetrization } :
              Type u))
        (Quotient.mk'' a) :
      (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
            str := instPartialOrderAntisymmetrization } :
        Type u))

Tactic:
exact Quotient.map'_mk'' _ (fun a b ↦ id) _

Premises used: id, Quotient.map'_mk''
-- Module: Mathlib.Order.Category.PartOrd
Goal:
X Y Z : Preord
f : X ⟶ Y
g : Y ⟶ Z
hf :
  ∀
    (x :
      (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
            str := instPartialOrderAntisymmetrization } :
        Type u)),
    Eq (α :=
      (↑{ carrier := Antisymmetrization (↑Z : Type u) fun (x1 x2 : (↑Z : Type u)) ↦ x1 ≤ x2,
            str := instPartialOrderAntisymmetrization } :
        Type u))
      ((PartOrd.Hom.hom (PartOrd.ofHom (Preord.Hom.hom (f ≫ g)).antisymmetrization) :
            (a :
                (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
                      str := instPartialOrderAntisymmetrization } :
                  Type u)) →
              (↑{ carrier := Antisymmetrization (↑Z : Type u) fun (x1 x2 : (↑Z : Type u)) ↦ x1 ≤ x2,
                    str := instPartialOrderAntisymmetrization } :
                Type u))
          x :
        (↑{ carrier := Antisymmetrization (↑Z : Type u) fun (x1 x2 : (↑Z : Type u)) ↦ x1 ≤ x2,
              str := instPartialOrderAntisymmetrization } :
          Type u))
      ((PartOrd.Hom.hom
              (PartOrd.ofHom (Preord.Hom.hom f).antisymmetrization ≫
                PartOrd.ofHom (Preord.Hom.hom g).antisymmetrization) :
            (a :
                (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
                      str := instPartialOrderAntisymmetrization } :
                  Type u)) →
              (↑{ carrier := Antisymmetrization (↑Z : Type u) fun (x1 x2 : (↑Z : Type u)) ↦ x1 ≤ x2,
                    str := instPartialOrderAntisymmetrization } :
                Type u))
          x :
        (↑{ carrier := Antisymmetrization (↑Z : Type u) fun (x1 x2 : (↑Z : Type u)) ↦ x1 ≤ x2,
              str := instPartialOrderAntisymmetrization } :
          Type u))
⊢ PartOrd.ofHom (Preord.Hom.hom (f ≫ g)).antisymmetrization =
    PartOrd.ofHom (Preord.Hom.hom f).antisymmetrization ≫ PartOrd.ofHom (Preord.Hom.hom g).antisymmetrization

Tactic:
ext x
-- Module: Mathlib.Order.Category.PartOrd
Goal:
X Y Z : Preord
f : X ⟶ Y
g : Y ⟶ Z
a : (↑X : Type u)
⊢ Eq (α :=
    (↑{ carrier := Antisymmetrization (↑Z : Type u) fun (x1 x2 : (↑Z : Type u)) ↦ x1 ≤ x2,
          str := instPartialOrderAntisymmetrization } :
      Type u))
    ((PartOrd.Hom.hom (PartOrd.ofHom (Preord.Hom.hom (f ≫ g)).antisymmetrization) :
          (a :
              (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
                    str := instPartialOrderAntisymmetrization } :
                Type u)) →
            (↑{ carrier := Antisymmetrization (↑Z : Type u) fun (x1 x2 : (↑Z : Type u)) ↦ x1 ≤ x2,
                  str := instPartialOrderAntisymmetrization } :
              Type u))
        (Quotient.mk'' a) :
      (↑{ carrier := Antisymmetrization (↑Z : Type u) fun (x1 x2 : (↑Z : Type u)) ↦ x1 ≤ x2,
            str := instPartialOrderAntisymmetrization } :
        Type u))
    ((PartOrd.Hom.hom
            (PartOrd.ofHom (Preord.Hom.hom f).antisymmetrization ≫
              PartOrd.ofHom (Preord.Hom.hom g).antisymmetrization) :
          (a :
              (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
                    str := instPartialOrderAntisymmetrization } :
                Type u)) →
            (↑{ carrier := Antisymmetrization (↑Z : Type u) fun (x1 x2 : (↑Z : Type u)) ↦ x1 ≤ x2,
                  str := instPartialOrderAntisymmetrization } :
              Type u))
        (Quotient.mk'' a) :
      (↑{ carrier := Antisymmetrization (↑Z : Type u) fun (x1 x2 : (↑Z : Type u)) ↦ x1 ≤ x2,
            str := instPartialOrderAntisymmetrization } :
        Type u))

Tactic:
OrderHom.antisymmetrization_apply_mk ..

Premises used: Antisymmetrization, Quotient, OrderHom.antisymmetrization_apply_mk, Quot.map, Quotient.map', toAntisymmetrization
-- Module: Mathlib.Order.Category.PartOrd
Goal:
X Y Z : Preord
f : X ⟶ Y
g : Y ⟶ Z
a : (↑X : Type u)
⊢ Eq (α :=
    (↑{ carrier := Antisymmetrization (↑Z : Type u) fun (x1 x2 : (↑Z : Type u)) ↦ x1 ≤ x2,
          str := instPartialOrderAntisymmetrization } :
      Type u))
    ((PartOrd.Hom.hom (PartOrd.ofHom (Preord.Hom.hom (f ≫ g)).antisymmetrization) :
          (a :
              (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
                    str := instPartialOrderAntisymmetrization } :
                Type u)) →
            (↑{ carrier := Antisymmetrization (↑Z : Type u) fun (x1 x2 : (↑Z : Type u)) ↦ x1 ≤ x2,
                  str := instPartialOrderAntisymmetrization } :
              Type u))
        (Quotient.mk'' a) :
      (↑{ carrier := Antisymmetrization (↑Z : Type u) fun (x1 x2 : (↑Z : Type u)) ↦ x1 ≤ x2,
            str := instPartialOrderAntisymmetrization } :
        Type u))
    ((PartOrd.Hom.hom
            (PartOrd.ofHom (Preord.Hom.hom f).antisymmetrization ≫
              PartOrd.ofHom (Preord.Hom.hom g).antisymmetrization) :
          (a :
              (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
                    str := instPartialOrderAntisymmetrization } :
                Type u)) →
            (↑{ carrier := Antisymmetrization (↑Z : Type u) fun (x1 x2 : (↑Z : Type u)) ↦ x1 ≤ x2,
                  str := instPartialOrderAntisymmetrization } :
              Type u))
        (Quotient.mk'' a) :
      (↑{ carrier := Antisymmetrization (↑Z : Type u) fun (x1 x2 : (↑Z : Type u)) ↦ x1 ≤ x2,
            str := instPartialOrderAntisymmetrization } :
        Type u))

Tactic:
exact OrderHom.antisymmetrization_apply_mk ..

Premises used: OrderHom.antisymmetrization_apply_mk
-- Module: Mathlib.Order.Category.PartOrd
Goal:
X : Preord
a : (↑(preordToPartOrd.obj (Preord.dual.obj X)) : Type u_1)
⊢ Eq (α := (↑(PartOrd.dual.obj (preordToPartOrd.obj X)) : Type u_1))
    ((PartOrd.Hom.hom (preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd.inv.app X) :
          (a : (↑(preordToPartOrd.obj (Preord.dual.obj X)) : Type u_1)) →
            (↑(PartOrd.dual.obj (preordToPartOrd.obj X)) : Type u_1))
        a :
      (↑(PartOrd.dual.obj (preordToPartOrd.obj X)) : Type u_1))
    ((OrderIso.symm (OrderIso.dualAntisymmetrization (↑X : Type u_1)) :
          (a : Antisymmetrization (↑X : Type u_1)ᵒᵈ fun (x1 x2 : (↑X : Type u_1)ᵒᵈ) ↦ x1 ≤ x2) →
            (Antisymmetrization (↑X : Type u_1) fun (x1 x2 : (↑X : Type u_1)) ↦ x1 ≤ x2)ᵒᵈ)
        a :
      (Antisymmetrization (↑X : Type u_1) fun (x1 x2 : (↑X : Type u_1)) ↦ x1 ≤ x2)ᵒᵈ)

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.PartOrdEmb
Goal:
X : PartOrdEmb
⊢ Hom.hom (𝟙 X) = RelEmbedding.refl fun (x1 x2 : (↑X : Type u_1)) ↦ x1 ≤ x2

Tactic:
rfl

Premises used: RelEmbedding.refl, rfl
-- Module: Mathlib.Order.Category.PartOrdEmb
Goal:
X : PartOrdEmb
x : (↑X : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{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.PartOrdEmb
Goal:
X Y Z : PartOrdEmb
f : X ⟶ Y
g : Y ⟶ Z
⊢ Hom.hom (f ≫ g) =
    RelEmbedding.trans (r := fun (x1 x2 : (↑X : Type u_1)) ↦ x1 ≤ x2) (s := fun (x1 x2 : (↑Y : Type u_1)) ↦ x1 ≤ x2)
      (t := fun (x1 x2 : (↑Z : Type u_1)) ↦ x1 ≤ x2) (Hom.hom f) (Hom.hom g)

Tactic:
rfl

Premises used: RelEmbedding.trans, rfl
-- Module: Mathlib.Order.Category.PartOrdEmb
Goal:
X Y Z : PartOrdEmb
f : X ⟶ Y
g : Y ⟶ Z
x : (↑X : Type u_1)
⊢ Eq (α := (↑Z : Type u_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{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 : PartOrdEmb.{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 : PartOrdEmb.{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.PartOrdEmb
Goal:
X Y : PartOrdEmb
f : X ⟶ Y
⊢ Function.Injective (α := (↑X : Type u)) (β := (↑Y : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier) f) :
      (a : (↑X : Type u)) → (↑Y : Type u))

Tactic:
f.hom'.injective

Premises used: RelEmbedding.injective, PartOrdEmb.Hom.hom'
-- Module: Mathlib.Order.Category.PartOrdEmb
Goal:
X Y : PartOrdEmb
f : X ⟶ Y
x₁ x₂ : (↑X : Type u)
⊢ LE.le (α := (↑Y : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier) f :
            (a : (↑X : Type u)) → (↑Y : Type u))
          x₁ :
        (↑Y : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier) f :
            (a : (↑X : Type u)) → (↑Y : Type u))
          x₂ :
        (↑Y : Type u)) ↔
    x₁ ≤ x₂

Tactic:
f.hom'.le_iff_le

Premises used: PartOrdEmb.Hom.hom', OrderEmbedding.le_iff_le
-- Module: Mathlib.Order.Category.PartOrdEmb
Goal:
X Y : PartOrdEmb
f g : X ⟶ Y
hf : Hom.hom f = Hom.hom g
⊢ f = g

Tactic:
Hom.ext hf

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

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.PartOrdEmb
Goal:
X : Type u
inst : PartialOrder X
⊢ ofHom (RelEmbedding.refl fun (x1 x2 : X) ↦ x1 ≤ x2) = 𝟙 { carrier := X, str := inst : PartOrdEmb.{u} }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.PartOrdEmb
Goal:
X Y Z : Type u
inst : PartialOrder X
inst_1 : PartialOrder Y
inst_2 : PartialOrder Z
f : X ↪o Y
g : Y ↪o Z
⊢ ofHom
      (RelEmbedding.trans (r := fun (x1 x2 : X) ↦ x1 ≤ x2) (s := fun (x1 x2 : Y) ↦ x1 ≤ x2) (t := fun (x1 x2 : Z) ↦
        x1 ≤ x2) f g) =
    ofHom f ≫ ofHom g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.PartOrdEmb
Goal:
X Y : Type u
inst : PartialOrder X
inst_1 : PartialOrder Y
f : X ↪o Y
x : X
⊢ Eq (α := (↑{ carrier := Y, str := inst_1 } : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{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.PartOrdEmb
Goal:
X Y : PartOrdEmb
e : X ≅ Y
x : (↑X : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{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 : PartOrdEmb.{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.PartOrdEmb
Goal:
X Y : PartOrdEmb
e : X ≅ Y
s : (↑Y : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{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 : PartOrdEmb.{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.PartOrdEmb
Goal:
⊢ PartOrdEmb.dual ⋙
      forget₂ PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u_1}) ↦ (↑x1 : Type u_1) ↪o (↑x2 : Type u_1)) (CC :=
        PartOrdEmb.carrier) PartOrd (FD := fun (x1 x2 : PartOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CD :=
        PartOrd.carrier) =
    forget₂ PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u_1}) ↦ (↑x1 : Type u_1) ↪o (↑x2 : Type u_1)) (CC :=
        PartOrdEmb.carrier) 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: PartOrdEmb.dual, CategoryTheory.Functor.comp, OrderHomClass.toOrderHom, OrderDual, 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
x : CoconePt hc
obtain :
  ∀ (j : J)
    (x' :
      (F ⋙
            forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
              carrier)).obj
        j)
    (hx :
      (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' =
        x),
    ∃ (j : J) (x' : (↑(F.obj j) : Type u)) (y' : (↑(F.obj j) : 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' =
        x)
      (_ :
      (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))
          y' =
        x),
      x' ≤ y'
⊢ ∃ (j : J) (x' : (↑(F.obj j) : Type u)) (y' : (↑(F.obj j) : 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' =
      x)
    (_ :
    (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))
        y' =
      x),
    x' ≤ y'

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

Premises used: CategoryTheory.Limits.Types.jointly_surjective_of_isColimit
-- 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
x : CoconePt hc
j : J
x' :
  (F ⋙ forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)).obj j
hx :
  (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' =
    x
⊢ ∃ (j : J) (x' : (↑(F.obj j) : Type u)) (y' : (↑(F.obj j) : 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' =
      x)
    (_ :
    (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))
        y' =
      x),
    x' ≤ y'

Tactic:
⟨j, x', x', hx, hx, le_rfl⟩

Premises used: le_rfl, Exists.intro
-- 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
x : CoconePt hc
j : J
x' :
  (F ⋙ forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)).obj j
hx :
  (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' =
    x
⊢ ∃ (j : J) (x' : (↑(F.obj j) : Type u)) (y' : (↑(F.obj j) : 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' =
      x)
    (_ :
    (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))
        y' =
      x),
    x' ≤ y'

Tactic:
exact ⟨j, x', x', hx, hx, le_rfl⟩