awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
p : Ideal S
hp : p.IsPrime
hI : Ideal.IsPrime (α := R × S) (Ideal.prod ⊤ p)
⊢ ∃ (a : Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S)),
    primeSpectrumProdOfSum R S a = { asIdeal := Ideal.prod ⊤ p, isPrime := hI }

Tactic:
⟨Sum.inr ⟨p, hp⟩, rfl⟩

Premises used: PrimeSpectrum.mk, Sum.inr, Exists.intro, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
p : Ideal S
hp : p.IsPrime
hI : Ideal.IsPrime (α := R × S) (Ideal.prod ⊤ p)
⊢ ∃ (a : Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S)),
    primeSpectrumProdOfSum R S a = { asIdeal := Ideal.prod ⊤ p, isPrime := hI }

Tactic:
exact ⟨Sum.inr ⟨p, hp⟩, rfl⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
x : PrimeSpectrum R
mk :
  ∀ (asIdeal : Ideal R) (isPrime : asIdeal.IsPrime),
    Eq (α := Ideal (R × S))
      (PrimeSpectrum.asIdeal
        ((Equiv.symm (primeSpectrumProd R S) : (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
          (Sum.inl { asIdeal := asIdeal, isPrime := isPrime })))
      ({ asIdeal := asIdeal, isPrime := isPrime }.asIdeal.prod ⊤)
⊢ Eq (α := Ideal (R × S))
    (asIdeal
      ((Equiv.symm (primeSpectrumProd R S) : (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
        (Sum.inl x)))
    (x.asIdeal.prod ⊤)

Tactic:
cases x
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
asIdeal : Ideal R
isPrime : asIdeal.IsPrime
⊢ Eq (α := Ideal (R × S))
    (PrimeSpectrum.asIdeal
      ((Equiv.symm (primeSpectrumProd R S) : (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
        (Sum.inl { asIdeal := asIdeal, isPrime := isPrime })))
    ({ asIdeal := asIdeal, isPrime := isPrime }.asIdeal.prod ⊤)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
x : PrimeSpectrum S
mk :
  ∀ (asIdeal : Ideal S) (isPrime : asIdeal.IsPrime),
    Eq (α := Ideal (R × S))
      (PrimeSpectrum.asIdeal
        ((Equiv.symm (primeSpectrumProd R S) : (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
          (Sum.inr { asIdeal := asIdeal, isPrime := isPrime })))
      (Ideal.prod ⊤ { asIdeal := asIdeal, isPrime := isPrime }.asIdeal)
⊢ Eq (α := Ideal (R × S))
    (asIdeal
      ((Equiv.symm (primeSpectrumProd R S) : (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
        (Sum.inr x)))
    (Ideal.prod ⊤ x.asIdeal)

Tactic:
cases x
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
asIdeal : Ideal S
isPrime : asIdeal.IsPrime
⊢ Eq (α := Ideal (R × S))
    (PrimeSpectrum.asIdeal
      ((Equiv.symm (primeSpectrumProd R S) : (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
        (Sum.inr { asIdeal := asIdeal, isPrime := isPrime })))
    (Ideal.prod ⊤ { asIdeal := asIdeal, isPrime := isPrime }.asIdeal)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
x : PrimeSpectrum R
s : Set R
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus s) x ↔ s ⊆ (↑x.asIdeal : Set R)

Tactic:
Iff.rfl

Premises used: PrimeSpectrum.zeroLocus, Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
s : Set R
h :
  ∀ (x : PrimeSpectrum R),
    Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑(Ideal.span s) : Set R)) x ↔
      Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus s) x
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑(Ideal.span s) : Set R)) (zeroLocus s)

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

Tactic:
(Submodule.gi R R).gc s x.asIdeal

Premises used: Submodule.gi, PrimeSpectrum.zeroLocus, Set.Mem, setOf, Set.Subset, PrimeSpectrum.asIdeal, GaloisInsertion.gc
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
s : Set R
x : PrimeSpectrum R
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑(Ideal.span s) : Set R)) x ↔
    Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus s) x

Tactic:
exact (Submodule.gi R R).gc s x.asIdeal

Premises used: Submodule.gi, PrimeSpectrum.asIdeal, GaloisInsertion.gc
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
t : Set (PrimeSpectrum R)
h : ∀ (f : R), f ∈ (↑(vanishingIdeal t) : Set R) ↔ Membership.mem (γ := Set R) {f : R | ∀ x ∈ t, f ∈ x.asIdeal} f
⊢ (↑(vanishingIdeal t) : Set R) = {f : R | ∀ x ∈ t, f ∈ x.asIdeal}

Tactic:
ext f
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
t : Set (PrimeSpectrum R)
f : R
h :
  (∀ (i : PrimeSpectrum R), Membership.mem (γ := Submodule R R) (⨅ (_ : i ∈ t), i.asIdeal) f) ↔
    Membership.mem (γ := Set R) {f : R | ∀ x ∈ t, f ∈ x.asIdeal} f
⊢ f ∈ (↑(vanishingIdeal t) : Set R) ↔ Membership.mem (γ := Set R) {f : R | ∀ x ∈ t, f ∈ x.asIdeal} f

Tactic:
rw [vanishingIdeal, SetLike.mem_coe, Submodule.mem_iInf]

Premises used: Submodule.mem_iInf, PrimeSpectrum.vanishingIdeal, SetLike.mem_coe
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
t : Set (PrimeSpectrum R)
f : R
h : ∀ (a : PrimeSpectrum R), Membership.mem (γ := Submodule R R) (⨅ (_ : a ∈ t), a.asIdeal) f ↔ a ∈ t → f ∈ a.asIdeal
⊢ (∀ (i : PrimeSpectrum R), Membership.mem (γ := Submodule R R) (⨅ (_ : i ∈ t), i.asIdeal) f) ↔
    Membership.mem (γ := Set R) {f : R | ∀ x ∈ t, f ∈ x.asIdeal} f

Tactic:
apply forall_congr'

Premises used: forall_congr'
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
t : Set (PrimeSpectrum R)
f : R
x : PrimeSpectrum R
h h₁ : (∀ (i : x ∈ t), f ∈ x.asIdeal) ↔ x ∈ t → f ∈ x.asIdeal
⊢ Membership.mem (γ := Submodule R R) (⨅ (_ : x ∈ t), x.asIdeal) f ↔ x ∈ t → f ∈ x.asIdeal

Tactic:
rw [Submodule.mem_iInf]

Premises used: Submodule.mem_iInf
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
t : Set (PrimeSpectrum R)
f : R
rw : f ∈ (↑(vanishingIdeal t) : Set R) ↔ ∀ x ∈ t, f ∈ x.asIdeal
rw₁ : Membership.mem (γ := Set R) {f : R | ∀ x ∈ t, f ∈ x.asIdeal} f ↔ ∀ x ∈ t, f ∈ x.asIdeal
rw₂ rw₃ : (∀ x ∈ t, f ∈ x.asIdeal) ↔ ∀ x ∈ t, f ∈ x.asIdeal
⊢ f ∈ vanishingIdeal t ↔ ∀ x ∈ t, f ∈ x.asIdeal

Tactic:
rw [← SetLike.mem_coe, coe_vanishingIdeal, Set.mem_setOf_eq]

Premises used: Set.mem_setOf_eq, SetLike.mem_coe, PrimeSpectrum.coe_vanishingIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
x : PrimeSpectrum R
⊢ vanishingIdeal {x} = x.asIdeal

Tactic:
simp [vanishingIdeal]

Premises used: PrimeSpectrum.vanishingIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
t : Set (PrimeSpectrum R)
I : Ideal R
⊢ t ⊆ zeroLocus (↑I : Set R) ↔ I ≤ vanishingIdeal t

Tactic:
⟨fun h _ k => (mem_vanishingIdeal _ _).mpr fun _ j => (mem_zeroLocus _ _).mpr (h j) k, fun h =>
    fun x j => (mem_zeroLocus _ _).mpr (le_trans h fun _ h => ((mem_vanishingIdeal _ _).mp h) x j)⟩

Premises used: Iff.mpr, PrimeSpectrum.mem_zeroLocus, SetLike.coe, Iff.intro, Iff.mp, PrimeSpectrum.mem_vanishingIdeal, le_trans
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
⊢ GaloisConnection (fun (I : Ideal R) ↦ zeroLocus (↑I : Set R)) fun (t : (Set (PrimeSpectrum R))ᵒᵈ) ↦ vanishingIdeal t

Tactic:
fun I t => subset_zeroLocus_iff_le_vanishingIdeal t I

Premises used: Set.Mem, PrimeSpectrum.subset_zeroLocus_iff_le_vanishingIdeal, GaloisConnection
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
⊢ GaloisConnection (β := Ideal R) Ideal.span SetLike.coe

Tactic:
have ideal_gc : GaloisConnection Ideal.span _ := (Submodule.gi R R).gc
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
ideal_gc : GaloisConnection (β := Ideal R) Ideal.span SetLike.coe
⊢ GaloisConnection (fun (s : Set R) ↦ zeroLocus s) fun (t : (Set (PrimeSpectrum R))ᵒᵈ) ↦ (↑(vanishingIdeal t) : Set R)

Tactic:
simpa [zeroLocus_span, Function.comp_def] using ideal_gc.compose (gc R)

Premises used: PrimeSpectrum.gc, PrimeSpectrum.zeroLocus_span, Function.comp_def, GaloisConnection.compose
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
t : Set (PrimeSpectrum R)
s : Set R
⊢ t ⊆ zeroLocus s ↔ s ⊆ (↑(vanishingIdeal t) : Set R)

Tactic:
(gc_set R) s t

Premises used: PrimeSpectrum.gc_set
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
s : Set R
⊢ s ⊆ (↑(vanishingIdeal (zeroLocus s)) : Set R)

Tactic:
(gc_set R).le_u_l s

Premises used: GaloisConnection.le_u_l, PrimeSpectrum.gc_set
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
⊢ I ≤ vanishingIdeal (zeroLocus (↑I : Set R))

Tactic:
(gc R).le_u_l I

Premises used: PrimeSpectrum.gc, GaloisConnection.le_u_l
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
f : R
rw :
  (∀ (x : PrimeSpectrum R), Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) x → f ∈ x.asIdeal) ↔
    ∀ (p : Submodule R R), Membership.mem (γ := Set (Submodule R R)) {J : Ideal R | I ≤ J ∧ J.IsPrime} p → f ∈ p
⊢ Membership.mem (γ := Ideal R) (vanishingIdeal (zeroLocus (↑I : Set R))) f ↔ f ∈ I.radical

Tactic:
rw [mem_vanishingIdeal, Ideal.radical_eq_sInf, Submodule.mem_sInf]

Premises used: Ideal.radical_eq_sInf, Submodule.mem_sInf, PrimeSpectrum.mem_vanishingIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
f : R
⊢ (∀ (x : PrimeSpectrum R), Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) x → f ∈ x.asIdeal) ↔
    ∀ (p : Submodule R R), Membership.mem (γ := Set (Submodule R R)) {J : Ideal R | I ≤ J ∧ J.IsPrime} p → f ∈ p

Tactic:
⟨fun h x hx => h ⟨x, hx.2⟩ hx.1, fun h x hx => h x.1 ⟨hx, x.2⟩⟩

Premises used: PrimeSpectrum.mk, PrimeSpectrum.isPrime, And.right, And.left, And.intro, Iff.intro, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
f : R
⊢ (∀ (x : PrimeSpectrum R), Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) x → f ∈ x.asIdeal) ↔
    ∀ (p : Submodule R R), Membership.mem (γ := Set (Submodule R R)) {J : Ideal R | I ≤ J ∧ J.IsPrime} p → f ∈ p

