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
x y : CoconePt hc
j : J
x₁ y₁ : (↑(F.obj j) : Type u)
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
hy₁ :
  (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₁ =
    y
h₁ : x₁ ≤ y₁
k : J
y₂ x₂ : (↑(F.obj k) : Type u)
hy₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app k) :
        (a : (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj k)) →
          (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj k))
      y₂ =
    y
hx₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app k) :
        (a : (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj k)) →
          (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj k))
      x₂ =
    x
h₂ : y₂ ≤ x₂
obtain :
  ∀ (l : J) (a : j ⟶ l) (b : k ⟶ l) (x₃ y₃ : (↑(F.obj l) : Type u))
    (h₃ :
      x₃ =
        (ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
              (F.map a) :
            (a : (↑(F.obj j) : Type u)) → (↑(F.obj l) : Type u))
          x₁)
    (h₄ :
      x₃ =
        (ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
              (F.map b) :
            (a : (↑(F.obj k) : Type u)) → (↑(F.obj l) : Type u))
          x₂)
    (h₅ :
      y₃ =
        (ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
              (F.map a) :
            (a : (↑(F.obj j) : Type u)) → (↑(F.obj l) : Type u))
          y₁)
    (h₆ :
      y₃ =
        (ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
              (F.map b) :
            (a : (↑(F.obj k) : Type u)) → (↑(F.obj l) : Type u))
          y₂),
    x = y
⊢ x = y

Tactic:
obtain ⟨l, a, b, x₃, y₃, h₃, h₄, h₅, h₆⟩ :
        ∃ (l : J) (a : j ⟶ l) (b : k ⟶ l) (x₃ y₃ : _),
        x₃ = F.map a x₁ ∧ x₃ = F.map b x₂ ∧ y₃ = F.map a y₁ ∧ y₃ = F.map b y₂ := by
      obtain ⟨l₁, a, b, h₃⟩ :=
        (Types.FilteredColimit.isColimit_eq_iff _ hc (xi := x₁) (xj := x₂)).1
          (hx₁.trans hx₂.symm)
      obtain ⟨l₂, a', b', h₄⟩ :=
        (Types.FilteredColimit.isColimit_eq_iff _ hc (xi := y₁) (xj := y₂)).1
          (hy₁.trans hy₂.symm)
      obtain ⟨l, d, d', h₅, h₆⟩ := IsFiltered.bowtie a a' b b'
      exact ⟨l, a ≫ d, b ≫ d, F.map (a ≫ d) x₁, F.map (a' ≫ d') y₁, rfl,
        by simpa, by rw [h₅], by simpa [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 y : CoconePt hc
j : J
x₁ y₁ : (↑(F.obj j) : Type u)
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
hy₁ :
  (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₁ =
    y
h₁ : x₁ ≤ y₁
k : J
y₂ x₂ : (↑(F.obj k) : Type u)
hy₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app k) :
        (a : (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj k)) →
          (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj k))
      y₂ =
    y
hx₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app k) :
        (a : (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj k)) →
          (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj k))
      x₂ =
    x
h₂ : y₂ ≤ x₂
l : J
a : j ⟶ l
b : k ⟶ l
x₃ y₃ : (↑(F.obj l) : Type u)
h₃ :
  x₃ =
    (ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
          (F.map a) :
        (a : (↑(F.obj j) : Type u)) → (↑(F.obj l) : Type u))
      x₁
h₄ :
  x₃ =
    (ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
          (F.map b) :
        (a : (↑(F.obj k) : Type u)) → (↑(F.obj l) : Type u))
      x₂
h₅ :
  y₃ =
    (ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
          (F.map a) :
        (a : (↑(F.obj j) : Type u)) → (↑(F.obj l) : Type u))
      y₁
h₆ :
  y₃ =
    (ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
          (F.map b) :
        (a : (↑(F.obj k) : Type u)) → (↑(F.obj l) : Type u))
      y₂
⊢ x₃ ≤ y₃

Tactic:
simpa only [h₃, h₅] using (F.map a).hom.monotone h₁

Premises used: OrderEmbedding.monotone, PartOrdEmb.Hom.hom, CategoryTheory.Functor.map
-- 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 y : CoconePt hc
j : J
x₁ y₁ : (↑(F.obj j) : Type u)
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
hy₁ :
  (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₁ =
    y
h₁ : x₁ ≤ y₁
k : J
y₂ x₂ : (↑(F.obj k) : Type u)
hy₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app k) :
        (a : (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj k)) →
          (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj k))
      y₂ =
    y
