∀ {I : Type u_2} {C : I → Type u_3} [inst : (i : I) → CategoryTheory.Category.{u_1, u_3} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] {A B X Y : (i : I) → C i} (f : A ⟶ B) (g : X ⟶ Y),
  CategoryTheory.MonoidalCategoryStruct.tensorHom f g =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X)
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B g)