-- Mathlib/Analysis/CStarAlgebra/Spectrum.lean
/-- For a unital C⋆-subalgebra `S` of `A` and `x : S`, if `↑x : A` is invertible in `A`, then
`x` is invertible in `S`. -/
lemma coe_isUnit {a : S} : IsUnit (a : A) ↔ IsUnit a

Proof state:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
S : StarSubalgebra ℂ A
hS : IsClosed ↑S
a : ↥S
ha : IsUnit ↑a
ha₁ : IsUnit (a⋆ * a)
ha₂ : IsUnit (a * a⋆)
spec_eq : ∀ {x : ↥S}, IsSelfAdjoint x → σ ℂ x = σ ℂ ↑x
h₁ : ↑ha₁.unit⁻¹ * a⋆ * a = 1
h₂ : a * (a⋆ * ↑ha₂.unit⁻¹) = 1
⊢ IsUnit a

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

Result:
no goals

Proof state:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
S : StarSubalgebra ℂ A
hS : IsClosed ↑S
a : ↥S
ha : IsUnit ↑a
ha₁ : 0 ∉ σ ℂ ↑(a⋆ * a)
ha₂ : 0 ∉ σ ℂ ↑(a * a⋆)
spec_eq : ∀ {x : ↥S}, IsSelfAdjoint x → σ ℂ x = σ ℂ ↑x
⊢ IsSelfAdjoint (a⋆ * a)

Tactic:
exact IsSelfAdjoint.star_mul_self a

Result:
no goals

Proof state:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
S : StarSubalgebra ℂ A
hS : IsClosed ↑S
a : ↥S
ha : IsUnit ↑a
ha₁ : IsUnit ((↑a)⋆ * ↑a)
⊢ IsUnit a

Tactic:
have ha₂ := ha.mul ha.star

Result:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
S : StarSubalgebra ℂ A
hS : IsClosed ↑S
a : ↥S
ha : IsUnit ↑a
ha₁ : IsUnit ((↑a)⋆ * ↑a)
ha₂ : IsUnit (↑a * (↑a)⋆)
⊢ IsUnit a

Proof state:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
S : StarSubalgebra ℂ A
hS : IsClosed ↑S
a : ↥S
ha : IsUnit ↑a
⊢ IsUnit a

Tactic:
have ha₁ := ha.star.mul ha

Result:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
S : StarSubalgebra ℂ A
hS : IsClosed ↑S
a : ↥S
ha : IsUnit ↑a
ha₁ : IsUnit ((↑a)⋆ * ↑a)
⊢ IsUnit a

Proof state:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
S : StarSubalgebra ℂ A
hS : IsClosed ↑S
a : ↥S
ha : IsUnit ↑a
ha₁ : IsUnit (a⋆ * a)
ha₂ : IsUnit (a * a⋆)
spec_eq : ∀ {x : ↥S}, IsSelfAdjoint x → σ ℂ x = σ ℂ ↑x
⊢ IsUnit a

Tactic:
have h₁ : ha₁.unit⁻¹ * star a * a = 1 := mul_assoc _ _ a ▸ ha₁.val_inv_mul

Result:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
S : StarSubalgebra ℂ A
hS : IsClosed ↑S
a : ↥S
ha : IsUnit ↑a
ha₁ : IsUnit (a⋆ * a)
ha₂ : IsUnit (a * a⋆)
spec_eq : ∀ {x : ↥S}, IsSelfAdjoint x → σ ℂ x = σ ℂ ↑x
h₁ : ↑ha₁.unit⁻¹ * a⋆ * a = 1
⊢ IsUnit a

Proof state:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
S : StarSubalgebra ℂ A
hS : IsClosed ↑S
a : ↥S
ha : IsUnit ↑a
ha₁ : IsUnit ((↑a)⋆ * ↑a)
ha₂ : IsUnit (↑a * (↑a)⋆)
⊢ IsUnit 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

