-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered
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 y : (j : J) × F.obj j
h : Relation.EqvGen F.ColimitTypeRel x y
mp :
  ∀ (x y : (j : J) × F.obj j) (h : F.ColimitTypeRel x y),
    ∃ (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))
mp₁ :
  ∀ (x : (j : J) × F.obj j),
    ∃ (k : J) (f : x.fst (β := fun (j : J) ↦ F.obj j) ⟶ k) (g : x.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 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))
mp₂ :
  ∀ (x y : (j : J) × F.obj j),
    Relation.EqvGen F.ColimitTypeRel x y →
      ∀
        (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))),
        ∃ (k : J) (f : y.fst (β := fun (j : J) ↦ F.obj j) ⟶ k) (g : x.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 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))
mp₃ :
  ∀ (x y z : (j : J) × F.obj j),
    Relation.EqvGen F.ColimitTypeRel x y →
      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))
⊢ ∃ (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))

Tactic:
induction h with
    | rel x y h =>
      obtain ⟨f, h⟩ := h
      exact ⟨y.1, f, 𝟙 _, by simpa using h.symm⟩
    | refl x => exact ⟨x.1, 𝟙 _, 𝟙 _, rfl⟩
    | symm _ _ _ h =>
      obtain ⟨k, f, g, h⟩ := h
      exact ⟨k, g, f, h.symm⟩
    | trans x y z _ _ h h' =>
      obtain ⟨k, f, g, h⟩ := h
      obtain ⟨k', f', g', h'⟩ := h'
      obtain ⟨l, a, b, h''⟩ := span g f'
      refine ⟨l, f ≫ a, g' ≫ b, ?_⟩
      simp only [map_comp, comp_apply, h, ← h']
      simp [← comp_apply, ← map_comp, h'']

Premises used: CategoryTheory.comp_apply, CategoryTheory.Functor.map_comp, symm, refl