∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, u_1, u_1, u_2, u_2}
        (CategoryTheory.MonoidalCategory.tensorLeft X)]
  {R S T U : CategoryTheory.Mon C} (P : Bimod R S) (Q : Bimod S T) (L : Bimod T U),
  CategoryTheory.Limits.PreservesColimit
    (CategoryTheory.Limits.parallelPair (CategoryTheory.MonoidalCategoryStruct.whiskerRight Q.actRight L.X)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Q.X T.X L.X).hom
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q.X L.actLeft)))
    (CategoryTheory.MonoidalCategory.tensorLeft P.X)