no goals
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
s : Set (Set A)
⊢ zeroLocus 𝒜 (⋃ (s' : Set A) (_ : s' ∈ s), s') = ⋂ (s' : Set A) (_ : s' ∈ s), zeroLocus 𝒜 s'
simp only [zeroLocus_iUnion]