no goals
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
x y : PrimeSpectrum R
⊢ x ≤ y ↔ y ∈ closure {x}
rw [← asIdeal_le_asIdeal, ← zeroLocus_vanishingIdeal_eq_closure, mem_zeroLocus,
  vanishingIdeal_singleton, SetLike.coe_subset_coe]