-- Lean 4 proof step from Mathlib.Algebra.Category.MonCat.FilteredColimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ MonCat
inst_1 : IsFiltered J
j₁ : J
y : (↑(F.obj j₁) : Type (max u v))
j₂ : J
x : (↑(F.obj j₂) : Type (max u v))
j₃ : J
y' : (↑(F.obj j₃) : Type (max u v))
hyy' :
  Types.FilteredColimit.Rel
    (F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier))
    (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₁ y)
    (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₃ y')
⊢ colimitMulAux F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₂ x)
      (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₁ y) =
    colimitMulAux F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₂ x)
      (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₃ y')
have obtain : ∀ (l : J)
  (f :
    Sigma.fst (β := fun (j : J) ↦
        (F ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                carrier)).obj
          j)
        (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₁ y) ⟶
      l)
  (g :
    Sigma.fst (β := fun (j : J) ↦
        (F ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                carrier)).obj
          j)
        (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₃ y') ⟶
      l)
  (hfg :
    Eq (α :=
      (fun (X : Type (max u v)) ↦ X)
        ((F ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                carrier)).obj
          l))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              ((F ⋙
                    forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                      carrier)).map
                f) :
            (a : (fun (X : Type (max u v)) ↦ X) ((F ⋙ forget MonCat).obj ⟨j₁, y⟩.fst)) →
              (fun (X : Type (max u v)) ↦ X) ((F ⋙ forget MonCat).obj l))
          (Sigma.snd (β := fun (j : J) ↦
            (F ⋙
                  forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                    carrier)).obj
              j)
            (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₁ y)) :
        (fun (X : Type (max u v)) ↦ X)
          ((F ⋙
                forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                  carrier)).obj
            l))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              ((F ⋙
                    forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                      carrier)).map
                g) :
            (a : (fun (X : Type (max u v)) ↦ X) ((F ⋙ forget MonCat).obj ⟨j₃, y'⟩.fst)) →
              (fun (X : Type (max u v)) ↦ X) ((F ⋙ forget MonCat).obj l))
          (Sigma.snd (β := fun (j : J) ↦
            (F ⋙
                  forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                    carrier)).obj
              j)
            (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₃ y')) :
        (fun (X : Type (max u v)) ↦ X)
          ((F ⋙
                forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                  carrier)).obj
            l))),
  colimitMulAux F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₂ x)
      (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₁ y) =
    colimitMulAux F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₂ x)
      (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₃ y')
Tactic: obtain ⟨l, f, g, hfg⟩ := hyy'
Cleared hypotheses: hyy'