∀ {R : Type u} [inst : CommSemiring R] {X₁ : SemimoduleCat R} {X₂ : SemimoduleCat R} {X₃ : SemimoduleCat R}
  {Y₁ : SemimoduleCat R} {Y₂ : SemimoduleCat R} {Y₃ : SemimoduleCat R} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃),
  CategoryTheory.CategoryStruct.comp
      (SemimoduleCat.MonoidalCategory.tensorHom (SemimoduleCat.MonoidalCategory.tensorHom f₁ f₂) f₃)
      (SemimoduleCat.MonoidalCategory.associator Y₁ Y₂ Y₃).hom =
    CategoryTheory.CategoryStruct.comp (SemimoduleCat.MonoidalCategory.associator X₁ X₂ X₃).hom
      (SemimoduleCat.MonoidalCategory.tensorHom f₁ (SemimoduleCat.MonoidalCategory.tensorHom f₂ f₃))