-- Mathlib.CategoryTheory.Monoidal.Transport
CategoryTheory.Monoidal.InducingFunctorData.mk.injEq : ∀ {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)