Tactic:
exact ⟨fun h x hx => h ⟨x, hx.2⟩ hx.1, fun h x hx => h x.1 ⟨hx, x.2⟩⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
⊢ Eq (α := Ideal R) (nilradical R) (iInf asIdeal)

Tactic:
apply range_asIdeal R ▸ nilradical_eq_sInf R
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
rw :
  Eq (α := Ideal R) (⨅ (x : PrimeSpectrum R), ⨅ (_ : Membership.mem (γ := Set (PrimeSpectrum R)) Set.univ x), x.asIdeal)
    (nilradical R)
rw₁ : Eq (α := Ideal R) (⨅ (x : PrimeSpectrum R), x.asIdeal) (nilradical R)
rw₂ rw₃ : Eq.{u + 1} (α := Ideal R) (⨅ (x : PrimeSpectrum R), x.asIdeal) (iInf asIdeal)
⊢ Eq (α := Ideal R) (vanishingIdeal Set.univ) (nilradical R)

Tactic:
rw [vanishingIdeal, iInf_univ, nilradical_eq_iInf]

Premises used: PrimeSpectrum.vanishingIdeal, PrimeSpectrum.nilradical_eq_iInf, iInf_univ
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I.radical : Set R)) (zeroLocus (↑I : Set R))

Tactic:
vanishingIdeal_zeroLocus_eq_radical I ▸ (gc R).l_u_l_eq_l I

