-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.CoreMonoidal.mk'_μIso : ∀ {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))
  (μIso_inv_natural_left :
    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)
  (μIso_inv_natural_right :
    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)
  (oplax_associativity :
    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)
  (oplax_left_unitality :
    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)
  (oplax_right_unitality :
    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)
  (X Y : C),
  (CategoryTheory.Functor.CoreMonoidal.mk' εIso μIso μIso_inv_natural_left μIso_inv_natural_right oplax_associativity
          oplax_left_unitality oplax_right_unitality).μIso
      X Y =
    μIso X Y