∀ {J : Type u_3} [inst : CategoryTheory.SmallCategory J] {C : Type u_2} [inst_1 : CategoryTheory.Category.{u_1, u_2} C]
  [inst_2 : CategoryTheory.Limits.HasLimitsOfShape J C] [inst_3 : CategoryTheory.MonoidalCategory C]
  (F : CategoryTheory.Functor J (CategoryTheory.Mon C)) (s : CategoryTheory.Limits.Cone F) (j : J),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul
        (CategoryTheory.Limits.limit.lift (F.comp (CategoryTheory.Mon.forget C))
          ((CategoryTheory.Mon.forget C).mapCone s)))
      (CategoryTheory.Limits.limit.π ((CategoryTheory.Monoidal.monFunctorCategoryEquivalence J C).inverse.obj F).X j) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom
          (CategoryTheory.Limits.limit.lift (F.comp (CategoryTheory.Mon.forget C))
            ((CategoryTheory.Mon.forget C).mapCone s))
          (CategoryTheory.Limits.limit.lift (F.comp (CategoryTheory.Mon.forget C))
            ((CategoryTheory.Mon.forget C).mapCone s)))
        CategoryTheory.MonObj.mul)
      (CategoryTheory.Limits.limit.π ((CategoryTheory.Monoidal.monFunctorCategoryEquivalence J C).inverse.obj F).X j)