∀ {R M : Type u_1} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {S : Type u_1}
  [inst_3 : CommRing S] {σ : R →+* S} (y : ↑(AlgebraicGeometry.PrimeSpectrum.Top S)),
  IsLocalizedModule (PrimeSpectrum.comap σ y).asIdeal.primeCompl
    (LocalizedModule.mkLinearMap (PrimeSpectrum.comap σ y).asIdeal.primeCompl M)