awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
this : I * J ≤ nilradical R
inr :
  ∀ (n : ℕ) (hn : (I * J) ^ n ≤ 0),
    ∃ (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 ⟨n, hn⟩ := Ideal.exists_pow_le_of_le_radical_of_fg this (Submodule.FG.mul hI hJ)

Premises used: Ideal.exists_pow_le_of_le_radical_of_fg, Submodule.FG.mul
-- 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
this : I * J ≤ nilradical R
hn : HPow.hPow (β := ℕ) (I * J) 0 ≤ 0
⊢ False

Tactic:
simp at hn
-- 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
this : I * J ≤ nilradical R
n : ℕ
hn : (I * J) ^ n ≤ 0
⊢ n ≠ 0

Tactic:
have hnz : n ≠ 0 := by rintro rfl; simp at hn
-- 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
this : I * J ≤ nilradical R
n : ℕ
hn : (I * J) ^ n ≤ 0
hnz : n ≠ 0
⊢ I ^ n * J ^ n ≤ ⊥

Tactic:
rw [mul_pow, Ideal.zero_eq_bot] at hn

Premises used: Ideal.zero_eq_bot, mul_pow
-- 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
this : I * J ≤ nilradical R
n : ℕ
hn : (I * J) ^ n ≤ 0
hnz : n ≠ 0
hn₁ : I ^ n * J ^ n ≤ ⊥
⊢ n ≠ 0

Tactic:
rw [mul_pow, Ideal.zero_eq_bot] at hn

Premises used: Ideal.zero_eq_bot, mul_pow
-- 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
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
rw :
  (fun (x : R) ↦ x ^ n) '' (↑I : Set R) ⊆ (↑(I ^ n ⊔ J ^ n) : Set R) ∧
    (fun (x : R) ↦ x ^ n) '' (↑J : Set R) ⊆ (↑(I ^ n ⊔ J ^ n) : Set R)
rw₁ : Eq (α := Ideal R) (Ideal.span ((↑I : Set R) ∪ (↑J : Set R))) ⊤
⊢ I ^ n ⊔ J ^ n = ⊤

Tactic:
rw [eq_top_iff, ← Ideal.span_pow_eq_top (I ∪ J : Set R) _ n, Ideal.span_le, Set.image_union,
      Set.union_subset_iff]

Premises used: Ideal.span_le, Ideal.span_pow_eq_top, eq_top_iff, Set.union_subset_iff, SetLike.coe, Union.union, Set.image_union
-- 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
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
left : (fun (x : R) ↦ x ^ n) '' (↑I : Set R) ⊆ (↑(I ^ n ⊔ J ^ n) : Set R)
right : (fun (x : R) ↦ x ^ n) '' (↑J : Set R) ⊆ (↑(I ^ n ⊔ J ^ n) : Set R)
⊢ (fun (x : R) ↦ x ^ n) '' (↑I : Set R) ⊆ (↑(I ^ n ⊔ J ^ n) : Set R) ∧
    (fun (x : R) ↦ x ^ n) '' (↑J : Set R) ⊆ (↑(I ^ n ⊔ J ^ n) : Set R)

Tactic:
constructor
-- 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
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
x : R
hx : x ∈ (↑I : Set R)
⊢ (fun (x : R) ↦ x ^ n) x ∈ (↑(I ^ n ⊔ J ^ n) : Set R)

Tactic:
Ideal.mem_sup_left (Ideal.pow_mem_pow hx n)

Premises used: Set.Mem, Ideal.mem_sup_left, setOf, Ideal.pow_mem_pow
-- 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
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
x : R
hx : x ∈ (↑I : Set R)
⊢ (fun (x : R) ↦ x ^ n) x ∈ (↑(I ^ n ⊔ J ^ n) : Set R)

Tactic:
exact Ideal.mem_sup_left (Ideal.pow_mem_pow hx n)

Premises used: Ideal.mem_sup_left, Ideal.pow_mem_pow
-- 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
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
x : R
hx : x ∈ (↑J : Set R)
⊢ (fun (x : R) ↦ x ^ n) x ∈ (↑(I ^ n ⊔ J ^ n) : Set R)

Tactic:
Ideal.mem_sup_right (Ideal.pow_mem_pow hx n)

Premises used: Set.Mem, setOf, Ideal.pow_mem_pow, Ideal.mem_sup_right
-- 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
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
x : R
hx : x ∈ (↑J : Set R)
⊢ (fun (x : R) ↦ x ^ n) x ∈ (↑(I ^ n ⊔ J ^ n) : Set R)

Tactic:
exact Ideal.mem_sup_right (Ideal.pow_mem_pow hx n)

Premises used: Ideal.pow_mem_pow, Ideal.mem_sup_right
-- 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
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
rw : Eq (α := Ideal R) (Ideal.span (↑I : Set R) ⊔ Ideal.span (↑J : Set R)) ⊤
rw₁ : I ⊔ Ideal.span (↑J : Set R) = ⊤
rw₂ : I ⊔ J = ⊤
rw₃ : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑(I ⊔ J) : Set R)) ∅
rw₄ : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R) ∩ zeroLocus (↑J : Set R)) ∅
rw₅ : sᶜ ∩ zeroLocus (↑J : Set R) = ∅
rw₆ : sᶜ ∩ s = ∅
rw₇ rw₈ : Eq.{u + 1} (α := Set (PrimeSpectrum R)) ∅ ∅
⊢ Eq (α := Ideal R) (Ideal.span ((↑I : Set R) ∪ (↑J : Set R))) ⊤

