∀ {C : Type u_4} [inst : CategoryTheory.Category.{u_3, u_4} C] {V : Type u_2}
  [inst_1 : CategoryTheory.Category.{u_1, u_2} V] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory V] [inst_4 : CategoryTheory.MonoidalClosed V]
  {F H G : CategoryTheory.Functor C V} [inst_5 : CategoryTheory.MonoidalCategory.DayConvolution F G]
  (ℌ :
    CategoryTheory.MonoidalCategory.DayConvolutionInternalHom F
      (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G) H)
  {c c' : C} (f : c ⟶ c'),
  CategoryTheory.CategoryStruct.comp (G.map f)
      (CategoryTheory.Limits.Wedge.IsLimit.lift (ℌ.isLimitWedge c')
        (fun c'_1 =>
          CategoryTheory.MonoidalClosed.curry
            ((CategoryTheory.MonoidalCategory.DayConvolution.unit F G).app (c'_1, c')))
        ⋯) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.Wedge.IsLimit.lift (ℌ.isLimitWedge c)
        (fun c' =>
          CategoryTheory.MonoidalClosed.curry ((CategoryTheory.MonoidalCategory.DayConvolution.unit F G).app (c', c)))
        ⋯)
      (H.map f)