-- 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:
case right.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 ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
x : R
hx : x ∈ ↑J
⊢ (fun x => x ^ n) x ∈ ↑(I ^ n ⊔ J ^ n)

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

Result:
no goals

Proof state:
case refine_1.inr.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
⊢ ∃ x, IsIdempotentElem x ∧ s = ↑(basicOpen x)

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

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
hI' : (zeroLocus ↑I)ᶜ = s
J : Ideal R
hJ : J.FG
hJ' : (zeroLocus ↑J)ᶜ = sᶜ
⊢ ∃ x, IsIdempotentElem x ∧ s = ↑(basicOpen x)

Proof state:
case left.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 ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
x : R
hx : x ∈ ↑I
⊢ (fun x => x ^ n) x ∈ ↑(I ^ n ⊔ J ^ n)

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

Result:
no goals

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 ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
this : I ^ n ⊔ J ^ n = ⊤
⊢ ∃ x, IsIdempotentElem x ∧ s = ↑(basicOpen x)

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

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 ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
this : ∃ y ∈ I ^ n, ∃ z ∈ J ^ n, y + z = 1
⊢ ∃ x, IsIdempotentElem x ∧ s = ↑(basicOpen x)

Proof state:
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

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

Result:
no goals

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
⊢ ∃ x, IsIdempotentElem x ∧ s = ↑(basicOpen x)

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]

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
this : I * J ≤ nilradical R
⊢ ∃ x, IsIdempotentElem x ∧ s = ↑(basicOpen x)

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

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:
swap

Result:
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₂

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

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 ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
this : ∃ y ∈ I ^ n, ∃ z ∈ J ^ n, y + z = 1
⊢ ∃ x, IsIdempotentElem x ∧ s = ↑(basicOpen x)

Tactic:
obtain ⟨x, hx, y, hy, e⟩ := this

Result:
case refine_1.inr.intro.intro.intro.intro.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 ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
x : R
hx : x ∈ I ^ n
y : R
hy : y ∈ J ^ n
e : x + y = 1
⊢ ∃ 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
this : I * J ≤ nilradical R
hn : (I * J) ^ 0 ≤ 0
⊢ False

Tactic:
simp at hn

Result:
no goals

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

Tactic:
cases subsingleton_or_nontrivial R

Result:
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)

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

Proof state:
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
⊢ ∃! e, IsIdempotentElem e ∧ s = ↑(basicOpen e)

Tactic:
refine existsUnique_of_exists_of_unique ?_ ?_

Result:
case refine_1
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
⊢ ∃ x, IsIdempotentElem x ∧ s = ↑(basicOpen x)

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₂

Proof state:
case refine_1.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
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
⊢ x + y ∈ Ideal.span {x} ⊔ J

Tactic:
exact Submodule.add_mem_sup (Ideal.subset_span (Set.mem_singleton _)) (Ideal.pow_le_self hnz hy)

Result:
no goals

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 * (x + y) = x * 1
⊢ IsIdempotentElem x

Tactic:
rwa [mul_add, hn (Ideal.mul_mem_mul hx hy), add_zero, mul_one] at e

Result:
no goals