∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_3, u_2} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat}
  (M₁ M₂ : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))),
  CategoryTheory.MonoidalCategoryStruct.whiskerLeft M₁ (CategoryTheory.CategoryStruct.id M₂) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj M₁ M₂)