-- Mathlib/CategoryTheory/Monoidal/Bimod.lean
theorem triangle_bimod {X Y Z : Mon_ C} (M : Bimod X Y) (N : Bimod Y Z) :
    (associatorBimod M (regular Y) N).hom ≫ whiskerLeft M (leftUnitorBimod N).hom =
      whiskerRight (rightUnitorBimod M).hom N

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)
X Y Z : Mon_ C
M : Bimod X Y
N : Bimod Y Z
⊢ ((α_ M.X Y.X N.X).hom ≫
        M.X ◁ coequalizer.π (Y.mul ▷ N.X) ((α_ Y.X Y.X N.X).hom ≫ Y.X ◁ N.actLeft) ≫
          coequalizer.π
            (M.actRight ▷
              TensorBimod.X
                { X := Y.X, actLeft := Y.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := Y.mul, actRight_one := ⋯,
                  right_assoc := ⋯, middle_assoc := ⋯ }
                N)
            ((α_ M.X Y.X
                  (TensorBimod.X
                    { X := Y.X, actLeft := Y.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := Y.mul,
                      actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }
                    N)).hom ≫
              M.X ◁
                TensorBimod.actLeft
                  { X := Y.X, actLeft := Y.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := Y.mul, actRight_one := ⋯,
                    right_assoc := ⋯, middle_assoc := ⋯ }
                  N)) ≫
      colimMap
        (parallelPairHom
          (M.actRight ▷
            TensorBimod.X
              { X := Y.X, actLeft := Y.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := Y.mul, actRight_one := ⋯,
                right_assoc := ⋯, middle_assoc := ⋯ }
              N)
          ((α_ M.X Y.X
                (TensorBimod.X
                  { X := Y.X, actLeft := Y.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := Y.mul, actRight_one := ⋯,
                    right_assoc := ⋯, middle_assoc := ⋯ }
                  N)).hom ≫
            M.X ◁
              TensorBimod.actLeft
                { X := Y.X, actLeft := Y.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := Y.mul, actRight_one := ⋯,
                  right_assoc := ⋯, middle_assoc := ⋯ }
                N)
          (M.actRight ▷ N.X) ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft) ((M.X ⊗ Y.X) ◁ LeftUnitorBimod.hom N)
          (M.X ◁ LeftUnitorBimod.hom N) ⋯ ⋯) =
    coequalizer.π (M.actRight ▷ Y.X) ((α_ M.X Y.X Y.X).hom ≫ M.X ◁ Y.mul) ▷ N.X ≫
      coequalizer.desc M.actRight ⋯ ▷ N.X ≫
        colimit.ι (parallelPair (M.actRight ▷ N.X) ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft)) WalkingParallelPair.one

