-- Mathlib/CategoryTheory/Monoidal/Bimod.lean
theorem comp_whiskerLeft_bimod {W X Y Z : Mon_ C} (M : Bimod W X) (N : Bimod X Y)
    {P P' : Bimod Y Z} (f : P ⟶ P') :
    whiskerLeft (M.tensorBimod N) f =
      (associatorBimod M N P).hom ≫
        whiskerLeft M (whiskerLeft N f) ≫ (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 : Bimod X Y
P P' : Bimod Y Z
f : P ⟶ P'
⊢ coequalizer.π (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ▷ P.X ≫
      coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ f.hom ≫
        colimit.ι
          (parallelPair (TensorBimod.actRight M N ▷ P'.X)
            ((α_ (coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft)) Y.X P'.X).hom ≫
              coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ P'.actLeft))
          WalkingParallelPair.one =
    ((M.X ⊗ N.X) ◁ f.hom ≫ 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_lhs 1 2 => rw [← whisker_exchange]

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 : Bimod X Y
P P' : Bimod Y Z
f : P ⟶ P'
⊢ ((M.X ⊗ N.X) ◁ f.hom ≫ coequalizer.π (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ▷ P'.X) ≫
      colimit.ι
        (parallelPair (TensorBimod.actRight M N ▷ P'.X)
          ((α_ (coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft)) Y.X P'.X).hom ≫
            coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ P'.actLeft))
        WalkingParallelPair.one =
    ((M.X ⊗ N.X) ◁ f.hom ≫ 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 : Bimod X Y
P P' : Bimod Y Z
f : P ⟶ P'
⊢ coequalizer.π (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ▷ P.X ≫
      coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ f.hom ≫
        colimit.ι
          (parallelPair (TensorBimod.actRight M N ▷ P'.X)
            ((α_ (coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft)) Y.X P'.X).hom ≫
              coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ P'.actLeft))
          WalkingParallelPair.one =
    (α_ M.X N.X P.X).hom ≫
      ((M.X ◁ N.X ◁ f.hom ≫
            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))
          ⋯

Tactic:
slice_rhs 3 5 => rw [id_tensor_π_preserves_coequalizer_inv_desc]

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 : Bimod X Y
P P' : Bimod Y Z
f : P ⟶ P'
⊢ coequalizer.π (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ▷ P.X ≫
      coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ f.hom ≫
        colimit.ι
          (parallelPair (TensorBimod.actRight M N ▷ P'.X)
            ((α_ (coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft)) Y.X P'.X).hom ≫
              coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ P'.actLeft))
          WalkingParallelPair.one =
    (α_ M.X N.X P.X).hom ≫
      M.X ◁ N.X ◁ f.hom ≫
        (α_ 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)