awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
this : IsConnected ((σ ℂ a)ᶜ ∩ {a : ℂ | 0 ≤ a.im ∨ a.im ≤ 0})
⊢ Eq (α := Set ℂ) 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)

Premises used: Eq.symm
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
suffices : IsConnected ((σ ℂ a)ᶜ ∩ {z : ℂ | 0 ≤ z.im} ∪ (σ ℂ a)ᶜ ∩ {z : ℂ | z.im ≤ 0})
⊢ 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)
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
⊢ IsConnected ((σ ℂ a)ᶜ ∩ {z : ℂ | 0 ≤ z.im} ∪ (σ ℂ a)ᶜ ∩ {z : ℂ | z.im ≤ 0})

Tactic:
IsConnected.union ?nonempty ?upper ?lower

Premises used: IsConnected.union
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
refine : ((σ ℂ a)ᶜ ∩ {z : ℂ | 0 ≤ z.im} ∩ ((σ ℂ a)ᶜ ∩ {z : ℂ | z.im ≤ 0})).Nonempty
upper : IsConnected ((σ ℂ a)ᶜ ∩ {z : ℂ | 0 ≤ z.im})
lower : IsConnected ((σ ℂ a)ᶜ ∩ {z : ℂ | z.im ≤ 0})
⊢ IsConnected ((σ ℂ a)ᶜ ∩ {z : ℂ | 0 ≤ z.im} ∪ (σ ℂ a)ᶜ ∩ {z : ℂ | z.im ≤ 0})

