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 𝒜
t : Set (ProjectiveSpectrum 𝒜)
f : A
⊢ f ∈ vanishingIdeal t ↔ ∀ (x : ProjectiveSpectrum 𝒜), x ∈ t → f ∈ x.asHomogeneousIdeal
rw [← SetLike.mem_coe, coe_vanishingIdeal, Set.mem_setOf_eq]