∀ {R : Type u_1} [inst : CommRing R] {S : Type u_1} [inst_1 : CommRing S] (f : R →+* S)
  (V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top S)) (y : ↥V),
  (PrimeSpectrum.comap f ↑y).asIdeal.IsPrime