∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat}
  (M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))) (X Y : Cᵒᵖ) (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (M.map f)
      ((ModuleCat.restrictScalars (RingCat.Hom.hom ((R.comp (CategoryTheory.forget₂ CommRingCat RingCat)).map f))).map
        ((fun x => (CategoryTheory.MonoidalCategoryStruct.leftUnitor (M.obj x)).symm) Y).hom) =
    CategoryTheory.CategoryStruct.comp
      ((fun x => (CategoryTheory.MonoidalCategoryStruct.leftUnitor (M.obj x)).symm) X).hom
      ((PresheafOfModules.Monoidal.tensorObj
            (PresheafOfModules.unit (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))) M).map
        f)