-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.associator_hom_unit_unit : ∀ {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' d'' : D) (x y z : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight
        ((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.convolutionExtensionUnit C V d
              d').app
          (x, y))
        (((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).obj d'').obj z))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.convolutionExtensionUnit C V
              (CategoryTheory.MonoidalCategoryStruct.tensorObj d d') d'').app
          (CategoryTheory.MonoidalCategoryStruct.tensorObj x y, z))
        (((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).map
              (CategoryTheory.MonoidalCategoryStruct.associator d d' d'').hom).app
          (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj x y) z))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator
          (((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).obj d).obj x)
          (((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).obj d',
                  (CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).obj d'').1.obj
            (y, z).1)
          (((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).obj d',
                  (CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).obj d'').2.obj
            (y, z).2)).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft
          (((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).obj d).obj x)
          ((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.convolutionExtensionUnit C V d'
                d'').app
            (y, z)))
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.convolutionExtensionUnit C V d
                (CategoryTheory.MonoidalCategoryStruct.tensorObj d' d'')).app
            (x, CategoryTheory.MonoidalCategoryStruct.tensorObj y z))
          (((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).obj
                (CategoryTheory.MonoidalCategoryStruct.tensorObj d
                  (CategoryTheory.MonoidalCategoryStruct.tensorObj d' d''))).map
            (CategoryTheory.MonoidalCategoryStruct.associator (x, CategoryTheory.MonoidalCategoryStruct.tensorObj y z).1
                y z).inv)))