Premises used: PrimeSpectrum.gc, PrimeSpectrum.vanishingIdeal_zeroLocus_eq_radical, GaloisConnection.l_u_l_eq_l, Eq.rec
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
t : Set (PrimeSpectrum R)
⊢ t ⊆ zeroLocus (↑(vanishingIdeal t) : Set R)

Tactic:
(gc R).l_u_le t

Premises used: PrimeSpectrum.gc, GaloisConnection.l_u_le
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
s t : Set R
h : s ⊆ t
⊢ Subset (α := Set (PrimeSpectrum R)) (zeroLocus t) (zeroLocus s)

Tactic:
(gc_set R).monotone_l h

Premises used: PrimeSpectrum.gc_set, GaloisConnection.monotone_l
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
s t : Ideal R
h : s ≤ t
⊢ Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑t : Set R)) (zeroLocus (↑s : Set R))

Tactic:
(gc R).monotone_l h

Premises used: PrimeSpectrum.gc, GaloisConnection.monotone_l
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
s t : Set (PrimeSpectrum R)
h : s ⊆ t
⊢ vanishingIdeal t ≤ vanishingIdeal s

Tactic:
(gc R).monotone_u h

Premises used: GaloisConnection.monotone_u, PrimeSpectrum.gc
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
rw : J ≤ vanishingIdeal (zeroLocus (↑I : Set R)) ↔ J ≤ I.radical
rw₁ rw₂ : J ≤ I.radical ↔ J ≤ I.radical
⊢ Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) (zeroLocus (↑J : Set R)) ↔ J ≤ I.radical

