-- Mathlib/RingTheory/Spectrum/Prime/Basic.lean
theorem exists_primeSpectrum_prod_le (I : Ideal R) :
    ∃ Z : Multiset (PrimeSpectrum R), Multiset.prod (Z.map asIdeal) ≤ I

Proof state:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I M : Ideal R
hgt : ∀ J > M, (fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
lt_add : ∀ 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.map asIdeal Wx).prod ≤ M + span R {x}
Wy : Multiset (PrimeSpectrum R)
h_Wy : (Multiset.map asIdeal Wy).prod ≤ M + span R {y}
⊢ M * (M + span R {y}) + span R {x} * (M + span R {y}) ≤ M

Tactic:
apply sup_le (show M * (M + span R {y}) ≤ M from Ideal.mul_le_right)

Result:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I M : Ideal R
hgt : ∀ J > M, (fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
lt_add : ∀ 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.map asIdeal Wx).prod ≤ M + span R {x}
Wy : Multiset (PrimeSpectrum R)
h_Wy : (Multiset.map asIdeal Wy).prod ≤ M + span R {y}
⊢ span R {x} * (M + span R {y}) ≤ M

Proof state:
case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I M : Ideal R
hgt : ∀ J > M, (fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
⊢ (fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) M

Tactic:
have lt_add : ∀ 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)

Result:
case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I M : Ideal R
hgt : ∀ J > M, (fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
lt_add : ∀ z ∉ M, M < M + span R {z}
⊢ (fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) M

Proof state:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I M : Ideal R
hgt : ∀ J > M, (fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
lt_add : ∀ 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.map asIdeal Wx).prod ≤ M + span R {x}
Wy : Multiset (PrimeSpectrum R)
h_Wy : (Multiset.map asIdeal Wy).prod ≤ M + span R {y}
⊢ span R {x} * span R {y} ≤ M

Tactic:
rwa [span_mul_span, Set.singleton_mul_singleton, span_singleton_le_iff_mem]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I M : Ideal R
hgt : ∀ J > M, (fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) J
⊢ (fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) M

Tactic:
by_cases h_prM : M.IsPrime

Result:
case pos
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I M : Ideal R
hgt : ∀ J > M, (fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) J
h_prM : M.IsPrime
⊢ (fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) M

case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I M : Ideal R
hgt : ∀ J > M, (fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) J
h_prM : ¬M.IsPrime
⊢ (fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) M

Proof state:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I M : Ideal R
hgt : ∀ J > M, (fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
lt_add : ∀ 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.map asIdeal Wx).prod ≤ M + span R {x}
Wy : Multiset (PrimeSpectrum R)
h_Wy : (Multiset.map asIdeal Wy).prod ≤ M + span R {y}
⊢ (Multiset.map asIdeal Wx).prod * (Multiset.map asIdeal Wy).prod ≤ M

Tactic:
apply le_trans (Submodule.mul_le_mul h_Wx h_Wy)

Result:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I M : Ideal R
hgt : ∀ J > M, (fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
lt_add : ∀ 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.map asIdeal Wx).prod ≤ M + span R {x}
Wy : Multiset (PrimeSpectrum R)
h_Wy : (Multiset.map asIdeal Wy).prod ≤ M + span R {y}
⊢ (M + span R {x}) * (M + span R {y}) ≤ M

Proof state:
case neg.intro.intro.intro.intro.intro.intro
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I M : Ideal R
hgt : ∀ J > M, (fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
lt_add : ∀ 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.map asIdeal Wx).prod ≤ M + span R {x}
Wy : Multiset (PrimeSpectrum R)
h_Wy : (Multiset.map asIdeal Wy).prod ≤ M + span R {y}
⊢ (fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) M

Tactic:
use Wx + Wy

Result:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I M : Ideal R
hgt : ∀ J > M, (fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
lt_add : ∀ 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.map asIdeal Wx).prod ≤ M + span R {x}
Wy : Multiset (PrimeSpectrum R)
h_Wy : (Multiset.map asIdeal Wy).prod ≤ M + span R {y}
⊢ (Multiset.map asIdeal (Wx + Wy)).prod ≤ M

Proof state:
case neg.intro.intro.intro.intro
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I M : Ideal R
hgt : ∀ J > M, (fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
lt_add : ∀ 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.map asIdeal Z).prod ≤ I) M

Tactic:
obtain ⟨Wx, h_Wx⟩ := hgt (M + span R {x}) (lt_add _ hx)

Result:
case neg.intro.intro.intro.intro.intro
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I M : Ideal R
hgt : ∀ J > M, (fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
lt_add : ∀ 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.map asIdeal Wx).prod ≤ M + span R {x}
⊢ (fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) M

Proof state:
case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I M : Ideal R
hgt : ∀ J > M, (fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
lt_add : ∀ z ∉ M, M < M + span R {z}
⊢ (fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) M

Tactic:
obtain ⟨x, hx, y, hy, hxy⟩ := (Ideal.not_isPrime_iff.mp h_prM).resolve_left htop

Result:
case neg.intro.intro.intro.intro
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I M : Ideal R
hgt : ∀ J > M, (fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
lt_add : ∀ 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.map asIdeal Z).prod ≤ I) M

Proof state:
case pos
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I M : Ideal R
hgt : ∀ J > M, (fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) J
h_prM : ¬M.IsPrime
htop : M = ⊤
⊢ (fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) M

Tactic:
rw [htop]

Result:
case pos
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I M : Ideal R
hgt : ∀ J > M, (fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) J
h_prM : ¬M.IsPrime
htop : M = ⊤
⊢ (fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) ⊤