awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
ι : Sort u_1
s : ι → Set R
⊢ Eq.{u + 1} (α := Set (PrimeSpectrum R)) (zeroLocus (⋃ (i : ι), s i)) (⋂ (i : ι), zeroLocus (s i))

Tactic:
(gc_set R).l_iSup

Premises used: iInf, Set.Mem, Set.iInter, setOf, GaloisConnection.l_iSup, PrimeSpectrum.gc_set, OrderDual, Set.iUnion
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
ι : Sort u_1
κ : (i : ι) → Sort u_2
s : (i : ι) → κ i → Set R
⊢ Eq.{u + 1} (α := Set (PrimeSpectrum R)) (zeroLocus (⋃ (i : ι), ⋃ (j : κ i), s i j))
    (⋂ (i : ι), ⋂ (j : κ i), zeroLocus (s i j))

Tactic:
(gc_set R).l_iSup₂

Premises used: iInf, Set.Mem, Set.iInter, setOf, GaloisConnection.l_iSup₂, PrimeSpectrum.gc_set, OrderDual, Set.iUnion
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
s : Set (Set R)
⊢ Eq.{u + 1} (α := Set (PrimeSpectrum R)) (zeroLocus (⋃ s' ∈ s, s')) (⋂ s' ∈ s, zeroLocus s')

Tactic:
simp only [zeroLocus_iUnion]

Premises used: PrimeSpectrum.zeroLocus_iUnion
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
ι : Sort u_1
t : ι → Set (PrimeSpectrum R)
⊢ Eq.{u + 1} (α := Ideal R) (vanishingIdeal (⋃ (i : ι), t i)) (⨅ (i : ι), vanishingIdeal (t i))

Tactic:
(gc R).u_iInf

Premises used: PrimeSpectrum.gc, Set.Mem, iSup, setOf, GaloisConnection.u_iInf, OrderDual, Set.iUnion
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑(I ⊓ J) : Set R)) (zeroLocus (↑I : Set R) ∪ zeroLocus (↑J : Set R))

Tactic:
Set.ext fun x => x.2.inf_le

Premises used: Set.ext, PrimeSpectrum.isPrime, Ideal.IsPrime.inf_le
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
s s' : Set R
rw :
  Eq (α := Set (PrimeSpectrum R)) (zeroLocus s ∪ zeroLocus s')
    (zeroLocus (↑(Ideal.span s) : Set R) ∪ zeroLocus (↑(Ideal.span s') : Set R))
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus s ∪ zeroLocus s') (zeroLocus (↑(Ideal.span s ⊓ Ideal.span s') : Set R))

Tactic:
rw [zeroLocus_inf]

Premises used: PrimeSpectrum.zeroLocus_inf
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
s s' : Set R
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus s ∪ zeroLocus s')
    (zeroLocus (↑(Ideal.span s) : Set R) ∪ zeroLocus (↑(Ideal.span s') : Set R))

Tactic:
simp
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑(I * J) : Set R)) (zeroLocus (↑I : Set R) ∪ zeroLocus (↑J : Set R))

Tactic:
Set.ext fun x => x.2.mul_le

Premises used: Set.ext, PrimeSpectrum.isPrime, Ideal.IsPrime.mul_le
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
f g : R
x : PrimeSpectrum R
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus {f * g}) x ↔
    Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus {f} ∪ zeroLocus {g}) x

Tactic:
simpa using x.2.mul_mem_iff_mem_or_mem

Premises used: PrimeSpectrum.isPrime, Ideal.IsPrime.mul_mem_iff_mem_or_mem
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
n : ℕ
hn : n ≠ 0
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑(I ^ n) : Set R)) (zeroLocus (↑I : Set R))

Tactic:
zeroLocus_radical (I ^ n) ▸ (I.radical_pow hn).symm ▸ zeroLocus_radical I

