∀ {J : Type u_1} [inst : CategoryTheory.SmallCategory J] {C : Type u_3} [inst_1 : CategoryTheory.Category.{u_2, u_3} C]
  [CategoryTheory.Limits.HasLimitsOfShape J C] [inst_3 : CategoryTheory.MonoidalCategory C]
  (F : CategoryTheory.Functor J (CategoryTheory.Mon C)),
  CategoryTheory.Limits.HasLimit (F.comp (CategoryTheory.Mon.forget C))