∀ (R M : Type u_1) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)),
  CategoryTheory.Limits.HasColimit
    (((CategoryTheory.Functor.whiskeringLeft (TopologicalSpace.OpenNhds x)ᵒᵖ
              (TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))ᵒᵖ (ModuleCat R)).obj
          (TopologicalSpace.OpenNhds.inclusion x).op).obj
      (AlgebraicGeometry.structurePresheafInModuleCat R M))