Premises used: PrimeSpectrum.zeroLocus_radical, Eq.rec, HPow.hPow, Ideal.radical_pow, Eq.symm
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
f : R
n : ℕ
hn : 0 < n
x : PrimeSpectrum R
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus {f ^ n}) x ↔
    Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus {f}) x

Tactic:
simpa using x.2.pow_mem_iff_mem n hn

Premises used: Ideal.IsPrime.pow_mem_iff_mem, PrimeSpectrum.isPrime
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
t t' : Set (PrimeSpectrum R)
r : R
rw : (∃ y ∈ vanishingIdeal t, ∃ z ∈ vanishingIdeal t', y + z = r) → ∀ x ∈ t ∩ t', r ∈ x.asIdeal
⊢ r ∈ vanishingIdeal t ⊔ vanishingIdeal t' → r ∈ vanishingIdeal (t ∩ t')

Tactic:
rw [Submodule.mem_sup, mem_vanishingIdeal]

Premises used: PrimeSpectrum.mem_vanishingIdeal, Submodule.mem_sup
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
t t' : Set (PrimeSpectrum R)
f : R
hf : f ∈ vanishingIdeal t
g : R
hg : g ∈ vanishingIdeal t'
x : PrimeSpectrum R
hxt : x ∈ t
hxt' : x ∈ t'
rw :
  ∀ (hf : ∀ x ∈ t, f ∈ x.asIdeal) (g : R) (hg : ∀ x ∈ t', g ∈ x.asIdeal) (x : PrimeSpectrum R) (hxt : x ∈ t)
    (hxt' : x ∈ t'), f + g ∈ x.asIdeal
⊢ f + g ∈ x.asIdeal

Tactic:
rw [mem_vanishingIdeal] at hf hg

Premises used: PrimeSpectrum.mem_vanishingIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
t t' : Set (PrimeSpectrum R)
f : R
hf : ∀ x ∈ t, f ∈ x.asIdeal
g : R
hg : ∀ x ∈ t', g ∈ x.asIdeal
x : PrimeSpectrum R
hxt : x ∈ t
hxt' : x ∈ t'
h₁ : f ∈ x.asIdeal
h₂ : g ∈ x.asIdeal
⊢ f + g ∈ x.asIdeal

Tactic:
apply Submodule.add_mem

Premises used: Submodule.add_mem
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
t t' : Set (PrimeSpectrum R)
f : R
hf : ∀ x ∈ t, f ∈ x.asIdeal
g : R
hg : ∀ x ∈ t', g ∈ x.asIdeal
x : PrimeSpectrum R
hxt : x ∈ t
hxt' : x ∈ t'
⊢ f ∈ x.asIdeal

Tactic:
solve_by_elim
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
t t' : Set (PrimeSpectrum R)
f : R
hf : ∀ x ∈ t, f ∈ x.asIdeal
g : R
hg : ∀ x ∈ t', g ∈ x.asIdeal
x : PrimeSpectrum R
hxt : x ∈ t
hxt' : x ∈ t'
⊢ g ∈ x.asIdeal

Tactic:
solve_by_elim
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
f : R
I : PrimeSpectrum R
rw : f ∉ (↑I.asIdeal : Set R) ↔ f ∉ I.asIdeal
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus {f})ᶜ I ↔ f ∉ I.asIdeal

Tactic:
rw [Set.mem_compl_iff, mem_zeroLocus, Set.singleton_subset_iff]

Premises used: Set.singleton_subset_iff, PrimeSpectrum.mem_zeroLocus, Set.mem_compl_iff
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
f : R
I : PrimeSpectrum R
⊢ f ∉ (↑I.asIdeal : Set R) ↔ f ∉ I.asIdeal

Tactic:
rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
s : Set R
rw : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (s ∪ {0})) (zeroLocus s)
rw₁ : Eq (α := Set (PrimeSpectrum R)) (zeroLocus s ∩ zeroLocus {0}) (zeroLocus s)
rw₂ : Eq (α := Set (PrimeSpectrum R)) (zeroLocus s ∩ Set.univ) (zeroLocus s)
rw₃ rw₄ : Eq (α := Set (PrimeSpectrum R)) (zeroLocus s) (zeroLocus s)
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus (insert 0 s)) (zeroLocus s)

