∀ {J : Type v} [inst : CategoryTheory.Category.{u, v} J] (F : CategoryTheory.Functor J MonCat)
  (x y : MonCat.Colimits.Prequotient F),
  Quot.mk (⇑(MonCat.Colimits.colimitSetoid F)) (x.mul y) =
    Quot.mk (⇑(MonCat.Colimits.colimitSetoid F)) x * Quot.mk (⇑(MonCat.Colimits.colimitSetoid F)) y