awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
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 : (M + R ∙ x) * (M + R ∙ y) ≤ M
⊢ (Multiset.map asIdeal Wx).prod * (Multiset.map asIdeal Wy).prod ≤ M

Tactic:
apply le_trans (mul_le_mul' h_Wx h_Wy)

Premises used: mul_le_mul', le_trans
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
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 : M * (M + R ∙ y) + (R ∙ x) * (M + R ∙ y) ≤ M
⊢ (M + R ∙ x) * (M + R ∙ y) ≤ M

Tactic:
rw [add_mul]

Premises used: add_mul
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
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 : (R ∙ x) * (M + R ∙ y) ≤ M
⊢ M * (M + R ∙ y) + (R ∙ x) * (M + R ∙ y) ≤ M

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

Premises used: Ideal.mul_le_right, sup_le
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
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 : (R ∙ x) * M + HMul.hMul (α := Ideal R) (R ∙ x) (R ∙ y) ≤ M
⊢ (R ∙ x) * (M + R ∙ y) ≤ M

Tactic:
rw [mul_add]

Premises used: mul_add
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
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 : HMul.hMul (α := Ideal R) (R ∙ x) (R ∙ y) ≤ M
⊢ (R ∙ x) * M + HMul.hMul (α := Ideal R) (R ∙ x) (R ∙ y) ≤ M

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

Premises used: Ideal.mul_le_left, sup_le
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
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
h₁ : R ∙ x * y ≤ M
h₂ h₃ h₄ h₅ : x * y ∈ M
⊢ HMul.hMul (α := Ideal R) (R ∙ x) (R ∙ y) ≤ M

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

Premises used: Submodule.span_mul_span, Submodule.span_singleton_le_iff_mem, Set.singleton_mul_singleton
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
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
⊢ ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ I

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]

Premises used: add_mul, IsNoetherian.induction, Multiset.map_singleton, Submodule.span_mul_span, Multiset.prod_singleton, Ideal, Multiset.prod_add, mul_add, Submodule.span_singleton_le_iff_mem, Multiset.map_add, Set.singleton_mul_singleton
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
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 ≠ ⊥
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 ≠ ⊥
⊢ ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ M ∧ (Multiset.map asIdeal Z).prod ≠ ⊥

Tactic:
change Ideal A at M

Premises used: Ideal
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
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 ≠ ⊥
⊢ Nontrivial A

Tactic:
have hA_nont : Nontrivial A := IsDomain.toNontrivial
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
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 ≠ ⊥
neg :
  ∀ (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 ≠ ⊥

Tactic:
by_cases h_topM : M = ⊤
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
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 = ⊤
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 ≠ ⊥
⊢ ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ M ∧ (Multiset.map asIdeal Z).prod ≠ ⊥

Tactic:
rcases h_topM with rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
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 : Ideal A), p ≠ ⊥ ∧ p.IsPrime

Tactic:
apply Ring.not_isField_iff_exists_prime.mp h_fA

Premises used: Ring.not_isField_iff_exists_prime, Iff.mp
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
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) ⊤ ⊥
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 ≠ ⊥
⊢ ∃ (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

Premises used: Ideal
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
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 (Multiset.map asIdeal {{ asIdeal := p_id, isPrime := h_pp : PrimeSpectrum A }})) ⊥
⊢ ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ ⊤ ∧ (Multiset.map asIdeal Z).prod ≠ ⊥

Tactic:
use ({⟨p_id, h_pp⟩} : Multiset (PrimeSpectrum A)), le_top

Premises used: le_top, Singleton.singleton
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
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}) ⊥
right₁ right₂ right₃ right₄ : { 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 }})) ⊥

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

Premises used: Multiset.map_singleton, Multiset.prod_singleton
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
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 = ⊤
pos :
  ∀ (h_prM : M.IsPrime),
    ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ M ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