Tactic:
rw [← Set.union_singleton, zeroLocus_union, zeroLocus_singleton_zero, Set.inter_univ]

Premises used: Set.inter_univ, PrimeSpectrum.zeroLocus_union, Set.union_singleton, PrimeSpectrum.zeroLocus_singleton_zero
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
s : Set R
rw : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (insert 0 (s \ {0}))) (zeroLocus (insert 0 s))
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus (s \ {0})) (zeroLocus s)

Tactic:
rw [← zeroLocus_insert_zero, ← zeroLocus_insert_zero (s := s)]

Premises used: PrimeSpectrum.zeroLocus_insert_zero
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
s : Set R
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus (insert 0 (s \ {0}))) (zeroLocus (insert 0 s))

Tactic:
simp
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
r : R
hr : IsUnit r
s : Set R
h :
  ∀ (x : PrimeSpectrum R),
    Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (r • s)) x ↔
      Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus s) x
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus (r • s)) (zeroLocus s)

Tactic:
ext
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
r : R
hr : IsUnit r
s : Set R
x : PrimeSpectrum R
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (r • s)) x ↔
    Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus s) x

Tactic:
simp [Set.subset_def, ← Set.image_smul, Ideal.unit_mul_mem_iff_mem _ hr]

Premises used: Set.image_smul, Set.subset_def, Ideal.unit_mul_mem_iff_mem
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsDomain R
⊢ Eq.{u + 1} (α := Ideal R) (asIdeal ⊥) ⊥

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
x : PrimeSpectrum R
⊢ IsMax x ↔ x.asIdeal.IsMaximal

Tactic:
⟨fun hx ↦ ⟨⟨x.2.ne_top, fun I hI ↦ ?_⟩⟩, fun hx y e ↦ (hx.eq_of_le y.2.ne_top e).ge⟩

Premises used: Eq.ge, PrimeSpectrum.isPrime, Ideal.IsMaximal.mk, Ideal.IsMaximal.eq_of_le, And.intro, Iff.intro, Ideal.IsPrime.ne_top
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
x : PrimeSpectrum R
refine : ∀ (hx : IsMax x) (I : Ideal R) (hI : x.asIdeal < I), I = ⊤
⊢ IsMax x ↔ x.asIdeal.IsMaximal

Tactic:
refine ⟨fun hx ↦ ⟨⟨x.2.ne_top, fun I hI ↦ ?_⟩⟩, fun hx y e ↦ (hx.eq_of_le y.2.ne_top e).ge⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
x : PrimeSpectrum R
hx : IsMax x
I : Ideal R
hI : x.asIdeal < I
by_contra : ∀ (e : ¬I = ⊤), False
⊢ I = ⊤

Tactic:
by_contra e
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
x : PrimeSpectrum R
hx : IsMax x
I : Ideal R
hI : x.asIdeal < I
e : ¬I = ⊤
obtain : ∀ (m : Ideal R) (hm : m.IsMaximal) (hm' : I ≤ m), False
⊢ False

Tactic:
obtain ⟨m, hm, hm'⟩ := Ideal.exists_le_maximal I e

Premises used: Ideal.exists_le_maximal
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
x : PrimeSpectrum R
hx : IsMax x
I : Ideal R
hI : x.asIdeal < I
e : ¬I = ⊤
m : Ideal R
hm : m.IsMaximal
hm' : I ≤ m
⊢ False

Tactic:
hx.not_lt (show x < ⟨m, hm.isPrime⟩ from hI.trans_le hm')

Premises used: LT.lt.trans_le, IsMax.not_lt
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
x : PrimeSpectrum R
hx : IsMax x
I : Ideal R
hI : x.asIdeal < I
e : ¬I = ⊤
m : Ideal R
hm : m.IsMaximal
hm' : I ≤ m
⊢ False

Tactic:
exact hx.not_lt (show x < ⟨m, hm.isPrime⟩ from hI.trans_le hm')

Premises used: LT.lt.trans_le, IsMax.not_lt
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
m : Ideal R
inst_1 : m.IsMaximal
h :
  ∀ (I : PrimeSpectrum R),
    Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑m : Set R)) I ↔
      Membership.mem (γ := Set (PrimeSpectrum R)) {{ asIdeal := m, isPrime := ⋯ : PrimeSpectrum R }} I
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑m : Set R)) {{ asIdeal := m, isPrime := ⋯ : PrimeSpectrum R }}

