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