awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 = ⊤
pos :
  ∀ (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 ≠ ⊥
have neg : ∀ (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
-- 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 = ⊤
h_prM : M.IsPrime
⊢ ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ M ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
have 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 }})) ⊥
Tactic: use ({⟨M, h_prM⟩} : Multiset (PrimeSpectrum A))
-- 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 = ⊤
h_prM : M.IsPrime
⊢ 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 }})) ⊥
have h : { asIdeal := M, isPrime := h_prM : PrimeSpectrum A }.asIdeal ≤ M ∧
  { asIdeal := M, isPrime := h_prM : PrimeSpectrum A }.asIdeal ≠ ⊥
Tactic: rw [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 = ⊤
h_prM : ¬M.IsPrime
⊢ ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ M ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
have 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 ≠ ⊥
Tactic: obtain ⟨x, hx, y, hy, h_xy⟩ := (Ideal.not_isPrime_iff.mp h_prM).resolve_left 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
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
have refine : ∀ (m_eq : M = M + A ∙ 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:
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
have rw : z ∈ M + A ∙ z
Tactic: rw [m_eq]
-- 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 ≠ ⊥
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 : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ M ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
have lt_add : ∀ 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)
-- 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 = ⊤
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
⊢ ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ M ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
have 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 ≠ ⊥
Tactic: obtain ⟨Wx, h_Wx_le, h_Wx_ne⟩ := hgt (M + span A {x}) (lt_add _ hx) (ne_bot_of_gt (lt_add _ hx))
-- 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 = ⊤
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 ≠ ⊥
⊢ ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ M ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
have 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 ≠ ⊥
Tactic: obtain ⟨Wy, h_Wy_le, h_Wx_ne⟩ := hgt (M + span A {y}) (lt_add _ hy) (ne_bot_of_gt (lt_add _ hy))
-- 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 = ⊤
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 ≠ ⊥
⊢ ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ M ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
have h : (Multiset.map asIdeal (Wx + Wy)).prod ≤ M ∧ (Multiset.map asIdeal (Wx + Wy)).prod ≠ ⊥
Tactic: use Wx + Wy
-- 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 = ⊤
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 ≠ ⊥
⊢ (Multiset.map asIdeal (Wx + Wy)).prod ≤ M ∧ (Multiset.map asIdeal (Wx + Wy)).prod ≠ ⊥
have h : (Multiset.map asIdeal Wx).prod * (Multiset.map asIdeal Wy).prod ≤ M ∧
  (Multiset.map asIdeal Wx).prod * (Multiset.map asIdeal Wy).prod ≠ ⊥
Tactic: rw [Multiset.map_add, Multiset.prod_add]
-- 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 = ⊤
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 ≠ ⊥
⊢ (Multiset.map asIdeal Wx).prod * (Multiset.map asIdeal Wy).prod ≤ M ∧
    (Multiset.map asIdeal Wx).prod * (Multiset.map asIdeal Wy).prod ≠ ⊥
have h : (M + A ∙ x) * (M + A ∙ y) ≤ M
Tactic: refine ⟨le_trans (mul_le_mul' h_Wx_le h_Wy_le) ?_, mt Ideal.mul_eq_bot.mp ?_⟩
-- 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 = ⊤
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 : (M + A ∙ x) * (M + A ∙ y) ≤ M
⊢ (Multiset.map asIdeal Wx).prod * (Multiset.map asIdeal Wy).prod ≤ M ∧
    (Multiset.map asIdeal Wx).prod * (Multiset.map asIdeal Wy).prod ≠ ⊥
have h₁ : ¬((Multiset.map asIdeal Wx).prod = ⊥ ∨ (Multiset.map asIdeal Wy).prod = ⊥)
Tactic: refine ⟨le_trans (mul_le_mul' h_Wx_le h_Wy_le) ?_, mt Ideal.mul_eq_bot.mp ?_⟩
-- 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 = ⊤
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 ≠ ⊥
⊢ (M + A ∙ x) * (M + A ∙ y) ≤ M
have h : M * (M + A ∙ y) + (A ∙ x) * (M + A ∙ y) ≤ M
Tactic: rw [add_mul]
-- 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 = ⊤
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 ≠ ⊥
⊢ M * (M + A ∙ y) + (A ∙ x) * (M + A ∙ y) ≤ M
have h : (A ∙ x) * (M + A ∙ y) ≤ M
Tactic: apply sup_le (show M * (M + span A {y}) ≤ M from Ideal.mul_le_right)
-- 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 = ⊤
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 ≠ ⊥
⊢ (A ∙ x) * (M + A ∙ y) ≤ M
have h : (A ∙ x) * M + HMul.hMul (α := Ideal A) (A ∙ x) (A ∙ y) ≤ M
Tactic: rw [mul_add]
-- 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 = ⊤
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 ≠ ⊥
⊢ (A ∙ x) * M + HMul.hMul (α := Ideal A) (A ∙ x) (A ∙ y) ≤ M
have h : HMul.hMul (α := Ideal A) (A ∙ x) (A ∙ y) ≤ M
Tactic: apply sup_le (show span A {x} * M ≤ M from Ideal.mul_le_left)
-- 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 = ⊤
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 ≠ ⊥
⊢ HMul.hMul (α := Ideal A) (A ∙ x) (A ∙ y) ≤ M
have h : span A (HMul.hMul (α := Set A) {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:
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 : span A (HMul.hMul (α := Set A) {x} {y}) ≤ M
⊢ HMul.hMul (α := Ideal A) (A ∙ x) (A ∙ y) ≤ M
have h₁ : A ∙ 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:
A : Type u
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsNoetherianRing A
h_fA : ¬IsField A
I : Ideal A
h_nzI : I ≠ ⊥
⊢ ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ I ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
have hgt : ∀ (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 ≠ ⊥
Tactic: induction I using IsNoetherian.induction with | hgt M hgt =>
  change Ideal A at M
  have hA_nont : Nontrivial A := IsDomain.toNontrivial
  by_cases h_topM : M = ⊤
  · rcases h_topM with rfl
    obtain ⟨p_id, h_nzp, h_pp⟩ : ∃ p : Ideal A, p ≠ ⊥ ∧ p.IsPrime := by
      apply Ring.not_isField_iff_exists_prime.mp h_fA
    use ({⟨p_id, h_pp⟩} : Multiset (PrimeSpectrum A)), le_top
    rwa [Multiset.map_singleton, Multiset.prod_singleton]
  by_cases h_prM : M.IsPrime
  · use ({⟨M, h_prM⟩} : Multiset (PrimeSpectrum A))
    rw [Multiset.map_singleton, Multiset.prod_singleton]
    exact ⟨le_rfl, h_nzI⟩
  obtain ⟨x, hx, y, hy, h_xy⟩ := (Ideal.not_isPrime_iff.mp h_prM).resolve_left h_topM
  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)
  obtain ⟨Wx, h_Wx_le, h_Wx_ne⟩ := hgt (M + span A {x}) (lt_add _ hx) (ne_bot_of_gt (lt_add _ hx))
  obtain ⟨Wy, h_Wy_le, h_Wx_ne⟩ := hgt (M + span A {y}) (lt_add _ hy) (ne_bot_of_gt (lt_add _ hy))
  use Wx + Wy
  rw [Multiset.map_add, Multiset.prod_add]
  refine ⟨le_trans (mul_le_mul' h_Wx_le h_Wy_le) ?_, mt Ideal.mul_eq_bot.mp ?_⟩
  · rw [add_mul]
    apply sup_le (show M * (M + span A {y}) ≤ M from Ideal.mul_le_right)
    rw [mul_add]
    apply sup_le (show span A {x} * M ≤ M from Ideal.mul_le_left)
    rwa [span_mul_span, Set.singleton_mul_singleton, span_singleton_le_iff_mem]
  · rintro (hx | hy) <;> contradiction
Cleared hypotheses: I, h_nzI
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Chevalley (goal)
Goal:
R : Type u_1
inst : CommRing R
s : Set (PrimeSpectrum R[X])
hs : IsConstructible s
⊢ IsConstructible (comap Polynomial.C '' s)
have obtain : ∀ (S : ConstructibleSetData R[X]) (hs : IsConstructible (X := PrimeSpectrum R[X]) S.toSet),
  IsConstructible (comap Polynomial.C '' S.toSet)
Tactic: obtain ⟨S, rfl⟩ := exists_constructibleSetData_iff.mpr hs
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Chevalley (goal)
Goal:
R : Type u_1
inst : CommRing R
S : ConstructibleSetData R[X]
hs : IsConstructible (X := PrimeSpectrum R[X]) S.toSet
⊢ IsConstructible (comap Polynomial.C '' S.toSet)
have obtain : ∀ (T : ConstructibleSetData R) (hT : comap Polynomial.C '' S.toSet = T.toSet),
  IsConstructible (comap Polynomial.C '' S.toSet)
Tactic: obtain ⟨T, hT, -⟩ := ChevalleyThm.chevalley_polynomialC _ Submodule.mem_top S (by simp)
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Chevalley (goal)
Goal:
R : Type u_1
inst : CommRing R
S : ConstructibleSetData R[X]
hs : IsConstructible (X := PrimeSpectrum R[X]) S.toSet
T : ConstructibleSetData R
hT : comap Polynomial.C '' S.toSet = T.toSet
⊢ IsConstructible (comap Polynomial.C '' S.toSet)
have rw : IsConstructible (X := PrimeSpectrum R) T.toSet
Tactic: rw [hT]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Chevalley (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.FinitePresentation
s : Set (PrimeSpectrum S)
hs : IsConstructible s
⊢ IsConstructible (comap f '' s)
have refine_1 : ∀ (R : Type u_1) [inst : CommRing R] (S : Type u_2) [inst_2 : CommRing S] (f : R →+* S),
  Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S) →
    Ideal.FG (RingHom.ker f) →
      (fun (x : Type u_1) (x_1 : CommRing x) (x_2 : Type u_2) (x_3 : CommRing x_2) (f : x →+* x_2) ↦
          ∀ (s : Set (PrimeSpectrum x_2)), IsConstructible s → IsConstructible (comap f '' s))
        R inst S inst_2 f
Tactic: refine hf.polynomial_induction
    (fun _ _ _ _ f ↦ ∀ s, IsConstructible s → IsConstructible (comap f '' s))
    (fun _ _ _ _ f ↦ ∀ s, IsConstructible s → IsConstructible (comap f '' s))
    (fun _ _ _ ↦ isConstructible_comap_C) ?_ ?_ f s hs
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Chevalley (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.FinitePresentation
s : Set (PrimeSpectrum S)
hs : IsConstructible s
refine_1 :
  ∀ (R : Type u_1) [inst : CommRing R] (S : Type u_2) [inst_2 : CommRing S] (f : R →+* S),
    Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S) →
      Ideal.FG (RingHom.ker f) →
        (fun (x : Type u_1) (x_1 : CommRing x) (x_2 : Type u_2) (x_3 : CommRing x_2) (f : x →+* x_2) ↦
            ∀ (s : Set (PrimeSpectrum x_2)), IsConstructible s → IsConstructible (comap f '' s))
          R inst S inst_2 f
⊢ IsConstructible (comap f '' s)
have refine_2 : ∀ (R : Type u_1) [inst : CommRing R] (S : Type u_1) [inst_2 : CommRing S] (T : Type u_2) [inst_3 : CommRing T]
  (f : R →+* S) (g : S →+* T),
  (fun (x : Type u_1) (x_1 : CommRing x) (x_2 : Type u_1) (x_3 : CommRing x_2) (f : x →+* x_2) ↦
        ∀ (s : Set (PrimeSpectrum x_2)), IsConstructible s → IsConstructible (comap f '' s))
      R inst S inst_2 f →
    (fun (x : Type u_1) (x_1 : CommRing x) (x_2 : Type u_2) (x_3 : CommRing x_2) (f : x →+* x_2) ↦
          ∀ (s : Set (PrimeSpectrum x_2)), IsConstructible s → IsConstructible (comap f '' s))
        S inst_2 T inst_3 g →
      (fun (x : Type u_1) (x_1 : CommRing x) (x_2 : Type u_2) (x_3 : CommRing x_2) (f : x →+* x_2) ↦
          ∀ (s : Set (PrimeSpectrum x_2)), IsConstructible s → IsConstructible (comap f '' s))
        R inst T inst_3 (g.comp f)
Tactic: refine hf.polynomial_induction
    (fun _ _ _ _ f ↦ ∀ s, IsConstructible s → IsConstructible (comap f '' s))
    (fun _ _ _ _ f ↦ ∀ s, IsConstructible s → IsConstructible (comap f '' s))
    (fun _ _ _ ↦ isConstructible_comap_C) ?_ ?_ f s hs
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Chevalley (goal)
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
f_1 : R_1 →+* S_1
hf_1 : f_1.FinitePresentation
s_1 : Set (PrimeSpectrum S_1)
hs_1 : IsConstructible s_1
R : Type u_1
inst_2 : CommRing R
S : Type u_2
inst_3 : CommRing S
f : R →+* S
hf : Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
hf' : Ideal.FG (RingHom.ker f)
s : Set (PrimeSpectrum S)
hs : IsConstructible s
⊢ IsConstructible (comap f '' s)
have refine_1 : IsRetrocompact (Set.range (comap f))ᶜ
Tactic: refine hs.image_of_isClosedEmbedding (isClosedEmbedding_comap_of_surjective _ f hf) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Chevalley (goal)
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
f_1 : R_1 →+* S_1
hf_1 : f_1.FinitePresentation
s_1 : Set (PrimeSpectrum S_1)
hs_1 : IsConstructible s_1
R : Type u_1
inst_2 : CommRing R
S : Type u_2
inst_3 : CommRing S
f : R →+* S
hf : Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
hf' : Ideal.FG (RingHom.ker f)
s : Set (PrimeSpectrum S)
hs : IsConstructible s
⊢ IsRetrocompact (Set.range (comap f))ᶜ
have refine_1 : IsRetrocompact (X := PrimeSpectrum R) (zeroLocus (↑(RingHom.ker f) : Set R))ᶜ
Tactic: rw [range_comap_of_surjective _ f hf]