Tactic:
refine IsConnected.union ?nonempty ?upper ?lower
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
⊢ (ofReal ⁻¹' (σ ℂ a)ᶜ).Nonempty

Tactic:
have := Filter.NeBot.nonempty_of_mem inferInstance <| Filter.mem_map.mp <|
      Complex.isometry_ofReal.antilipschitz.tendsto_cobounded (spectrum.isBounded a |>.compl)
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : 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
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : 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

Premises used: Complex.ofReal, Set.Nonempty.mono, Set.Nonempty.image
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
⊢ ((σ ℂ a)ᶜ ∩ {z : ℂ | 0 ≤ z.im} ∩ ((σ ℂ a)ᶜ ∩ {z : ℂ | z.im ≤ 0})).Nonempty

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
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
upper : {z : ℂ | 0 < z.im} ⊆ (σ ℂ a)ᶜ ∩ {z : ℂ | 0 ≤ z.im}
⊢ IsConnected ((σ ℂ a)ᶜ ∩ {z : ℂ | 0 ≤ z.im})

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

Premises used: Complex.isConnected_of_upperHalfPlane, Set.inter_subset_right
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
upper : {z : ℂ | 0 < z.im} ⊆ (σ ℂ a)ᶜ ∩ {z : ℂ | 0 ≤ z.im}
⊢ IsConnected ((σ ℂ a)ᶜ ∩ {z : ℂ | 0 ≤ z.im})

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

Premises used: Complex.isConnected_of_upperHalfPlane, Set.inter_subset_right
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
lower : {z : ℂ | z.im < 0} ⊆ (σ ℂ a)ᶜ ∩ {z : ℂ | z.im ≤ 0}
⊢ IsConnected ((σ ℂ a)ᶜ ∩ {z : ℂ | z.im ≤ 0})

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

Premises used: Complex.isConnected_of_lowerHalfPlane, Set.inter_subset_right
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
lower : {z : ℂ | z.im < 0} ⊆ (σ ℂ a)ᶜ ∩ {z : ℂ | z.im ≤ 0}
⊢ IsConnected ((σ ℂ a)ᶜ ∩ {z : ℂ | z.im ≤ 0})

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

Premises used: Complex.isConnected_of_lowerHalfPlane, Set.inter_subset_right
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
x : ℂ
⊢ Membership.mem (γ := Set ℂ) {z : ℂ | z.im < 0} x → Membership.mem (γ := Set ℂ) {z : ℂ | z.im ≤ 0} x

Tactic:
simpa using le_of_lt

Premises used: le_of_lt
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
lower : ∀ (z : ℂ) (hz : Membership.mem (γ := Set ℂ) {z : ℂ | z.im < 0} z) (hz' : z ∈ σ ℂ a), False
⊢ {z : ℂ | z.im < 0} ⊆ (σ ℂ a)ᶜ ∩ {z : ℂ | z.im ≤ 0}

Tactic:
refine Set.subset_inter (fun z hz hz' ↦ ?_) (fun _ ↦ by simpa using le_of_lt)
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | z.im < 0} z
hz' : z ∈ σ ℂ a
⊢ LT.lt (α := ℝ) 0 0

Tactic:
rw [Set.mem_setOf_eq, ha.im_eq_zero_of_mem_spectrum hz'] at hz

Premises used: Set.mem_setOf_eq, IsSelfAdjoint.im_eq_zero_of_mem_spectrum
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | z.im < 0} z
hz' : z ∈ σ ℂ a
hz₁ : LT.lt (α := ℝ) 0 0
⊢ z ∈ σ ℂ a

Tactic:
rw [Set.mem_setOf_eq, ha.im_eq_zero_of_mem_spectrum hz'] at hz

Premises used: Set.mem_setOf_eq, IsSelfAdjoint.im_eq_zero_of_mem_spectrum
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : LT.lt (α := ℝ) 0 0
hz' : z ∈ σ ℂ a
⊢ False

Tactic:
simp_all
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
x : ℂ
⊢ Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im} x → Membership.mem (γ := Set ℂ) {z : ℂ | 0 ≤ z.im} x

Tactic:
simpa using le_of_lt

Premises used: le_of_lt
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
upper : ∀ (z : ℂ) (hz : Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im} z) (hz' : z ∈ σ ℂ a), False
⊢ {z : ℂ | 0 < z.im} ⊆ (σ ℂ a)ᶜ ∩ {z : ℂ | 0 ≤ z.im}

Tactic:
refine Set.subset_inter (fun z hz hz' ↦ ?_) (fun _ ↦ by simpa using le_of_lt)
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im} z
hz' : z ∈ σ ℂ a
⊢ LT.lt (α := ℝ) 0 0

Tactic:
rw [Set.mem_setOf_eq, ha.im_eq_zero_of_mem_spectrum hz'] at hz

Premises used: Set.mem_setOf_eq, IsSelfAdjoint.im_eq_zero_of_mem_spectrum
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im} z
hz' : z ∈ σ ℂ a
hz₁ : LT.lt (α := ℝ) 0 0
⊢ z ∈ σ ℂ a

Tactic:
rw [Set.mem_setOf_eq, ha.im_eq_zero_of_mem_spectrum hz'] at hz

Premises used: Set.mem_setOf_eq, IsSelfAdjoint.im_eq_zero_of_mem_spectrum
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
a : ↥S
⊢ IsUnit (↑a : A) ↔ IsUnit a

Tactic:
⟨fun ha ↦ ?_, IsUnit.map S.subtype⟩

Premises used: StarSubalgebra.subtype, Iff.intro, IsUnit.map
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
a : ↥S
refine : ∀ (ha : IsUnit (↑a : A)), IsUnit a
⊢ IsUnit (↑a : A) ↔ IsUnit a

Tactic:
refine ⟨fun ha ↦ ?_, IsUnit.map S.subtype⟩
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
a : ↥S
ha : IsUnit (↑a : A)
⊢ IsUnit ((↑a : A)⋆ * (↑a : A))

Tactic:
have ha₁ := ha.star.mul ha
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
a : ↥S
ha : IsUnit (↑a : A)
ha₁ : IsUnit ((↑a : A)⋆ * (↑a : A))
⊢ IsUnit ((↑a : A) * (↑a : A)⋆)

Tactic:
have ha₂ := ha.mul ha.star
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
a : ↥S
ha : IsUnit (↑a : A)
ha₁ : IsUnit ((↑a : A)⋆ * (↑a : A))
ha₂ : IsUnit ((↑a : A) * (↑a : A)⋆)
⊢ ∀ {x : ↥S} (hx : IsSelfAdjoint x), σ ℂ x = σ ℂ (↑x : A)

Tactic:
have spec_eq {x : S} (hx : IsSelfAdjoint x) : spectrum ℂ x = spectrum ℂ (x : A) :=
    Subalgebra.spectrum_eq_of_isPreconnected_compl S _ <|
      (hx.map S.subtype).isConnected_spectrum_compl.isPreconnected
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
a : ↥S
ha : IsUnit (↑a : A)
ha₁ : IsUnit ((↑a : A)⋆ * (↑a : A))
ha₂ : IsUnit ((↑a : A) * (↑a : A)⋆)
spec_eq : ∀ {x : ↥S} (hx : IsSelfAdjoint x), σ ℂ x = σ ℂ (↑x : A)
rw :
  ∀ (ha₁ : IsUnit (a⋆ * a)) (ha₂ : IsUnit (a * a⋆)) (spec_eq : ∀ {x : ↥S} (hx : IsSelfAdjoint x), σ ℂ x = σ ℂ (↑x : A)),
    IsUnit a
rw₁ :
  ∀ (ha₁ : 0 ∉ σ ℂ (a⋆ * a)) (ha₂ : 0 ∉ σ ℂ (↑(a * a⋆) : A))
    (spec_eq : ∀ {x : ↥S} (hx : IsSelfAdjoint x), σ ℂ x = σ ℂ (↑x : A)), IsSelfAdjoint (a * a⋆)
rw₂ :
  ∀ (ha₁ : 0 ∉ σ ℂ (↑(a⋆ * a) : A)) (ha₂ : 0 ∉ σ ℂ (↑(a * a⋆) : A))
    (spec_eq : ∀ {x : ↥S} (hx : IsSelfAdjoint x), σ ℂ x = σ ℂ (↑x : A)), IsSelfAdjoint (a⋆ * a)
⊢ IsUnit a

Tactic:
rw [← StarMemClass.coe_star, ← MulMemClass.coe_mul, ← spectrum.zero_notMem_iff ℂ, ← spec_eq,
    spectrum.zero_notMem_iff] at ha₁ ha₂

Premises used: spectrum.zero_notMem_iff, StarMemClass.coe_star, MulMemClass.coe_mul, Complex
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
a : ↥S
ha : IsUnit (↑a : A)
ha₁ : IsUnit (a⋆ * a)
ha₂ : IsUnit (a * a⋆)
spec_eq : ∀ {x : ↥S} (hx : IsSelfAdjoint x), σ ℂ x = σ ℂ (↑x : A)
⊢ (↑ha₁.unit⁻¹ : ↥S) * a⋆ * a = 1

Tactic:
have h₁ : ha₁.unit⁻¹ * star a * a = 1 := mul_assoc _ _ a ▸ ha₁.val_inv_mul
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
a : ↥S
ha : IsUnit (↑a : A)
ha₁ : IsUnit (a⋆ * a)
ha₂ : IsUnit (a * a⋆)
spec_eq : ∀ {x : ↥S} (hx : IsSelfAdjoint x), σ ℂ x = σ ℂ (↑x : A)
h₁ : (↑ha₁.unit⁻¹ : ↥S) * a⋆ * a = 1
⊢ a * (a⋆ * (↑ha₂.unit⁻¹ : ↥S)) = 1

Tactic:
have h₂ : a * (star a * ha₂.unit⁻¹) = 1 := (mul_assoc a _ _).symm ▸ ha₂.mul_val_inv
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
a : ↥S
ha : IsUnit (↑a : A)
ha₁ : IsUnit (a⋆ * a)
ha₂ : IsUnit (a * a⋆)
spec_eq : ∀ {x : ↥S} (hx : IsSelfAdjoint x), σ ℂ x = σ ℂ (↑x : A)
h₁ : (↑ha₁.unit⁻¹ : ↥S) * a⋆ * a = 1
h₂ : a * (a⋆ * (↑ha₂.unit⁻¹ : ↥S)) = 1
⊢ IsUnit a

Tactic:
⟨⟨a, ha₁.unit⁻¹ * star a, left_inv_eq_right_inv h₁ h₂ ▸ h₂, h₁⟩, rfl⟩

Premises used: Units.val, HMul.hMul, IsUnit, Eq.rec, left_inv_eq_right_inv, Inv.inv, Units.mk, Exists.intro, IsUnit.unit, Eq.symm, rfl, Star.star
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
a : ↥S
ha : IsUnit (↑a : A)
ha₁ : IsUnit (a⋆ * a)
ha₂ : IsUnit (a * a⋆)
spec_eq : ∀ {x : ↥S} (hx : IsSelfAdjoint x), σ ℂ x = σ ℂ (↑x : A)
h₁ : (↑ha₁.unit⁻¹ : ↥S) * a⋆ * a = 1
h₂ : a * (a⋆ * (↑ha₂.unit⁻¹ : ↥S)) = 1
⊢ IsUnit a

Tactic:
exact ⟨⟨a, ha₁.unit⁻¹ * star a, left_inv_eq_right_inv h₁ h₂ ▸ h₂, h₁⟩, rfl⟩
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
a : ↥S
ha : IsUnit (↑a : A)
ha₁ : 0 ∉ σ ℂ (a⋆ * a)
ha₂ : 0 ∉ σ ℂ (↑(a * a⋆) : A)
spec_eq : ∀ {x : ↥S} (hx : IsSelfAdjoint x), σ ℂ x = σ ℂ (↑x : A)
⊢ IsSelfAdjoint (a * a⋆)

Tactic:
IsSelfAdjoint.mul_star_self a

Premises used: IsSelfAdjoint.mul_star_self
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
a : ↥S
ha : IsUnit (↑a : A)
ha₁ : 0 ∉ σ ℂ (a⋆ * a)
ha₂ : 0 ∉ σ ℂ (↑(a * a⋆) : A)
spec_eq : ∀ {x : ↥S} (hx : IsSelfAdjoint x), σ ℂ x = σ ℂ (↑x : A)
⊢ IsSelfAdjoint (a * a⋆)

Tactic:
exact IsSelfAdjoint.mul_star_self a

Premises used: IsSelfAdjoint.mul_star_self
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
a : ↥S
ha : IsUnit (↑a : A)
ha₁ : 0 ∉ σ ℂ (↑(a⋆ * a) : A)
ha₂ : 0 ∉ σ ℂ (↑(a * a⋆) : A)
spec_eq : ∀ {x : ↥S} (hx : IsSelfAdjoint x), σ ℂ x = σ ℂ (↑x : A)
⊢ IsSelfAdjoint (a⋆ * a)

Tactic:
IsSelfAdjoint.star_mul_self a

Premises used: IsSelfAdjoint.star_mul_self
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
a : ↥S
ha : IsUnit (↑a : A)
ha₁ : 0 ∉ σ ℂ (↑(a⋆ * a) : A)
ha₂ : 0 ∉ σ ℂ (↑(a * a⋆) : A)
spec_eq : ∀ {x : ↥S} (hx : IsSelfAdjoint x), σ ℂ x = σ ℂ (↑x : A)
⊢ IsSelfAdjoint (a⋆ * a)

Tactic:
exact IsSelfAdjoint.star_mul_self a

Premises used: IsSelfAdjoint.star_mul_self
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
a : ↥S
z : ℂ
⊢ z ∈ σ ℂ a ↔ z ∈ σ ℂ (↑a : A)

Tactic:
not_iff_not.mpr S.coe_isUnit.symm

Premises used: not_iff_not, Iff.mpr, spectrum, Set.Mem, setOf, StarSubalgebra.coe_isUnit, Not, Iff.symm
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
S : StarSubalgebra ℂ A
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
a : ↥S
⊢ σ ℂ a = σ ℂ (↑a : A)

Tactic:
Set.ext fun _ ↦ S.mem_spectrum_iff

Premises used: Set.ext, StarSubalgebra.mem_spectrum_iff
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : NonUnitalCStarAlgebra A
inst_1 : NonUnitalCStarAlgebra B
inst_2 : FunLike F A B
inst_3 : NonUnitalAlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
φ : F
a : A
ψ : StarAlgHom.{0, u_2, u_3} ℂ (Unitization ℂ A) (Unitization ℂ B)
x : Unitization ℂ A
this :
  ∀ {s : Unitization ℂ A},
    IsSelfAdjoint s →
      nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) s : Unitization ℂ B) ≤ ‖s‖₊
⊢ nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) x : Unitization ℂ B) ≤ ‖x‖₊