Tactic:
rw [subset_zeroLocus_iff_le_vanishingIdeal, vanishingIdeal_zeroLocus_eq_radical]

Premises used: PrimeSpectrum.vanishingIdeal_zeroLocus_eq_radical, PrimeSpectrum.subset_zeroLocus_iff_le_vanishingIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
f g : R
rw :
  Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑(Ideal.span {f}) : Set R)) (zeroLocus {g}) ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {f})) g
rw₁ :
  Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑(Ideal.span {f}) : Set R)) (zeroLocus (↑(Ideal.span {g}) : Set R)) ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {f})) g
rw₂ :
  LE.le (α := Ideal R) (Ideal.span {g}) (Ideal.radical (Ideal.span {f})) ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {f})) g
rw₃ :
  {g} ⊆ (↑(Ideal.radical (Ideal.span {f})) : Set R) ↔ Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {f})) g
rw₄ : g ∈ (↑(Ideal.radical (Ideal.span {f})) : Set R) ↔ Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {f})) g
rw₅ rw₆ :
  Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {f})) g ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {f})) g
⊢ Subset (α := Set (PrimeSpectrum R)) (zeroLocus {f}) (zeroLocus {g}) ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {f})) g

Tactic:
rw [← zeroLocus_span {f}, ← zeroLocus_span {g}, zeroLocus_subset_zeroLocus_iff, Ideal.span_le,
    Set.singleton_subset_iff, SetLike.mem_coe]

Premises used: Ideal.span_le, Set.singleton_subset_iff, PrimeSpectrum.zeroLocus_subset_zeroLocus_iff, PrimeSpectrum.zeroLocus_span, SetLike.mem_coe, Singleton.singleton
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑⊥ : Set R)) Set.univ

Tactic:
(gc R).l_bot

Premises used: PrimeSpectrum.gc, GaloisConnection.l_bot, OrderDual
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
rw : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑(Ideal.radical 0) : Set R)) Set.univ
rw₁ : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑0 : Set R)) Set.univ
rw₂ : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑⊥ : Set R)) Set.univ
rw₃ rw₄ : Eq.{u + 1} (α := Set (PrimeSpectrum R)) Set.univ Set.univ
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑(nilradical R) : Set R)) Set.univ

