R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t t' : Set (PrimeSpectrum R)
r : R
⊢ r ∈ vanishingIdeal t ⊔ vanishingIdeal t' → r ∈ vanishingIdeal (t ∩ t')
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t t' : Set (PrimeSpectrum R)
⊢ vanishingIdeal t ⊔ vanishingIdeal t' ≤ vanishingIdeal (t ∩ t')
intro r
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t t' : Set (PrimeSpectrum R)
r : R
⊢ (∃ y, y ∈ vanishingIdeal t ∧ ∃ z, z ∈ vanishingIdeal t' ∧ y + z = r) →
    ∀ (x : PrimeSpectrum R), x ∈ t ∩ t' → r ∈ x.asIdeal
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t t' : Set (PrimeSpectrum R)
r : R
⊢ r ∈ vanishingIdeal t ⊔ vanishingIdeal t' → r ∈ vanishingIdeal (t ∩ t')
rw [Submodule.mem_sup, mem_vanishingIdeal]
case intro.intro.intro.intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t t' : Set (PrimeSpectrum R)
f : R
hf : f ∈ vanishingIdeal t
g : R
hg : g ∈ vanishingIdeal t'
x : PrimeSpectrum R
hxt : x ∈ t
hxt' : x ∈ t'
⊢ f + g ∈ x.asIdeal
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t t' : Set (PrimeSpectrum R)
r : R
⊢ (∃ y, y ∈ vanishingIdeal t ∧ ∃ z, z ∈ vanishingIdeal t' ∧ y + z = r) →
    ∀ (x : PrimeSpectrum R), x ∈ t ∩ t' → r ∈ x.asIdeal
rintro ⟨f, hf, g, hg, rfl⟩ x ⟨hxt, hxt'⟩
case intro.intro.intro.intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t t' : Set (PrimeSpectrum R)
f : R
hf : ∀ (x : PrimeSpectrum R), x ∈ t → f ∈ x.asIdeal
g : R
hg : ∀ (x : PrimeSpectrum R), x ∈ t' → g ∈ x.asIdeal
x : PrimeSpectrum R
hxt : x ∈ t
hxt' : x ∈ t'
⊢ f + g ∈ x.asIdeal
case intro.intro.intro.intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t t' : Set (PrimeSpectrum R)
f : R
hf : f ∈ vanishingIdeal t
g : R
hg : g ∈ vanishingIdeal t'
x : PrimeSpectrum R
hxt : x ∈ t
hxt' : x ∈ t'
⊢ f + g ∈ x.asIdeal
rw [mem_vanishingIdeal] at hf hg
no goals
case intro.intro.intro.intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t t' : Set (PrimeSpectrum R)
f : R
hf : ∀ (x : PrimeSpectrum R), x ∈ t → f ∈ x.asIdeal
g : R
hg : ∀ (x : PrimeSpectrum R), x ∈ t' → g ∈ x.asIdeal
x : PrimeSpectrum R
hxt : x ∈ t
hxt' : x ∈ t'
⊢ f + g ∈ x.asIdeal
apply Submodule.add_mem <;> solve_by_elim