∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} (V : Type u₂) {inst_1 : CategoryTheory.Category.{v₂, u₂} V}
  {inst_2 : CategoryTheory.MonoidalCategory C} {inst_3 : CategoryTheory.MonoidalCategory V} {D : Type u₃}
  {inst_4 : CategoryTheory.Category.{v₃, u₃} D} {inst_5 : CategoryTheory.MonoidalCategoryStruct D}
  [self : CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct C V D] (d : D) (y : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft
        (((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).obj d).obj y)
        (CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.unitUnit C V D))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.convolutionExtensionUnit C V d
              (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).app
          (y, CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
        (((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).map
              (CategoryTheory.MonoidalCategoryStruct.rightUnitor d).hom).app
          (CategoryTheory.MonoidalCategoryStruct.tensorObj y (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor
          (((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).obj d).obj y)).hom
      (((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).obj d).map
        (CategoryTheory.MonoidalCategoryStruct.rightUnitor y).inv)