∀ {J : Type u_1} [inst : CategoryTheory.SmallCategory J] {C : Type u_3} [inst_1 : CategoryTheory.Category.{u_2, u_3} C]
  [inst_2 : CategoryTheory.Limits.HasLimitsOfShape J C] [inst_3 : CategoryTheory.MonoidalCategory C]
  (F G H : CategoryTheory.Functor J C) (j j' : J) (f : j ⟶ j'),
  CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.Functor.const J).obj
            (CategoryTheory.MonoidalCategoryStruct.tensorObj
              (CategoryTheory.Limits.limit (CategoryTheory.MonoidalCategoryStruct.tensorObj F G))
              (CategoryTheory.Limits.limit H))).map
        f)
      (CategoryTheory.MonoidalCategoryStruct.tensorHom
        (CategoryTheory.Limits.limit.π (CategoryTheory.MonoidalCategoryStruct.tensorObj F G) j')
        (CategoryTheory.Limits.limit.π H j')) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom
        (CategoryTheory.Limits.limit.π (CategoryTheory.MonoidalCategoryStruct.tensorObj F G) j)
        (CategoryTheory.Limits.limit.π H j))
      ((CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj F G) H).map f)