∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasCoequalizers C] {R S T : CategoryTheory.Mon C} (P : Bimod R S) (Q : Bimod S T)
  [inst_3 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorLeft X)],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R.X
        (CategoryTheory.Limits.coequalizer.π (CategoryTheory.MonoidalCategoryStruct.whiskerRight P.actRight Q.X)
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P.X S.X Q.X).hom
            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X Q.actLeft))))
      (Bimod.TensorBimod.actLeft P Q) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator R.X P.X Q.X).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight P.actLeft Q.X)
        (CategoryTheory.Limits.coequalizer.π (CategoryTheory.MonoidalCategoryStruct.whiskerRight P.actRight Q.X)
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P.X S.X Q.X).hom
            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X Q.actLeft))))