Tactic:
nonneg_le_nonneg_of_sq_le_sq zero_le' ?_

Premises used: nonneg_le_nonneg_of_sq_le_sq, zero_le'
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : NonUnitalCStarAlgebra A
inst_1 : NonUnitalCStarAlgebra B
inst_2 : FunLike F A B
inst_3 : NonUnitalAlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
φ : F
a : A
ψ : StarAlgHom.{0, u_2, u_3} ℂ (Unitization ℂ A) (Unitization ℂ B)
x : Unitization ℂ A
this :
  ∀ {s : Unitization ℂ A},
    IsSelfAdjoint s →
      nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) s : Unitization ℂ B) ≤ ‖s‖₊
refine :
  nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) x : Unitization ℂ B) *
      nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) x : Unitization ℂ B) ≤
    ‖x‖₊ * ‖x‖₊
⊢ nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) x : Unitization ℂ B) ≤ ‖x‖₊

Tactic:
refine nonneg_le_nonneg_of_sq_le_sq zero_le' ?_

Premises used: nonneg_le_nonneg_of_sq_le_sq, zero_le'
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : NonUnitalCStarAlgebra A
inst_1 : NonUnitalCStarAlgebra B
inst_2 : FunLike F A B
inst_3 : NonUnitalAlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
φ : F
a : A
ψ : StarAlgHom.{0, u_2, u_3} ℂ (Unitization ℂ A) (Unitization ℂ B)
x : Unitization ℂ A
this :
  ∀ {s : Unitization ℂ A},
    IsSelfAdjoint s →
      nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) s : Unitization ℂ B) ≤ ‖s‖₊
