awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
x : PrimeSpectrum R
simp_rw : (∀ (a : PrimeSpectrum R) (a_1 : x ≤ a), a = x) ↔ IsMax x
⊢ StableUnderSpecialization (X := PrimeSpectrum R) {x} ↔ x.asIdeal.IsMaximal

Tactic:
simp_rw [← isMax_iff, StableUnderSpecialization, ← le_iff_specializes, Set.mem_singleton_iff,
    @forall_comm _ (_ = _), forall_eq]

Premises used: StableUnderSpecialization, PrimeSpectrum.isMax_iff, forall_eq, forall_comm, Set.mem_singleton_iff, PrimeSpectrum.le_iff_specializes
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
x : PrimeSpectrum R
⊢ (∀ (a : PrimeSpectrum R) (a_1 : x ≤ a), a = x) ↔ IsMax x

Tactic:
⟨fun H a h ↦ (H a h).le, fun H a h ↦ le_antisymm (H h) h⟩

Premises used: Eq.le, le_antisymm, Iff.intro
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
x : PrimeSpectrum R
⊢ (∀ (a : PrimeSpectrum R) (a_1 : x ≤ a), a = x) ↔ IsMax x

Tactic:
exact ⟨fun H a h ↦ (H a h).le, fun H a h ↦ le_antisymm (H h) h⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
x : PrimeSpectrum R
simp_rw : (∀ (a : PrimeSpectrum R) (a_1 : a ≤ x), a = x) ↔ IsMin x
⊢ StableUnderGeneralization (X := PrimeSpectrum R) {x} ↔ Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) x.asIdeal

Tactic:
simp_rw [← isMin_iff, StableUnderGeneralization, ← le_iff_specializes, Set.mem_singleton_iff,
    @forall_comm _ (_ = _), forall_eq]

Premises used: PrimeSpectrum.isMin_iff, forall_eq, forall_comm, Set.mem_singleton_iff, PrimeSpectrum.le_iff_specializes, StableUnderGeneralization
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
x : PrimeSpectrum R
⊢ (∀ (a : PrimeSpectrum R) (a_1 : a ≤ x), a = x) ↔ IsMin x

Tactic:
⟨fun H a h ↦ (H a h).ge, fun H a h ↦ le_antisymm h (H h)⟩

Premises used: Eq.ge, le_antisymm, Iff.intro
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
x : PrimeSpectrum R
⊢ (∀ (a : PrimeSpectrum R) (a_1 : a ≤ x), a = x) ↔ IsMin x

Tactic:
exact ⟨fun H a h ↦ (H a h).ge, fun H a h ↦ le_antisymm h (H h)⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
rw :
  (∃ (s_1 : Set R), s_1.Finite ∧ s = ⋃ i ∈ s_1, (↑(basicOpen i) : Set (PrimeSpectrum R))) ↔
    ∃ (t : Finset R), (zeroLocus (↑t : Set R))ᶜ = s
⊢ IsCompact s ∧ IsOpen s ↔ ∃ (t : Finset R), (zeroLocus (↑t : Set R))ᶜ = s

Tactic:
rw [isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis _
    isTopologicalBasis_basic_opens isCompact_basicOpen]

Premises used: PrimeSpectrum.isTopologicalBasis_basic_opens, isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis, PrimeSpectrum.isCompact_basicOpen
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
simp : (∃ (s_1 : Set R), s_1.Finite ∧ s = (zeroLocus s_1)ᶜ) ↔ ∃ (t : Finset R), (zeroLocus (↑t : Set R))ᶜ = s
⊢ (∃ (s_1 : Set R), s_1.Finite ∧ s = ⋃ i ∈ s_1, (↑(basicOpen i) : Set (PrimeSpectrum R))) ↔
    ∃ (t : Finset R), (zeroLocus (↑t : Set R))ᶜ = s

Tactic:
simp only [basicOpen_eq_zeroLocus_compl, ← Set.compl_iInter₂, ← zeroLocus_iUnion₂,
    Set.biUnion_of_singleton]

