no goals
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f g : R
⊢ basicOpen f ≤ basicOpen g ↔ f ∈ Ideal.radical (Ideal.span {g})
rw [← SetLike.coe_subset_coe, basicOpen_eq_zeroLocus_compl, basicOpen_eq_zeroLocus_compl,
  Set.compl_subset_compl, zeroLocus_subset_zeroLocus_singleton_iff]