no goals
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
x : PrimeSpectrum R
⊢ x ∈ ↑(basicOpen r) ↔ x ∈ zeroLocus {r}ᶜ
simp only [SetLike.mem_coe, mem_basicOpen, Set.mem_compl_iff, mem_zeroLocus,
Set.singleton_subset_iff]