awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Category.OmegaCompletePartialOrder (goal)
Goal:
X Y : ωCPO
f g : X ⟶ Y
s : Fork f g
m : s.pt ⟶ (equalizer f g).pt
hm : m ≫ (equalizer f g).ι = s.ι
⊢ m =
    {
      toFun := fun (x : s.pt.carrier) ↦
        Subtype.mk (p := fun (a : X.carrier) ↦
          Eq (α := Y.carrier)
            ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) f :
                  (a : X.carrier) → Y.carrier)
                a :
              Y.carrier)
            ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) g :
                  (a : X.carrier) → Y.carrier)
                a :
              Y.carrier))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) s.ι :
              (a : s.pt.carrier) → X.carrier)
            x)
          ⋯,
      monotone' := ⋯, map_ωSup' := ⋯ }
have h : ∀ (x : s.pt.carrier),
  Eq (α := (equalizer f g).pt.carrier)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) m :
          (a : s.pt.carrier) → (equalizer f g).pt.carrier)
        x :
      (equalizer f g).pt.carrier)
    ((@ConcreteCategory.hom _ instLargeCategory (fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) carrier _ _ s.pt
            (equalizer f g).pt
            {
              toFun := fun (x : s.pt.carrier) ↦
                Subtype.mk (p := fun (a : X.carrier) ↦
                  Eq (α := Y.carrier)
                    ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) f :
                          (a : X.carrier) → Y.carrier)
                        a :
                      Y.carrier)
                    ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) g :
                          (a : X.carrier) → Y.carrier)
                        a :
                      Y.carrier))
                  ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) s.ι :
                      (a : s.pt.carrier) → X.carrier)
                    x)
                  sorry,
              monotone' := sorry, map_ωSup' := sorry } :
          (a : s.pt.carrier) → (equalizer f g).pt.carrier)
        x :
      (equalizer f g).pt.carrier)
Tactic: ext x : 2
-- Lean 4 proof step from Mathlib.Order.Category.OmegaCompletePartialOrder (goal)
Goal:
X Y : ωCPO
f g : X ⟶ Y
s : Fork f g
m : s.pt ⟶ (equalizer f g).pt
hm : m ≫ (equalizer f g).ι = s.ι
x : s.pt.carrier
⊢ Eq (α := (equalizer f g).pt.carrier)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) m :
          (a : s.pt.carrier) → (equalizer f g).pt.carrier)
        x :
      (equalizer f g).pt.carrier)
    ((@ConcreteCategory.hom _ instLargeCategory (fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) carrier _ _ s.pt
            (equalizer f g).pt
            {
              toFun := fun (x : s.pt.carrier) ↦
                Subtype.mk (p := fun (a : X.carrier) ↦
                  Eq (α := Y.carrier)
                    ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) f :
                          (a : X.carrier) → Y.carrier)
                        a :
                      Y.carrier)
                    ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) g :
                          (a : X.carrier) → Y.carrier)
                        a :
                      Y.carrier))
                  ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) s.ι :
                      (a : s.pt.carrier) → X.carrier)
                    x)
                  ⋯,
              monotone' := ⋯, map_ωSup' := ⋯ } :
          (a : s.pt.carrier) → (equalizer f g).pt.carrier)
        x :
      (equalizer f g).pt.carrier)
have apply : Eq.{v + 1} (α := X.carrier)
  (↑((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) m :
          (a : s.pt.carrier) → (equalizer f g).pt.carrier)
        x) :
    X.carrier)
  (↑((@ConcreteCategory.hom _ instLargeCategory (fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) carrier _ _ s.pt
            (equalizer f g).pt
            {
              toFun := fun (x : s.pt.carrier) ↦
                Subtype.mk (p := fun (a : X.carrier) ↦
                  Eq (α := Y.carrier)
                    ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) f :
                          (a : X.carrier) → Y.carrier)
                        a :
                      Y.carrier)
                    ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) g :
                          (a : X.carrier) → Y.carrier)
                        a :
                      Y.carrier))
                  ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) s.ι :
                      (a : s.pt.carrier) → X.carrier)
                    x)
                  sorry,
              monotone' := sorry, map_ωSup' := sorry } :
          (a : s.pt.carrier) → (equalizer f g).pt.carrier)
        x) :
    X.carrier)
Tactic: apply Subtype.ext ?_
-- Lean 4 proof step from Mathlib.Order.Category.PartOrd (goal)
Goal:
X : Preord
⊢ PartOrd.ofHom (Preord.Hom.hom (𝟙 X)).antisymmetrization =
    𝟙
      { carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
        str := instPartialOrderAntisymmetrization }
have hf : ∀
  (x :
    (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
          str := instPartialOrderAntisymmetrization } :
      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))
        x :
      (↑{ 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))
        x :
      (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
            str := instPartialOrderAntisymmetrization } :
        Type u))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Category.PartOrd (goal)
Goal:
X Y Z : Preord
f : X ⟶ Y
g : Y ⟶ Z
⊢ PartOrd.ofHom (Preord.Hom.hom (f ≫ g)).antisymmetrization =
    PartOrd.ofHom (Preord.Hom.hom f).antisymmetrization ≫ PartOrd.ofHom (Preord.Hom.hom g).antisymmetrization
have 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))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Category.PartOrdEmb (goal)
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.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'
have 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'
Tactic: obtain ⟨j, x', hx⟩ := Types.jointly_surjective_of_isColimit hc x
-- Lean 4 proof step from Mathlib.Order.Category.PartOrdEmb (goal)
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₂
⊢ x = y
have 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
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₆]⟩
-- Lean 4 proof step from Mathlib.Order.Category.PartOrdEmb (hypothesis)
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
have h₇ : 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₂)
-- Lean 4 proof step from Mathlib.Order.Category.PartOrdEmb (goal)
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))
⊢ x = y
have 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
Tactic: obtain ⟨k, a, ha⟩ := (Types.FilteredColimit.isColimit_eq_iff' hc x y).1 h
-- Lean 4 proof step from Mathlib.Order.Category.PartOrdEmb (goal)
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
have 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' := sorry } :
          (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' := sorry } :
          (a : (↑(F.1 j) : Type u)) → CoconePt hc)
        y :
      CoconePt hc) →
  x ≤ y
Tactic: refine ⟨?_, fun h ↦ ⟨j, x, y, rfl, rfl, h⟩⟩
-- Lean 4 proof step from Mathlib.Order.Category.PartOrdEmb (goal)
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))
⊢ x ≤ y
have obtain : ∀ (m : J) (d : l₁ ⟶ m) (d' : l₂ ⟶ m) (h₁ : a₁ ≫ d = a₂ ≫ d') (h₂ : b₁ ≫ d = b₂ ≫ d'), x ≤ y
Tactic: obtain ⟨m, d, d', h₁, h₂⟩ := bowtie a₁ a₂ b₁ b₂