Tactic:
rw [Ideal.span_union, Ideal.span_eq, Ideal.span_eq, ← zeroLocus_empty_iff_eq_top,
        zeroLocus_sup, hI', hJ', Set.compl_inter_self]

Premises used: Ideal.span_eq, Set.compl_inter_self, Ideal.span_union, PrimeSpectrum.zeroLocus_sup, PrimeSpectrum.zeroLocus_empty_iff_eq_top
-- 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
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
⊢ I ^ n ⊔ J ^ n = ⊤

Tactic:
have : I ^ n ⊔ J ^ n = ⊤ := by
    rw [eq_top_iff, ← Ideal.span_pow_eq_top (I ∪ J : Set R) _ n, Ideal.span_le, Set.image_union,
      Set.union_subset_iff]
    constructor
    · rintro _ ⟨x, hx, rfl⟩; exact Ideal.mem_sup_left (Ideal.pow_mem_pow hx n)
    · rintro _ ⟨x, hx, rfl⟩; exact Ideal.mem_sup_right (Ideal.pow_mem_pow hx n)
    · rw [Ideal.span_union, Ideal.span_eq, Ideal.span_eq, ← zeroLocus_empty_iff_eq_top,
        zeroLocus_sup, hI', hJ', Set.compl_inter_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
this_1 : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
this : I ^ n ⊔ J ^ n = ⊤
⊢ ∃ y ∈ I ^ n, ∃ z ∈ J ^ n, y + z = 1

Tactic:
rw [Ideal.eq_top_iff_one, Submodule.mem_sup] at this

Premises used: Ideal.eq_top_iff_one, Submodule.mem_sup
-- 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
this_1 : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
this : ∃ y ∈ I ^ n, ∃ z ∈ J ^ n, y + z = 1
inr :
  ∀ (x : R) (hx : x ∈ I ^ n) (y : R) (hy : y ∈ J ^ n) (add : x + y = 1),
    ∃ (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 ⟨x, hx, y, hy, add⟩ := this
-- 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
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
x : R
hx : x ∈ I ^ n
y : R
hy : y ∈ J ^ n
add : x + y = 1
⊢ x * y = 0

Tactic:
have mul : x * y = 0 := hn (Ideal.mul_mem_mul hx hy)
-- 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
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
x : R
hx : x ∈ I ^ n
y : R
hy : y ∈ J ^ n
add : x + y = 1
mul : x * y = 0
⊢ s = (↑(basicOpen x) : Set (PrimeSpectrum R))

Tactic:
subset_antisymm ?_ ?_

Premises used: subset_antisymm
-- 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
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
x : R
hx : x ∈ I ^ n
y : R
hy : y ∈ J ^ n
add : x + y = 1
mul : x * y = 0
refine_1 : s ⊆ (↑(basicOpen x) : Set (PrimeSpectrum R))
refine_2 : (↑(basicOpen x) : Set (PrimeSpectrum R)) ⊆ s
⊢ s = (↑(basicOpen x) : Set (PrimeSpectrum R))

Tactic:
refine subset_antisymm ?_ ?_

Premises used: subset_antisymm
-- 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
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
x : R
hx : x ∈ I ^ n
y : R
hy : y ∈ J ^ n
add : x + y = 1
mul : x * y = 0
refine_1 : Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑J : Set R)) (zeroLocus {y})
⊢ s ⊆ (↑(basicOpen x) : Set (PrimeSpectrum R))

