∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasCoequalizers C]
  [inst_3 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorLeft X)]
  [inst_4 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorRight X)]
  {X Y Z : CategoryTheory.Mon C} (M : Bimod X Y) {N₁ N₂ : Bimod Y Z} (f : N₁ ⟶ N₂),
  (M.whiskerLeft f).hom =
    CategoryTheory.Limits.colimMap
      (CategoryTheory.Limits.parallelPairHom (CategoryTheory.MonoidalCategoryStruct.whiskerRight M.actRight N₁.X)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M.X Y.X N₁.X).hom
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X N₁.actLeft))
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight M.actRight N₂.X)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M.X Y.X N₂.X).hom
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X N₂.actLeft))
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X Y.X)
          f.hom)
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X f.hom) ⋯ ⋯)