∀ (R M : Type u_1) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (X Y : (TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))ᵒᵖ) (f : X ⟶ Y)
  (r :
    ↑((CategoryTheory.Functor.comp (AlgebraicGeometry.structurePresheafInCommRingCat R)
            (CategoryTheory.forget₂ CommRingCat RingCat)).obj
        X))
  (m :
    ↑((CategoryTheory.Functor.comp (AlgebraicGeometry.structurePresheafInModuleCat R M)
            (CategoryTheory.forget₂ (ModuleCat R) Ab)).obj
        X)),
  (CategoryTheory.ConcreteCategory.hom
        ((CategoryTheory.Functor.comp (AlgebraicGeometry.structurePresheafInModuleCat R M)
              (CategoryTheory.forget₂ (ModuleCat R) Ab)).map
          f))
      (r • m) =
    (CategoryTheory.ConcreteCategory.hom
        ((CategoryTheory.Functor.comp (AlgebraicGeometry.structurePresheafInModuleCat R M)
              (CategoryTheory.forget₂ (ModuleCat R) Ab)).map
          f))
      (r • m)