R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t t' : Set (ProjectiveSpectrum 𝒜)
r : A
⊢ r ∈ vanishingIdeal t ⊔ vanishingIdeal t' → r ∈ vanishingIdeal (t ∩ t')
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t t' : Set (ProjectiveSpectrum 𝒜)
⊢ vanishingIdeal t ⊔ vanishingIdeal t' ≤ vanishingIdeal (t ∩ t')
intro r
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t t' : Set (ProjectiveSpectrum 𝒜)
r : A
⊢ (∃ y,
      y ∈ HomogeneousIdeal.toIdeal (vanishingIdeal t) ∧
        ∃ z, z ∈ HomogeneousIdeal.toIdeal (vanishingIdeal t') ∧ y + z = r) →
    ∀ (x : ProjectiveSpectrum 𝒜), x ∈ t ∩ t' → r ∈ 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 t' : Set (ProjectiveSpectrum 𝒜)
r : A
⊢ r ∈ vanishingIdeal t ⊔ vanishingIdeal t' → r ∈ vanishingIdeal (t ∩ t')
rw [← HomogeneousIdeal.mem_iff, HomogeneousIdeal.toIdeal_sup, mem_vanishingIdeal,
  Submodule.mem_sup]
case intro.intro.intro.intro.intro
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t t' : Set (ProjectiveSpectrum 𝒜)
f : A
hf : f ∈ HomogeneousIdeal.toIdeal (vanishingIdeal t)
g : A
hg : g ∈ HomogeneousIdeal.toIdeal (vanishingIdeal t')
x : ProjectiveSpectrum 𝒜
hxt : x ∈ t
hxt' : x ∈ t'
⊢ f + g ∈ 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 t' : Set (ProjectiveSpectrum 𝒜)
r : A
⊢ (∃ y,
      y ∈ HomogeneousIdeal.toIdeal (vanishingIdeal t) ∧
        ∃ z, z ∈ HomogeneousIdeal.toIdeal (vanishingIdeal t') ∧ y + z = r) →
    ∀ (x : ProjectiveSpectrum 𝒜), x ∈ t ∩ t' → r ∈ x.asHomogeneousIdeal
rintro ⟨f, hf, g, hg, rfl⟩ x ⟨hxt, hxt'⟩
case intro.intro.intro.intro.intro
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t t' : Set (ProjectiveSpectrum 𝒜)
f : A
hf : ∀ (x : ProjectiveSpectrum 𝒜), x ∈ t → f ∈ x.asHomogeneousIdeal
g : A
hg : ∀ (x : ProjectiveSpectrum 𝒜), x ∈ t' → g ∈ x.asHomogeneousIdeal
x : ProjectiveSpectrum 𝒜
hxt : x ∈ t
hxt' : x ∈ t'
⊢ f + g ∈ x.asHomogeneousIdeal
case intro.intro.intro.intro.intro
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t t' : Set (ProjectiveSpectrum 𝒜)
f : A
hf : f ∈ HomogeneousIdeal.toIdeal (vanishingIdeal t)
g : A
hg : g ∈ HomogeneousIdeal.toIdeal (vanishingIdeal t')
x : ProjectiveSpectrum 𝒜
hxt : x ∈ t
hxt' : x ∈ t'
⊢ f + g ∈ x.asHomogeneousIdeal
erw [mem_vanishingIdeal] at hf hg
no goals
case intro.intro.intro.intro.intro
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t t' : Set (ProjectiveSpectrum 𝒜)
f : A
hf : ∀ (x : ProjectiveSpectrum 𝒜), x ∈ t → f ∈ x.asHomogeneousIdeal
g : A
hg : ∀ (x : ProjectiveSpectrum 𝒜), x ∈ t' → g ∈ x.asHomogeneousIdeal
x : ProjectiveSpectrum 𝒜
hxt : x ∈ t
hxt' : x ∈ t'
⊢ f + g ∈ x.asHomogeneousIdeal
apply Submodule.add_mem <;> solve_by_elim