∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasLimitsOfShape J C] [inst_3 : CategoryTheory.MonoidalCategory C]
  (F : CategoryTheory.Functor J (CategoryTheory.Mon C)),
  CategoryTheory.MonObj.mul =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Limits.lim (F.comp (CategoryTheory.Mon.forget C))
        (F.comp (CategoryTheory.Mon.forget C)))
      (CategoryTheory.Limits.limMap CategoryTheory.MonObj.mul)