∀ {R : Type u} [inst : CommSemiring R] {X Y : SemimoduleCat R} (f : X ⟶ Y) (Z : SemimoduleCat R),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z) (Y.braiding Z).hom =
    CategoryTheory.CategoryStruct.comp (X.braiding Z).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z f)