Premises used: Set.compl_iInter₂, Set.biUnion_of_singleton, PrimeSpectrum.zeroLocus_iUnion₂, PrimeSpectrum.basicOpen_eq_zeroLocus_compl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s_1 : Set (PrimeSpectrum R)
h : ∃ (s : Set R), s.Finite ∧ s_1 = (zeroLocus s)ᶜ
s : Set R
hs : s.Finite
e : s_1 = (zeroLocus s)ᶜ
⊢ (zeroLocus (↑(hs.toFinset (s := s)) : Set R))ᶜ = s_1

Tactic:
simpa using e.symm

Premises used: Eq.symm
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s_1 : Set (PrimeSpectrum R)
h : ∃ (t : Finset R), (zeroLocus (↑t : Set R))ᶜ = s_1
s : Finset R
e : (zeroLocus (↑s : Set R))ᶜ = s_1
⊢ s_1 = (zeroLocus (↑s : Set R))ᶜ

Tactic:
simpa using e.symm

Premises used: Eq.symm
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ (∃ (s_1 : Set R), s_1.Finite ∧ s = (zeroLocus s_1)ᶜ) ↔ ∃ (t : Finset R), (zeroLocus (↑t : Set R))ᶜ = s

Tactic:
exact ⟨fun ⟨s, hs, e⟩ ↦ ⟨hs.toFinset, by simpa using e.symm⟩,
    fun ⟨s, e⟩ ↦ ⟨s, s.finite_toSet, by simpa using e.symm⟩⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
rw : (∃ (t : Finset R), (zeroLocus (↑t : Set R))ᶜ = s) ↔ ∃ (I : Ideal R), I.FG ∧ (zeroLocus (↑I : Set R))ᶜ = s
⊢ IsCompact s ∧ IsOpen s ↔ ∃ (I : Ideal R), I.FG ∧ (zeroLocus (↑I : Set R))ᶜ = s

Tactic:
rw [isCompact_isOpen_iff]

Premises used: PrimeSpectrum.isCompact_isOpen_iff
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s_1 : Set (PrimeSpectrum R)
h : ∃ (t : Finset R), (zeroLocus (↑t : Set R))ᶜ = s_1
s : Finset R
e : (zeroLocus (↑s : Set R))ᶜ = s_1
⊢ (zeroLocus (↑(Ideal.span (↑s : Set R)) : Set R))ᶜ = s_1

Tactic:
simpa using e
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s_1 : Set (PrimeSpectrum R)
h : ∃ (I : Ideal R), I.FG ∧ (zeroLocus (↑I : Set R))ᶜ = s_1
I : Ideal R
s : Finset R
hs : Ideal.span (↑s : Set R) = I
e : (zeroLocus (↑I : Set R))ᶜ = s_1
⊢ (zeroLocus (↑s : Set R))ᶜ = s_1

Tactic:
simpa [hs.symm] using e

Premises used: Eq.symm
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ (∃ (t : Finset R), (zeroLocus (↑t : Set R))ᶜ = s) ↔ ∃ (I : Ideal R), I.FG ∧ (zeroLocus (↑I : Set R))ᶜ = s

Tactic:
exact ⟨fun ⟨s, e⟩ ↦ ⟨.span s, ⟨s, rfl⟩, by simpa using e⟩,
    fun ⟨I, ⟨s, hs⟩, e⟩ ↦ ⟨s, by simpa [hs.symm] using e⟩⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
e f : R
mul : e * f = 0
add : e + f = 1
h :
  ∀ (p : PrimeSpectrum R),
    p ∈ (↑(basicOpen e) : Set (PrimeSpectrum R)) ↔ Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus {f}) p
⊢ (↑(basicOpen e) : Set (PrimeSpectrum R)) = zeroLocus {f}

Tactic:
ext p
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
e f : R
mul : e * f = 0
add : e + f = 1
p : PrimeSpectrum R
this : e ∉ p.asIdeal ↔ f ∈ p.asIdeal
⊢ p ∈ (↑(basicOpen e) : Set (PrimeSpectrum R)) ↔ Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus {f}) p

Tactic:
simpa
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
e f : R
mul : e * f = 0
add : e + f = 1
p : PrimeSpectrum R
h : e ∉ p.asIdeal ↔ f ∈ p.asIdeal
⊢ p ∈ (↑(basicOpen e) : Set (PrimeSpectrum R)) ↔ Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus {f}) p