Tactic:
rw [nilradical, zeroLocus_radical, Ideal.zero_eq_bot, zeroLocus_bot]

Premises used: PrimeSpectrum.zeroLocus_radical, Ideal.zero_eq_bot, PrimeSpectrum.zeroLocus_bot, nilradical
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus {0}) Set.univ

Tactic:
zeroLocus_bot

Premises used: setOf, PrimeSpectrum.zeroLocus_bot, Set.singleton
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
⊢ Eq.{u + 1} (α := Set (PrimeSpectrum R)) (zeroLocus ∅) Set.univ

Tactic:
(gc_set R).l_bot

Premises used: PrimeSpectrum.gc_set, GaloisConnection.l_bot, OrderDual
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
⊢ Eq.{u + 1} (α := Ideal R) (vanishingIdeal ∅) ⊤

Tactic:
simpa using (gc R).u_top

Premises used: PrimeSpectrum.gc, GaloisConnection.u_top
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
s : Set R
h : 1 ∈ s
rw : ∀ (x : PrimeSpectrum R), x ∉ zeroLocus s
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus s) ∅

Tactic:
rw [Set.eq_empty_iff_forall_notMem]

Premises used: Set.eq_empty_iff_forall_notMem
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus s) x
⊢ s ⊆ (↑x.asIdeal : Set R)

Tactic:
rw [mem_zeroLocus] at hx

Premises used: PrimeSpectrum.mem_zeroLocus
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : s ⊆ (↑x.asIdeal : Set R)
⊢ x.asIdeal.IsPrime

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : s ⊆ (↑x.asIdeal : Set R)
⊢ x.asIdeal.IsPrime

Tactic:
have x_prime : x.asIdeal.IsPrime := by infer_instance
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : s ⊆ (↑x.asIdeal : Set R)
x_prime : x.asIdeal.IsPrime
rw : 1 ∈ x.asIdeal
⊢ x.asIdeal = ⊤

Tactic:
rw [Ideal.eq_top_iff_one]

Premises used: Ideal.eq_top_iff_one
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : s ⊆ (↑x.asIdeal : Set R)
x_prime : x.asIdeal.IsPrime
⊢ 1 ∈ x.asIdeal

Tactic:
hx h
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : s ⊆ (↑x.asIdeal : Set R)
x_prime : x.asIdeal.IsPrime
⊢ 1 ∈ x.asIdeal

Tactic:
exact hx h
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : s ⊆ (↑x.asIdeal : Set R)
x_prime : x.asIdeal.IsPrime
⊢ x.asIdeal = ⊤

Tactic:
have eq_top : x.asIdeal = ⊤ := by
    rw [Ideal.eq_top_iff_one]
    exact hx h
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : s ⊆ (↑x.asIdeal : Set R)
x_prime : x.asIdeal.IsPrime
eq_top : x.asIdeal = ⊤
⊢ False

Tactic:
apply x_prime.ne_top eq_top

Premises used: Ideal.IsPrime.ne_top
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus {1}) ∅

Tactic:
zeroLocus_empty_of_one_mem (Set.mem_singleton (1 : R))

Premises used: Set.mem_singleton, PrimeSpectrum.zeroLocus_empty_of_one_mem, OfNat.ofNat
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
mp : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) ∅ → I = ⊤
mpr : I = ⊤ → Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) ∅
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) ∅ ↔ I = ⊤

Tactic:
constructor
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
mp : I ≠ ⊤ → Set.Nonempty (α := PrimeSpectrum R) (zeroLocus (↑I : Set R))
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) ∅ → I = ⊤

Tactic:
contrapose!
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
h : I ≠ ⊤
mp : ∀ (M : Ideal R) (hM : M.IsMaximal) (hIM : I ≤ M), Set.Nonempty (α := PrimeSpectrum R) (zeroLocus (↑I : Set R))
⊢ Set.Nonempty (α := PrimeSpectrum R) (zeroLocus (↑I : Set R))

Tactic:
rcases Ideal.exists_le_maximal I h with ⟨M, hM, hIM⟩

