-- Mathlib.CategoryTheory.Monoidal.Transport
CategoryTheory.Monoidal.InducingFunctorData.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.MonoidalCategoryStruct D] →
            {F : CategoryTheory.Functor D C} →
              (μIso :
                  (X Y : D) →
                    CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y) ≅
                      F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) →
                autoParam
                    (∀ (X : D) {Y₁ Y₂ : D} (f : Y₁ ⟶ Y₂),
                      F.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f) =
                        CategoryTheory.CategoryStruct.comp (μIso X Y₁).inv
                          (CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (F.map f)) (μIso X Y₂).hom))
                    CategoryTheory.Monoidal.InducingFunctorData.whiskerLeft_eq._autoParam →
                  autoParam
                      (∀ {X₁ X₂ : D} (f : X₁ ⟶ X₂) (Y : D),
                        F.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y) =
                          CategoryTheory.CategoryStruct.comp (μIso X₁ Y).inv
                            (CategoryTheory.CategoryStruct.comp
                              (CategoryTheory.MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj Y)) (μIso X₂ Y).hom))
                      CategoryTheory.Monoidal.InducingFunctorData.whiskerRight_eq._autoParam →
                    autoParam
                        (∀ {X₁ Y₁ X₂ Y₂ : D} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
                          F.map (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) =
                            CategoryTheory.CategoryStruct.comp (μIso X₁ X₂).inv
                              (CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.MonoidalCategoryStruct.tensorHom (F.map f) (F.map g)) (μIso Y₁ Y₂).hom))
                        CategoryTheory.Monoidal.InducingFunctorData.tensorHom_eq._autoParam →
                      (εIso :
                          CategoryTheory.MonoidalCategoryStruct.tensorUnit C ≅
                            F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) →
                        autoParam
                            (∀ (X Y Z : D),
                              F.map (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom =
                                (((μIso (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).symm ≪≫
                                      CategoryTheory.MonoidalCategory.tensorIso (μIso X Y).symm
                                        (CategoryTheory.Iso.refl (F.obj Z))) ≪≫
                                    CategoryTheory.MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z) ≪≫
                                      CategoryTheory.MonoidalCategory.tensorIso (CategoryTheory.Iso.refl (F.obj X))
                                          (μIso Y Z) ≪≫
                                        μIso X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).hom)
                            CategoryTheory.Monoidal.InducingFunctorData.associator_eq._autoParam →
                          autoParam
                              (∀ (X : D),
                                F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom =
                                  (((μIso (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) X).symm ≪≫
                                        CategoryTheory.MonoidalCategory.tensorIso εIso.symm
                                          (CategoryTheory.Iso.refl (F.obj X))) ≪≫
                                      CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj X)).hom)
                              CategoryTheory.Monoidal.InducingFunctorData.leftUnitor_eq._autoParam →
                            autoParam
                                (∀ (X : D),
                                  F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom =
                                    (((μIso X (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).symm ≪≫
                                          CategoryTheory.MonoidalCategory.tensorIso (CategoryTheory.Iso.refl (F.obj X))
                                            εIso.symm) ≪≫
                                        CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj X)).hom)
                                CategoryTheory.Monoidal.InducingFunctorData.rightUnitor_eq._autoParam →
                              CategoryTheory.Monoidal.InducingFunctorData F