-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered (goal)
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : IsFiltered.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
x_1 y_1 x y z : (j : J) × F.obj j
h_1 : Relation.EqvGen F.ColimitTypeRel x y
h_2 : Relation.EqvGen F.ColimitTypeRel y z
h' :
  ∃ (k : J) (f : y.fst (β := fun (j : J) ↦ F.obj j) ⟶ k) (g : z.fst (β := fun (j : J) ↦ F.obj j) ⟶ k),
    Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
            (a : (fun (X : Type w₀) ↦ X) (F.obj y.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
          (y.snd (β := fun (j : J) ↦ F.obj j)) :
        (fun (X : Type w₀) ↦ X) (F.obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
            (a : (fun (X : Type w₀) ↦ X) (F.obj z.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
          (z.snd (β := fun (j : J) ↦ F.obj j)) :
        (fun (X : Type w₀) ↦ X) (F.obj k))
k : J
f : x.fst (β := fun (j : J) ↦ F.obj j) ⟶ k
g : y.fst (β := fun (j : J) ↦ F.obj j) ⟶ k
h :
  Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type w₀) ↦ X) (F.obj x.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
        (x.snd (β := fun (j : J) ↦ F.obj j)) :
      (fun (X : Type w₀) ↦ X) (F.obj k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
          (a : (fun (X : Type w₀) ↦ X) (F.obj y.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
        (y.snd (β := fun (j : J) ↦ F.obj j)) :
      (fun (X : Type w₀) ↦ X) (F.obj k))
⊢ ∃ (k : J) (f : x.fst (β := fun (j : J) ↦ F.obj j) ⟶ k) (g : z.fst (β := fun (j : J) ↦ F.obj j) ⟶ k),
    Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
            (a : (fun (X : Type w₀) ↦ X) (F.obj x.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
          (x.snd (β := fun (j : J) ↦ F.obj j)) :
        (fun (X : Type w₀) ↦ X) (F.obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
            (a : (fun (X : Type w₀) ↦ X) (F.obj z.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
          (z.snd (β := fun (j : J) ↦ F.obj j)) :
        (fun (X : Type w₀) ↦ X) (F.obj k))
have mp : ∀ (k' : J) (f' : y.fst (β := fun (j : J) ↦ F.obj j) ⟶ k') (g' : z.fst (β := fun (j : J) ↦ F.obj j) ⟶ k')
  (h' :
    Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k'))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f') :
            (a : (fun (X : Type w₀) ↦ X) (F.obj y.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k'))
          (y.snd (β := fun (j : J) ↦ F.obj j)) :
        (fun (X : Type w₀) ↦ X) (F.obj k'))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g') :
            (a : (fun (X : Type w₀) ↦ X) (F.obj z.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k'))
          (z.snd (β := fun (j : J) ↦ F.obj j)) :
        (fun (X : Type w₀) ↦ X) (F.obj k'))),
  ∃ (k : J) (f : x.fst (β := fun (j : J) ↦ F.obj j) ⟶ k) (g : z.fst (β := fun (j : J) ↦ F.obj j) ⟶ k),
    Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
            (a : (fun (X : Type w₀) ↦ X) (F.obj x.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
          (x.snd (β := fun (j : J) ↦ F.obj j)) :
        (fun (X : Type w₀) ↦ X) (F.obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
            (a : (fun (X : Type w₀) ↦ X) (F.obj z.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
          (z.snd (β := fun (j : J) ↦ F.obj j)) :
        (fun (X : Type w₀) ↦ X) (F.obj k))
Tactic: obtain ⟨k', f', g', h'⟩ := h'
Cleared hypotheses: h'