Tactic:
rw [← hJ', basicOpen_eq_zeroLocus_of_mul_add _ _ mul add]

Premises used: PrimeSpectrum.basicOpen_eq_zeroLocus_of_mul_add
-- 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
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
x : R
hx : x ∈ I ^ n
y : R
hy : y ∈ J ^ n
add : x + y = 1
mul : x * y = 0
⊢ Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑J : Set R)) (zeroLocus {y})

Tactic:
zeroLocus_anti_mono (Set.singleton_subset_iff.mpr <| Ideal.pow_le_self hnz hy)

Premises used: PrimeSpectrum.zeroLocus_anti_mono, Iff.mpr, Set.singleton_subset_iff, Ideal.pow_le_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
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
x : R
hx : x ∈ I ^ n
y : R
hy : y ∈ J ^ n
add : x + y = 1
mul : x * y = 0
⊢ Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑J : Set R)) (zeroLocus {y})

Tactic:
exact zeroLocus_anti_mono (Set.singleton_subset_iff.mpr <| Ideal.pow_le_self hnz hy)

Premises used: PrimeSpectrum.zeroLocus_anti_mono, Iff.mpr, Set.singleton_subset_iff, Ideal.pow_le_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
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
x : R
hx : x ∈ I ^ n
y : R
hy : y ∈ J ^ n
add : x + y = 1
mul : x * y = 0
refine_2 : Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) (zeroLocus {x})
⊢ (↑(basicOpen x) : Set (PrimeSpectrum R)) ⊆ s

Tactic:
rw [basicOpen_eq_zeroLocus_compl, Set.compl_subset_comm, ← hI']

Premises used: Set.compl_subset_comm, PrimeSpectrum.basicOpen_eq_zeroLocus_compl
-- 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
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
x : R
hx : x ∈ I ^ n
y : R
hy : y ∈ J ^ n
add : x + y = 1
mul : x * y = 0
⊢ Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) (zeroLocus {x})

Tactic:
zeroLocus_anti_mono (Set.singleton_subset_iff.mpr <| Ideal.pow_le_self hnz hx)

Premises used: PrimeSpectrum.zeroLocus_anti_mono, Iff.mpr, Set.singleton_subset_iff, Ideal.pow_le_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
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
x : R
hx : x ∈ I ^ n
y : R
hy : y ∈ J ^ n
add : x + y = 1
mul : x * y = 0
⊢ Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) (zeroLocus {x})

Tactic:
exact zeroLocus_anti_mono (Set.singleton_subset_iff.mpr <| Ideal.pow_le_self hnz hx)

Premises used: PrimeSpectrum.zeroLocus_anti_mono, Iff.mpr, Set.singleton_subset_iff, Ideal.pow_le_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
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
x : R
hx : x ∈ I ^ n
y : R
hy : y ∈ J ^ n
add : x + y = 1
mul : x * y = 0
⊢ s = (↑(basicOpen x) : Set (PrimeSpectrum R))

