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