hx₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app k) :
        (a : (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj k)) →
          (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj k))
      x₂ =
    x
h₂ : y₂ ≤ x₂
l : J
a : j ⟶ l
b : k ⟶ l
x₃ y₃ : (↑(F.obj l) : Type u)
h₃ :
  x₃ =
    (ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
          (F.map a) :
        (a : (↑(F.obj j) : Type u)) → (↑(F.obj l) : Type u))
      x₁
h₄ :
  x₃ =
    (ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
          (F.map b) :
        (a : (↑(F.obj k) : Type u)) → (↑(F.obj l) : Type u))
      x₂
h₅ :
  y₃ =
    (ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
          (F.map a) :
        (a : (↑(F.obj j) : Type u)) → (↑(F.obj l) : Type u))
      y₁
h₆ :
  y₃ =
    (ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
          (F.map b) :
        (a : (↑(F.obj k) : Type u)) → (↑(F.obj l) : Type u))
      y₂
⊢ y₃ ≤ x₃

Tactic:
simpa only [h₄, h₆] using (F.map b).hom.monotone h₂

Premises used: OrderEmbedding.monotone, PartOrdEmb.Hom.hom, CategoryTheory.Functor.map
-- 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 y : CoconePt hc
j : J
x₁ y₁ : (↑(F.obj j) : Type u)
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
hy₁ :
  (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₁ =
    y
h₁ : x₁ ≤ y₁
k : J
y₂ x₂ : (↑(F.obj k) : Type u)
hy₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app k) :
        (a : (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj k)) →
          (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj k))
      y₂ =
    y
hx₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app k) :
        (a : (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj k)) →
          (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj k))
      x₂ =
    x
h₂ : y₂ ≤ x₂
l : J
a : j ⟶ l
b : k ⟶ l
x₃ y₃ : (↑(F.obj l) : Type u)
h₃ :
  x₃ =
    (ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
          (F.map a) :
        (a : (↑(F.obj j) : Type u)) → (↑(F.obj l) : Type u))
      x₁
h₄ :
  x₃ =
    (ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
          (F.map b) :
        (a : (↑(F.obj k) : Type u)) → (↑(F.obj l) : Type u))
      x₂
h₅ :
  y₃ =
    (ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
          (F.map a) :
        (a : (↑(F.obj j) : Type u)) → (↑(F.obj l) : Type u))
      y₁
h₆ :
  y₃ =
    (ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
          (F.map b) :
        (a : (↑(F.obj k) : Type u)) → (↑(F.obj l) : Type u))
      y₂
⊢ x₃ = y₃

Tactic:
have h₇ : x₃ = y₃ :=
      le_antisymm
        (by simpa only [h₃, h₅] using (F.map a).hom.monotone h₁)
        (by simpa only [h₄, h₆] using (F.map b).hom.monotone 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 y : CoconePt hc
j : J
x₁ y₁ : (↑(F.obj j) : Type u)
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
hy₁ :
  (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₁ =
    y
h₁ : x₁ ≤ y₁
k : J
y₂ x₂ : (↑(F.obj k) : Type u)
hy₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app k) :
        (a : (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj k)) →
          (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj k))
      y₂ =
    y
hx₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app k) :
        (a : (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj k)) →
          (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj k))
      x₂ =
    x
h₂ : y₂ ≤ x₂
l : J
a : j ⟶ l
b : k ⟶ l
x₃ y₃ : (↑(F.obj l) : Type u)
h₃ :
  x₃ =
    (ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
          (F.map a) :
        (a : (↑(F.obj j) : Type u)) → (↑(F.obj l) : Type u))
      x₁
h₄ :
  x₃ =
    (ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
          (F.map b) :
        (a : (↑(F.obj k) : Type u)) → (↑(F.obj l) : Type u))
      x₂
h₅ :
  y₃ =
    (ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
          (F.map a) :
        (a : (↑(F.obj j) : Type u)) → (↑(F.obj l) : Type u))
      y₁
h₆ :
  y₃ =
    (ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
          (F.map b) :
        (a : (↑(F.obj k) : Type u)) → (↑(F.obj l) : Type u))
      y₂
h₇ : x₃ = y₃
⊢ x = y

Tactic:
hx₁.symm.trans ((ConcreteCategory.congr_hom (c.w a) x₁).symm.trans
      ((congr_arg (c.ι.app l) (h₃.symm.trans (h₇.trans h₅))).trans
        ((ConcreteCategory.congr_hom (c.w a) y₁).trans hy₁)))

