-- Mathlib/Analysis/CStarAlgebra/Spectrum.lean
/-- The complement of the spectrum of a selfadjoint element in a C⋆-algebra is connected. -/
lemma IsSelfAdjoint.isConnected_spectrum_compl {a : A} (ha : IsSelfAdjoint a) :
    IsConnected (σ ℂ a)ᶜ

Proof state:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
⊢ ((σ ℂ a)ᶜ ∩ {z | 0 ≤ z.im} ∩ ((σ ℂ a)ᶜ ∩ {z | z.im ≤ 0})).Nonempty

Tactic:
have := Filter.NeBot.nonempty_of_mem inferInstance <| Filter.mem_map.mp <|
  Complex.isometry_ofReal.antilipschitz.tendsto_cobounded (spectrum.isBounded a |>.compl)

Result:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
this : (ofReal ⁻¹' (σ ℂ a)ᶜ).Nonempty
⊢ ((σ ℂ a)ᶜ ∩ {z | 0 ≤ z.im} ∩ ((σ ℂ a)ᶜ ∩ {z | z.im ≤ 0})).Nonempty

Proof state:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
⊢ IsConnected ((σ ℂ a)ᶜ ∩ {z | 0 ≤ z.im} ∪ (σ ℂ a)ᶜ ∩ {z | z.im ≤ 0})

Tactic:
refine IsConnected.union ?nonempty ?upper ?lower

Result:
case nonempty
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
⊢ ((σ ℂ a)ᶜ ∩ {z | 0 ≤ z.im} ∩ ((σ ℂ a)ᶜ ∩ {z | z.im ≤ 0})).Nonempty

case upper
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
⊢ IsConnected ((σ ℂ a)ᶜ ∩ {z | 0 ≤ z.im})

case lower
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
⊢ IsConnected ((σ ℂ a)ᶜ ∩ {z | z.im ≤ 0})

Proof state:
case h.e'_3.h.e'_4
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
this : IsConnected ((σ ℂ a)ᶜ ∩ {a | 0 ≤ a.im ∨ a.im ≤ 0})
⊢ Set.univ = {a | 0 ≤ a.im ∨ a.im ≤ 0}

Tactic:
exact Eq.symm <| Set.eq_univ_of_forall (fun z ↦ le_total 0 z.im)

Result:
no goals

Proof state:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
⊢ IsConnected (σ ℂ a)ᶜ

Tactic:
suffices IsConnected (((σ ℂ a)ᶜ ∩ {z | 0 ≤ z.im}) ∪ (σ ℂ a)ᶜ ∩ {z | z.im ≤ 0}) by
  rw [← Set.inter_union_distrib_left, ← Set.setOf_or] at this
  rw [← Set.inter_univ (σ ℂ a)ᶜ]
  convert this using 2
  exact Eq.symm <| Set.eq_univ_of_forall (fun z ↦ le_total 0 z.im)

Result:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
⊢ IsConnected ((σ ℂ a)ᶜ ∩ {z | 0 ≤ z.im} ∪ (σ ℂ a)ᶜ ∩ {z | z.im ≤ 0})

Proof state:
case nonempty
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
⊢ ((σ ℂ a)ᶜ ∩ {z | 0 ≤ z.im} ∩ ((σ ℂ a)ᶜ ∩ {z | z.im ≤ 0})).Nonempty

case upper
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
⊢ IsConnected ((σ ℂ a)ᶜ ∩ {z | 0 ≤ z.im})

case lower
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
⊢ IsConnected ((σ ℂ a)ᶜ ∩ {z | z.im ≤ 0})

Tactic:
case nonempty =>
  have := Filter.NeBot.nonempty_of_mem inferInstance <| Filter.mem_map.mp <|
    Complex.isometry_ofReal.antilipschitz.tendsto_cobounded (spectrum.isBounded a |>.compl)
  exact this.image Complex.ofReal |>.mono <| by simp

Result:
case upper
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
⊢ IsConnected ((σ ℂ a)ᶜ ∩ {z | 0 ≤ z.im})

case lower
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
⊢ IsConnected ((σ ℂ a)ᶜ ∩ {z | z.im ≤ 0})

Proof state:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
this : IsConnected ((σ ℂ a)ᶜ ∩ {a | 0 ≤ a.im ∨ a.im ≤ 0})
⊢ IsConnected ((σ ℂ a)ᶜ ∩ Set.univ)

Tactic:
convert this using 2

Result:
case h.e'_3.h.e'_4
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
this : IsConnected ((σ ℂ a)ᶜ ∩ {a | 0 ≤ a.im ∨ a.im ≤ 0})
⊢ Set.univ = {a | 0 ≤ a.im ∨ a.im ≤ 0}

Proof state:
case lower
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
⊢ IsConnected ((σ ℂ a)ᶜ ∩ {z | z.im ≤ 0})

Tactic:
apply Complex.isConnected_of_lowerHalfPlane ?_ <| Set.inter_subset_right

Result:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
⊢ {z | z.im < 0} ⊆ (σ ℂ a)ᶜ ∩ {z | z.im ≤ 0}

Proof state:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
this : (ofReal ⁻¹' (σ ℂ a)ᶜ).Nonempty
⊢ ofReal '' (ofReal ⁻¹' (σ ℂ a)ᶜ) ⊆ (σ ℂ a)ᶜ ∩ {z | 0 ≤ z.im} ∩ ((σ ℂ a)ᶜ ∩ {z | z.im ≤ 0})

Tactic:
simp

Result:
no goals

Proof state:
case upper
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
⊢ {z | 0 < z.im} ⊆ (σ ℂ a)ᶜ ∩ {z | 0 ≤ z.im}

case lower
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
⊢ IsConnected ((σ ℂ a)ᶜ ∩ {z | z.im ≤ 0})

Tactic:
case' lower => apply Complex.isConnected_of_lowerHalfPlane ?_ <| Set.inter_subset_right

Result:
case lower
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
⊢ {z | z.im < 0} ⊆ (σ ℂ a)ᶜ ∩ {z | z.im ≤ 0}

case upper
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
⊢ {z | 0 < z.im} ⊆ (σ ℂ a)ᶜ ∩ {z | 0 ≤ z.im}

Proof state:
case upper
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : 0 < 0
hz' : z ∈ σ ℂ a
⊢ False

Tactic:
simp_all

Result:
no goals

Proof state:
case upper
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
⊢ IsConnected ((σ ℂ a)ᶜ ∩ {z | 0 ≤ z.im})

case lower
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
⊢ IsConnected ((σ ℂ a)ᶜ ∩ {z | z.im ≤ 0})

Tactic:
case' upper => apply Complex.isConnected_of_upperHalfPlane ?_ <| Set.inter_subset_right

Result:
case upper
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
⊢ {z | 0 < z.im} ⊆ (σ ℂ a)ᶜ ∩ {z | 0 ≤ z.im}

case lower
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
⊢ IsConnected ((σ ℂ a)ᶜ ∩ {z | z.im ≤ 0})

Proof state:
case upper
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
⊢ IsConnected ((σ ℂ a)ᶜ ∩ {z | 0 ≤ z.im})

Tactic:
apply Complex.isConnected_of_upperHalfPlane ?_ <| Set.inter_subset_right

Result:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
⊢ {z | 0 < z.im} ⊆ (σ ℂ a)ᶜ ∩ {z | 0 ≤ z.im}

Proof state:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
this : (ofReal ⁻¹' (σ ℂ a)ᶜ).Nonempty
⊢ ((σ ℂ a)ᶜ ∩ {z | 0 ≤ z.im} ∩ ((σ ℂ a)ᶜ ∩ {z | z.im ≤ 0})).Nonempty

Tactic:
exact this.image Complex.ofReal |>.mono <| by simp

Result:
no goals

Proof state:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
this : IsConnected ((σ ℂ a)ᶜ ∩ {z | 0 ≤ z.im} ∪ (σ ℂ a)ᶜ ∩ {z | z.im ≤ 0})
⊢ IsConnected (σ ℂ a)ᶜ

Tactic:
rw [← Set.inter_union_distrib_left, ← Set.setOf_or] at this

Result:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
this : IsConnected ((σ ℂ a)ᶜ ∩ {a | 0 ≤ a.im ∨ a.im ≤ 0})
⊢ IsConnected (σ ℂ a)ᶜ

Proof state:
case lower
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
⊢ {z | z.im < 0} ⊆ (σ ℂ a)ᶜ ∩ {z | z.im ≤ 0}

case upper
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
⊢ {z | 0 < z.im} ⊆ (σ ℂ a)ᶜ ∩ {z | 0 ≤ z.im}

Tactic:
all_goals
  refine Set.subset_inter (fun z hz hz' ↦ ?_) (fun _ ↦ by simpa using le_of_lt)
  rw [Set.mem_setOf_eq, ha.im_eq_zero_of_mem_spectrum hz'] at hz
  simp_all

Result:
no goals

Proof state:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
x✝ : ℂ
⊢ x✝ ∈ {z | 0 < z.im} → x✝ ∈ {z | 0 ≤ z.im}

Tactic:
simpa using le_of_lt

Result:
no goals