-- 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
t : Cocone F
y : M.{v, u} F
i : J
x : (↑(F.obj i) : Type (max u v))
⊢ (F ⋙
          forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            carrier)).descColimitType
      (((F ⋙
                forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                  carrier)).coconeTypesEquiv.symm :
          (a : Cocone (F ⋙ forget MonCat)) → (F ⋙ forget MonCat).CoconeTypes)
        (Functor.mapCocone
          (forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            carrier))
          t))
      (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) i x) * y) =
    HMul.hMul (α := (↑t.1 : Type (max u v))) (β := (↑t.1 : Type (max u v)))
      ((F ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                carrier)).descColimitType
          (((F ⋙
                    forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                      carrier)).coconeTypesEquiv.symm :
              (a : Cocone (F ⋙ forget MonCat)) → (F ⋙ forget MonCat).CoconeTypes)
            (Functor.mapCocone
              (forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                carrier))
              t))
          (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) i x)) :
        Functor.CoconeTypes.pt (J := J) (F :=
          F ⋙
            forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              carrier))
          (((F ⋙
                    forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                      carrier)).coconeTypesEquiv.symm :
              (a : Cocone (F ⋙ forget MonCat)) → (F ⋙ forget MonCat).CoconeTypes)
            (Functor.mapCocone
              (forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                carrier))
              t)))
      ((F ⋙
            forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              carrier)).descColimitType
        (((F ⋙
                  forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                    carrier)).coconeTypesEquiv.symm :
            (a : Cocone (F ⋙ forget MonCat)) → (F ⋙ forget MonCat).CoconeTypes)
          (Functor.mapCocone
            (forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              carrier))
            t))
        y)
have obtain : ∀ (j : J) (y : (↑(F.obj j) : Type (max u v))),
  (F ⋙
          forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            carrier)).descColimitType
      (((F ⋙
                forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                  carrier)).coconeTypesEquiv.symm :
          (a : Cocone (F ⋙ forget MonCat)) → (F ⋙ forget MonCat).CoconeTypes)
        (Functor.mapCocone
          (forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            carrier))
          t))
      (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) i x) *
        M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j y)) =
    HMul.hMul (α := (↑t.1 : Type (max u v))) (β := (↑t.1 : Type (max u v)))
      ((F ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                carrier)).descColimitType
          (((F ⋙
                    forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                      carrier)).coconeTypesEquiv.symm :
              (a : Cocone (F ⋙ forget MonCat)) → (F ⋙ forget MonCat).CoconeTypes)
            (Functor.mapCocone
              (forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                carrier))
              t))
          (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) i x)) :
        Functor.CoconeTypes.pt (J := J) (F :=
          F ⋙
            forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              carrier))
          (((F ⋙
                    forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                      carrier)).coconeTypesEquiv.symm :
              (a : Cocone (F ⋙ forget MonCat)) → (F ⋙ forget MonCat).CoconeTypes)
            (Functor.mapCocone
              (forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                carrier))
              t)))
      ((F ⋙
            forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              carrier)).descColimitType
        (((F ⋙
                  forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                    carrier)).coconeTypesEquiv.symm :
            (a : Cocone (F ⋙ forget MonCat)) → (F ⋙ forget MonCat).CoconeTypes)
          (Functor.mapCocone
            (forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              carrier))
            t))
        (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j y)))
Tactic: obtain ⟨j, y, rfl⟩ := y.mk_surjective
Cleared hypotheses: y