-- 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:
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
⊢ whiskerRight (M.whiskerLeft f) P =
    (isoOfIso { hom := AssociatorBimod.hom M N P, inv := AssociatorBimod.inv M N P, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
          ⋯).hom ≫
      M.whiskerLeft (whiskerRight f P) ≫
        (isoOfIso
            { hom := AssociatorBimod.hom M N' P, inv := AssociatorBimod.inv M N' P, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
            ⋯).inv

Tactic:
ext

Result:
case 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
⊢ (whiskerRight (M.whiskerLeft f) P).hom =
    ((isoOfIso { hom := AssociatorBimod.hom M N P, inv := AssociatorBimod.inv M N P, hom_inv_id := ⋯, inv_hom_id := ⋯ }
            ⋯ ⋯).hom ≫
        M.whiskerLeft (whiskerRight f P) ≫
          (isoOfIso
              { hom := AssociatorBimod.hom M N' P, inv := AssociatorBimod.inv M N' P, hom_inv_id := ⋯, inv_hom_id := ⋯ }
              ⋯ ⋯).inv).hom

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 ≫
        (α_ 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 3 => rw [associator_inv_naturality_middle]

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 N.X P.X).inv ≫ (M.X ◁ f.hom) ▷ P.X) ≫
          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
⊢ (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) ≫
          colimit.ι
            (parallelPair (M.actRight ▷ TensorBimod.X N' P)
              ((α_ M.X X.X (TensorBimod.X N' P)).hom ≫ M.X ◁ TensorBimod.actLeft N' P))
            WalkingParallelPair.one) ≫
        AssociatorBimod.inv M N' P

Tactic:
dsimp [AssociatorBimod.inv]

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 ≫
              colimit.ι (parallelPair (N'.actRight ▷ P.X) ((α_ N'.X Y.X P.X).hom ≫ N'.X ◁ P.actLeft))
                WalkingParallelPair.one) ≫
          colimit.ι
            (parallelPair (M.actRight ▷ TensorBimod.X N' P)
              ((α_ M.X X.X (TensorBimod.X N' P)).hom ≫ M.X ◁ TensorBimod.actLeft N' P))
            WalkingParallelPair.one) ≫
        coequalizer.desc (AssociatorBimod.invAux M N' P) ⋯