-- Mathlib/Analysis/Normed/Algebra/Spectrum.lean
/-- If `S` is a closed subalgebra of a Banach algebra `A`, then for any `x : S`, the spectrum of `x`
is the spectrum of `↑x : A` along with the connected components of the complement of the spectrum of
`↑x : A` which contain an element of the spectrum of `x : S`. -/
lemma Subalgebra.spectrum_sUnion_connectedComponentIn :
    σ 𝕜 x = σ 𝕜 (x : A) ∪ (⋃ z ∈ (σ 𝕜 x \ σ 𝕜 (x : A)), connectedComponentIn (σ 𝕜 (x : A))ᶜ z)

Proof state:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst✝⁵ : NormedRing A
inst✝⁴ : CompleteSpace A
inst✝³ : SetLike SA A
inst✝² : SubringClass SA A
inst✝¹ : NormedField 𝕜
inst✝ : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed ↑S
x : ↥S
this : CompleteSpace ↥S
⊢ IsOpen (σ 𝕜 x \ σ 𝕜 ↑x)

Tactic:
rw [← (spectrum.isClosed (𝕜 := 𝕜) x).closure_eq, closure_eq_interior_union_frontier,
  union_diff_distrib, diff_eq_empty.mpr (frontier_spectrum S x),
  diff_eq_compl_inter, union_empty]

Result:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst✝⁵ : NormedRing A
inst✝⁴ : CompleteSpace A
inst✝³ : SetLike SA A
inst✝² : SubringClass SA A
inst✝¹ : NormedField 𝕜
inst✝ : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed ↑S
x : ↥S
this : CompleteSpace ↥S
⊢ IsOpen ((σ 𝕜 ↑x)ᶜ ∩ interior (σ 𝕜 x))

Proof state:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst✝⁵ : NormedRing A
inst✝⁴ : CompleteSpace A
inst✝³ : SetLike SA A
inst✝² : SubringClass SA A
inst✝¹ : NormedField 𝕜
inst✝ : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed ↑S
x : ↥S
⊢ σ 𝕜 x = σ 𝕜 ↑x ∪ ⋃ z ∈ σ 𝕜 x \ σ 𝕜 ↑x, connectedComponentIn (σ 𝕜 ↑x)ᶜ z

Tactic:
suffices IsClopen ((σ 𝕜 (x : A))ᶜ ↓∩ (σ 𝕜 x \ σ 𝕜 (x : A))) by
  rw [← this.biUnion_connectedComponentIn (diff_subset_compl _ _),
    union_diff_cancel (spectrum.subset_subalgebra x)]

Result:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst✝⁵ : NormedRing A
inst✝⁴ : CompleteSpace A
inst✝³ : SetLike SA A
inst✝² : SubringClass SA A
inst✝¹ : NormedField 𝕜
inst✝ : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed ↑S
x : ↥S
⊢ IsClopen ((σ 𝕜 ↑x)ᶜ ↓∩ σ 𝕜 x \ σ 𝕜 ↑x)

Proof state:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst✝⁵ : NormedRing A
inst✝⁴ : CompleteSpace A
inst✝³ : SetLike SA A
inst✝² : SubringClass SA A
inst✝¹ : NormedField 𝕜
inst✝ : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed ↑S
x : ↥S
this : CompleteSpace ↥S
h_open : IsOpen (σ 𝕜 x \ σ 𝕜 ↑x)
⊢ frontier (σ 𝕜 ↑x)ᶜ ∩ closure (σ 𝕜 x) ∪ closure (σ 𝕜 ↑x)ᶜ ∩ frontier (σ 𝕜 x) ⊆ frontier (σ 𝕜 ↑x)

Tactic:
rw [frontier_compl]

Result:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst✝⁵ : NormedRing A
inst✝⁴ : CompleteSpace A
inst✝³ : SetLike SA A
inst✝² : SubringClass SA A
inst✝¹ : NormedField 𝕜
inst✝ : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed ↑S
x : ↥S
this : CompleteSpace ↥S
h_open : IsOpen (σ 𝕜 x \ σ 𝕜 ↑x)
⊢ frontier (σ 𝕜 ↑x) ∩ closure (σ 𝕜 x) ∪ closure (σ 𝕜 ↑x)ᶜ ∩ frontier (σ 𝕜 x) ⊆ frontier (σ 𝕜 ↑x)

Proof state:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst✝⁵ : NormedRing A
inst✝⁴ : CompleteSpace A
inst✝³ : SetLike SA A
inst✝² : SubringClass SA A
inst✝¹ : NormedField 𝕜
inst✝ : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed ↑S
x : ↥S
this : IsClopen ((σ 𝕜 ↑x)ᶜ ↓∩ σ 𝕜 x \ σ 𝕜 ↑x)
⊢ σ 𝕜 x = σ 𝕜 ↑x ∪ ⋃ z ∈ σ 𝕜 x \ σ 𝕜 ↑x, connectedComponentIn (σ 𝕜 ↑x)ᶜ z

Tactic:
rw [← this.biUnion_connectedComponentIn (diff_subset_compl _ _),
  union_diff_cancel (spectrum.subset_subalgebra x)]

Result:
no goals