-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Set (goal)
Goal:
J : Type w
inst : Category.{w', w} J
X : Type u
inst_1 : IsFilteredOrEmpty.{w', w} J
F : CategoryTheory.Functor.{w', u, w, u} J (Set X)
i j : J
x : X
hx : x ∈ F.obj i
y : X
hy : y ∈ F.obj j
h :
  Eq (α :=
    (fun (X : Type u) ↦ X)
      (Functor.obj.{w', u, w, u + 1}
        (Functor.obj (Functor.const J)
          (Cocone.pt (F := F ⋙ functorToTypes) (Functor.mapCocone functorToTypes (colimitCocone F).cocone)))
        i))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι (Functor.mapCocone functorToTypes (colimitCocone F).cocone)) i) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj i)) →
            (fun (X : Type u) ↦ X)
              (((Functor.const J).obj (functorToTypes.mapCocone (colimitCocone F).cocone).pt).obj i))
        (Subtype.mk (p := fun (x : X) ↦ x ∈ F.obj i) x hx) :
      (fun (X : Type u) ↦ X)
        (Functor.obj.{w', u, w, u + 1}
          (Functor.obj (Functor.const J)
            (Cocone.pt (F := F ⋙ functorToTypes) (Functor.mapCocone functorToTypes (colimitCocone F).cocone)))
          i))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι (Functor.mapCocone functorToTypes (colimitCocone F).cocone)) j) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj j)) →
            (fun (X : Type u) ↦ X)
              (((Functor.const J).obj (functorToTypes.mapCocone (colimitCocone F).cocone).pt).obj j))
        (Subtype.mk (p := fun (x : X) ↦ x ∈ F.obj j) y hy) :
      (fun (X : Type u) ↦ X)
        (Functor.obj.{w', u, w, u + 1}
          (Functor.obj (Functor.const J)
            (Cocone.pt (F := F ⋙ functorToTypes) (Functor.mapCocone functorToTypes (colimitCocone F).cocone)))
          j))
⊢ ∃ (k : J) (f : i ⟶ k) (g : j ⟶ k),
    Eq (α := (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ functorToTypes).map f) :
            (a : (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj i)) →
              (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj k))
          (Subtype.mk (p := fun (x : X) ↦ x ∈ F.obj i) x hx) :
        (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ functorToTypes).map g) :
            (a : (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj j)) →
              (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj k))
          (Subtype.mk (p := fun (x : X) ↦ x ∈ F.obj j) y hy) :
        (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj k))
have hinj : ∀ (hy : x ∈ F.obj j)
  (h :
    Eq (α :=
      (fun (X : Type u) ↦ X)
        (Functor.obj.{w', u, w, u + 1}
          (Functor.obj (Functor.const J)
            (Cocone.pt (F := F ⋙ functorToTypes) (Functor.mapCocone functorToTypes (colimitCocone F).cocone)))
          i))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app (Cocone.ι (Functor.mapCocone functorToTypes (colimitCocone F).cocone)) i) :
            (a : (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj i)) →
              (fun (X : Type u) ↦ X)
                (((Functor.const J).obj (functorToTypes.mapCocone (colimitCocone F).cocone).pt).obj i))
          (Subtype.mk (p := fun (x : X) ↦ x ∈ F.obj i) x hx) :
        (fun (X : Type u) ↦ X)
          (Functor.obj.{w', u, w, u + 1}
            (Functor.obj (Functor.const J)
              (Cocone.pt (F := F ⋙ functorToTypes) (Functor.mapCocone functorToTypes (colimitCocone F).cocone)))
            i))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app (Cocone.ι (Functor.mapCocone functorToTypes (colimitCocone F).cocone)) j) :
            (a : (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj j)) →
              (fun (X : Type u) ↦ X)
                (((Functor.const J).obj (functorToTypes.mapCocone (colimitCocone F).cocone).pt).obj j))
          (Subtype.mk (p := fun (x : X) ↦ x ∈ F.obj j) x hy) :
        (fun (X : Type u) ↦ X)
          (Functor.obj.{w', u, w, u + 1}
            (Functor.obj (Functor.const J)
              (Cocone.pt (F := F ⋙ functorToTypes) (Functor.mapCocone functorToTypes (colimitCocone F).cocone)))
            j))),
  ∃ (k : J) (f : i ⟶ k) (g : j ⟶ k),
    Eq (α := (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ functorToTypes).map f) :
            (a : (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj i)) →
              (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj k))
          (Subtype.mk (p := fun (x : X) ↦ x ∈ F.obj i) x hx) :
        (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ functorToTypes).map g) :
            (a : (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj j)) →
              (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj k))
          (Subtype.mk (p := fun (x : X) ↦ x ∈ F.obj j) x hy) :
        (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj k))
Tactic: obtain rfl : x = y := by simpa using h
Cleared hypotheses: y, hy, h