Premises used: PartOrdEmb.Limits.CoconePt, 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
x y : CoconePt hc
j : J
x₁ y₁ : (↑(F.obj j) : Type u)
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
hy₁ :
  (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₁ =
    y
h₁ : x₁ ≤ y₁
k : J
y₂ x₂ : (↑(F.obj k) : Type u)
hy₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app k) :
        (a : (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj k)) →
          (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj k))
      y₂ =
    y
hx₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app k) :
        (a : (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj k)) →
          (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj k))
      x₂ =
    x
h₂ : y₂ ≤ x₂
l : J
a : j ⟶ l
b : k ⟶ l
x₃ y₃ : (↑(F.obj l) : Type u)
h₃ :
  x₃ =
    (ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
          (F.map a) :
        (a : (↑(F.obj j) : Type u)) → (↑(F.obj l) : Type u))
      x₁
h₄ :
  x₃ =
    (ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
          (F.map b) :
        (a : (↑(F.obj k) : Type u)) → (↑(F.obj l) : Type u))
      x₂
h₅ :
  y₃ =
    (ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
          (F.map a) :
        (a : (↑(F.obj j) : Type u)) → (↑(F.obj l) : Type u))
      y₁
h₆ :
  y₃ =
    (ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
          (F.map b) :
        (a : (↑(F.obj k) : Type u)) → (↑(F.obj l) : Type u))
      y₂
h₇ : x₃ = y₃
⊢ x = y

Tactic:
exact hx₁.symm.trans ((ConcreteCategory.congr_hom (c.w a) x₁).symm.trans
      ((congr_arg (c.ι.app l) (h₃.symm.trans (h₇.trans h₅))).trans
        ((ConcreteCategory.congr_hom (c.w a) y₁).trans hy₁)))

Premises used: 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
j : J
x y : (↑(F.1 j) : Type u)
h :
  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))
        y :
      (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) j))
obtain :
  ∀ (k : J) (a : j ⟶ k)
    (ha :
      Eq (α :=
        (fun (X : Type u) ↦ X)
          ((F ⋙
                forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                  carrier)).obj
            k))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                ((F ⋙
                      forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                        carrier)).map
                  a) :
              (a : (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj j)) →
                (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj k))
            x :
          (fun (X : Type u) ↦ X)
            ((F ⋙
                  forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                    carrier)).obj
              k))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                ((F ⋙
                      forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                        carrier)).map
                  a) :
              (a : (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj j)) →
                (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj k))
            y :
          (fun (X : Type u) ↦ X)
            ((F ⋙
                  forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                    carrier)).obj
              k))),
    x = y
⊢ x = y

Tactic:
obtain ⟨k, a, ha⟩ := (Types.FilteredColimit.isColimit_eq_iff' hc x y).1 h

Premises used: Iff.mp, CategoryTheory.Limits.Types.FilteredColimit.isColimit_eq_iff'
-- 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)
h :
  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))
        y :
      (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) j))
k : J
a : j ⟶ k
ha :
  Eq (α :=
    (fun (X : Type u) ↦ X)
      ((F ⋙
            forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
              carrier)).obj
        k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((F ⋙
                  forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                    carrier)).map
              a) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj j)) →
            (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj k))
        x :
      (fun (X : Type u) ↦ X)
        ((F ⋙
              forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                carrier)).obj
          k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((F ⋙
                  forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                    carrier)).map
              a) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj j)) →
            (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj k))
        y :
      (fun (X : Type u) ↦ X)
        ((F ⋙
              forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                carrier)).obj
          k))
⊢ x = y

Tactic:
(F.map a).injective ha

Premises used: CategoryTheory.Functor.map, PartOrdEmb.Hom.injective
-- 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)
h :
  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))
        y :
      (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) j))
k : J
a : j ⟶ k
ha :
  Eq (α :=
    (fun (X : Type u) ↦ X)
      ((F ⋙
            forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
              carrier)).obj
        k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((F ⋙
                  forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                    carrier)).map
              a) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj j)) →
            (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj k))
        x :
      (fun (X : Type u) ↦ X)
        ((F ⋙
              forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                carrier)).obj
          k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((F ⋙
                  forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                    carrier)).map
              a) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj j)) →
            (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj k))
        y :
      (fun (X : Type u) ↦ X)
        ((F ⋙
              forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                carrier)).obj
          k))
⊢ x = y

Tactic:
exact (F.map a).injective ha

Premises used: CategoryTheory.Functor.map, PartOrdEmb.Hom.injective
-- 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)
⊢ 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:
⟨?_, fun h ↦ ⟨j, x, y, rfl, rfl, h⟩⟩

Premises used: Iff.intro, Exists.intro, rfl