-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.OplaxMonoidal.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F : CategoryTheory.Functor C D} →
              (η :
                  F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ⟶
                    CategoryTheory.MonoidalCategoryStruct.tensorUnit D) →
                (δ :
                    (X Y : C) →
                      F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) ⟶
                        CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)) →
                  autoParam
                      (∀ {X Y : C} (f : X ⟶ Y) (X' : C),
                        CategoryTheory.CategoryStruct.comp (δ X X')
                            (CategoryTheory.MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X')) =
                          CategoryTheory.CategoryStruct.comp
                            (F.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X')) (δ Y X'))
                      CategoryTheory.Functor.OplaxMonoidal.δ_natural_left._autoParam →
                    autoParam
                        (∀ {X Y : C} (X' : C) (f : X ⟶ Y),
                          CategoryTheory.CategoryStruct.comp (δ X' X)
                              (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f)) =
                            CategoryTheory.CategoryStruct.comp
                              (F.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X' f)) (δ X' Y))
                        CategoryTheory.Functor.OplaxMonoidal.δ_natural_right._autoParam →
                      autoParam
                          (∀ (X Y Z : C),
                            CategoryTheory.CategoryStruct.comp
                                (δ (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)
                                (CategoryTheory.CategoryStruct.comp
                                  (CategoryTheory.MonoidalCategoryStruct.whiskerRight (δ X Y) (F.obj Z))
                                  (CategoryTheory.MonoidalCategoryStruct.associator (F.obj X) (F.obj Y)
                                      (F.obj Z)).hom) =
                              CategoryTheory.CategoryStruct.comp
                                (F.map (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)
                                (CategoryTheory.CategoryStruct.comp
                                  (δ X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))
                                  (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (δ Y Z))))
                          CategoryTheory.Functor.OplaxMonoidal.oplax_associativity._autoParam →
                        autoParam
                            (∀ (X : C),
                              (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj X)).inv =
                                CategoryTheory.CategoryStruct.comp
                                  (F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv)
                                  (CategoryTheory.CategoryStruct.comp
                                    (δ (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X)
                                    (CategoryTheory.MonoidalCategoryStruct.whiskerRight η (F.obj X))))
                            CategoryTheory.Functor.OplaxMonoidal.oplax_left_unitality._autoParam →
                          autoParam
                              (∀ (X : C),
                                (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj X)).inv =
                                  CategoryTheory.CategoryStruct.comp
                                    (F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv)
                                    (CategoryTheory.CategoryStruct.comp
                                      (δ X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
                                      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) η)))
                              CategoryTheory.Functor.OplaxMonoidal.oplax_right_unitality._autoParam →
                            F.OplaxMonoidal