∀ (R M : Type u_1) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (r : R)
  (m : ↑(TopCat.Presheaf.stalk (AlgebraicGeometry.moduleStructurePresheaf R M).presheaf x)),
  (CategoryTheory.Limits.colimit.isoColimitCocone
            {
              cocone :=
                (CategoryTheory.forget₂ (ModuleCat R) Ab).mapCocone
                  (CategoryTheory.Limits.colimit.cocone
                    ((TopologicalSpace.OpenNhds.inclusion x).op.comp
                      (AlgebraicGeometry.structurePresheafInModuleCat R M))),
              isColimit :=
                CategoryTheory.Limits.isColimitOfPreserves (CategoryTheory.forget₂ (ModuleCat R) Ab)
                  (CategoryTheory.Limits.colimit.isColimit
                    ((TopologicalSpace.OpenNhds.inclusion x).op.comp
                      (AlgebraicGeometry.structurePresheafInModuleCat R M))) }).addCommGroupIsoToAddEquiv.toFun
      (r • m) =
    (RingHom.id R) r •
      (CategoryTheory.Limits.colimit.isoColimitCocone
              {
                cocone :=
                  (CategoryTheory.forget₂ (ModuleCat R) Ab).mapCocone
                    (CategoryTheory.Limits.colimit.cocone
                      ((TopologicalSpace.OpenNhds.inclusion x).op.comp
                        (AlgebraicGeometry.structurePresheafInModuleCat R M))),
                isColimit :=
                  CategoryTheory.Limits.isColimitOfPreserves (CategoryTheory.forget₂ (ModuleCat R) Ab)
                    (CategoryTheory.Limits.colimit.isColimit
                      ((TopologicalSpace.OpenNhds.inclusion x).op.comp
                        (AlgebraicGeometry.structurePresheafInModuleCat R M))) }).addCommGroupIsoToAddEquiv.toFun
        m