-- 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 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))
⊢ ∃ (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))
have 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))
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'']
Cleared hypotheses: h