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
j : J
x y : (↑(F.1 j) : Type u)
refine :
  LE.le (α := CoconePt hc)
      (({
              toFun :=
                (⇑(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)),
              inj' := ⋯ } :
            (a : (↑(F.1 j) : Type u)) → CoconePt hc)
          x :
        CoconePt hc)
      (({
              toFun :=
                (⇑(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)),
              inj' := ⋯ } :
            (a : (↑(F.1 j) : Type u)) → CoconePt hc)
          y :
        CoconePt hc) →
    x ≤ y
⊢ LE.le (α := CoconePt hc)
      (({
              toFun :=
                (⇑(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)),
              inj' := ⋯ } :
            (a : (↑(F.1 j) : Type u)) → CoconePt hc)
          x :
        CoconePt hc)
      (({
              toFun :=
                (⇑(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)),
              inj' := ⋯ } :
            (a : (↑(F.1 j) : Type u)) → CoconePt hc)
          y :
        CoconePt hc) ↔
    x ≤ y

Tactic:
refine ⟨?_, fun h ↦ ⟨j, x, y, rfl, rfl, h⟩⟩
-- 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
j : J
x y : (↑(F.1 j) : Type u)
k : J
x' y' : (↑(F.obj k) : Type u)
hx :
  Eq (α := c.pt) ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app k) : (a : ToType (F.obj k)) → c.pt) x' : c.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j) : (a : ToType (F.obj j)) → c.pt) x : c.pt)
hy :
  Eq (α := c.pt) ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app k) : (a : ToType (F.obj k)) → c.pt) y' : c.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j) : (a : ToType (F.obj j)) → c.pt) y : c.pt)
h : x' ≤ y'
l₁ : J
a₁ : k ⟶ l₁
b₁ : j ⟶ l₁
hl₁ :
  Eq (α := ToType (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier) (F.obj l₁))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
            (F.map a₁) :
          (a : (↑(F.obj k) : Type u)) → (↑(F.obj l₁) : Type u))
        x' :
      (↑(F.obj l₁) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
            (F.map b₁) :
          (a : (↑(F.obj j) : Type u)) → (↑(F.obj l₁) : Type u))
        x :
      (↑(F.obj l₁) : Type u))
l₂ : J
a₂ : k ⟶ l₂
b₂ : j ⟶ l₂
hl₂ :
  Eq (α := ToType (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier) (F.obj l₂))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
            (F.map a₂) :
          (a : (↑(F.obj k) : Type u)) → (↑(F.obj l₂) : Type u))
        y' :
      (↑(F.obj l₂) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
            (F.map b₂) :
          (a : (↑(F.obj j) : Type u)) → (↑(F.obj l₂) : Type u))
        y :
      (↑(F.obj l₂) : Type u))
obtain : ∀ (m : J) (d : l₁ ⟶ m) (d' : l₂ ⟶ m) (h₁ : a₁ ≫ d = a₂ ≫ d') (h₂ : b₁ ≫ d = b₂ ≫ d'), x ≤ y
⊢ x ≤ y

Tactic:
obtain ⟨m, d, d', h₁, h₂⟩ := bowtie a₁ a₂ b₁ b₂

Premises used: CategoryTheory.IsFiltered.bowtie
-- 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
j : J
x y : (↑(F.1 j) : Type u)
k : J
x' y' : (↑(F.obj k) : Type u)
hx :
  Eq (α := c.pt) ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app k) : (a : ToType (F.obj k)) → c.pt) x' : c.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j) : (a : ToType (F.obj j)) → c.pt) x : c.pt)
hy :
  Eq (α := c.pt) ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app k) : (a : ToType (F.obj k)) → c.pt) y' : c.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j) : (a : ToType (F.obj j)) → c.pt) y : c.pt)
h : x' ≤ y'
l₁ : J
a₁ : k ⟶ l₁
b₁ : j ⟶ l₁
hl₁ :
  Eq (α := ToType (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier) (F.obj l₁))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
            (F.map a₁) :
          (a : (↑(F.obj k) : Type u)) → (↑(F.obj l₁) : Type u))
        x' :
      (↑(F.obj l₁) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
            (F.map b₁) :
          (a : (↑(F.obj j) : Type u)) → (↑(F.obj l₁) : Type u))
        x :
      (↑(F.obj l₁) : Type u))