Tactic:
ext I
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
m : Ideal R
inst_1 : m.IsMaximal
I : PrimeSpectrum R
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑m : Set R)) I ↔
    Membership.mem (γ := Set (PrimeSpectrum R)) {{ asIdeal := m, isPrime := ⋯ : PrimeSpectrum R }} I

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
m : Ideal R
inst_1 : m.IsMaximal
I : PrimeSpectrum R
h :
  ∀ (h : Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑m : Set R)) I),
    Membership.mem (γ := Set (PrimeSpectrum R)) {{ asIdeal := m, isPrime := ⋯ : PrimeSpectrum R }} I
h₁ :
  ∀ (h : Membership.mem (γ := Set (PrimeSpectrum R)) {{ asIdeal := m, isPrime := ⋯ : PrimeSpectrum R }} I),
    Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑m : Set R)) I
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑m : Set R)) I ↔
    Membership.mem (γ := Set (PrimeSpectrum R)) {{ asIdeal := m, isPrime := ⋯ : PrimeSpectrum R }} I

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
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
⊢ m ≤ I.asIdeal

Tactic:
simp only [mem_zeroLocus, SetLike.coe_subset_coe] at h

Premises used: PrimeSpectrum.mem_zeroLocus, SetLike.coe_subset_coe
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
m : Ideal R
inst_1 : m.IsMaximal
I : PrimeSpectrum R
h : m ≤ I.asIdeal
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) {{ asIdeal := m, isPrime := ⋯ : PrimeSpectrum R }} I

Tactic:
simpa using PrimeSpectrum.ext_iff.mpr (Ideal.IsMaximal.eq_of_le ‹_› I.2.ne_top h).symm

Premises used: Iff.mpr, PrimeSpectrum.ext_iff
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
m : Ideal R
inst_1 : m.IsMaximal
I : PrimeSpectrum R
h : Membership.mem (γ := Set (PrimeSpectrum R)) {{ asIdeal := m, isPrime := ⋯ : PrimeSpectrum R }} I
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑m : Set R)) I

Tactic:
simp [Set.mem_singleton_iff.mp h]

Premises used: Set.mem_singleton_iff, Iff.mp
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
x : PrimeSpectrum R
simp : (∀ ⦃b : PrimeSpectrum R⦄, b ≤ x → x ≤ b) ↔ ∀ ⦃y : Ideal R⦄, y.IsPrime → y ≤ x.asIdeal → x.asIdeal ≤ y
⊢ IsMin x ↔ Minimal (fun (q : Ideal R) ↦ q.IsPrime ∧ ⊥ ≤ q) x.asIdeal

Tactic:
simp only [IsMin, Minimal, x.2, bot_le, and_self, and_true, true_and]

Premises used: and_true, PrimeSpectrum.isPrime, and_self, Minimal, bot_le, IsMin, true_and
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
x : PrimeSpectrum R
⊢ (∀ ⦃b : PrimeSpectrum R⦄, b ≤ x → x ≤ b) ↔ ∀ ⦃y : Ideal R⦄, y.IsPrime → y ≤ x.asIdeal → x.asIdeal ≤ y

Tactic:
⟨fun H y hy e ↦ @H ⟨y, hy⟩ e, fun H y e ↦ H y.2 e⟩

