∀ {J : Type u_4} [inst : CategoryTheory.Category.{u_3, u_4} J] {C : Type u_2}
  [inst_1 : CategoryTheory.Category.{u_1, u_2} C] [inst_2 : CategoryTheory.MonoidalCategory C]
  (F : CategoryTheory.Functor J (CategoryTheory.Mon C))
  (c : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Mon.forget C))) (i j : J) (f : i ⟶ j),
  CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.Functor.const J).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj c.1 c.1)).map f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (c.π.app j) (c.π.app j))
        CategoryTheory.MonObj.mul) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (c.π.app i) (c.π.app i))
        CategoryTheory.MonObj.mul)
      ((F.comp (CategoryTheory.Mon.forget C)).map f)