∀ {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]
  {F G : CategoryTheory.Functor C V} (h h' : CategoryTheory.MonoidalCategory.DayConvolution F G)
  {Z : CategoryTheory.Functor (C × C) V}
  (h_1 :
    (CategoryTheory.MonoidalCategory.tensor C).comp (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.unit F G)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.MonoidalCategory.tensor C).whiskerLeft (h.uniqueUpToIso h').hom) h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.unit F G) h_1