l₂ : J
a₂ : k ⟶ l₂
b₂ : j ⟶ l₂
hl₂ :
  Eq (α := ToType (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier) (F.obj l₂))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
            (F.map a₂) :
          (a : (↑(F.obj k) : Type u)) → (↑(F.obj l₂) : Type u))
        y' :
      (↑(F.obj l₂) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
            (F.map b₂) :
          (a : (↑(F.obj j) : Type u)) → (↑(F.obj l₂) : Type u))
        y :
      (↑(F.obj l₂) : Type u))
m : J
d : l₁ ⟶ m
d' : l₂ ⟶ m
h₁ : a₁ ≫ d = a₂ ≫ d'
h₂ : b₁ ≫ d = b₂ ≫ d'
rw :
  ∀
    (h :
      LE.le (α := (↑(F.obj m) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
                (F.map (a₁ ≫ d)) :
              (a : (↑(F.obj k) : Type u)) → (↑(F.obj m) : Type u))
            x' :
          (↑(F.obj m) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
                (F.map (a₁ ≫ d)) :
              (a : (↑(F.obj k) : Type u)) → (↑(F.obj m) : Type u))
            y' :
          (↑(F.obj m) : Type u)))
    (d' : l₂ ⟶ m) (h₁ : a₁ ≫ d = a₂ ≫ d') (h₂ : b₁ ≫ d = b₂ ≫ d'), x ≤ y
⊢ x ≤ y

Tactic:
rw [← (F.map (a₁ ≫ d)).le_iff_le] at h

Premises used: CategoryTheory.Functor.map, PartOrdEmb.Hom.le_iff_le, CategoryTheory.CategoryStruct.comp
-- 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
j : J
x y : (↑(F.1 j) : Type u)
k : J
x' y' : (↑(F.obj k) : Type u)
hx :
  Eq (α := c.pt) ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app k) : (a : ToType (F.obj k)) → c.pt) x' : c.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j) : (a : ToType (F.obj j)) → c.pt) x : c.pt)
hy :
  Eq (α := c.pt) ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app k) : (a : ToType (F.obj k)) → c.pt) y' : c.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j) : (a : ToType (F.obj j)) → c.pt) y : c.pt)
l₁ : J
a₁ : k ⟶ l₁
b₁ : j ⟶ l₁
hl₁ :
  Eq (α := ToType (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier) (F.obj l₁))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
            (F.map a₁) :
          (a : (↑(F.obj k) : Type u)) → (↑(F.obj l₁) : Type u))
        x' :
      (↑(F.obj l₁) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
            (F.map b₁) :
          (a : (↑(F.obj j) : Type u)) → (↑(F.obj l₁) : Type u))
        x :
      (↑(F.obj l₁) : Type u))
l₂ : J
a₂ : k ⟶ l₂
b₂ : j ⟶ l₂
hl₂ :
  Eq (α := ToType (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier) (F.obj l₂))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
            (F.map a₂) :
          (a : (↑(F.obj k) : Type u)) → (↑(F.obj l₂) : Type u))
        y' :
      (↑(F.obj l₂) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
            (F.map b₂) :
          (a : (↑(F.obj j) : Type u)) → (↑(F.obj l₂) : Type u))
        y :
      (↑(F.obj l₂) : Type u))
m : J
d : l₁ ⟶ m
h :
  LE.le (α := (↑(F.obj m) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
            (F.map (a₁ ≫ d)) :
          (a : (↑(F.obj k) : Type u)) → (↑(F.obj m) : Type u))
        x' :
      (↑(F.obj m) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
            (F.map (a₁ ≫ d)) :
          (a : (↑(F.obj k) : Type u)) → (↑(F.obj m) : Type u))
        y' :
      (↑(F.obj m) : Type u))
d' : l₂ ⟶ m
h₁ : a₁ ≫ d = a₂ ≫ d'
h₂ : b₁ ≫ d = b₂ ≫ d'
rw :
  ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
          (F.map (b₂ ≫ d')) :
        (a : (↑(F.obj j) : Type u)) → (↑(F.obj m) : Type u))
      y :
    (↑(F.obj m) : Type u))
| ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
          (F.map (b₁ ≫ d)) :
        (a : (↑(F.obj j) : Type u)) → (↑(F.obj m) : Type u))
      y :
    (↑(F.obj m) : Type u))

