awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
m : Ideal R
inst_1 : m.IsMaximal
I : PrimeSpectrum R
h : Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑m : Set R)) I
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) {{ asIdeal := m, isPrime := ⋯ : PrimeSpectrum R }} I
have h₁ : m ≤ I.asIdeal
Tactic: simp only [mem_zeroLocus, SetLike.coe_subset_coe] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
x : PrimeSpectrum R
⊢ IsMin x ↔ Minimal (fun (q : Ideal R) ↦ q.IsPrime ∧ ⊥ ≤ q) x.asIdeal
have simp : (∀ ⦃b : PrimeSpectrum R⦄, b ≤ x → x ≤ b) ↔ ∀ ⦃y : Ideal R⦄, y.IsPrime → y ≤ x.asIdeal → x.asIdeal ≤ y
Tactic: simp only [IsMin, Minimal, x.2, bot_le, and_self, and_true, true_and]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsNoetherianRing R
M : Submodule R R
hgt : ∀ J > M, ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ J
⊢ ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ M
have hgt₁ : ∀ (M : Ideal R) (hgt : ∀ J > M, ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ J),
  ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ M
Tactic: change Ideal R at M
Cleared hypotheses: M, hgt
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ J
⊢ ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ M
have pos : ∀ (h_prM : M.IsPrime), ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ M
Tactic: by_cases h_prM : M.IsPrime
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ J
pos : ∀ (h_prM : M.IsPrime), ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ M
⊢ ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ M
have neg : ∀ (h_prM : ¬M.IsPrime), ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ M
Tactic: by_cases h_prM : M.IsPrime
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ J
h_prM : M.IsPrime
⊢ ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ M
have h : Multiset.prod (Multiset.map asIdeal {{ asIdeal := M, isPrime := h_prM : PrimeSpectrum R }}) ≤ M
Tactic: use {⟨M, h_prM⟩}
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ J
h_prM : M.IsPrime
⊢ Multiset.prod (Multiset.map asIdeal {{ asIdeal := M, isPrime := h_prM : PrimeSpectrum R }}) ≤ M
have h : Multiset.prod {{ asIdeal := M, isPrime := h_prM : PrimeSpectrum R }.asIdeal} ≤ M
Tactic: rw [Multiset.map_singleton, Multiset.prod_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ J
h_prM : M.IsPrime
h : Multiset.prod {{ asIdeal := M, isPrime := h_prM : PrimeSpectrum R }.asIdeal} ≤ M
⊢ Multiset.prod (Multiset.map asIdeal {{ asIdeal := M, isPrime := h_prM : PrimeSpectrum R }}) ≤ M
have h₁ : { asIdeal := M, isPrime := h_prM : PrimeSpectrum R }.asIdeal ≤ { asIdeal := M, isPrime := h_prM }.asIdeal
Tactic: rw [Multiset.map_singleton, Multiset.prod_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ J
h_prM : ¬M.IsPrime
⊢ ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ M
have pos : ∀ (htop : M = ⊤), ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ M
Tactic: by_cases htop : M = ⊤
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ J
h_prM : ¬M.IsPrime
pos : ∀ (htop : M = ⊤), ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ M
⊢ ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ M
have neg : ∀ (htop : ¬M = ⊤), ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ M
Tactic: by_cases htop : M = ⊤
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ J
h_prM : ¬M.IsPrime
htop : M = ⊤
⊢ ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ M
have pos : ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ ⊤
Tactic: rw [htop]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
z : R
hz : z ∉ M
⊢ M < M + R ∙ z
have refine : ∀ (m_eq : M = M + R ∙ z), z ∈ M
Tactic: refine lt_of_le_of_ne le_sup_left fun m_eq => hz ?_
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
z : R
hz : z ∉ M
m_eq : M = M + R ∙ z
⊢ z ∈ M
have rw : z ∈ M + R ∙ z
Tactic: rw [m_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
⊢ ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ M
have lt_add : ∀ z ∉ M, M < M + R ∙ z
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)
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
lt_add : ∀ z ∉ M, M < M + R ∙ z
⊢ ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ M
have neg : ∀ (x : R) (hx : x ∉ M) (y : R) (hy : y ∉ M) (hxy : x * y ∈ M),
  ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ M
Tactic: obtain ⟨x, hx, y, hy, hxy⟩ := (Ideal.not_isPrime_iff.mp h_prM).resolve_left htop
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
lt_add : ∀ z ∉ M, M < M + R ∙ z
x : R
hx : x ∉ M
y : R
hy : y ∉ M
hxy : x * y ∈ M
⊢ ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ M
have neg : ∀ (Wx : Multiset (PrimeSpectrum R)) (h_Wx : (Multiset.map asIdeal Wx).prod ≤ M + R ∙ x),
  ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ M
Tactic: obtain ⟨Wx, h_Wx⟩ := hgt (M + span R {x}) (lt_add _ hx)
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
lt_add : ∀ z ∉ M, M < M + 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 + R ∙ x
⊢ ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ M
have neg : ∀ (Wy : Multiset (PrimeSpectrum R)) (h_Wy : (Multiset.map asIdeal Wy).prod ≤ M + R ∙ y),
  ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ M
Tactic: obtain ⟨Wy, h_Wy⟩ := hgt (M + span R {y}) (lt_add _ hy)
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
lt_add : ∀ z ∉ M, M < M + 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 + R ∙ x
Wy : Multiset (PrimeSpectrum R)
h_Wy : (Multiset.map asIdeal Wy).prod ≤ M + R ∙ y
⊢ ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ M
have h : (Multiset.map asIdeal (Wx + Wy)).prod ≤ M
Tactic: use Wx + Wy
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
lt_add : ∀ z ∉ M, M < M + 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 + R ∙ x
Wy : Multiset (PrimeSpectrum R)
h_Wy : (Multiset.map asIdeal Wy).prod ≤ M + R ∙ y
⊢ (Multiset.map asIdeal (Wx + Wy)).prod ≤ M
have h : (Multiset.map asIdeal Wx).prod * (Multiset.map asIdeal Wy).prod ≤ M
Tactic: rw [Multiset.map_add, Multiset.prod_add]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
lt_add : ∀ z ∉ M, M < M + 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 + R ∙ x
Wy : Multiset (PrimeSpectrum R)
h_Wy : (Multiset.map asIdeal Wy).prod ≤ M + R ∙ y
⊢ (Multiset.map asIdeal Wx).prod * (Multiset.map asIdeal Wy).prod ≤ M
have h : (M + R ∙ x) * (M + R ∙ y) ≤ M
Tactic: apply le_trans (mul_le_mul' h_Wx h_Wy)
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
lt_add : ∀ z ∉ M, M < M + 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 + R ∙ x
Wy : Multiset (PrimeSpectrum R)
h_Wy : (Multiset.map asIdeal Wy).prod ≤ M + R ∙ y
⊢ (M + R ∙ x) * (M + R ∙ y) ≤ M
have h : M * (M + R ∙ y) + (R ∙ x) * (M + R ∙ y) ≤ M
Tactic: rw [add_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
lt_add : ∀ z ∉ M, M < M + 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 + R ∙ x
Wy : Multiset (PrimeSpectrum R)
h_Wy : (Multiset.map asIdeal Wy).prod ≤ M + R ∙ y
⊢ M * (M + R ∙ y) + (R ∙ x) * (M + R ∙ y) ≤ M
have h : (R ∙ x) * (M + R ∙ y) ≤ M
Tactic: apply sup_le (show M * (M + span R {y}) ≤ M from Ideal.mul_le_right)
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
lt_add : ∀ z ∉ M, M < M + 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 + R ∙ x
Wy : Multiset (PrimeSpectrum R)
h_Wy : (Multiset.map asIdeal Wy).prod ≤ M + R ∙ y
⊢ (R ∙ x) * (M + R ∙ y) ≤ M
have h : (R ∙ x) * M + HMul.hMul (α := Ideal R) (R ∙ x) (R ∙ y) ≤ M
Tactic: rw [mul_add]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
lt_add : ∀ z ∉ M, M < M + 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 + R ∙ x
Wy : Multiset (PrimeSpectrum R)
h_Wy : (Multiset.map asIdeal Wy).prod ≤ M + R ∙ y
⊢ (R ∙ x) * M + HMul.hMul (α := Ideal R) (R ∙ x) (R ∙ y) ≤ M
have h : HMul.hMul (α := Ideal R) (R ∙ x) (R ∙ y) ≤ M
Tactic: apply sup_le (show span R {x} * M ≤ M from Ideal.mul_le_left)
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
lt_add : ∀ z ∉ M, M < M + 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 + R ∙ x
Wy : Multiset (PrimeSpectrum R)
h_Wy : (Multiset.map asIdeal Wy).prod ≤ M + R ∙ y
⊢ HMul.hMul (α := Ideal R) (R ∙ x) (R ∙ y) ≤ M
have h : span R (HMul.hMul (α := Set R) {x} {y}) ≤ M
Tactic: rwa [span_mul_span, Set.singleton_mul_singleton, span_singleton_le_iff_mem]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
lt_add : ∀ z ∉ M, M < M + 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 + R ∙ x
Wy : Multiset (PrimeSpectrum R)
h_Wy : (Multiset.map asIdeal Wy).prod ≤ M + R ∙ y
h : span R (HMul.hMul (α := Set R) {x} {y}) ≤ M
⊢ HMul.hMul (α := Ideal R) (R ∙ x) (R ∙ y) ≤ M
have h₁ : R ∙ x * y ≤ M
Tactic: rwa [span_mul_span, Set.singleton_mul_singleton, span_singleton_le_iff_mem]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
⊢ ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ I
have hgt : ∀ (M : Submodule R R) (hgt : ∀ J > M, ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ J),
  ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ M
Tactic: induction I using IsNoetherian.induction with | hgt M hgt =>
  change Ideal R at M
  by_cases h_prM : M.IsPrime
  · use {⟨M, h_prM⟩}
    rw [Multiset.map_singleton, Multiset.prod_singleton]
  by_cases htop : M = ⊤
  · rw [htop]
    exact ⟨0, le_top⟩
  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)
  obtain ⟨x, hx, y, hy, hxy⟩ := (Ideal.not_isPrime_iff.mp h_prM).resolve_left htop
  obtain ⟨Wx, h_Wx⟩ := hgt (M + span R {x}) (lt_add _ hx)
  obtain ⟨Wy, h_Wy⟩ := hgt (M + span R {y}) (lt_add _ hy)
  use Wx + Wy
  rw [Multiset.map_add, Multiset.prod_add]
  apply le_trans (mul_le_mul' h_Wx h_Wy)
  rw [add_mul]
  apply sup_le (show M * (M + span R {y}) ≤ M from Ideal.mul_le_right)
  rw [mul_add]
  apply sup_le (show span R {x} * M ≤ M from Ideal.mul_le_left)
  rwa [span_mul_span, Set.singleton_mul_singleton, span_singleton_le_iff_mem]
Cleared hypotheses: I
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
A : Type u
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsNoetherianRing A
h_fA : ¬IsField A
M : Submodule A A
hgt :
  ∀ J > M,
    ∀ (h_nzI : J ≠ ⊥),
      ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : M ≠ ⊥
⊢ ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ M ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
have hgt₁ : ∀ (M : Ideal A)
  (hgt :
    ∀ J > M,
      ∀ (h_nzI : J ≠ ⊥),
        ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥)
  (h_nzI : M ≠ ⊥),
  ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ M ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
Tactic: change Ideal A at M
Cleared hypotheses: M, hgt, h_nzI
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (hypothesis)
Goal:
A : Type u
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsNoetherianRing A
h_fA : ¬IsField A
M : Ideal A
hgt :
  ∀ J > M,
    ∀ (h_nzI : J ≠ ⊥),
      ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : M ≠ ⊥
⊢ ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ M ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
have hA_nont : Nontrivial A
Tactic: have hA_nont : Nontrivial A := IsDomain.toNontrivial
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
A : Type u
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsNoetherianRing A
h_fA : ¬IsField A
M : Ideal A
hgt :
  ∀ J > M,
    ∀ (h_nzI : J ≠ ⊥),
      ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : M ≠ ⊥
hA_nont : Nontrivial A
⊢ ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ M ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
have pos : ∀ (h_topM : M = ⊤),
  ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ M ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
Tactic: by_cases h_topM : M = ⊤
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
A : Type u
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsNoetherianRing A
h_fA : ¬IsField A
M : Ideal A
hgt :
  ∀ J > M,
    ∀ (h_nzI : J ≠ ⊥),
      ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : M ≠ ⊥
hA_nont : Nontrivial A
pos :
  ∀ (h_topM : M = ⊤),
    ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ M ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
⊢ ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ M ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
have neg : ∀ (h_topM : ¬M = ⊤),
  ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ M ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
Tactic: by_cases h_topM : M = ⊤
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
A : Type u
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsNoetherianRing A
h_fA : ¬IsField A
M : Ideal A
hgt :
  ∀ J > M,
    ∀ (h_nzI : J ≠ ⊥),
      ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : M = ⊤
⊢ ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ M ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
have pos : ∀
  (hgt :
    ∀ J > ⊤,
      ∀ (h_nzI : J ≠ ⊥),
        ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥)
  (h_nzI : Ne.{u + 1} (α := Ideal A) ⊤ ⊥),
  ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ ⊤ ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
Tactic: rcases h_topM with rfl
Cleared hypotheses: M, hgt, h_nzI, h_topM
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
A : Type u
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsNoetherianRing A
h_fA : ¬IsField A
hA_nont : Nontrivial A
hgt :
  ∀ J > ⊤,
    ∀ (h_nzI : J ≠ ⊥),
      ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : Ne.{u + 1} (α := Ideal A) ⊤ ⊥
⊢ ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ ⊤ ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
have pos : ∀ (p_id : Ideal A) (h_nzp : p_id ≠ ⊥) (h_pp : p_id.IsPrime),
  ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ ⊤ ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
Tactic: obtain ⟨p_id, h_nzp, h_pp⟩ : ∃ p : Ideal A, p ≠ ⊥ ∧ p.IsPrime := by
      apply Ring.not_isField_iff_exists_prime.mp h_fA
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
A : Type u
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsNoetherianRing A
h_fA : ¬IsField A
hA_nont : Nontrivial A
hgt :
  ∀ J > ⊤,
    ∀ (h_nzI : J ≠ ⊥),
      ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : Ne.{u + 1} (α := Ideal A) ⊤ ⊥
p_id : Ideal A
h_nzp : p_id ≠ ⊥
h_pp : p_id.IsPrime
⊢ ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ ⊤ ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
have right : Ne (α := Ideal A) (Multiset.prod (Multiset.map asIdeal {{ asIdeal := p_id, isPrime := h_pp : PrimeSpectrum A }})) ⊥
Tactic: use ({⟨p_id, h_pp⟩} : Multiset (PrimeSpectrum A)), le_top
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
A : Type u
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsNoetherianRing A
h_fA : ¬IsField A
hA_nont : Nontrivial A
hgt :
  ∀ J > ⊤,
    ∀ (h_nzI : J ≠ ⊥),
      ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : Ne.{u + 1} (α := Ideal A) ⊤ ⊥
p_id : Ideal A
h_nzp : p_id ≠ ⊥
h_pp : p_id.IsPrime
⊢ Ne (α := Ideal A) (Multiset.prod (Multiset.map asIdeal {{ asIdeal := p_id, isPrime := h_pp : PrimeSpectrum A }})) ⊥
have right : Ne (α := Ideal A) (Multiset.prod {{ asIdeal := p_id, isPrime := h_pp : PrimeSpectrum A }.asIdeal}) ⊥
Tactic: rwa [Multiset.map_singleton, Multiset.prod_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
A : Type u
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsNoetherianRing A
h_fA : ¬IsField A
hA_nont : Nontrivial A
hgt :
  ∀ J > ⊤,
    ∀ (h_nzI : J ≠ ⊥),
      ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : Ne.{u + 1} (α := Ideal A) ⊤ ⊥
p_id : Ideal A
h_nzp : p_id ≠ ⊥
h_pp : p_id.IsPrime
right : Ne (α := Ideal A) (Multiset.prod {{ asIdeal := p_id, isPrime := h_pp : PrimeSpectrum A }.asIdeal}) ⊥
⊢ Ne (α := Ideal A) (Multiset.prod (Multiset.map asIdeal {{ asIdeal := p_id, isPrime := h_pp : PrimeSpectrum A }})) ⊥
have right₁ : { asIdeal := p_id, isPrime := h_pp : PrimeSpectrum A }.asIdeal ≠ ⊥
Tactic: rwa [Multiset.map_singleton, Multiset.prod_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
A : Type u
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsNoetherianRing A
h_fA : ¬IsField A
M : Ideal A
hgt :
  ∀ J > M,
    ∀ (h_nzI : J ≠ ⊥),
      ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
⊢ ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ M ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
have pos : ∀ (h_prM : M.IsPrime),
  ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ M ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
Tactic: by_cases h_prM : M.IsPrime