-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.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] →
                [inst_5 : CategoryTheory.MonoidalCategoryStruct D] →
                  (ι : CategoryTheory.Functor D (CategoryTheory.Functor C V)) →
                    (convolutionExtensionUnit :
                        (d d' : D) →
                          CategoryTheory.MonoidalCategory.externalProduct (ι.obj d) (ι.obj d') ⟶
                            (CategoryTheory.MonoidalCategory.tensor C).comp
                              (ι.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj d d'))) →
                      ((d d' : D) →
                          (CategoryTheory.Functor.LeftExtension.mk
                              (ι.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj d d'))
                              (convolutionExtensionUnit d d')).IsPointwiseLeftKanExtension) →
                        (unitUnit :
                            CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶
                              (ι.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).obj
                                (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) →
                          (CategoryTheory.Functor.LeftExtension.mk
                                (ι.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit D))
                                { app := fun x => unitUnit, naturality := ⋯ }).IsPointwiseLeftKanExtension →
                            autoParam ι.Faithful
                                CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.faithful_ι._autoParam →
                              (∀ {d₁ d₂ d₁' d₂' : D} (f₁ : d₁ ⟶ d₁') (f₂ : d₂ ⟶ d₂') (x y : C),
                                  CategoryTheory.CategoryStruct.comp ((convolutionExtensionUnit d₁ d₂).app (x, y))
                                      ((ι.map (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ f₂)).app
                                        (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)) =
                                    CategoryTheory.CategoryStruct.comp
                                      (CategoryTheory.MonoidalCategoryStruct.tensorHom ((ι.map f₁).app x)
                                        ((ι.map f₂).app y))
                                      ((convolutionExtensionUnit d₁' d₂').app (x, y))) →
                                (∀ (d₁ : D) {d₂ d₂' : D} (f₂ : d₂ ⟶ d₂') (x y : C),
                                    CategoryTheory.CategoryStruct.comp ((convolutionExtensionUnit d₁ d₂).app (x, y))
                                        ((ι.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft d₁ f₂)).app
                                          (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)) =
                                      CategoryTheory.CategoryStruct.comp
                                        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft ((ι.obj d₁).obj x)
                                          ((ι.map f₂).app y))
                                        ((convolutionExtensionUnit d₁ d₂').app (x, y))) →
                                  (∀ {d₁ d₁' : D} (f₁ : d₁ ⟶ d₁') (d₂ : D) (x y : C),
                                      CategoryTheory.CategoryStruct.comp ((convolutionExtensionUnit d₁ d₂).app (x, y))
                                          ((ι.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f₁ d₂)).app
                                            (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)) =
                                        CategoryTheory.CategoryStruct.comp
                                          (CategoryTheory.MonoidalCategoryStruct.whiskerRight ((ι.map f₁).app x)
                                            ((ι.obj d₂).obj y))
                                          ((convolutionExtensionUnit d₁' d₂).app (x, y))) →
                                    (∀ (d d' d'' : D) (x y z : C),
                                        CategoryTheory.CategoryStruct.comp
                                            (CategoryTheory.MonoidalCategoryStruct.whiskerRight
                                              ((convolutionExtensionUnit d d').app (x, y)) ((ι.obj d'').obj z))
                                            (CategoryTheory.CategoryStruct.comp
                                              ((convolutionExtensionUnit
                                                    (CategoryTheory.MonoidalCategoryStruct.tensorObj d d') d'').app
                                                (CategoryTheory.MonoidalCategoryStruct.tensorObj x y, z))
                                              ((ι.map
                                                    (CategoryTheory.MonoidalCategoryStruct.associator d d' d'').hom).app
                                                (CategoryTheory.MonoidalCategoryStruct.tensorObj
                                                  (CategoryTheory.MonoidalCategoryStruct.tensorObj x y) z))) =
                                          CategoryTheory.CategoryStruct.comp
                                            (CategoryTheory.MonoidalCategoryStruct.associator ((ι.obj d).obj x)
                                                ((ι.obj d', ι.obj d'').1.obj (y, z).1)
                                                ((ι.obj d', ι.obj d'').2.obj (y, z).2)).hom
                                            (CategoryTheory.CategoryStruct.comp
                                              (CategoryTheory.MonoidalCategoryStruct.whiskerLeft ((ι.obj d).obj x)
                                                ((convolutionExtensionUnit d' d'').app (y, z)))
                                              (CategoryTheory.CategoryStruct.comp
                                                ((convolutionExtensionUnit d
                                                      (CategoryTheory.MonoidalCategoryStruct.tensorObj d' d'')).app
                                                  (x, CategoryTheory.MonoidalCategoryStruct.tensorObj y z))
                                                ((ι.obj
                                                      (CategoryTheory.MonoidalCategoryStruct.tensorObj d
                                                        (CategoryTheory.MonoidalCategoryStruct.tensorObj d' d''))).map
                                                  (CategoryTheory.MonoidalCategoryStruct.associator
                                                      (x, CategoryTheory.MonoidalCategoryStruct.tensorObj y z).1 y
                                                      z).inv)))) →
                                      (∀ (d : D) (y : C),
                                          CategoryTheory.CategoryStruct.comp
                                              (CategoryTheory.MonoidalCategoryStruct.whiskerRight unitUnit
                                                ((ι.obj d).obj y))
                                              (CategoryTheory.CategoryStruct.comp
                                                ((convolutionExtensionUnit
                                                      (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) d).app
                                                  (CategoryTheory.MonoidalCategoryStruct.tensorUnit C, y))
                                                ((ι.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor d).hom).app
                                                  (CategoryTheory.MonoidalCategoryStruct.tensorObj
                                                    (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) y))) =
                                            CategoryTheory.CategoryStruct.comp
                                              (CategoryTheory.MonoidalCategoryStruct.leftUnitor ((ι.obj d).obj y)).hom
                                              ((ι.obj d).map
                                                (CategoryTheory.MonoidalCategoryStruct.leftUnitor y).inv)) →
                                        (∀ (d : D) (y : C),
                                            CategoryTheory.CategoryStruct.comp
                                                (CategoryTheory.MonoidalCategoryStruct.whiskerLeft ((ι.obj d).obj y)
                                                  unitUnit)
                                                (CategoryTheory.CategoryStruct.comp
                                                  ((convolutionExtensionUnit d
                                                        (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).app
                                                    (y, CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
                                                  ((ι.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor d).hom).app
                                                    (CategoryTheory.MonoidalCategoryStruct.tensorObj y
                                                      (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))) =
                                              CategoryTheory.CategoryStruct.comp
                                                (CategoryTheory.MonoidalCategoryStruct.rightUnitor
                                                    ((ι.obj d).obj y)).hom
                                                ((ι.obj d).map
                                                  (CategoryTheory.MonoidalCategoryStruct.rightUnitor y).inv)) →
                                          CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct C V
                                            D