Tactic:
rw [h₂]
-- 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
j : J
x y : (↑(F.1 j) : Type u)
k : J
x' y' : (↑(F.obj k) : Type u)
hx :
  Eq (α := c.pt) ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app k) : (a : ToType (F.obj k)) → c.pt) x' : c.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j) : (a : ToType (F.obj j)) → c.pt) x : c.pt)
hy :
  Eq (α := c.pt) ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app k) : (a : ToType (F.obj k)) → c.pt) y' : c.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j) : (a : ToType (F.obj j)) → c.pt) y : c.pt)
l₁ : J
a₁ : k ⟶ l₁
b₁ : j ⟶ l₁
hl₁ :
  Eq (α := ToType (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier) (F.obj l₁))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
            (F.map a₁) :
          (a : (↑(F.obj k) : Type u)) → (↑(F.obj l₁) : Type u))
        x' :
      (↑(F.obj l₁) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
            (F.map b₁) :
          (a : (↑(F.obj j) : Type u)) → (↑(F.obj l₁) : Type u))
        x :
      (↑(F.obj l₁) : Type u))
l₂ : J
a₂ : k ⟶ l₂
b₂ : j ⟶ l₂
hl₂ :
  Eq (α := ToType (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier) (F.obj l₂))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
            (F.map a₂) :
          (a : (↑(F.obj k) : Type u)) → (↑(F.obj l₂) : Type u))
        y' :
      (↑(F.obj l₂) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
            (F.map b₂) :
          (a : (↑(F.obj j) : Type u)) → (↑(F.obj l₂) : Type u))
        y :
      (↑(F.obj l₂) : Type u))
m : J
d : l₁ ⟶ m
h :
  LE.le (α := (↑(F.obj m) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
            (F.map (a₁ ≫ d)) :
          (a : (↑(F.obj k) : Type u)) → (↑(F.obj m) : Type u))
        x' :
      (↑(F.obj m) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
            (F.map (a₁ ≫ d)) :
          (a : (↑(F.obj k) : Type u)) → (↑(F.obj m) : Type u))
        y' :
      (↑(F.obj m) : Type u))
d' : l₂ ⟶ m
h₁ : a₁ ≫ d = a₂ ≫ d'
h₂ : b₁ ≫ d = b₂ ≫ d'
rw :
  ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
          (F.map (a₂ ≫ d')) :
        (a : (↑(F.obj k) : Type u)) → (↑(F.obj m) : Type u))
      y' :
    (↑(F.obj m) : Type u))
| ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
          (F.map (a₁ ≫ d)) :
        (a : (↑(F.obj k) : Type u)) → (↑(F.obj m) : Type u))
      y' :
    (↑(F.obj m) : Type u))

Tactic:
rw [h₁]
-- 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_1 x_2 : J
f : x_1 ⟶ x_2
x : (↑(F.obj x_1) : Type u)
⊢ Eq (α :=
    (↑(Functor.obj
          (Functor.obj (Functor.const J)
            { carrier := CoconePt hc, str := instPartialOrderCoconePt hc : PartOrdEmb.{u} })
          x_2) :
      Type u))
    ((Hom.hom
            (F.map f ≫
              ofHom
                (RelEmbedding.mk (r := fun (x1 x2 : (↑(F.1 x_2) : Type u)) ↦ x1 ≤ x2) (s := fun (x1 x2 : CoconePt hc) ↦
                  x1 ≤ x2)
                  {
                    toFun :=
                      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app x_2)) :
                        (a : (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj x_2)) →
                          (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj x_2)),
                    inj' := ⋯ }
                  ⋯)) :
          (a : (↑(F.obj x_1) : Type u)) →
            (↑(((Functor.const J).obj { carrier := CoconePt hc, str := instPartialOrderCoconePt hc }).obj x_2) :
              Type u))
        x :
      (↑(Functor.obj
            (Functor.obj (Functor.const J)
              { carrier := CoconePt hc, str := instPartialOrderCoconePt hc : PartOrdEmb.{u} })
            x_2) :
        Type u))
    ((Hom.hom
            (ofHom
                (RelEmbedding.mk (r := fun (x1 x2 : (↑(F.1 x_1) : Type u)) ↦ x1 ≤ x2) (s := fun (x1 x2 : CoconePt hc) ↦
                  x1 ≤ x2)
                  {
                    toFun :=
                      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app x_1)) :
                        (a : (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj x_1)) →
                          (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj x_1)),
                    inj' := ⋯ }
                  ⋯) ≫
              CategoryTheory.Functor.map
                (Functor.obj (Functor.const J)
                  { carrier := CoconePt hc, str := instPartialOrderCoconePt hc : PartOrdEmb.{u} })
                f) :
          (a : (↑(F.obj x_1) : Type u)) →
            (↑(((Functor.const J).obj { carrier := CoconePt hc, str := instPartialOrderCoconePt hc }).obj x_2) :
              Type u))
        x :
      (↑(Functor.obj
            (Functor.obj (Functor.const J)
              { carrier := CoconePt hc, str := instPartialOrderCoconePt hc : PartOrdEmb.{u} })
            x_2) :
        Type u))

