-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.mk : {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] →
                (ι : CategoryTheory.Functor D (CategoryTheory.Functor C V)) →
                  ι.FullyFaithful →
                    (tensorObj : D → D → D) →
                      (convolutions' :
                          (d d' : D) → CategoryTheory.MonoidalCategory.DayConvolution (ι.obj d) (ι.obj d')) →
                        (tensorObjIsoConvolution :
                            (d d' : D) →
                              ι.obj (tensorObj d d') ≅
                                CategoryTheory.MonoidalCategory.DayConvolution.convolution (ι.obj d) (ι.obj d')) →
                          (convolutionUnitApp :
                              (d d' : D) →
                                (x y : C) →
                                  CategoryTheory.MonoidalCategoryStruct.tensorObj ((ι.obj d).obj x) ((ι.obj d').obj y) ⟶
                                    (ι.obj (tensorObj d d')).obj
                                      (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)) →
                            autoParam
                                (∀ (d d' : D) (x y : C),
                                  convolutionUnitApp d d' x y =
                                    CategoryTheory.CategoryStruct.comp
                                      ((CategoryTheory.MonoidalCategory.DayConvolution.unit (ι.obj d) (ι.obj d')).app
                                        (x, y))
                                      ((tensorObjIsoConvolution d d').inv.app
                                        (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)))
                                CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.convolutionUnitApp_eq._autoParam →
                              (tensorHom :
                                  {d₁ d₂ d₁' d₂' : D} →
                                    (d₁ ⟶ d₂) → (d₁' ⟶ d₂') → (tensorObj d₁ d₁' ⟶ tensorObj d₂ d₂')) →
                                autoParam
                                    (∀ {d₁ d₂ d₁' d₂' : D} (f : d₁ ⟶ d₂) (f' : d₁' ⟶ d₂'),
                                      ι.map (tensorHom f f') =
                                        CategoryTheory.CategoryStruct.comp (tensorObjIsoConvolution d₁ d₁').hom
                                          (CategoryTheory.CategoryStruct.comp
                                            (CategoryTheory.MonoidalCategory.DayConvolution.map (ι.map f) (ι.map f'))
                                            (tensorObjIsoConvolution d₂ d₂').inv))
                                    CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.tensorHom_eq._autoParam →
                                  (tensorUnit : D) →
                                    CategoryTheory.MonoidalCategory.DayConvolutionUnit (ι.obj tensorUnit) →
                                      CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore
                                        C V D