case h
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) ↔ f ∈ {f | ∀ (x : ProjectiveSpectrum 𝒜), x ∈ t → f ∈ x.asHomogeneousIdeal}
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 𝒜)
⊢ ↑(vanishingIdeal t) = {f | ∀ (x : ProjectiveSpectrum 𝒜), x ∈ t → f ∈ x.asHomogeneousIdeal}
ext f
case h
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
⊢ (∀ (i : ProjectiveSpectrum 𝒜), f ∈ HomogeneousIdeal.toIdeal (⨅ (_ : i ∈ t), i.asHomogeneousIdeal)) ↔
    f ∈ {f | ∀ (x : ProjectiveSpectrum 𝒜), x ∈ t → f ∈ x.asHomogeneousIdeal}
case h
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) ↔ f ∈ {f | ∀ (x : ProjectiveSpectrum 𝒜), x ∈ t → f ∈ x.asHomogeneousIdeal}
rw [vanishingIdeal, SetLike.mem_coe, ← HomogeneousIdeal.mem_iff, HomogeneousIdeal.toIdeal_iInf,
  Submodule.mem_iInf]
case h
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
x : ProjectiveSpectrum 𝒜
⊢ f ∈ HomogeneousIdeal.toIdeal (⨅ (_ : x ∈ t), x.asHomogeneousIdeal) ↔ x ∈ t → f ∈ x.asHomogeneousIdeal
case h
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
⊢ (∀ (i : ProjectiveSpectrum 𝒜), f ∈ HomogeneousIdeal.toIdeal (⨅ (_ : i ∈ t), i.asHomogeneousIdeal)) ↔
    f ∈ {f | ∀ (x : ProjectiveSpectrum 𝒜), x ∈ t → f ∈ x.asHomogeneousIdeal}
refine' forall_congr' fun x => _
no goals
case h
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
x : ProjectiveSpectrum 𝒜
⊢ f ∈ HomogeneousIdeal.toIdeal (⨅ (_ : x ∈ t), x.asHomogeneousIdeal) ↔ x ∈ t → f ∈ x.asHomogeneousIdeal
rw [HomogeneousIdeal.toIdeal_iInf, Submodule.mem_iInf, HomogeneousIdeal.mem_iff]