-- Module: Mathlib.CategoryTheory.Monoidal.Transport
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategoryStruct.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
inst_4 : F.Faithful
fData : InducingFunctorData F
W X Y Z : D
simp :
  Iso.inv (fData.μIso (tensorObj.{v₂, u₂} (𝒞 := inst_2) W X) Y) ▷ F.obj Z ≫
      (fData.μIso W X).inv ▷ F.obj Y ▷ F.obj Z ≫
        Iso.hom (α_ (F.obj W) (F.obj X) (F.obj Y)) ▷ F.obj Z ≫
          Iso.hom (α_ (F.obj W) (tensorObj.{v₁, u₁} (𝒞 := inst) (F.obj X) (F.obj Y)) (F.obj Z)) ≫
            F.obj W ◁ (fData.μIso X Y).hom ▷ F.obj Z ≫
              F.obj W ◁ (fData.μIso X Y).inv ▷ F.obj Z ≫
                F.obj W ◁ Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫
                  F.obj W ◁ F.obj X ◁ (fData.μIso Y Z).hom ≫
                    F.obj W ◁ Iso.hom (fData.μIso X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)) ≫
                      Iso.hom
                        (fData.μIso W (tensorObj.{v₂, u₂} (𝒞 := inst_2) X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z))) =
    Iso.inv (fData.μIso (tensorObj.{v₂, u₂} (𝒞 := inst_2) W X) Y) ▷ F.obj Z ≫
      Iso.hom (α_ (F.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) W X)) (F.obj Y) (F.obj Z)) ≫
        F.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) W X) ◁ (fData.μIso Y Z).hom ≫
          (fData.μIso W X).inv ▷ F.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z) ≫
            Iso.hom (α_ (F.obj W) (F.obj X) (F.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z))) ≫
              F.obj W ◁ Iso.hom (fData.μIso X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)) ≫
                Iso.hom (fData.μIso W (tensorObj.{v₂, u₂} (𝒞 := inst_2) X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)))
⊢ F.map (Iso.hom (α_ W X Y) ▷ Z ≫ Iso.hom (α_ W (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y) Z) ≫ W ◁ Iso.hom (α_ X Y Z)) =
    F.map
      (Iso.hom (α_ (tensorObj.{v₂, u₂} (𝒞 := inst_2) W X) Y Z) ≫
        Iso.hom (α_ W X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)))

Tactic:
simp only [Functor.map_comp, fData.whiskerRight_eq, fData.associator_eq, Iso.trans_assoc,
      Iso.trans_hom, Iso.symm_hom, tensorIso_hom, Iso.refl_hom, tensorHom_id, id_tensorHom,
      comp_whiskerRight, whisker_assoc, assoc, fData.whiskerLeft_eq, whiskerLeft_comp,
      Iso.hom_inv_id_assoc, whiskerLeft_hom_inv_assoc, hom_inv_whiskerRight_assoc,
      Iso.inv_hom_id_assoc, Iso.cancel_iso_inv_left]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.id_tensorHom, CategoryTheory.Monoidal.InducingFunctorData.associator_eq, CategoryTheory.MonoidalCategory.hom_inv_whiskerRight_assoc, CategoryTheory.MonoidalCategory.tensorIso_hom, CategoryTheory.Iso.symm_hom, CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.MonoidalCategory.comp_whiskerRight, CategoryTheory.Iso.cancel_iso_inv_left, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.Iso.trans_assoc, CategoryTheory.Monoidal.InducingFunctorData.whiskerRight_eq, CategoryTheory.Iso.trans_hom, CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.Monoidal.InducingFunctorData.whiskerLeft_eq, CategoryTheory.Functor.map_comp, CategoryTheory.MonoidalCategory.whiskerLeft_hom_inv_assoc, CategoryTheory.MonoidalCategory.whisker_assoc, CategoryTheory.Iso.refl_hom, CategoryTheory.MonoidalCategory.tensorHom_id