∀ {R : Type u} [inst : CommSemiring R] (W : SemimoduleCat R) (X : SemimoduleCat R) (Y : SemimoduleCat R)
  (Z : SemimoduleCat R),
  CategoryTheory.CategoryStruct.comp
      (SemimoduleCat.MonoidalCategory.whiskerRight (SemimoduleCat.MonoidalCategory.associator W X Y).hom Z)
      (CategoryTheory.CategoryStruct.comp
        (SemimoduleCat.MonoidalCategory.associator W (SemimoduleCat.MonoidalCategory.tensorObj X Y) Z).hom
        (SemimoduleCat.MonoidalCategory.whiskerLeft W (SemimoduleCat.MonoidalCategory.associator X Y Z).hom)) =
    CategoryTheory.CategoryStruct.comp
      (SemimoduleCat.MonoidalCategory.associator (SemimoduleCat.MonoidalCategory.tensorObj W X) Y Z).hom
      (SemimoduleCat.MonoidalCategory.associator W X (SemimoduleCat.MonoidalCategory.tensorObj Y Z)).hom