-- 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
slice_lhs :
  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 ◁
                      𝟙
                        (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (F.obj X) (F.obj Y))
                          (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)))
⊢ 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)))

Tactic:
slice_lhs 5 6 =>
      rw [← whiskerLeft_comp, hom_inv_whiskerRight]

Premises used: CategoryTheory.MonoidalCategory.hom_inv_whiskerRight, CategoryTheory.MonoidalCategory.whiskerLeft_comp