Tactic:
suffices e ∉ p.asIdeal ↔ f ∈ p.asIdeal by simpa
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
e f : R
mul : e * f = 0
add : e + f = 1
p : PrimeSpectrum R
⊢ e ∉ p.asIdeal ↔ f ∈ p.asIdeal

Tactic:
⟨(p.2.mem_or_mem_of_mul_eq_zero mul).resolve_left, fun h₁ h₂ ↦ p.2.1 ?_⟩

Premises used: PrimeSpectrum.isPrime, Or.resolve_left, Ideal.IsPrime.mem_or_mem_of_mul_eq_zero, Iff.intro, Ideal.IsPrime.ne_top'
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
e f : R
mul : e * f = 0
add : e + f = 1
p : PrimeSpectrum R
h : ∀ (h₁ : f ∈ p.asIdeal) (h₂ : e ∈ p.asIdeal), p.asIdeal = ⊤
⊢ e ∉ p.asIdeal ↔ f ∈ p.asIdeal

Tactic:
refine ⟨(p.2.mem_or_mem_of_mul_eq_zero mul).resolve_left, fun h₁ h₂ ↦ p.2.1 ?_⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
e f : R
mul : e * f = 0
add : e + f = 1
p : PrimeSpectrum R
h₁ : f ∈ p.asIdeal
h₂ : e ∈ p.asIdeal
h : e + f ∈ p.asIdeal
⊢ p.asIdeal = ⊤

Tactic:
rw [Ideal.eq_top_iff_one, ← add]

Premises used: Ideal.eq_top_iff_one
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
e f : R
mul : e * f = 0
add : e + f = 1
p : PrimeSpectrum R
h₁ : f ∈ p.asIdeal
h₂ : e ∈ p.asIdeal
⊢ e + f ∈ p.asIdeal

Tactic:
add_mem h₂ h₁

Premises used: AddMemClass.add_mem
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
e f : R
mul : e * f = 0
add : e + f = 1
p : PrimeSpectrum R
h₁ : f ∈ p.asIdeal
h₂ : e ∈ p.asIdeal
⊢ e + f ∈ p.asIdeal

Tactic:
exact add_mem h₂ h₁

Premises used: AddMemClass.add_mem
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
e f : R
mul : e * f = 0
add : e + f = 1
mul₁ : f * e = 0
add₁ : f + e = 1
⊢ zeroLocus {e} = (↑(basicOpen f) : Set (PrimeSpectrum R))

Tactic:
rw [basicOpen_eq_zeroLocus_of_mul_add f e]

Premises used: PrimeSpectrum.basicOpen_eq_zeroLocus_of_mul_add
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
e f : R
mul : e * f = 0
add : e + f = 1
⊢ f * e = 0

Tactic:
simp only [mul, add, mul_comm, add_comm]

Premises used: add_comm, mul_comm
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
e f : R
mul : e * f = 0
add : e + f = 1
⊢ f + e = 1

Tactic:
simp only [mul, add, mul_comm, add_comm]

Premises used: add_comm, mul_comm
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
e f : R
mul : e * f = 0
add : e + f = 1
⊢ IsClopen (↑(basicOpen e) : Set (PrimeSpectrum R))

Tactic:
⟨basicOpen_eq_zeroLocus_of_mul_add e f mul add ▸ isClosed_zeroLocus _, (basicOpen e).2⟩

Premises used: PrimeSpectrum.isClosed_zeroLocus, PrimeSpectrum.basicOpen_eq_zeroLocus_of_mul_add, PrimeSpectrum.basicOpen, Eq.rec, And.intro, TopologicalSpace.Opens.is_open', IsClopen, Eq.symm
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
x : R
hx : Membership.mem (γ := Set R) {e : R | IsIdempotentElem e} x
y : R
hy : Membership.mem (γ := Set R) {e : R | IsIdempotentElem e} y
eq : Eq (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen x) (basicOpen y)
by_contra! : ∀ (ne : x ≠ y), False
⊢ x = y