Premises used: Ideal.exists_le_maximal
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
h : I ≠ ⊤
M : Ideal R
hM : M.IsMaximal
hIM : I ≤ M
⊢ Set.Nonempty (α := PrimeSpectrum R) (zeroLocus (↑I : Set R))

Tactic:
⟨⟨M, hM.isPrime⟩, hIM⟩

Premises used: PrimeSpectrum.mk, Ideal.IsMaximal.isPrime, Set.Nonempty, Exists.intro
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
h : I ≠ ⊤
M : Ideal R
hM : M.IsMaximal
hIM : I ≤ M
⊢ Set.Nonempty (α := PrimeSpectrum R) (zeroLocus (↑I : Set R))

Tactic:
exact ⟨⟨M, hM.isPrime⟩, hIM⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
mpr : 1 ∈ (↑⊤ : Set R)
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑⊤ : Set R)) ∅

Tactic:
apply zeroLocus_empty_of_one_mem

Premises used: PrimeSpectrum.zeroLocus_empty_of_one_mem
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
⊢ 1 ∈ (↑⊤ : Set R)

Tactic:
trivial
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
⊢ Eq.{u + 1} (α := Set (PrimeSpectrum R)) (zeroLocus Set.univ) ∅

Tactic:
zeroLocus_empty_of_one_mem (Set.mem_univ 1)

Premises used: Set.mem_univ, PrimeSpectrum.zeroLocus_empty_of_one_mem, OfNat.ofNat
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
rw : ⊤ ≤ vanishingIdeal s ↔ s = ∅
rw₁ : s ⊆ zeroLocus (↑⊤ : Set R) ↔ s = ∅
rw₂ : s ⊆ zeroLocus Set.univ ↔ s = ∅
rw₃ : s ⊆ ∅ ↔ s = ∅
rw₄ rw₅ : s = ∅ ↔ s = ∅
⊢ vanishingIdeal s = ⊤ ↔ s = ∅

Tactic:
rw [← top_le_iff, ← subset_zeroLocus_iff_le_vanishingIdeal, Submodule.top_coe, zeroLocus_univ,
    Set.subset_empty_iff]

Premises used: PrimeSpectrum.subset_zeroLocus_iff_le_vanishingIdeal, PrimeSpectrum.zeroLocus_univ, top_le_iff, Set.subset_empty_iff, Submodule.top_coe
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
s : Set R
rw : Subset (α := Set (PrimeSpectrum R)) Set.univ (zeroLocus s) ↔ s ⊆ (↑(nilradical R) : Set R)
rw₁ : s ⊆ (↑(vanishingIdeal Set.univ) : Set R) ↔ s ⊆ (↑(nilradical R) : Set R)
rw₂ rw₃ : s ⊆ (↑(nilradical R) : Set R) ↔ s ⊆ (↑(nilradical R) : Set R)
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus s) Set.univ ↔ s ⊆ (↑(nilradical R) : Set R)

Tactic:
rw [← Set.univ_subset_iff, subset_zeroLocus_iff_subset_vanishingIdeal, vanishingIdeal_univ]

Premises used: Set.univ_subset_iff, PrimeSpectrum.vanishingIdeal_univ, PrimeSpectrum.subset_zeroLocus_iff_subset_vanishingIdeal
-- 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:
(gc R).l_sup

Premises used: PrimeSpectrum.gc, OrderDual, GaloisConnection.l_sup
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
s s' : Set R
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus (s ∪ s')) (zeroLocus s ∩ zeroLocus s')

Tactic:
(gc_set R).l_sup

Premises used: PrimeSpectrum.gc_set, OrderDual, GaloisConnection.l_sup
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
t t' : Set (PrimeSpectrum R)
⊢ vanishingIdeal (t ∪ t') = vanishingIdeal t ⊓ vanishingIdeal t'

Tactic:
(gc R).u_inf

Premises used: PrimeSpectrum.gc, GaloisConnection.u_inf
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
ι : Sort u_1
I : ι → Ideal R
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑(⨆ (i : ι), I i) : Set R)) (⋂ (i : ι), zeroLocus (↑(I i) : Set R))

Tactic:
(gc R).l_iSup

Premises used: iInf, PrimeSpectrum.gc, Set.Mem, Set.iInter, setOf, GaloisConnection.l_iSup, OrderDual