Premises used: PrimeSpectrum.isPrime, Iff.intro
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
x : PrimeSpectrum R
⊢ (∀ ⦃b : PrimeSpectrum R⦄, b ≤ x → x ≤ b) ↔ ∀ ⦃y : Ideal R⦄, y.IsPrime → y ≤ x.asIdeal → x.asIdeal ≤ y

Tactic:
exact ⟨fun H y hy e ↦ @H ⟨y, hy⟩ e, fun H y e ↦ H y.2 e⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
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
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
⊢ ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ M

Tactic:
change Ideal R at M

Premises used: Ideal
-- 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
pos : ∀ (h_prM : M.IsPrime), ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ M
neg : ∀ (h_prM : ¬M.IsPrime), ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ M
⊢ ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ M

Tactic:
by_cases h_prM : M.IsPrime

Premises used: Ideal.IsPrime
-- 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
h : Multiset.prod (Multiset.map asIdeal {{ asIdeal := M, isPrime := h_prM : PrimeSpectrum R }}) ≤ M
⊢ ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ M

Tactic:
use {⟨M, h_prM⟩}
-- 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
h : Multiset.prod {{ asIdeal := M, isPrime := h_prM : PrimeSpectrum R }.asIdeal} ≤ M
h₁ h₂ : { asIdeal := M, isPrime := h_prM : PrimeSpectrum R }.asIdeal ≤ { asIdeal := M, isPrime := h_prM }.asIdeal
⊢ Multiset.prod (Multiset.map asIdeal {{ asIdeal := M, isPrime := h_prM : PrimeSpectrum R }}) ≤ M

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

Premises used: Multiset.map_singleton, Multiset.prod_singleton
-- 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
pos : ∀ (htop : M = ⊤), ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ M
neg : ∀ (htop : ¬M = ⊤), ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ M
⊢ ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ M

Tactic:
by_cases htop : M = ⊤
-- 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 = ⊤
pos : ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ ⊤
⊢ ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ M

Tactic:
rw [htop]
-- 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 = ⊤
⊢ ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ ⊤

Tactic:
⟨0, le_top⟩

Premises used: le_top, Exists.intro, OfNat.ofNat
-- 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 = ⊤
⊢ ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ ⊤

Tactic:
exact ⟨0, le_top⟩
-- 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 = ⊤
z : R
hz : z ∉ M
⊢ M < M + R ∙ 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:
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
refine : ∀ (m_eq : M = M + R ∙ z), z ∈ M
⊢ M < M + R ∙ 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:
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
rw : z ∈ M + R ∙ z
⊢ z ∈ M

Tactic:
rw [m_eq]
-- 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 = ⊤
z : R
hz : z ∉ M
m_eq : M = M + R ∙ z
⊢ z ∈ M + R ∙ z

Tactic:
Ideal.mem_sup_right (mem_span_singleton_self z)

Premises used: Set.Mem, Submodule.mem_span_singleton_self, Ideal.mem_sup_right
-- 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 = ⊤
z : R
hz : z ∉ M
m_eq : M = M + R ∙ z
⊢ z ∈ M + R ∙ z

Tactic:
exact Ideal.mem_sup_right (mem_span_singleton_self z)

Premises used: Submodule.mem_span_singleton_self, Ideal.mem_sup_right
-- 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 = ⊤
⊢ ∀ 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)
-- 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
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
⊢ ∃ (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

Premises used: Or.resolve_left, Ideal.not_isPrime_iff, Iff.mp
-- 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
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
⊢ ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ M

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

Premises used: HAdd.hAdd, Submodule.span, Singleton.singleton
-- 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
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
⊢ ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ M

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

Premises used: HAdd.hAdd, Submodule.span, Singleton.singleton
-- 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 : (Multiset.map asIdeal (Wx + Wy)).prod ≤ M
⊢ ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ M

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

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

Premises used: Multiset.prod_add, Multiset.map_add