-- 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
h_open : IsOpen (σ 𝕜 x \ σ 𝕜 ↑x)
⊢ frontier (σ 𝕜 x) ⊆ frontier (σ 𝕜 ↑x)

Tactic:
exact frontier_subset_frontier S x

Result:
no goals

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)ᶜ ∩ σ 𝕜 x) ⊆ frontier (σ 𝕜 ↑x)

Tactic:
apply (frontier_inter_subset _ _).trans

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 : CompleteSpace ↥S
h_open : IsOpen (σ 𝕜 x \ σ 𝕜 ↑x)
⊢ frontier (σ 𝕜 x \ σ 𝕜 ↑x) ⊆ frontier (σ 𝕜 ↑x)

Tactic:
rw [diff_eq_compl_inter]

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)ᶜ ∩ σ 𝕜 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
⊢ IsClopen ((σ 𝕜 ↑x)ᶜ ↓∩ σ 𝕜 x \ σ 𝕜 ↑x)

Tactic:
have : CompleteSpace S := hS.completeSpace_coe

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
⊢ 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)
⊢ closure (σ 𝕜 ↑x)ᶜ ∩ frontier (σ 𝕜 x) ⊆ frontier (σ 𝕜 ↑x)

Tactic:
refine inter_subset_inter_right _ ?_ |>.trans <| inter_subset_right

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) ⊆ 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 : CompleteSpace ↥S
h_open : IsOpen (σ 𝕜 x \ σ 𝕜 ↑x)
⊢ Disjoint (frontier (σ 𝕜 x \ σ 𝕜 ↑x)) (σ 𝕜 ↑x)ᶜ

Tactic:
suffices h_frontier : frontier (σ 𝕜 x \ σ 𝕜 (x : A)) ⊆ frontier (σ 𝕜 (x : A)) from
  disjoint_of_subset_left h_frontier <| disjoint_compl_right.frontier_left
    (spectrum.isClosed _).isOpen_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 \ σ 𝕜 ↑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 : CompleteSpace ↥S
⊢ IsOpen ((σ 𝕜 ↑x)ᶜ ∩ interior (σ 𝕜 x))

Tactic:
exact (spectrum.isClosed _).isOpen_compl.inter isOpen_interior

Result:
no goals

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
⊢ IsClopen ((σ 𝕜 ↑x)ᶜ ↓∩ σ 𝕜 x \ σ 𝕜 ↑x)

Tactic:
have h_open : IsOpen (σ 𝕜 x \ σ 𝕜 (x : A)) := by
  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]
  exact (spectrum.isClosed _).isOpen_compl.inter isOpen_interior

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)
⊢ 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)
⊢ IsClopen ((σ 𝕜 ↑x)ᶜ ↓∩ σ 𝕜 x \ σ 𝕜 ↑x)

Tactic:
apply isClopen_preimage_val h_open

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)
⊢ Disjoint (frontier (σ 𝕜 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:
apply union_subset <| inter_subset_left

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)
⊢ closure (σ 𝕜 ↑x)ᶜ ∩ frontier (σ 𝕜 x) ⊆ frontier (σ 𝕜 ↑x)