-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.CoreMonoidal.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} →
              (εIso :
                  CategoryTheory.MonoidalCategoryStruct.tensorUnit D ≅
                    F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) →
                (μIso :
                    (X Y : C) →
                      CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y) ≅
                        F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) →
                  autoParam
                      (∀ {X Y : C} (f : X ⟶ Y) (X' : C),
                        CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X')) (μIso Y X').hom =
                          CategoryTheory.CategoryStruct.comp (μIso X X').hom
                            (F.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X')))
                      CategoryTheory.Functor.CoreMonoidal.μIso_hom_natural_left._autoParam →
                    autoParam
                        (∀ {X Y : C} (X' : C) (f : X ⟶ Y),
                          CategoryTheory.CategoryStruct.comp
                              (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f)) (μIso X' Y).hom =
                            CategoryTheory.CategoryStruct.comp (μIso X' X).hom
                              (F.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X' f)))
                        CategoryTheory.Functor.CoreMonoidal.μIso_hom_natural_right._autoParam →
                      autoParam
                          (∀ (X Y Z : C),
                            CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.MonoidalCategoryStruct.whiskerRight (μIso X Y).hom (F.obj Z))
                                (CategoryTheory.CategoryStruct.comp
                                  (μIso (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).hom
                                  (F.map (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)) =
                              CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom
                                (CategoryTheory.CategoryStruct.comp
                                  (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (μIso Y Z).hom)
                                  (μIso X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).hom))
                          CategoryTheory.Functor.CoreMonoidal.associativity._autoParam →
                        autoParam
                            (∀ (X : C),
                              (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj X)).hom =
                                CategoryTheory.CategoryStruct.comp
                                  (CategoryTheory.MonoidalCategoryStruct.whiskerRight εIso.hom (F.obj X))
                                  (CategoryTheory.CategoryStruct.comp
                                    (μIso (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X).hom
                                    (F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom)))
                            CategoryTheory.Functor.CoreMonoidal.left_unitality._autoParam →
                          autoParam
                              (∀ (X : C),
                                (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj X)).hom =
                                  CategoryTheory.CategoryStruct.comp
                                    (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) εIso.hom)
                                    (CategoryTheory.CategoryStruct.comp
                                      (μIso X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom
                                      (F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom)))
                              CategoryTheory.Functor.CoreMonoidal.right_unitality._autoParam →
                            F.CoreMonoidal