R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
⊢ (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) M
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I : Ideal R
⊢ ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I
refine' IsNoetherian.induction
  (P := fun I => ∃ Z : Multiset (PrimeSpectrum R), Multiset.prod (Z.map asIdeal) ≤ I)
  (fun (M : Ideal R) hgt => _) I
case pos
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : Ideal.IsPrime M
⊢ (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) M

case neg
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
⊢ (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) M
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
⊢ (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) M
by_cases h_prM : M.IsPrime
case pos
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : M = ⊤
⊢ (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) M

case neg
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : ¬M = ⊤
⊢ (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) M
case neg
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
⊢ (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) M
by_cases htop : M = ⊤
case neg
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : ¬M = ⊤
lt_add : ∀ (z : R), ¬z ∈ M → M < M + span R {z}
⊢ (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) M
case neg
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : ¬M = ⊤
⊢ (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) M
have lt_add : ∀ (z) (_ : z ∉ M), M < M + span R {z} := by
  intro z hz
  refine' lt_of_le_of_ne le_sup_left fun m_eq => hz _
  rw [m_eq]
  exact Ideal.mem_sup_right (mem_span_singleton_self z)
case neg.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : ¬M = ⊤
lt_add : ∀ (z : R), ¬z ∈ M → M < M + span R {z}
x : R
hx : ¬x ∈ M
y : R
hy : ¬y ∈ M
hxy : x * y ∈ M
⊢ (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) M
case neg
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : ¬M = ⊤
lt_add : ∀ (z : R), ¬z ∈ M → M < M + span R {z}
⊢ (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) M
obtain ⟨x, hx, y, hy, hxy⟩ := (Ideal.not_isPrime_iff.mp h_prM).resolve_left htop
case neg.intro.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : ¬M = ⊤
lt_add : ∀ (z : R), ¬z ∈ M → M < M + span R {z}
x : R
hx : ¬x ∈ M
y : R
hy : ¬y ∈ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span R {x}
⊢ (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) M
case neg.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : ¬M = ⊤
lt_add : ∀ (z : R), ¬z ∈ M → M < M + span R {z}
x : R
hx : ¬x ∈ M
y : R
hy : ¬y ∈ M
hxy : x * y ∈ M
⊢ (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) M
obtain ⟨Wx, h_Wx⟩ := hgt (M + span R {x}) (lt_add _ hx)
case neg.intro.intro.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : ¬M = ⊤
lt_add : ∀ (z : R), ¬z ∈ M → M < M + span R {z}
x : R
hx : ¬x ∈ M
y : R
hy : ¬y ∈ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span R {x}
Wy : Multiset (PrimeSpectrum R)
h_Wy : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span R {y}
⊢ (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) M
case neg.intro.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : ¬M = ⊤
lt_add : ∀ (z : R), ¬z ∈ M → M < M + span R {z}
x : R
hx : ¬x ∈ M
y : R
hy : ¬y ∈ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span R {x}
⊢ (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) M
obtain ⟨Wy, h_Wy⟩ := hgt (M + span R {y}) (lt_add _ hy)
case neg.intro.intro.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : ¬M = ⊤
lt_add : ∀ (z : R), ¬z ∈ M → M < M + span R {z}
x : R
hx : ¬x ∈ M
y : R
hy : ¬y ∈ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span R {x}
Wy : Multiset (PrimeSpectrum R)
h_Wy : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span R {y}
⊢ Multiset.prod (Multiset.map asIdeal (Wx + Wy)) ≤ M
case neg.intro.intro.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : ¬M = ⊤
lt_add : ∀ (z : R), ¬z ∈ M → M < M + span R {z}
x : R
hx : ¬x ∈ M
y : R
hy : ¬y ∈ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span R {x}
Wy : Multiset (PrimeSpectrum R)
h_Wy : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span R {y}
⊢ (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) M
use Wx + Wy
case neg.intro.intro.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : ¬M = ⊤
lt_add : ∀ (z : R), ¬z ∈ M → M < M + span R {z}
x : R
hx : ¬x ∈ M
y : R
hy : ¬y ∈ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span R {x}
Wy : Multiset (PrimeSpectrum R)
h_Wy : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span R {y}
⊢ Multiset.prod (Multiset.map asIdeal Wx) * Multiset.prod (Multiset.map asIdeal Wy) ≤ M
case neg.intro.intro.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : ¬M = ⊤
lt_add : ∀ (z : R), ¬z ∈ M → M < M + span R {z}
x : R
hx : ¬x ∈ M
y : R
hy : ¬y ∈ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span R {x}
Wy : Multiset (PrimeSpectrum R)
h_Wy : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span R {y}
⊢ Multiset.prod (Multiset.map asIdeal (Wx + Wy)) ≤ M
rw [Multiset.map_add, Multiset.prod_add]
case neg.intro.intro.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : ¬M = ⊤
lt_add : ∀ (z : R), ¬z ∈ M → M < M + span R {z}
x : R
hx : ¬x ∈ M
y : R
hy : ¬y ∈ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span R {x}
Wy : Multiset (PrimeSpectrum R)
h_Wy : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span R {y}
⊢ (M + span R {x}) * (M + span R {y}) ≤ M
case neg.intro.intro.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : ¬M = ⊤
lt_add : ∀ (z : R), ¬z ∈ M → M < M + span R {z}
x : R
hx : ¬x ∈ M
y : R
hy : ¬y ∈ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span R {x}
Wy : Multiset (PrimeSpectrum R)
h_Wy : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span R {y}
⊢ Multiset.prod (Multiset.map asIdeal Wx) * Multiset.prod (Multiset.map asIdeal Wy) ≤ M
apply le_trans (Submodule.mul_le_mul h_Wx h_Wy)
case neg.intro.intro.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : ¬M = ⊤
lt_add : ∀ (z : R), ¬z ∈ M → M < M + span R {z}
x : R
hx : ¬x ∈ M
y : R
hy : ¬y ∈ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span R {x}
Wy : Multiset (PrimeSpectrum R)
h_Wy : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span R {y}
⊢ M * (M + span R {y}) + span R {x} * (M + span R {y}) ≤ M
case neg.intro.intro.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : ¬M = ⊤
lt_add : ∀ (z : R), ¬z ∈ M → M < M + span R {z}
x : R
hx : ¬x ∈ M
y : R
hy : ¬y ∈ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span R {x}
Wy : Multiset (PrimeSpectrum R)
h_Wy : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span R {y}
⊢ (M + span R {x}) * (M + span R {y}) ≤ M
rw [add_mul]
case neg.intro.intro.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : ¬M = ⊤
lt_add : ∀ (z : R), ¬z ∈ M → M < M + span R {z}
x : R
hx : ¬x ∈ M
y : R
hy : ¬y ∈ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span R {x}
Wy : Multiset (PrimeSpectrum R)
h_Wy : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span R {y}
⊢ span R {x} * (M + span R {y}) ≤ M
case neg.intro.intro.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : ¬M = ⊤
lt_add : ∀ (z : R), ¬z ∈ M → M < M + span R {z}
x : R
hx : ¬x ∈ M
y : R
hy : ¬y ∈ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span R {x}
Wy : Multiset (PrimeSpectrum R)
h_Wy : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span R {y}
⊢ M * (M + span R {y}) + span R {x} * (M + span R {y}) ≤ M
apply sup_le (show M * (M + span R {y}) ≤ M from Ideal.mul_le_right)
case neg.intro.intro.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : ¬M = ⊤
lt_add : ∀ (z : R), ¬z ∈ M → M < M + span R {z}
x : R
hx : ¬x ∈ M
y : R
hy : ¬y ∈ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span R {x}
Wy : Multiset (PrimeSpectrum R)
h_Wy : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span R {y}
⊢ span R {x} * M + span R {x} * span R {y} ≤ M
case neg.intro.intro.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : ¬M = ⊤
lt_add : ∀ (z : R), ¬z ∈ M → M < M + span R {z}
x : R
hx : ¬x ∈ M
y : R
hy : ¬y ∈ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span R {x}
Wy : Multiset (PrimeSpectrum R)
h_Wy : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span R {y}
⊢ span R {x} * (M + span R {y}) ≤ M
rw [mul_add]
case neg.intro.intro.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : ¬M = ⊤
lt_add : ∀ (z : R), ¬z ∈ M → M < M + span R {z}
x : R
hx : ¬x ∈ M
y : R
hy : ¬y ∈ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span R {x}
Wy : Multiset (PrimeSpectrum R)
h_Wy : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span R {y}
⊢ span R {x} * span R {y} ≤ M
case neg.intro.intro.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : ¬M = ⊤
lt_add : ∀ (z : R), ¬z ∈ M → M < M + span R {z}
x : R
hx : ¬x ∈ M
y : R
hy : ¬y ∈ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span R {x}
Wy : Multiset (PrimeSpectrum R)
h_Wy : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span R {y}
⊢ span R {x} * M + span R {x} * span R {y} ≤ M
apply sup_le (show span R {x} * M ≤ M from Ideal.mul_le_left)
no goals
case neg.intro.intro.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : ¬M = ⊤
lt_add : ∀ (z : R), ¬z ∈ M → M < M + span R {z}
x : R
hx : ¬x ∈ M
y : R
hy : ¬y ∈ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span R {x}
Wy : Multiset (PrimeSpectrum R)
h_Wy : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span R {y}
⊢ span R {x} * span R {y} ≤ M
rwa [span_mul_span, Set.singleton_mul_singleton, span_singleton_le_iff_mem]
case pos
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : Ideal.IsPrime M
⊢ Multiset.prod (Multiset.map asIdeal {{ asIdeal := M, IsPrime := h_prM }}) ≤ M
case pos
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : Ideal.IsPrime M
⊢ (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) M
use {⟨M, h_prM⟩}
no goals
case pos
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : Ideal.IsPrime M
⊢ Multiset.prod (Multiset.map asIdeal {{ asIdeal := M, IsPrime := h_prM }}) ≤ M
rw [Multiset.map_singleton, Multiset.prod_singleton]
case pos
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : M = ⊤
⊢ (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) ⊤
case pos
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : M = ⊤
⊢ (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) M
rw [htop]
no goals
case pos
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : M = ⊤
⊢ (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) ⊤
exact ⟨0, le_top⟩
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : ¬M = ⊤
z : R
hz : ¬z ∈ M
⊢ M < M + span R {z}
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : ¬M = ⊤
⊢ ∀ (z : R), ¬z ∈ M → M < M + span R {z}
intro z hz
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : ¬M = ⊤
z : R
hz : ¬z ∈ M
m_eq : M = M + span R {z}
⊢ z ∈ M
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : ¬M = ⊤
z : R
hz : ¬z ∈ M
⊢ M < M + span R {z}
refine' lt_of_le_of_ne le_sup_left fun m_eq => hz _
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : ¬M = ⊤
z : R
hz : ¬z ∈ M
m_eq : M = M + span R {z}
⊢ z ∈ M + span R {z}
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : ¬M = ⊤
z : R
hz : ¬z ∈ M
m_eq : M = M + span R {z}
⊢ z ∈ M
rw [m_eq]
no goals
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : ¬M = ⊤
z : R
hz : ¬z ∈ M
m_eq : M = M + span R {z}
⊢ z ∈ M + span R {z}
exact Ideal.mem_sup_right (mem_span_singleton_self z)