Tactic:
ConcreteCategory.congr_hom (c.w f) x

Premises used: PartOrdEmb.Limits.CoconePt, CategoryTheory.Limits.Cocone.w, 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
x_1 x_2 : J
f : x_1 ⟶ x_2
x : (↑(F.obj x_1) : Type u)
⊢ Eq (α :=
    (↑(Functor.obj
          (Functor.obj (Functor.const J)
            { carrier := CoconePt hc, str := instPartialOrderCoconePt hc : PartOrdEmb.{u} })
          x_2) :
      Type u))
    ((Hom.hom
            (F.map f ≫
              ofHom
                (RelEmbedding.mk (r := fun (x1 x2 : (↑(F.1 x_2) : Type u)) ↦ x1 ≤ x2) (s := fun (x1 x2 : CoconePt hc) ↦
                  x1 ≤ x2)
                  {
                    toFun :=
                      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app x_2)) :
                        (a : (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj x_2)) →
                          (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj x_2)),
                    inj' := ⋯ }
                  ⋯)) :
          (a : (↑(F.obj x_1) : Type u)) →
            (↑(((Functor.const J).obj { carrier := CoconePt hc, str := instPartialOrderCoconePt hc }).obj x_2) :
              Type u))
        x :
      (↑(Functor.obj
            (Functor.obj (Functor.const J)
              { carrier := CoconePt hc, str := instPartialOrderCoconePt hc : PartOrdEmb.{u} })
            x_2) :
        Type u))
    ((Hom.hom
            (ofHom
                (RelEmbedding.mk (r := fun (x1 x2 : (↑(F.1 x_1) : Type u)) ↦ x1 ≤ x2) (s := fun (x1 x2 : CoconePt hc) ↦
                  x1 ≤ x2)
                  {
                    toFun :=
                      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app x_1)) :
                        (a : (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj x_1)) →
                          (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj x_1)),
                    inj' := ⋯ }
                  ⋯) ≫
              CategoryTheory.Functor.map
                (Functor.obj (Functor.const J)
                  { carrier := CoconePt hc, str := instPartialOrderCoconePt hc : PartOrdEmb.{u} })
                f) :
          (a : (↑(F.obj x_1) : Type u)) →
            (↑(((Functor.const J).obj { carrier := CoconePt hc, str := instPartialOrderCoconePt hc }).obj x_2) :
              Type u))
        x :
      (↑(Functor.obj
            (Functor.obj (Functor.const J)
              { carrier := CoconePt hc, str := instPartialOrderCoconePt hc : PartOrdEmb.{u} })
            x_2) :
        Type u))

Tactic:
exact ConcreteCategory.congr_hom (c.w f) x

Premises used: CategoryTheory.Limits.Cocone.w, 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 ⋙ forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)).obj j
h :
  Eq (α := (↑s.pt : Type u))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (hc.desc
              (Functor.mapCocone
                (forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                  carrier))
                s)) :
          (a : (fun (X : Type u) ↦ X) c.pt) → (fun (X : Type u) ↦ X) ((forget PartOrdEmb).mapCocone s).pt)
        ((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)) :
      (fun (X : Type u) ↦ 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 (FC := TypeCat.Fun)
            (hc.desc
              (Functor.mapCocone
                (forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                  carrier))
                s)) :
          (a : (fun (X : Type u) ↦ X) c.pt) → (fun (X : Type u) ↦ X) ((forget PartOrdEmb).mapCocone s).pt)
        ((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)) :
      (fun (X : Type u) ↦ 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)))
⊢ Eq (α := CoconePt hc)
    ((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))
    ((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))

Tactic:
rfl