∀ (C : Type u_3) [inst : CategoryTheory.Category.{u_6, u_3} C] (V : Type u_5)
  [inst_1 : CategoryTheory.Category.{u_4, u_5} V] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory V] (D : Type u_2) [inst_4 : CategoryTheory.Category.{u_1, u_2} D]
  [inst_5 : CategoryTheory.MonoidalCategoryStruct D]
  [CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct C V D] (x y : D),
  CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id x)
      (CategoryTheory.CategoryStruct.id y) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)