-- Mathlib/Analysis/Normed/Algebra/Spectrum.lean
/-- Let `S` be a closed subalgebra of a Banach algebra `A`. If for `x : S` the complement of the
spectrum of `↑x : A` is connected, then `spectrum 𝕜 x = spectrum 𝕜 (x : A)`. -/
lemma Subalgebra.spectrum_eq_of_isPreconnected_compl (h : IsPreconnected (σ 𝕜 (x : A))ᶜ) :
    σ 𝕜 x = σ 𝕜 (x : A)

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✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed ↑S
x : ↥S
h : IsPreconnected (σ 𝕜 ↑x)ᶜ
a✝ : Nontrivial A
⊢ σ 𝕜 x \ σ 𝕜 ↑x = ∅

Tactic:
refine eq_empty_of_forall_not_mem fun z hz ↦ NormedSpace.unbounded_univ 𝕜 𝕜 ?_

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✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed ↑S
x : ↥S
h : IsPreconnected (σ 𝕜 ↑x)ᶜ
a✝ : Nontrivial A
z : 𝕜
hz : z ∈ σ 𝕜 x \ σ 𝕜 ↑x
⊢ Bornology.IsBounded univ

Proof state:
case intro
𝕜 : 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✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed ↑S
x : ↥S
h : IsPreconnected (σ 𝕜 ↑x)ᶜ
a✝ : Nontrivial A
z : 𝕜
hz✝ : z ∈ σ 𝕜 x \ σ 𝕜 ↑x
hz : z ∈ σ 𝕜 x
hz' : z ∉ σ 𝕜 ↑x
⊢ Bornology.IsBounded univ

Tactic:
have := (spectrum.isBounded (x : A)).union <|
  h.connectedComponentIn hz' ▸ spectrum_isBounded_connectedComponentIn S x hz

Result:
case intro
𝕜 : 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✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed ↑S
x : ↥S
h : IsPreconnected (σ 𝕜 ↑x)ᶜ
a✝ : Nontrivial A
z : 𝕜
hz✝ : z ∈ σ 𝕜 x \ σ 𝕜 ↑x
hz : z ∈ σ 𝕜 x
hz' : z ∉ σ 𝕜 ↑x
this : Bornology.IsBounded (σ 𝕜 ↑x ∪ (σ 𝕜 ↑x)ᶜ)
⊢ Bornology.IsBounded univ

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✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed ↑S
x : ↥S
h : IsPreconnected (σ 𝕜 ↑x)ᶜ
a✝ : Nontrivial A
⊢ σ 𝕜 x = σ 𝕜 ↑x

Tactic:
suffices σ 𝕜 x \ σ 𝕜 (x : A) = ∅ by
  rw [spectrum_sUnion_connectedComponentIn, this]
  simp

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✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed ↑S
x : ↥S
h : IsPreconnected (σ 𝕜 ↑x)ᶜ
a✝ : Nontrivial A
⊢ σ 𝕜 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✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed ↑S
x : ↥S
h : IsPreconnected (σ 𝕜 ↑x)ᶜ
⊢ σ 𝕜 x = σ 𝕜 ↑x

Tactic:
nontriviality A

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✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed ↑S
x : ↥S
h : IsPreconnected (σ 𝕜 ↑x)ᶜ
a✝ : Nontrivial A
⊢ σ 𝕜 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✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed ↑S
x : ↥S
h : IsPreconnected (σ 𝕜 ↑x)ᶜ
a✝ : Nontrivial A
this : σ 𝕜 x \ σ 𝕜 ↑x = ∅
⊢ σ 𝕜 ↑x ∪ ⋃ z ∈ ∅, connectedComponentIn (σ 𝕜 ↑x)ᶜ z = σ 𝕜 ↑x

Tactic:
simp

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✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed ↑S
x : ↥S
h : IsPreconnected (σ 𝕜 ↑x)ᶜ
a✝ : Nontrivial A
this : σ 𝕜 x \ σ 𝕜 ↑x = ∅
⊢ σ 𝕜 x = σ 𝕜 ↑x

Tactic:
rw [spectrum_sUnion_connectedComponentIn, this]

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✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed ↑S
x : ↥S
h : IsPreconnected (σ 𝕜 ↑x)ᶜ
a✝ : Nontrivial A
this : σ 𝕜 x \ σ 𝕜 ↑x = ∅
⊢ σ 𝕜 ↑x ∪ ⋃ z ∈ ∅, connectedComponentIn (σ 𝕜 ↑x)ᶜ z = σ 𝕜 ↑x

Proof state:
case intro
𝕜 : 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✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed ↑S
x : ↥S
h : IsPreconnected (σ 𝕜 ↑x)ᶜ
a✝ : Nontrivial A
z : 𝕜
hz✝ : z ∈ σ 𝕜 x \ σ 𝕜 ↑x
hz : z ∈ σ 𝕜 x
hz' : z ∉ σ 𝕜 ↑x
this : Bornology.IsBounded (σ 𝕜 ↑x ∪ (σ 𝕜 ↑x)ᶜ)
⊢ Bornology.IsBounded univ

Tactic:
simpa

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✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed ↑S
x : ↥S
h : IsPreconnected (σ 𝕜 ↑x)ᶜ
a✝ : Nontrivial A
z : 𝕜
hz : z ∈ σ 𝕜 x \ σ 𝕜 ↑x
⊢ Bornology.IsBounded univ

Tactic:
obtain ⟨hz, hz'⟩ := mem_diff _ |>.mp hz

Result:
case intro
𝕜 : 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✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed ↑S
x : ↥S
h : IsPreconnected (σ 𝕜 ↑x)ᶜ
a✝ : Nontrivial A
z : 𝕜
hz✝ : z ∈ σ 𝕜 x \ σ 𝕜 ↑x
hz : z ∈ σ 𝕜 x
hz' : z ∉ σ 𝕜 ↑x
⊢ Bornology.IsBounded univ