Result:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
S : StarSubalgebra ℂ A
hS : IsClosed ↑S
a : ↥S
ha : IsUnit ↑a
ha₁ : IsUnit ((↑a)⋆ * ↑a)
ha₂ : IsUnit (↑a * (↑a)⋆)
spec_eq : ∀ {x : ↥S}, IsSelfAdjoint x → σ ℂ x = σ ℂ ↑x
⊢ IsUnit a

Proof state:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
S : StarSubalgebra ℂ A
hS : IsClosed ↑S
a : ↥S
⊢ IsUnit ↑a ↔ IsUnit a

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

Result:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
S : StarSubalgebra ℂ A
hS : IsClosed ↑S
a : ↥S
ha : IsUnit ↑a
⊢ IsUnit a

Proof state:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
S : StarSubalgebra ℂ A
hS : IsClosed ↑S
a : ↥S
ha : IsUnit ↑a
ha₁ : 0 ∉ σ ℂ (a⋆ * a)
ha₂ : 0 ∉ σ ℂ ↑(a * a⋆)
spec_eq : ∀ {x : ↥S}, IsSelfAdjoint x → σ ℂ x = σ ℂ ↑x
⊢ IsSelfAdjoint (a * a⋆)

Tactic:
exact IsSelfAdjoint.mul_star_self a

Result:
no goals

Proof state:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
S : StarSubalgebra ℂ A
hS : IsClosed ↑S
a : ↥S
ha : IsUnit ↑a
ha₁ : IsUnit ((↑a)⋆ * ↑a)
ha₂ : IsUnit (↑a * (↑a)⋆)
spec_eq : ∀ {x : ↥S}, IsSelfAdjoint x → σ ℂ x = σ ℂ ↑x
⊢ IsUnit a

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

Result:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
S : StarSubalgebra ℂ A
hS : IsClosed ↑S
a : ↥S
ha : IsUnit ↑a
ha₁ : IsUnit (a⋆ * a)
ha₂ : IsUnit (a * a⋆)
spec_eq : ∀ {x : ↥S}, IsSelfAdjoint x → σ ℂ x = σ ℂ ↑x
⊢ IsUnit a

A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
S : StarSubalgebra ℂ A
hS : IsClosed ↑S
a : ↥S
ha : IsUnit ↑a
ha₁ : 0 ∉ σ ℂ (a⋆ * a)
ha₂ : 0 ∉ σ ℂ ↑(a * a⋆)
spec_eq : ∀ {x : ↥S}, IsSelfAdjoint x → σ ℂ x = σ ℂ ↑x
⊢ IsSelfAdjoint (a * a⋆)

A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
S : StarSubalgebra ℂ A
hS : IsClosed ↑S
a : ↥S
ha : IsUnit ↑a
ha₁ : 0 ∉ σ ℂ ↑(a⋆ * a)
ha₂ : 0 ∉ σ ℂ ↑(a * a⋆)
spec_eq : ∀ {x : ↥S}, IsSelfAdjoint x → σ ℂ x = σ ℂ ↑x
⊢ IsSelfAdjoint (a⋆ * a)

Proof state:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
S : StarSubalgebra ℂ A
hS : IsClosed ↑S
a : ↥S
ha : IsUnit ↑a
ha₁ : IsUnit (a⋆ * a)
ha₂ : IsUnit (a * a⋆)
spec_eq : ∀ {x : ↥S}, IsSelfAdjoint x → σ ℂ x = σ ℂ ↑x
h₁ : ↑ha₁.unit⁻¹ * a⋆ * a = 1
⊢ IsUnit a

Tactic:
have h₂ : a * (star a * ha₂.unit⁻¹) = 1 := (mul_assoc a _ _).symm ▸ ha₂.mul_val_inv

Result:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
S : StarSubalgebra ℂ A
hS : IsClosed ↑S
a : ↥S
ha : IsUnit ↑a
ha₁ : IsUnit (a⋆ * a)
ha₂ : IsUnit (a * a⋆)
spec_eq : ∀ {x : ↥S}, IsSelfAdjoint x → σ ℂ x = σ ℂ ↑x
h₁ : ↑ha₁.unit⁻¹ * a⋆ * a = 1
h₂ : a * (a⋆ * ↑ha₂.unit⁻¹) = 1
⊢ IsUnit a