∀ {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]
  [inst_4 : CategoryTheory.MonoidalClosed V] {F G H : CategoryTheory.Functor C V}
  (self : CategoryTheory.MonoidalCategory.DayConvolutionInternalHom F G H) (c : C) ⦃i j : C⦄ (f : i ⟶ j) {Z : V}
  (h : F.obj i ⟹ G.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj j c) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.π c i)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.ihom (F.obj i)).map (G.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f c))) h) =
    CategoryTheory.CategoryStruct.comp (self.π c j)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.MonoidalClosed.pre (F.map f)).app
          (G.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj j c)))
        h)