-- 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 : x.fst (β := fun (j : J) ↦ F.obj j) ⟶ k) (g : y.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 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))
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 : 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 : 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))
Tactic: obtain ⟨k, f, g, h⟩ := h
Cleared hypotheses: h