Tactic:
by_contra! ne
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
x : R
hx : Membership.mem (γ := Set R) {e : R | IsIdempotentElem e} x
y : R
hy : Membership.mem (γ := Set R) {e : R | IsIdempotentElem e} y
eq : Eq (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen x) (basicOpen y)
ne : x ≠ y
inr :
  ∀
    (this :
      ∀ (x : R) (hx : Membership.mem (γ := Set R) {e : R | IsIdempotentElem e} x) (y : R)
        (hy : Membership.mem (γ := Set R) {e : R | IsIdempotentElem e} y)
        (eq : Eq (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen x) (basicOpen y)) (ne : x ≠ y)
        (ne' : x * y ≠ x), False)
    (ne' : ¬x * y ≠ x), False
wlog :
  ∀ (x : R) (hx : Membership.mem (γ := Set R) {e : R | IsIdempotentElem e} x) (y : R)
    (hy : Membership.mem (γ := Set R) {e : R | IsIdempotentElem e} y)
    (eq : Eq (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen x) (basicOpen y)) (ne : x ≠ y)
    (ne' : x * y ≠ x), False
⊢ False

Tactic:
wlog ne' : x * y ≠ x generalizing x y
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
x : R
hx : Membership.mem (γ := Set R) {e : R | IsIdempotentElem e} x
y : R
hy : Membership.mem (γ := Set R) {e : R | IsIdempotentElem e} y
eq : Eq (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen x) (basicOpen y)
ne : x ≠ y
this :
  ∀ (x : R) (hx : Membership.mem (γ := Set R) {e : R | IsIdempotentElem e} x) (y : R)
    (hy : Membership.mem (γ := Set R) {e : R | IsIdempotentElem e} y)
    (eq : Eq (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen x) (basicOpen y)) (ne : x ≠ y)
    (ne' : x * y ≠ x), False
ne' : ¬x * y ≠ x
inr : y * x ≠ y
⊢ False

Tactic:
apply this y hy x hx eq.symm ne.symm

Premises used: Ne.symm, Eq.symm
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
x : R
hx : Membership.mem (γ := Set R) {e : R | IsIdempotentElem e} x
y : R
hy : Membership.mem (γ := Set R) {e : R | IsIdempotentElem e} y
eq : Eq (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen x) (basicOpen y)
ne : x ≠ y
this :
  ∀ (x : R) (hx : Membership.mem (γ := Set R) {e : R | IsIdempotentElem e} x) (y : R)
    (hy : Membership.mem (γ := Set R) {e : R | IsIdempotentElem e} y)
    (eq : Eq (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen x) (basicOpen y)) (ne : x ≠ y)
    (ne' : x * y ≠ x), False
ne' : ¬x * y ≠ x
inr : x * y ≠ y
inr₁ inr₂ inr₃ inr₄ : x ≠ y
⊢ y * x ≠ y

Tactic:
rwa [mul_comm, of_not_not ne']

Premises used: mul_comm, of_not_not
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
x : R
hx : Membership.mem (γ := Set R) {e : R | IsIdempotentElem e} x
y : R
hy : Membership.mem (γ := Set R) {e : R | IsIdempotentElem e} y
eq : Eq (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen x) (basicOpen y)
ne : x ≠ y
ne' : x * y ≠ x
mem : Membership.mem (γ := Ideal R) (Ideal.span {y}) x
obtain :
  ∀ (r : R) (hx : Membership.mem (γ := Set R) {e : R | IsIdempotentElem e} (r * y))
    (eq : Eq (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen (r * y)) (basicOpen y)) (ne : r * y ≠ y)
    (ne' : r * y * y ≠ r * y) (mem : Membership.mem (γ := Ideal R) (Ideal.span {y}) (r * y)), r * y * y = r * y
⊢ x * y = x

Tactic:
obtain ⟨r, rfl⟩ := Ideal.mem_span_singleton'.mp mem

Premises used: Ideal.mem_span_singleton', Iff.mp, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
y : R
hy : Membership.mem (γ := Set R) {e : R | IsIdempotentElem e} y
r : R
hx : Membership.mem (γ := Set R) {e : R | IsIdempotentElem e} (r * y)
eq : Eq (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen (r * y)) (basicOpen y)
ne : r * y ≠ y
ne' : r * y * y ≠ r * y
mem : Membership.mem (γ := Ideal R) (Ideal.span {y}) (r * y)
rw : r * (y * y) = r * y
rw₁ rw₂ : r * y = r * y
⊢ r * y * y = r * y

Tactic:
rw [mul_assoc, hy]

Premises used: mul_assoc
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
x : R
hx : Membership.mem (γ := Set R) {e : R | IsIdempotentElem e} x
y : R
hy : Membership.mem (γ := Set R) {e : R | IsIdempotentElem e} y
eq : Eq (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen x) (basicOpen y)
ne : x ≠ y
ne' : x * y ≠ x
⊢ x ∉ Ideal.span {y}

Tactic:
have : x ∉ Ideal.span {y} := fun mem ↦ ne' <| by
    obtain ⟨r, rfl⟩ := Ideal.mem_span_singleton'.mp mem
    rw [mul_assoc, hy]
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
x : R
hx : Membership.mem (γ := Set R) {e : R | IsIdempotentElem e} x
y : R
hy : Membership.mem (γ := Set R) {e : R | IsIdempotentElem e} y
eq : Eq (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen x) (basicOpen y)
ne : x ≠ y
ne' : x * y ≠ x
this : x ∉ Ideal.span {y}
have : ∀ (p : Ideal R) (prime : p.IsPrime) (le : Ideal.span {y} ≤ p) (notMem : x ∉ p), False
⊢ False

Tactic:
have ⟨p, prime, le, notMem⟩ := Ideal.exists_le_prime_notMem_of_isIdempotentElem _ x hx this
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
x : R
hx : Membership.mem (γ := Set R) {e : R | IsIdempotentElem e} x
y : R
hy : Membership.mem (γ := Set R) {e : R | IsIdempotentElem e} y
eq : Eq (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen x) (basicOpen y)
ne : x ≠ y
ne' : x * y ≠ x
this : x ∉ Ideal.span {y}
p : Ideal R
prime : p.IsPrime
le : Ideal.span {y} ≤ p
notMem : x ∉ p
⊢ False

Tactic:
ne_of_mem_of_not_mem' (a := ⟨p, prime⟩) notMem
    (not_not.mpr <| p.span_singleton_le_iff_mem.mp le) eq

Premises used: ne_of_mem_of_not_mem'
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
x : R
hx : Membership.mem (γ := Set R) {e : R | IsIdempotentElem e} x
y : R
hy : Membership.mem (γ := Set R) {e : R | IsIdempotentElem e} y
eq : Eq (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen x) (basicOpen y)
ne : x ≠ y
ne' : x * y ≠ x
this : x ∉ Ideal.span {y}
p : Ideal R
prime : p.IsPrime
le : Ideal.span {y} ≤ p
notMem : x ∉ p
⊢ False

Tactic:
exact ne_of_mem_of_not_mem' (a := ⟨p, prime⟩) notMem
    (not_not.mpr <| p.span_singleton_le_iff_mem.mp le) eq

Premises used: ne_of_mem_of_not_mem'
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
inl :
  Subsingleton R →
    ∃ (e : R) (f : R),
      e * f = 0 ∧
        e + f = 1 ∧ s = (↑(basicOpen e) : Set (PrimeSpectrum R)) ∧ sᶜ = (↑(basicOpen f) : Set (PrimeSpectrum R))
inr :
  Nontrivial R →
    ∃ (e : R) (f : R),
      e * f = 0 ∧
        e + f = 1 ∧ s = (↑(basicOpen e) : Set (PrimeSpectrum R)) ∧ sᶜ = (↑(basicOpen f) : Set (PrimeSpectrum R))
⊢ ∃ (e : R) (f : R),
    e * f = 0 ∧ e + f = 1 ∧ s = (↑(basicOpen e) : Set (PrimeSpectrum R)) ∧ sᶜ = (↑(basicOpen f) : Set (PrimeSpectrum R))

Tactic:
cases subsingleton_or_nontrivial R

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h : Subsingleton R
⊢ ∃ (e : R) (f : R),
    e * f = 0 ∧ e + f = 1 ∧ s = (↑(basicOpen e) : Set (PrimeSpectrum R)) ∧ sᶜ = (↑(basicOpen f) : Set (PrimeSpectrum R))

Tactic:
⟨0, 0, ?_, ?_, ?_, ?_⟩

Premises used: And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h : Subsingleton R
inl : HMul.hMul (α := R) 0 0 = 0
inl₁ : HAdd.hAdd (α := R) 0 0 = 1
inl₂ : s = (↑(basicOpen 0) : Set (PrimeSpectrum R))
inl₃ : sᶜ = (↑(basicOpen 0) : Set (PrimeSpectrum R))
⊢ ∃ (e : R) (f : R),
    e * f = 0 ∧ e + f = 1 ∧ s = (↑(basicOpen e) : Set (PrimeSpectrum R)) ∧ sᶜ = (↑(basicOpen f) : Set (PrimeSpectrum R))

Tactic:
refine ⟨0, 0, ?_, ?_, ?_, ?_⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h : Subsingleton R
⊢ HMul.hMul (α := R) 0 0 = 0

Tactic:
apply Subsingleton.elim

Premises used: Subsingleton.elim
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h : Subsingleton R
⊢ HAdd.hAdd (α := R) 0 0 = 1

Tactic:
apply Subsingleton.elim

Premises used: Subsingleton.elim
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h : Subsingleton R
⊢ s = (↑(basicOpen 0) : Set (PrimeSpectrum R))

Tactic:
apply Subsingleton.elim

Premises used: Subsingleton.elim
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h : Subsingleton R
⊢ sᶜ = (↑(basicOpen 0) : Set (PrimeSpectrum R))

Tactic:
apply Subsingleton.elim

Premises used: Subsingleton.elim
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h : Nontrivial R
inr :
  ∀ (I : Ideal R) (hI : I.FG) (hI' : (zeroLocus (↑I : Set R))ᶜ = s),
    ∃ (e : R) (f : R),
      e * f = 0 ∧
        e + f = 1 ∧ s = (↑(basicOpen e) : Set (PrimeSpectrum R)) ∧ sᶜ = (↑(basicOpen f) : Set (PrimeSpectrum R))
⊢ ∃ (e : R) (f : R),
    e * f = 0 ∧ e + f = 1 ∧ s = (↑(basicOpen e) : Set (PrimeSpectrum R)) ∧ sᶜ = (↑(basicOpen f) : Set (PrimeSpectrum R))

Tactic:
obtain ⟨I, hI, hI'⟩ := isCompact_isOpen_iff_ideal.mp ⟨hs.1.isCompact, hs.2⟩

Premises used: And.right, And.left, And.intro, IsClosed.isCompact, Iff.mp, PrimeSpectrum.isCompact_isOpen_iff_ideal
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h : Nontrivial R
I : Ideal R
hI : I.FG
hI' : (zeroLocus (↑I : Set R))ᶜ = s
inr :
  ∀ (J : Ideal R) (hJ : J.FG) (hJ' : (zeroLocus (↑J : Set R))ᶜ = sᶜ),
    ∃ (e : R) (f : R),
      e * f = 0 ∧
        e + f = 1 ∧ s = (↑(basicOpen e) : Set (PrimeSpectrum R)) ∧ sᶜ = (↑(basicOpen f) : Set (PrimeSpectrum R))
⊢ ∃ (e : R) (f : R),
    e * f = 0 ∧ e + f = 1 ∧ s = (↑(basicOpen e) : Set (PrimeSpectrum R)) ∧ sᶜ = (↑(basicOpen f) : Set (PrimeSpectrum R))

Tactic:
obtain ⟨J, hJ, hJ'⟩ := isCompact_isOpen_iff_ideal.mp
    ⟨hs.2.isClosed_compl.isCompact, hs.1.isOpen_compl⟩

Premises used: IsClosed.isOpen_compl, IsOpen.isClosed_compl, And.right, And.intro, IsClosed.isCompact, Iff.mp, PrimeSpectrum.isCompact_isOpen_iff_ideal
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h : Nontrivial R
I : Ideal R
hI : I.FG
hI' : (zeroLocus (↑I : Set R))ᶜ = s
J : Ideal R
hJ : J.FG
hJ' : (zeroLocus (↑J : Set R))ᶜ = sᶜ
⊢ zeroLocus (↑I : Set R) = sᶜ

Tactic:
simp only [compl_eq_iff_isCompl, ← eq_compl_iff_isCompl, compl_compl] at hI' hJ'

Premises used: compl_compl, eq_compl_iff_isCompl, compl_eq_iff_isCompl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h : Nontrivial R
I : Ideal R
hI : I.FG
hI' : (zeroLocus (↑I : Set R))ᶜ = s
J : Ideal R
hJ : J.FG
hJ' : (zeroLocus (↑J : Set R))ᶜ = sᶜ
hI'₁ : zeroLocus (↑I : Set R) = sᶜ
⊢ zeroLocus (↑J : Set R) = s

Tactic:
simp only [compl_eq_iff_isCompl, ← eq_compl_iff_isCompl, compl_compl] at hI' hJ'

Premises used: compl_compl, eq_compl_iff_isCompl, compl_eq_iff_isCompl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h : Nontrivial R
I : Ideal R
hI : I.FG
J : Ideal R
hJ : J.FG
hI' : zeroLocus (↑I : Set R) = sᶜ
hJ' : zeroLocus (↑J : Set R) = s
⊢ I * J ≤ nilradical R

Tactic:
Ideal.radical_le_radical_iff.mp (le_of_eq ?_)

Premises used: Set.Mem, Ideal.radical_le_radical_iff, Iff.mp, le_of_eq
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h : Nontrivial R
I : Ideal R
hI : I.FG
J : Ideal R
hJ : J.FG
hI' : zeroLocus (↑I : Set R) = sᶜ
hJ' : zeroLocus (↑J : Set R) = s
refine : (I * J).radical = Ideal.radical 0
⊢ I * J ≤ nilradical R

Tactic:
refine Ideal.radical_le_radical_iff.mp (le_of_eq ?_)

Premises used: Ideal.radical_le_radical_iff, Iff.mp, le_of_eq
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h : Nontrivial R
I : Ideal R
hI : I.FG
J : Ideal R
hJ : J.FG
hI' : zeroLocus (↑I : Set R) = sᶜ
hJ' : zeroLocus (↑J : Set R) = s
rw : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑(I * J) : Set R)) (zeroLocus (↑0 : Set R))
rw₁ : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑(I * J) : Set R)) (zeroLocus (↑⊥ : Set R))
rw₂ : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑(I * J) : Set R)) Set.univ
rw₃ : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R) ∪ zeroLocus (↑J : Set R)) Set.univ
rw₄ : sᶜ ∪ zeroLocus (↑J : Set R) = Set.univ
rw₅ : sᶜ ∪ s = Set.univ
rw₆ rw₇ : Eq.{u + 1} (α := Set (PrimeSpectrum R)) Set.univ Set.univ
⊢ (I * J).radical = Ideal.radical 0

Tactic:
rw [← zeroLocus_eq_iff, Ideal.zero_eq_bot, zeroLocus_bot,
      zeroLocus_mul, hI', hJ', Set.compl_union_self]

Premises used: PrimeSpectrum.zeroLocus_eq_iff, Ideal.zero_eq_bot, PrimeSpectrum.zeroLocus_bot, PrimeSpectrum.zeroLocus_mul, Set.compl_union_self
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h : Nontrivial R
I : Ideal R
hI : I.FG
J : Ideal R
hJ : J.FG
hI' : zeroLocus (↑I : Set R) = sᶜ
hJ' : zeroLocus (↑J : Set R) = s
⊢ I * J ≤ nilradical R

Tactic:
have : I * J ≤ nilradical R := by
    refine Ideal.radical_le_radical_iff.mp (le_of_eq ?_)
    rw [← zeroLocus_eq_iff, Ideal.zero_eq_bot, zeroLocus_bot,
      zeroLocus_mul, hI', hJ', Set.compl_union_self]