-- Module: Mathlib.Algebra.Category.MonCat.FilteredColimits
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))
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)))
⊢ (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)

Tactic:
obtain ⟨j, y, rfl⟩ := y.mk_surjective

Premises used: rfl, MonCat.FilteredColimits.M.mk_surjective