-- Mathlib.CategoryTheory.Monoidal.Functor
/-- Alternative constructor for `CoreMonoidal`, for which the axioms are stated
in terms on the inverses of `εIso` and `μIso`.  -/
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 (μIso X X').inv
                            (CategoryTheory.MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X')) =
                          CategoryTheory.CategoryStruct.comp
                            (F.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X')) (μIso Y X').inv)
                      CategoryTheory.Functor.CoreMonoidal.mk'._auto_1 →
                    autoParam
                        (∀ {X Y : C} (X' : C) (f : X ⟶ Y),
                          CategoryTheory.CategoryStruct.comp (μIso X' X).inv
                              (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f)) =
                            CategoryTheory.CategoryStruct.comp
                              (F.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X' f)) (μIso X' Y).inv)
                        CategoryTheory.Functor.CoreMonoidal.mk'._auto_3 →
                      autoParam
                          (∀ (X Y Z : C),
                            CategoryTheory.CategoryStruct.comp
                                (μIso (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).inv
                                (CategoryTheory.CategoryStruct.comp
                                  (CategoryTheory.MonoidalCategoryStruct.whiskerRight (μIso X Y).inv (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
                                  (μIso X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).inv
                                  (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (μIso Y Z).inv)))
                          CategoryTheory.Functor.CoreMonoidal.mk'._auto_5 →
                        autoParam
                            (∀ (X : C),
                              (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj X)).inv =
                                CategoryTheory.CategoryStruct.comp
                                  (F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv)
                                  (CategoryTheory.CategoryStruct.comp
                                    (μIso (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X).inv
                                    (CategoryTheory.MonoidalCategoryStruct.whiskerRight εIso.inv (F.obj X))))
                            CategoryTheory.Functor.CoreMonoidal.mk'._auto_7 →
                          autoParam
                              (∀ (X : C),
                                (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj X)).inv =
                                  CategoryTheory.CategoryStruct.comp
                                    (F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv)
                                    (CategoryTheory.CategoryStruct.comp
                                      (μIso X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
                                      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) εIso.inv)))
                              CategoryTheory.Functor.CoreMonoidal.mk'._auto_9 →
                            F.CoreMonoidal