Tactic:
slice_lhs 3 4 => rw [ι_colimMap, parallelPairHom_app_one]

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)
X Y Z : Mon_ C
M : Bimod X Y
N : Bimod Y Z
⊢ (α_ M.X Y.X N.X).hom ≫
      M.X ◁ coequalizer.π (Y.mul ▷ N.X) ((α_ Y.X Y.X N.X).hom ≫ Y.X ◁ N.actLeft) ≫
        M.X ◁ LeftUnitorBimod.hom N ≫
          colimit.ι (parallelPair (M.actRight ▷ N.X) ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft)) WalkingParallelPair.one =
    coequalizer.π (M.actRight ▷ Y.X) ((α_ M.X Y.X Y.X).hom ≫ M.X ◁ Y.mul) ▷ N.X ≫
      coequalizer.desc M.actRight ⋯ ▷ N.X ≫
        colimit.ι (parallelPair (M.actRight ▷ N.X) ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft)) WalkingParallelPair.one

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)
X Y Z : Mon_ C
M : Bimod X Y
N : Bimod Y Z
⊢ (tensorRight N.X).map
        (coequalizer.π (M.actRight ▷ (regular Y).X) ((α_ M.X Y.X (regular Y).X).hom ≫ M.X ◁ (regular Y).actLeft)) ≫
      ((PreservesCoequalizer.iso (tensorRight N.X) (M.actRight ▷ Y.X) ((α_ M.X Y.X Y.X).hom ≫ M.X ◁ Y.mul)).inv ≫
          coequalizer.desc
            ((α_ M.X Y.X N.X).hom ≫
              M.X ◁ coequalizer.π (Y.mul ▷ N.X) ((α_ Y.X Y.X N.X).hom ≫ Y.X ◁ N.actLeft) ≫
                coequalizer.π (M.actRight ▷ TensorBimod.X (regular Y) N)
                  ((α_ M.X Y.X (TensorBimod.X (regular Y) N)).hom ≫ M.X ◁ TensorBimod.actLeft (regular Y) N))
            ⋯) ≫
        colimMap
          (parallelPairHom (M.actRight ▷ TensorBimod.X (regular Y) N)
            ((α_ M.X Y.X (TensorBimod.X (regular Y) N)).hom ≫ M.X ◁ TensorBimod.actLeft (regular Y) N)
            (M.actRight ▷ N.X) ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft) ((M.X ⊗ Y.X) ◁ LeftUnitorBimod.hom N)
            (M.X ◁ LeftUnitorBimod.hom N) ⋯ ⋯) =
    (tensorRight N.X).map
        (coequalizer.π (M.actRight ▷ (regular Y).X) ((α_ M.X Y.X (regular Y).X).hom ≫ M.X ◁ (regular Y).actLeft)) ≫
      coequalizer.desc M.actRight ⋯ ▷ N.X ≫
        colimit.ι (parallelPair (M.actRight ▷ N.X) ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft)) WalkingParallelPair.one

Tactic:
dsimp [regular]

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)
X Y Z : Mon_ C
M : Bimod X Y
N : Bimod Y Z
⊢ coequalizer.π (M.actRight ▷ Y.X) ((α_ M.X Y.X Y.X).hom ≫ M.X ◁ Y.mul) ▷ N.X ≫
      ((PreservesCoequalizer.iso (tensorRight N.X) (M.actRight ▷ Y.X) ((α_ M.X Y.X Y.X).hom ≫ M.X ◁ Y.mul)).inv ≫
          coequalizer.desc
            ((α_ M.X Y.X N.X).hom ≫
              M.X ◁ coequalizer.π (Y.mul ▷ N.X) ((α_ Y.X Y.X N.X).hom ≫ Y.X ◁ N.actLeft) ≫
                coequalizer.π
                  (M.actRight ▷
                    TensorBimod.X
                      { X := Y.X, actLeft := Y.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := Y.mul,
                        actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }
                      N)
                  ((α_ M.X Y.X
                        (TensorBimod.X
                          { X := Y.X, actLeft := Y.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := Y.mul,
                            actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }
                          N)).hom ≫
                    M.X ◁
                      TensorBimod.actLeft
                        { X := Y.X, actLeft := Y.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := Y.mul,
                          actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }
                        N))
            ⋯) ≫
        colimMap
          (parallelPairHom
            (M.actRight ▷
              TensorBimod.X
                { X := Y.X, actLeft := Y.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := Y.mul, actRight_one := ⋯,
                  right_assoc := ⋯, middle_assoc := ⋯ }
                N)
            ((α_ M.X Y.X
                  (TensorBimod.X
                    { X := Y.X, actLeft := Y.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := Y.mul,
                      actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }
                    N)).hom ≫
              M.X ◁
                TensorBimod.actLeft
                  { X := Y.X, actLeft := Y.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := Y.mul, actRight_one := ⋯,
                    right_assoc := ⋯, middle_assoc := ⋯ }
                  N)
            (M.actRight ▷ N.X) ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft) ((M.X ⊗ Y.X) ◁ LeftUnitorBimod.hom N)
            (M.X ◁ LeftUnitorBimod.hom N) ⋯ ⋯) =
    coequalizer.π (M.actRight ▷ Y.X) ((α_ M.X Y.X Y.X).hom ≫ M.X ◁ Y.mul) ▷ N.X ≫
      coequalizer.desc M.actRight ⋯ ▷ N.X ≫
        colimit.ι (parallelPair (M.actRight ▷ N.X) ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft)) WalkingParallelPair.one