neg :
  ∀ (h_prM : ¬M.IsPrime),
    ∃ (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 ≠ ⊥

Tactic:
by_cases h_prM : M.IsPrime

Premises used: Ideal.IsPrime
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
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 = ⊤
h_prM : M.IsPrime
h :
  Multiset.prod (Multiset.map asIdeal {{ asIdeal := M, isPrime := h_prM : PrimeSpectrum A }}) ≤ M ∧
    Ne (α := Ideal A) (Multiset.prod (Multiset.map asIdeal {{ asIdeal := M, isPrime := h_prM : PrimeSpectrum A }})) ⊥
⊢ ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ M ∧ (Multiset.map asIdeal Z).prod ≠ ⊥

Tactic:
use ({⟨M, h_prM⟩} : Multiset (PrimeSpectrum A))

Premises used: Singleton.singleton
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
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 = ⊤
h_prM : M.IsPrime
h :
  { asIdeal := M, isPrime := h_prM : PrimeSpectrum A }.asIdeal ≤ M ∧
    { asIdeal := M, isPrime := h_prM : PrimeSpectrum A }.asIdeal ≠ ⊥
⊢ Multiset.prod (Multiset.map asIdeal {{ asIdeal := M, isPrime := h_prM : PrimeSpectrum A }}) ≤ M ∧
    Ne (α := Ideal A) (Multiset.prod (Multiset.map asIdeal {{ asIdeal := M, isPrime := h_prM : PrimeSpectrum A }})) ⊥

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

Premises used: Multiset.map_singleton, Multiset.prod_singleton
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
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 = ⊤
h_prM : M.IsPrime
⊢ { asIdeal := M, isPrime := h_prM : PrimeSpectrum A }.asIdeal ≤ M ∧
    { asIdeal := M, isPrime := h_prM : PrimeSpectrum A }.asIdeal ≠ ⊥

Tactic:
⟨le_rfl, h_nzI⟩

Premises used: le_rfl, And.intro
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
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 = ⊤
h_prM : M.IsPrime
⊢ { asIdeal := M, isPrime := h_prM : PrimeSpectrum A }.asIdeal ≤ M ∧
    { asIdeal := M, isPrime := h_prM : PrimeSpectrum A }.asIdeal ≠ ⊥

Tactic:
exact ⟨le_rfl, h_nzI⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
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 = ⊤
h_prM : ¬M.IsPrime
neg :
  ∀ (x : A) (hx : x ∉ M) (y : A) (hy : y ∉ M) (h_xy : x * y ∈ 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 ≠ ⊥

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

Premises used: Or.resolve_left, Ideal.not_isPrime_iff, Iff.mp
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
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 = ⊤
h_prM : ¬M.IsPrime
x : A
hx : x ∉ M
y : A
hy : y ∉ M
h_xy : x * y ∈ M
z : A
hz : z ∉ M
⊢ M < M + A ∙ z

Tactic:
lt_of_le_of_ne le_sup_left fun m_eq => hz ?_

Premises used: le_sup_left, lt_of_le_of_ne
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
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 = ⊤
h_prM : ¬M.IsPrime
x : A
hx : x ∉ M
y : A
hy : y ∉ M
h_xy : x * y ∈ M
z : A
hz : z ∉ M
refine : ∀ (m_eq : M = M + A ∙ z), z ∈ M
⊢ M < M + A ∙ z

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

Premises used: le_sup_left, lt_of_le_of_ne
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
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 = ⊤
h_prM : ¬M.IsPrime
x : A
hx : x ∉ M
y : A
hy : y ∉ M
h_xy : x * y ∈ M
z : A
hz : z ∉ M
m_eq : M = M + A ∙ z
rw : z ∈ M + A ∙ z
⊢ z ∈ M

Tactic:
rw [m_eq]
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
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 = ⊤
h_prM : ¬M.IsPrime
x : A
hx : x ∉ M
y : A
hy : y ∉ M
h_xy : x * y ∈ M
z : A
hz : z ∉ M
m_eq : M = M + A ∙ z
⊢ z ∈ M + A ∙ z

Tactic:
mem_sup_right (mem_span_singleton_self z)

Premises used: Set.Mem, Submodule.mem_span_singleton_self, Submodule.mem_sup_right
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
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 = ⊤
h_prM : ¬M.IsPrime
x : A
hx : x ∉ M
y : A
hy : y ∉ M
h_xy : x * y ∈ M
z : A
hz : z ∉ M
m_eq : M = M + A ∙ z
⊢ z ∈ M + A ∙ z

Tactic:
exact mem_sup_right (mem_span_singleton_self z)

Premises used: Submodule.mem_span_singleton_self, Submodule.mem_sup_right
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
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 = ⊤
h_prM : ¬M.IsPrime
x : A
hx : x ∉ M
y : A
hy : y ∉ M
h_xy : x * y ∈ M
⊢ ∀ z ∉ M, M < M + A ∙ z

Tactic:
have lt_add : ∀ z ∉ M, M < M + span A {z} := by
    intro z hz
    refine lt_of_le_of_ne le_sup_left fun m_eq => hz ?_
    rw [m_eq]
    exact mem_sup_right (mem_span_singleton_self z)
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
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 = ⊤
h_prM : ¬M.IsPrime
x : A
hx : x ∉ M
y : A
hy : y ∉ M
h_xy : x * y ∈ M
lt_add : ∀ z ∉ M, M < M + A ∙ z
neg :
  ∀ (Wx : Multiset (PrimeSpectrum A)) (h_Wx_le : (Multiset.map asIdeal Wx).prod ≤ M + A ∙ x)
    (h_Wx_ne : (Multiset.map asIdeal Wx).prod ≠ ⊥),
    ∃ (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 ≠ ⊥

Tactic:
obtain ⟨Wx, h_Wx_le, h_Wx_ne⟩ := hgt (M + span A {x}) (lt_add _ hx) (ne_bot_of_gt (lt_add _ hx))

Premises used: HAdd.hAdd, Submodule.span, Singleton.singleton, ne_bot_of_gt
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
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 = ⊤
h_prM : ¬M.IsPrime
x : A
hx : x ∉ M
y : A
hy : y ∉ M
h_xy : x * y ∈ M
lt_add : ∀ z ∉ M, M < M + A ∙ z
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : (Multiset.map asIdeal Wx).prod ≤ M + A ∙ x
h_Wx_ne : (Multiset.map asIdeal Wx).prod ≠ ⊥
neg :
  ∀ (Wy : Multiset (PrimeSpectrum A)) (h_Wy_le : (Multiset.map asIdeal Wy).prod ≤ M + A ∙ y)
    (h_Wx_ne : (Multiset.map asIdeal Wy).prod ≠ ⊥),
    ∃ (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 ≠ ⊥

Tactic:
obtain ⟨Wy, h_Wy_le, h_Wx_ne⟩ := hgt (M + span A {y}) (lt_add _ hy) (ne_bot_of_gt (lt_add _ hy))

Premises used: HAdd.hAdd, Submodule.span, Singleton.singleton, ne_bot_of_gt
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
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 = ⊤
h_prM : ¬M.IsPrime
x : A
hx : x ∉ M
y : A
hy : y ∉ M
h_xy : x * y ∈ M
lt_add : ∀ z ∉ M, M < M + A ∙ z
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : (Multiset.map asIdeal Wx).prod ≤ M + A ∙ x
h_Wx_ne_1 : (Multiset.map asIdeal Wx).prod ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : (Multiset.map asIdeal Wy).prod ≤ M + A ∙ y
h_Wx_ne : (Multiset.map asIdeal Wy).prod ≠ ⊥
h : (Multiset.map asIdeal (Wx + Wy)).prod ≤ M ∧ (Multiset.map asIdeal (Wx + Wy)).prod ≠ ⊥
⊢ ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ M ∧ (Multiset.map asIdeal Z).prod ≠ ⊥

Tactic:
use Wx + Wy
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
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 = ⊤
h_prM : ¬M.IsPrime
x : A
hx : x ∉ M
y : A
hy : y ∉ M
h_xy : x * y ∈ M
lt_add : ∀ z ∉ M, M < M + A ∙ z
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : (Multiset.map asIdeal Wx).prod ≤ M + A ∙ x
h_Wx_ne_1 : (Multiset.map asIdeal Wx).prod ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : (Multiset.map asIdeal Wy).prod ≤ M + A ∙ y
h_Wx_ne : (Multiset.map asIdeal Wy).prod ≠ ⊥
h :
  (Multiset.map asIdeal Wx).prod * (Multiset.map asIdeal Wy).prod ≤ M ∧
    (Multiset.map asIdeal Wx).prod * (Multiset.map asIdeal Wy).prod ≠ ⊥
⊢ (Multiset.map asIdeal (Wx + Wy)).prod ≤ M ∧ (Multiset.map asIdeal (Wx + Wy)).prod ≠ ⊥

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

Premises used: Multiset.prod_add, Multiset.map_add