no goals
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f g : R
⊢ zeroLocus {f} ⊆ zeroLocus {g} ↔ g ∈ Ideal.radical (Ideal.span {f})
rw [← zeroLocus_span {f}, ← zeroLocus_span {g}, zeroLocus_subset_zeroLocus_iff, Ideal.span_le,
  Set.singleton_subset_iff, SetLike.mem_coe]