-- Mathlib.CategoryTheory.Monoidal.Braided.Transport
CategoryTheory.Functor.CoreMonoidal.mk.congr_simp : ∀ {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 εIso_1 :
    CategoryTheory.MonoidalCategoryStruct.tensorUnit D ≅ F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
  (e_εIso : εIso = εIso_1)
  (μIso μIso_1 :
    (X Y : C) →
      CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y) ≅
        F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))
  (e_μIso : μIso = μIso_1)
  (μIso_hom_natural_left :
    ∀ {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')))
  (μIso_hom_natural_right :
    ∀ {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)))
  (associativity :
    ∀ (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))
  (left_unitality :
    ∀ (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)))
  (right_unitality :
    ∀ (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))),
  { ε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_right := ⋯, associativity := ⋯,
      left_unitality := ⋯, right_unitality := ⋯ }