∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat}
  {M₁ M₂ M₃ M₄ : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} (f : M₁ ⟶ M₂) (g : M₃ ⟶ M₄)
  {X Y : Cᵒᵖ} (φ : X ⟶ Y) (m₁ : ↑(M₁.obj X)) (m₃ : ↑(M₃.obj X)),
  (ModuleCat.Hom.hom
        (CategoryTheory.CategoryStruct.comp ((PresheafOfModules.Monoidal.tensorObj M₁ M₃).map φ)
          ((ModuleCat.restrictScalars
                (RingCat.Hom.hom ((R.comp (CategoryTheory.forget₂ CommRingCat RingCat)).map φ))).map
            (CategoryTheory.MonoidalCategoryStruct.tensorHom (f.app Y) (g.app Y)))))
      (m₁ ⊗ₜ[↑((R.comp (CategoryTheory.forget₂ CommRingCat RingCat)).obj X)] m₃) =
    (ModuleCat.Hom.hom
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (f.app X) (g.app X))
          ((PresheafOfModules.Monoidal.tensorObj M₂ M₄).map φ)))
      (m₁ ⊗ₜ[↑((R.comp (CategoryTheory.forget₂ CommRingCat RingCat)).obj X)] m₃)