Tactic:
have : s = basicOpen x := by
    refine subset_antisymm ?_ ?_
    · rw [← hJ', basicOpen_eq_zeroLocus_of_mul_add _ _ mul add]
      exact zeroLocus_anti_mono (Set.singleton_subset_iff.mpr <| Ideal.pow_le_self hnz hy)
    · rw [basicOpen_eq_zeroLocus_compl, Set.compl_subset_comm, ← hI']
      exact zeroLocus_anti_mono (Set.singleton_subset_iff.mpr <| Ideal.pow_le_self hnz hx)
-- 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
this_1 : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
x : R
hx : x ∈ I ^ n
y : R
hy : y ∈ J ^ n
add : x + y = 1
mul : x * y = 0
this : s = (↑(basicOpen x) : 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:
⟨x, y, mul, add, this, ?_⟩

Premises used: And.intro, Exists.intro
-- 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
this_1 : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
x : R
hx : x ∈ I ^ n
y : R
hy : y ∈ J ^ n
add : x + y = 1
mul : x * y = 0
this : s = (↑(basicOpen x) : Set (PrimeSpectrum R))
inr : sᶜ = (↑(basicOpen y) : 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 ⟨x, y, mul, add, this, ?_⟩
-- 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
this_1 : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
x : R
hx : x ∈ I ^ n
y : R
hy : y ∈ J ^ n
add : x + y = 1
mul : x * y = 0
this : s = (↑(basicOpen x) : Set (PrimeSpectrum R))
inr : (↑(basicOpen x) : Set (PrimeSpectrum R))ᶜ = (↑(basicOpen y) : Set (PrimeSpectrum R))
inr₁ : (zeroLocus {y})ᶜ = (↑(basicOpen y) : Set (PrimeSpectrum R))
inr₂ inr₃ : Eq (α := Set (PrimeSpectrum R)) (zeroLocus {y})ᶜ (zeroLocus {y})ᶜ
⊢ sᶜ = (↑(basicOpen y) : Set (PrimeSpectrum R))

Tactic:
rw [this, basicOpen_eq_zeroLocus_of_mul_add _ _ mul add, basicOpen_eq_zeroLocus_compl]

Premises used: PrimeSpectrum.basicOpen_eq_zeroLocus_of_mul_add, PrimeSpectrum.basicOpen_eq_zeroLocus_compl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
⊢ ∃ (e : R), IsIdempotentElem e ∧ s = (↑(basicOpen e) : Set (PrimeSpectrum R))

Tactic:
have ⟨e, _, mul, add, eq, _⟩ := exists_mul_eq_zero_add_eq_one_basicOpen_eq_of_isClopen hs
  ⟨e, (IsIdempotentElem.of_mul_add mul add).1, eq⟩

Premises used: IsIdempotentElem.of_mul_add, PrimeSpectrum.basicOpen, Exists, PrimeSpectrum.exists_mul_eq_zero_add_eq_one_basicOpen_eq_of_isClopen, _private.0.PrimeSpectrum.exists_idempotent_basicOpen_eq_of_isClopen.match_1, And, IsIdempotentElem, SetLike.coe, And.left, And.intro, Exists.intro, Eq
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
⊢ ∃! e : R, IsIdempotentElem e ∧ s = (↑(basicOpen e) : Set (PrimeSpectrum R))

Tactic:
existsUnique_of_exists_of_unique (exists_idempotent_basicOpen_eq_of_isClopen hs) ?_

Premises used: existsUnique_of_exists_of_unique, PrimeSpectrum.exists_idempotent_basicOpen_eq_of_isClopen
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
refine :
  ∀ (y₁ y₂ : R),
    IsIdempotentElem y₁ ∧ s = (↑(basicOpen y₁) : Set (PrimeSpectrum R)) →
      IsIdempotentElem y₂ ∧ s = (↑(basicOpen y₂) : Set (PrimeSpectrum R)) → y₁ = y₂
⊢ ∃! e : R, IsIdempotentElem e ∧ s = (↑(basicOpen e) : Set (PrimeSpectrum R))

Tactic:
refine existsUnique_of_exists_of_unique (exists_idempotent_basicOpen_eq_of_isClopen hs) ?_

Premises used: existsUnique_of_exists_of_unique, PrimeSpectrum.exists_idempotent_basicOpen_eq_of_isClopen
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
x y : R
hx : IsIdempotentElem x
hs : IsClopen (↑(basicOpen x) : Set (PrimeSpectrum R))
hy : IsIdempotentElem y
eq : (↑(basicOpen x) : Set (PrimeSpectrum R)) = (↑(basicOpen y) : Set (PrimeSpectrum R))
⊢ x = y

Tactic:
basicOpen_injOn_isIdempotentElem hx hy (SetLike.ext' eq)

Premises used: PrimeSpectrum.basicOpen_injOn_isIdempotentElem, SetLike.ext'
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
x y : R
hx : IsIdempotentElem x
hs : IsClopen (↑(basicOpen x) : Set (PrimeSpectrum R))
hy : IsIdempotentElem y
eq : (↑(basicOpen x) : Set (PrimeSpectrum R)) = (↑(basicOpen y) : Set (PrimeSpectrum R))
⊢ x = y

Tactic:
exact basicOpen_injOn_isIdempotentElem hx hy (SetLike.ext' eq)

Premises used: PrimeSpectrum.basicOpen_injOn_isIdempotentElem, SetLike.ext'
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ IsClopen s ↔ ∃ (e : R) (f : R), e * f = 0 ∧ e + f = 1 ∧ s = (↑(basicOpen e) : Set (PrimeSpectrum R))

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

Premises used: Iff.intro
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
refine_1 : ∀ (h : IsClopen s), ∃ (e : R) (f : R), e * f = 0 ∧ e + f = 1 ∧ s = (↑(basicOpen e) : Set (PrimeSpectrum R))
refine_2 : (∃ (e : R) (f : R), e * f = 0 ∧ e + f = 1 ∧ s = (↑(basicOpen e) : Set (PrimeSpectrum R))) → IsClopen s
⊢ IsClopen s ↔ ∃ (e : R) (f : R), e * f = 0 ∧ e + f = 1 ∧ s = (↑(basicOpen e) : Set (PrimeSpectrum R))

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
h : IsClopen s
refine_1 :
  ∀ (e f : R)
    (h :
      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))
⊢ ∃ (e : R) (f : R), e * f = 0 ∧ e + f = 1 ∧ s = (↑(basicOpen e) : Set (PrimeSpectrum R))

Tactic:
have ⟨e, f, h⟩ := exists_mul_eq_zero_add_eq_one_basicOpen_eq_of_isClopen h
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
h_1 : IsClopen s
e f : R
h : e * f = 0 ∧ e + f = 1 ∧ s = (↑(basicOpen e) : Set (PrimeSpectrum R)) ∧ sᶜ = (↑(basicOpen f) : Set (PrimeSpectrum R))
⊢ e * f = 0 ∧ e + f = 1 ∧ s = (↑(basicOpen e) : Set (PrimeSpectrum R))

Tactic:
simp only [h, and_self]

Premises used: and_self
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
h_1 : IsClopen s
e f : R
h : 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))

Tactic:
exact ⟨e, f, by simp only [h, and_self]⟩
-- 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:
isClopen_basicOpen_of_mul_add e f mul add

Premises used: PrimeSpectrum.isClopen_basicOpen_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
⊢ IsClopen (↑(basicOpen e) : Set (PrimeSpectrum R))

Tactic:
exact isClopen_basicOpen_of_mul_add e f mul add

Premises used: PrimeSpectrum.isClopen_basicOpen_of_mul_add
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
rw :
  (∃ (b : R) (a : R), a * b = 0 ∧ a + b = 1 ∧ s = (↑(basicOpen a) : Set (PrimeSpectrum R))) ↔
    ∃ (e : R) (f : R), e * f = 0 ∧ e + f = 1 ∧ s = zeroLocus {e}
⊢ IsClopen s ↔ ∃ (e : R) (f : R), e * f = 0 ∧ e + f = 1 ∧ s = zeroLocus {e}

Tactic:
rw [isClopen_iff_mul_add, exists_comm]

Premises used: PrimeSpectrum.isClopen_iff_mul_add, exists_comm
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ (∃ (b : R) (a : R), a * b = 0 ∧ a + b = 1 ∧ s = (↑(basicOpen a) : Set (PrimeSpectrum R))) ↔
    ∃ (e : R) (f : R), e * f = 0 ∧ e + f = 1 ∧ s = zeroLocus {e}

Tactic:
exists₂_congr fun e f ↦ ?_

Premises used: exists₂_congr