simp_rw :
  nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) (x⋆ * x) : Unitization ℂ B) ≤
    ‖x⋆ * x‖₊
⊢ nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) x : Unitization ℂ B) *
      nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) x : Unitization ℂ B) ≤
    ‖x‖₊ * ‖x‖₊

Tactic:
simp_rw [← nnnorm_star_mul_self, ← map_star, ← map_mul]

Premises used: StarHomClass.map_star, map_mul, CStarRing.nnnorm_star_mul_self
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : NonUnitalCStarAlgebra A
inst_1 : NonUnitalCStarAlgebra B
inst_2 : FunLike F A B
inst_3 : NonUnitalAlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
φ : F
a : A
ψ : StarAlgHom.{0, u_2, u_3} ℂ (Unitization ℂ A) (Unitization ℂ B)
x : Unitization ℂ A
this :
  ∀ {s : Unitization ℂ A},
    IsSelfAdjoint s →
      nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) s : Unitization ℂ B) ≤ ‖s‖₊
⊢ nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) (x⋆ * x) : Unitization ℂ B) ≤
    ‖x⋆ * x‖₊

Tactic:
this <| .star_mul_self x

Premises used: IsSelfAdjoint.star_mul_self
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : NonUnitalCStarAlgebra A
inst_1 : NonUnitalCStarAlgebra B
inst_2 : FunLike F A B
inst_3 : NonUnitalAlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
φ : F
a : A
ψ : StarAlgHom.{0, u_2, u_3} ℂ (Unitization ℂ A) (Unitization ℂ B)
x : Unitization ℂ A
this :
  ∀ {s : Unitization ℂ A},
    IsSelfAdjoint s →
      nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) s : Unitization ℂ B) ≤ ‖s‖₊
