no goals
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s : Set (PrimeSpectrum R)
⊢ IsIrreducible s ↔ Ideal.IsPrime (vanishingIdeal s)
rw [← isIrreducible_iff_closure, ← zeroLocus_vanishingIdeal_eq_closure,
  isIrreducible_zeroLocus_iff_of_radical _ (isRadical_vanishingIdeal s)]