-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
@[stacks 00EE]
lemma existsUnique_idempotent_basicOpen_eq_of_isClopen {s : Set (PrimeSpectrum R)}
    (hs : IsClopen s) : ∃! e : R, IsIdempotentElem e ∧ s = basicOpen e

Proof state:
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 = sᶜ
hJ' : zeroLocus ↑J = s
⊢ I * J ≤ nilradical R

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

Result:
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 = sᶜ
hJ' : zeroLocus ↑J = s
⊢ (I * J).radical = Ideal.radical 0

Proof state:
case refine_1.inr.intro.intro.intro.intro
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)ᶜ = s
J : Ideal R
hJ : J.FG
hJ' : (zeroLocus ↑J)ᶜ = sᶜ
⊢ ∃ x, IsIdempotentElem x ∧ s = ↑(basicOpen x)

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

Result:
case refine_1.inr.intro.intro.intro.intro
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 = sᶜ
hJ' : zeroLocus ↑J = s
⊢ ∃ x, IsIdempotentElem x ∧ s = ↑(basicOpen x)

Proof state:
case refine_1.inr.intro.intro.intro.intro
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 = sᶜ
hJ' : zeroLocus ↑J = s
this : I * J ≤ nilradical R
⊢ ∃ x, IsIdempotentElem x ∧ s = ↑(basicOpen x)

Tactic:
obtain ⟨n, hn⟩ := Ideal.exists_pow_le_of_le_radical_of_fg this (Submodule.FG.mul hI hJ)

Result:
case refine_1.inr.intro.intro.intro.intro.intro
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 = sᶜ
hJ' : zeroLocus ↑J = s
this : I * J ≤ nilradical R
n : ℕ
hn : (I * J) ^ n ≤ 0
⊢ ∃ x, IsIdempotentElem x ∧ s = ↑(basicOpen x)

Proof state:
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 = sᶜ
hJ' : zeroLocus ↑J = s
⊢ (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]

Result:
no goals

Proof state:
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 = sᶜ
hJ' : zeroLocus ↑J = s
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
⊢ 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]

Result:
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 = sᶜ
hJ' : zeroLocus ↑J = s
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
⊢ (fun x => x ^ n) '' ↑I ⊆ ↑(I ^ n ⊔ J ^ n) ∧ (fun x => x ^ n) '' ↑J ⊆ ↑(I ^ n ⊔ J ^ n)

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 = sᶜ
hJ' : zeroLocus ↑J = s
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
⊢ Ideal.span (↑I ∪ ↑J) = ⊤

Proof state:
case refine_2
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
⊢ ∀ (y₁ y₂ : R), IsIdempotentElem y₁ ∧ s = ↑(basicOpen y₁) → IsIdempotentElem y₂ ∧ s = ↑(basicOpen y₂) → y₁ = y₂

Tactic:
rintro x y ⟨hx, rfl⟩ ⟨hy, eq⟩

Result:
case refine_2.intro.intro
R : Type u
inst✝ : CommSemiring R
x y : R
hx : IsIdempotentElem x
hs : IsClopen ↑(basicOpen x)
hy : IsIdempotentElem y
eq : ↑(basicOpen x) = ↑(basicOpen y)
⊢ x = y

Proof state:
case refine_1.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
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 = sᶜ
hJ' : zeroLocus ↑J = 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
e : x + y = 1
⊢ IsIdempotentElem x

Tactic:
replace e := congr(x * $e)

Result:
case refine_1.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
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 = sᶜ
hJ' : zeroLocus ↑J = 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
e : x * (x + y) = x * 1
⊢ IsIdempotentElem x

Proof state:
case refine_1.inl
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h✝ : Subsingleton R
⊢ ∃ x, IsIdempotentElem x ∧ s = ↑(basicOpen x)

Tactic:
exact ⟨0, Subsingleton.elim _ _, Subsingleton.elim _ _⟩

Result:
no goals

Proof state:
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 = sᶜ
hJ' : zeroLocus ↑J = s
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
⊢ (fun x => x ^ n) '' ↑I ⊆ ↑(I ^ n ⊔ J ^ n) ∧ (fun x => x ^ n) '' ↑J ⊆ ↑(I ^ n ⊔ J ^ n)

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 = sᶜ
hJ' : zeroLocus ↑J = s
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
⊢ Ideal.span (↑I ∪ ↑J) = ⊤

Tactic:
constructor

Result:
case left
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 = sᶜ
hJ' : zeroLocus ↑J = s
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
⊢ (fun x => x ^ n) '' ↑I ⊆ ↑(I ^ n ⊔ J ^ n)

case right
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 = sᶜ
hJ' : zeroLocus ↑J = s
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
⊢ (fun x => x ^ n) '' ↑J ⊆ ↑(I ^ n ⊔ J ^ n)

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 = sᶜ
hJ' : zeroLocus ↑J = s
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
⊢ Ideal.span (↑I ∪ ↑J) = ⊤

Proof state:
case refine_1.inr.intro.intro.intro.intro.intro
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 = sᶜ
hJ' : zeroLocus ↑J = s
this : I * J ≤ nilradical R
n : ℕ
hn : (I * J) ^ n ≤ 0
⊢ ∃ x, IsIdempotentElem x ∧ s = ↑(basicOpen x)

Tactic:
have hnz : n ≠ 0 := by rintro rfl; simp at hn

Result:
case refine_1.inr.intro.intro.intro.intro.intro
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 = sᶜ
hJ' : zeroLocus ↑J = s
this : I * J ≤ nilradical R
n : ℕ
hn : (I * J) ^ n ≤ 0
hnz : n ≠ 0
⊢ ∃ x, IsIdempotentElem x ∧ s = ↑(basicOpen x)