no goals
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s : Set (Set R)
⊢ zeroLocus (⋃ (s' : Set R) (_ : s' ∈ s), s') = ⋂ (s' : Set R) (_ : s' ∈ s), zeroLocus s'
simp only [zeroLocus_iUnion]