⊢ nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) (x⋆ * x) : Unitization ℂ B) ≤
    ‖x⋆ * x‖₊

Tactic:
exact this <| .star_mul_self x
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : NonUnitalCStarAlgebra A
inst_1 : NonUnitalCStarAlgebra B
inst_2 : FunLike F A B
inst_3 : NonUnitalAlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
φ : F
a : A
ψ : StarAlgHom.{0, u_2, u_3} ℂ (Unitization ℂ A) (Unitization ℂ B)
x : Unitization ℂ A
suffices :
  ∀ {s : Unitization ℂ A},
    IsSelfAdjoint s →
      nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) s : Unitization ℂ B) ≤ ‖s‖₊
⊢ nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) x : Unitization ℂ B) ≤ ‖x‖₊

Tactic:
suffices ∀ {s}, IsSelfAdjoint s → ‖ψ s‖₊ ≤ ‖s‖₊ by
      refine nonneg_le_nonneg_of_sq_le_sq zero_le' ?_
      simp_rw [← nnnorm_star_mul_self, ← map_star, ← map_mul]
      exact this <| .star_mul_self x
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : NonUnitalCStarAlgebra A
inst_1 : NonUnitalCStarAlgebra B
inst_2 : FunLike F A B
inst_3 : NonUnitalAlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
φ : F
a : A
ψ : StarAlgHom.{0, u_2, u_3} ℂ (Unitization ℂ A) (Unitization ℂ B)
x s : Unitization ℂ A
hs : IsSelfAdjoint s
this :
  spectralRadius.{0, u_3} ℂ (A := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) s : Unitization ℂ B) ≤
    spectralRadius ℂ s
