-- 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 P.X).hom ≫
      M.X ◁
          (N.X ◁ f.hom ≫
            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 : 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))
          ⋯

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.π
        ({ X := TensorBimod.X M N, actLeft := TensorBimod.actLeft M N, one_actLeft := ⋯, left_assoc := ⋯,
              actRight := TensorBimod.actRight M N, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.actRight ▷
          P.X)
        ((α_
              { X := TensorBimod.X M N, actLeft := TensorBimod.actLeft M N, one_actLeft := ⋯, left_assoc := ⋯,
                  actRight := TensorBimod.actRight M N, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.X
              Y.X P.X).hom ≫
          { X := TensorBimod.X M N, actLeft := TensorBimod.actLeft M N, one_actLeft := ⋯, left_assoc := ⋯,
                actRight := TensorBimod.actRight M N, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.X ◁
            P.actLeft) ≫
      ({ X := TensorBimod.X M N, actLeft := TensorBimod.actLeft M N, one_actLeft := ⋯, left_assoc := ⋯,
              actRight := TensorBimod.actRight M N, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.whiskerLeft
          f).hom =
    coequalizer.π
        ({ X := TensorBimod.X M N, actLeft := TensorBimod.actLeft M N, one_actLeft := ⋯, left_assoc := ⋯,
              actRight := TensorBimod.actRight M N, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.actRight ▷
          P.X)
        ((α_
              { X := TensorBimod.X M N, actLeft := TensorBimod.actLeft M N, one_actLeft := ⋯, left_assoc := ⋯,
                  actRight := TensorBimod.actRight M N, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.X
              Y.X P.X).hom ≫
          { X := TensorBimod.X M N, actLeft := TensorBimod.actLeft M N, one_actLeft := ⋯, left_assoc := ⋯,
                actRight := TensorBimod.actRight M N, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.X ◁
            P.actLeft) ≫
      ((isoOfIso
              { hom := AssociatorBimod.hom M N P, inv := AssociatorBimod.inv M N P, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
              ⋯).hom ≫
          M.whiskerLeft (N.whiskerLeft f) ≫
            (isoOfIso
                { hom := AssociatorBimod.hom M N P', inv := AssociatorBimod.inv M N P', hom_inv_id := ⋯,
                  inv_hom_id := ⋯ }
                ⋯ ⋯).inv).hom

Tactic:
dsimp

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.π (TensorBimod.actRight M N ▷ P.X)
        ((α_ (TensorBimod.X M N) Y.X P.X).hom ≫ TensorBimod.X M N ◁ P.actLeft) ≫
      colimMap
        (parallelPairHom (TensorBimod.actRight M N ▷ P.X)
          ((α_ (TensorBimod.X M N) Y.X P.X).hom ≫ TensorBimod.X M N ◁ P.actLeft) (TensorBimod.actRight M N ▷ P'.X)
          ((α_ (TensorBimod.X M N) Y.X P'.X).hom ≫ TensorBimod.X M N ◁ P'.actLeft) ((TensorBimod.X M N ⊗ Y.X) ◁ f.hom)
          (TensorBimod.X M N ◁ f.hom) ⋯ ⋯) =
    coequalizer.π (TensorBimod.actRight M N ▷ P.X)
        ((α_ (TensorBimod.X M N) Y.X P.X).hom ≫ TensorBimod.X M N ◁ P.actLeft) ≫
      AssociatorBimod.hom M 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) ((N.X ⊗ Y.X) ◁ f.hom) (N.X ◁ f.hom) ⋯ ⋯))
              (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) ((N.X ⊗ Y.X) ◁ f.hom) (N.X ◁ f.hom) ⋯ ⋯))
              ⋯ ⋯) ≫
          AssociatorBimod.inv M N P'