-- 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}
⊢ (Multiset.map asIdeal (Wx + Wy)).prod ≤ M

Tactic:
rw [Multiset.map_add, Multiset.prod_add]

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).prod * (Multiset.map asIdeal Wy).prod ≤ 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
⊢ (fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) M

Tactic:
use {⟨M, h_prM⟩}

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
⊢ (Multiset.map asIdeal {{ asIdeal := M, isPrime := h_prM }}).prod ≤ 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} * M + span R {x} * span R {y} ≤ M

Tactic:
apply sup_le (show span R {x} * M ≤ M from Ideal.mul_le_left)

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} * 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
⊢ (fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) M

Tactic:
by_cases htop : M = ⊤

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) 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
htop : ¬M = ⊤
⊢ (fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) M

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
⊢ ∃ Z, (Multiset.map asIdeal Z).prod ≤ I

Tactic:
refine IsNoetherian.induction
  (P := fun I => ∃ Z : Multiset (PrimeSpectrum R), Multiset.prod (Z.map asIdeal) ≤ I)
  (fun (M : Ideal R) hgt => ?_) I

Result:
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

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
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
⊢ ∀ z ∉ M, M < M + span R {z}

Tactic:
intro z hz

Result:
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 = ⊤
z : R
hz : z ∉ M
⊢ M < M + span R {z}

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
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
z : R
hz : z ∉ M
⊢ M < M + span R {z}

Tactic:
refine lt_of_le_of_ne le_sup_left fun m_eq => hz ?_

Result:
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 = ⊤
z : R
hz : z ∉ M
m_eq : M = M + span R {z}
⊢ z ∈ 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
⊢ (Multiset.map asIdeal {{ asIdeal := M, isPrime := h_prM }}).prod ≤ M

Tactic:
rw [Multiset.map_singleton, Multiset.prod_singleton]

Result:
no goals

Proof state:
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

Tactic:
obtain ⟨Wy, h_Wy⟩ := hgt (M + span R {y}) (lt_add _ hy)

Result:
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

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
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
z : R
hz : z ∉ M
m_eq : M = M + span R {z}
⊢ z ∈ M

Tactic:
rw [m_eq]

Result:
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 = ⊤
z : R
hz : z ∉ M
m_eq : M = M + span R {z}
⊢ z ∈ M + span R {z}

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) ⊤

Tactic:
exact ⟨0, le_top⟩

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
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
z : R
hz : z ∉ M
m_eq : M = M + span R {z}
⊢ z ∈ M + span R {z}

Tactic:
exact Ideal.mem_sup_right (mem_span_singleton_self z)

Result:
no goals