rwa :
  ∀
    (this :
      (↑(nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) s : Unitization ℂ B)) :
          ℝ≥0∞) ≤
        spectralRadius ℂ s),
    nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) s : Unitization ℂ B) ≤ ‖s‖₊
rwa₁ :
  ∀
    (this :
      (↑(nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) s : Unitization ℂ B)) :
          ℝ≥0∞) ≤
        (↑‖s‖₊ : ℝ≥0∞)),
    nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) s : Unitization ℂ B) ≤ ‖s‖₊
rwa₂ rwa₃ rwa₄ rwa₅ :
  ∀
    (this :
      nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) s : Unitization ℂ B) ≤ ‖s‖₊),
    nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) s : Unitization ℂ B) ≤ ‖s‖₊
⊢ nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) s : Unitization ℂ B) ≤ ‖s‖₊

Tactic:
rwa [(hs.map ψ).spectralRadius_eq_nnnorm, hs.spectralRadius_eq_nnnorm, coe_le_coe]
        at this

Premises used: IsSelfAdjoint.map, ENNReal.coe_le_coe, IsSelfAdjoint.spectralRadius_eq_nnnorm
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : NonUnitalCStarAlgebra A
inst_1 : NonUnitalCStarAlgebra B
inst_2 : FunLike F A B
inst_3 : NonUnitalAlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
φ : F
a : A
ψ : StarAlgHom.{0, u_2, u_3} ℂ (Unitization ℂ A) (Unitization ℂ B)
x s : Unitization ℂ A
hs : IsSelfAdjoint s
suffices :
  spectralRadius.{0, u_3} ℂ (A := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) s : Unitization ℂ B) ≤
    spectralRadius ℂ s
⊢ nnnorm.{u_3} (E := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) s : Unitization ℂ B) ≤ ‖s‖₊

Tactic:
suffices this : spectralRadius ℂ (ψ s) ≤ spectralRadius ℂ s by
      rwa [(hs.map ψ).spectralRadius_eq_nnnorm, hs.spectralRadius_eq_nnnorm, coe_le_coe]
        at this
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : NonUnitalCStarAlgebra A
inst_1 : NonUnitalCStarAlgebra B
inst_2 : FunLike F A B
inst_3 : NonUnitalAlgHomClass F ℂ A B
inst_4 : StarHomClass F A B
φ : F
a : A
ψ : StarAlgHom.{0, u_2, u_3} ℂ (Unitization ℂ A) (Unitization ℂ B)
x s : Unitization ℂ A
hs : IsSelfAdjoint s
⊢ spectralRadius.{0, u_3} ℂ (A := Unitization ℂ B) ((ψ : (a : Unitization ℂ A) → Unitization ℂ B) s : Unitization ℂ B) ≤
    spectralRadius ℂ s

Tactic:
iSup_le_iSup_of_subset (AlgHom.spectrum_apply_subset ψ s)

Premises used: spectralRadius, AlgHom.spectrum_apply_subset, iSup_le_iSup_of_subset