-- Mathlib/CategoryTheory/Monoidal/Bimod.lean
theorem whisker_assoc_bimod {W X Y Z : Mon_ C} (M : Bimod W X) {N N' : Bimod X Y} (f : N ⟶ N')
    (P : Bimod Y Z) :
    whiskerRight (whiskerLeft M f) P =
      (associatorBimod M N P).hom ≫
        whiskerLeft M (whiskerRight f P) ≫ (associatorBimod M N' P).inv

Proof state:
case h.h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
W X Y Z : Mon_ C
M : Bimod W X
N N' : Bimod X Y
f : N ⟶ N'
P : Bimod Y Z
⊢ (M.X ◁ f.hom ≫
          colimit.ι (parallelPair (M.actRight ▷ N'.X) ((α_ M.X X.X N'.X).hom ≫ M.X ◁ N'.actLeft))
            WalkingParallelPair.one) ▷
        P.X ≫
      colimit.ι
        (parallelPair (TensorBimod.actRight M N' ▷ P.X)
          ((α_ (TensorBimod.X M N') Y.X P.X).hom ≫ TensorBimod.X M N' ◁ P.actLeft))
        WalkingParallelPair.one =
    (α_ M.X N.X P.X).hom ≫
      M.X ◁
          (f.hom ▷ P.X ≫
            colimit.ι (parallelPair (N'.actRight ▷ P.X) ((α_ N'.X Y.X P.X).hom ≫ N'.X ◁ P.actLeft))
              WalkingParallelPair.one) ≫
        (PreservesCoequalizer.iso (tensorLeft M.X) (N'.actRight ▷ P.X) ((α_ N'.X Y.X P.X).hom ≫ N'.X ◁ P.actLeft)).inv ≫
          coequalizer.desc
            ((α_ M.X N'.X P.X).inv ≫
              coequalizer.π (M.actRight ▷ N'.X) ((α_ M.X X.X N'.X).hom ≫ M.X ◁ N'.actLeft) ▷ P.X ≫
                coequalizer.π (TensorBimod.actRight M N' ▷ P.X)
                  ((α_ (TensorBimod.X M N') Y.X P.X).hom ≫ TensorBimod.X M N' ◁ P.actLeft))
            ⋯

Tactic:
slice_rhs 2 2 => rw [MonoidalCategory.whiskerLeft_comp]

Result:
case h.h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
W X Y Z : Mon_ C
M : Bimod W X
N N' : Bimod X Y
f : N ⟶ N'
P : Bimod Y Z
⊢ (M.X ◁ f.hom ≫
          colimit.ι (parallelPair (M.actRight ▷ N'.X) ((α_ M.X X.X N'.X).hom ≫ M.X ◁ N'.actLeft))
            WalkingParallelPair.one) ▷
        P.X ≫
      colimit.ι
        (parallelPair (TensorBimod.actRight M N' ▷ P.X)
          ((α_ (TensorBimod.X M N') Y.X P.X).hom ≫ TensorBimod.X M N' ◁ P.actLeft))
        WalkingParallelPair.one =
    (α_ M.X N.X P.X).hom ≫
      ((M.X ◁ f.hom ▷ P.X ≫
            M.X ◁
              colimit.ι (parallelPair (N'.actRight ▷ P.X) ((α_ N'.X Y.X P.X).hom ≫ N'.X ◁ P.actLeft))
                WalkingParallelPair.one) ≫
          (PreservesCoequalizer.iso (tensorLeft M.X) (N'.actRight ▷ P.X)
              ((α_ N'.X Y.X P.X).hom ≫ N'.X ◁ P.actLeft)).inv) ≫
        coequalizer.desc
          ((α_ M.X N'.X P.X).inv ≫
            coequalizer.π (M.actRight ▷ N'.X) ((α_ M.X X.X N'.X).hom ≫ M.X ◁ N'.actLeft) ▷ P.X ≫
              coequalizer.π (TensorBimod.actRight M N' ▷ P.X)
                ((α_ (TensorBimod.X M N') Y.X P.X).hom ≫ TensorBimod.X M N' ◁ P.actLeft))
          ⋯

Proof state:
case h.h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
W X Y Z : Mon_ C
M : Bimod W X
N N' : Bimod X Y
f : N ⟶ N'
P : Bimod Y Z
⊢ (tensorRight P.X).map (coequalizer.π (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft)) ≫
      colimMap
            (parallelPairHom (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) (M.actRight ▷ N'.X)
              ((α_ M.X X.X N'.X).hom ≫ M.X ◁ N'.actLeft) ((M.X ⊗ X.X) ◁ f.hom) (M.X ◁ f.hom) ⋯ ⋯) ▷
          P.X ≫
        colimit.ι
          (parallelPair (TensorBimod.actRight M N' ▷ P.X)
            ((α_ (TensorBimod.X M N') Y.X P.X).hom ≫ TensorBimod.X M N' ◁ P.actLeft))
          WalkingParallelPair.one =
    (tensorRight P.X).map (coequalizer.π (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft)) ≫
      (((PreservesCoequalizer.iso (tensorRight P.X) (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft)).inv ≫
            coequalizer.desc
              ((α_ M.X N.X P.X).hom ≫
                M.X ◁ coequalizer.π (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) ≫
                  coequalizer.π (M.actRight ▷ TensorBimod.X N P)
                    ((α_ M.X X.X (TensorBimod.X N P)).hom ≫ M.X ◁ TensorBimod.actLeft N P))
              ⋯) ≫
          colimMap
            (parallelPairHom (M.actRight ▷ TensorBimod.X N P)
              ((α_ M.X X.X (TensorBimod.X N P)).hom ≫ M.X ◁ TensorBimod.actLeft N P) (M.actRight ▷ TensorBimod.X N' P)
              ((α_ M.X X.X (TensorBimod.X N' P)).hom ≫ M.X ◁ TensorBimod.actLeft N' P)
              ((M.X ⊗ X.X) ◁
                colimMap
                  (parallelPairHom (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) (N'.actRight ▷ P.X)
                    ((α_ N'.X Y.X P.X).hom ≫ N'.X ◁ P.actLeft) (f.hom ▷ Y.X ▷ P.X) (f.hom ▷ P.X) ⋯ ⋯))
              (M.X ◁
                colimMap
                  (parallelPairHom (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) (N'.actRight ▷ P.X)
                    ((α_ N'.X Y.X P.X).hom ≫ N'.X ◁ P.actLeft) (f.hom ▷ Y.X ▷ P.X) (f.hom ▷ P.X) ⋯ ⋯))
              ⋯ ⋯)) ≫
        AssociatorBimod.inv M N' P

Tactic:
rw [tensorRight_map]

Result:
case h.h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
W X Y Z : Mon_ C
M : Bimod W X
N N' : Bimod X Y
f : N ⟶ N'
P : Bimod Y Z
⊢ coequalizer.π (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ▷ P.X ≫
      colimMap
            (parallelPairHom (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) (M.actRight ▷ N'.X)
              ((α_ M.X X.X N'.X).hom ≫ M.X ◁ N'.actLeft) ((M.X ⊗ X.X) ◁ f.hom) (M.X ◁ f.hom) ⋯ ⋯) ▷
          P.X ≫
        colimit.ι
          (parallelPair (TensorBimod.actRight M N' ▷ P.X)
            ((α_ (TensorBimod.X M N') Y.X P.X).hom ≫ TensorBimod.X M N' ◁ P.actLeft))
          WalkingParallelPair.one =
    coequalizer.π (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ▷ P.X ≫
      (((PreservesCoequalizer.iso (tensorRight P.X) (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft)).inv ≫
            coequalizer.desc
              ((α_ M.X N.X P.X).hom ≫
                M.X ◁ coequalizer.π (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) ≫
                  coequalizer.π (M.actRight ▷ TensorBimod.X N P)
                    ((α_ M.X X.X (TensorBimod.X N P)).hom ≫ M.X ◁ TensorBimod.actLeft N P))
              ⋯) ≫
          colimMap
            (parallelPairHom (M.actRight ▷ TensorBimod.X N P)
              ((α_ M.X X.X (TensorBimod.X N P)).hom ≫ M.X ◁ TensorBimod.actLeft N P) (M.actRight ▷ TensorBimod.X N' P)
              ((α_ M.X X.X (TensorBimod.X N' P)).hom ≫ M.X ◁ TensorBimod.actLeft N' P)
              ((M.X ⊗ X.X) ◁
                colimMap
                  (parallelPairHom (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) (N'.actRight ▷ P.X)
                    ((α_ N'.X Y.X P.X).hom ≫ N'.X ◁ P.actLeft) (f.hom ▷ Y.X ▷ P.X) (f.hom ▷ P.X) ⋯ ⋯))
              (M.X ◁
                colimMap
                  (parallelPairHom (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) (N'.actRight ▷ P.X)
                    ((α_ N'.X Y.X P.X).hom ≫ N'.X ◁ P.actLeft) (f.hom ▷ Y.X ▷ P.X) (f.hom ▷ P.X) ⋯ ⋯))
              ⋯ ⋯)) ≫
        AssociatorBimod.inv M N' P