-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Basic.lean
theorem bijective_characterSpaceToSpectrum :
    Function.Bijective (characterSpaceToSpectrum a)

Proof state:
case refine_4.mk
A : Type u_1
inst✝¹ : CStarAlgebra A
a : A
inst✝ : IsStarNormal a
z : ℂ
hz : z ∈ spectrum ℂ a
hz' : z ∈ spectrum ℂ ⟨a, ⋯⟩
⊢ ∃ a_1, characterSpaceToSpectrum a a_1 = ⟨z, hz⟩

Tactic:
rw [CharacterSpace.mem_spectrum_iff_exists] at hz'

Result:
case refine_4.mk
A : Type u_1
inst✝¹ : CStarAlgebra A
a : A
inst✝ : IsStarNormal a
z : ℂ
hz : z ∈ spectrum ℂ a
hz' : ∃ f, f ⟨a, ⋯⟩ = z
⊢ ∃ a_1, characterSpaceToSpectrum a a_1 = ⟨z, hz⟩

Proof state:
case refine_4.mk
A : Type u_1
inst✝¹ : CStarAlgebra A
a : A
inst✝ : IsStarNormal a
z : ℂ
hz : z ∈ spectrum ℂ a
⊢ ∃ a_1, characterSpaceToSpectrum a a_1 = ⟨z, hz⟩

Tactic:
have hz' := (StarSubalgebra.spectrum_eq (hS := isClosed ℂ a)
  (a := ⟨a, self_mem ℂ a⟩) ▸ hz)

Result:
case refine_4.mk
A : Type u_1
inst✝¹ : CStarAlgebra A
a : A
inst✝ : IsStarNormal a
z : ℂ
hz : z ∈ spectrum ℂ a
hz' : z ∈ spectrum ℂ ⟨a, ⋯⟩
⊢ ∃ a_1, characterSpaceToSpectrum a a_1 = ⟨z, hz⟩

Proof state:
case refine_4.mk.intro
A : Type u_1
inst✝¹ : CStarAlgebra A
a : A
inst✝ : IsStarNormal a
φ : ↑(characterSpace ℂ ↥(elemental ℂ a))
hz : φ ⟨a, ⋯⟩ ∈ spectrum ℂ a
⊢ ∃ a_1, characterSpaceToSpectrum a a_1 = ⟨φ ⟨a, ⋯⟩, hz⟩

Tactic:
exact ⟨φ, rfl⟩

Result:
no goals

Proof state:
A : Type u_1
inst✝¹ : CStarAlgebra A
a : A
inst✝ : IsStarNormal a
⊢ Function.Bijective (characterSpaceToSpectrum a)

Tactic:
refine ⟨fun φ ψ h => starAlgHomClass_ext ℂ ?_ ?_ ?_, ?_⟩

Result:
case refine_1
A : Type u_1
inst✝¹ : CStarAlgebra A
a : A
inst✝ : IsStarNormal a
φ ψ : ↑(characterSpace ℂ ↥(elemental ℂ a))
h : characterSpaceToSpectrum a φ = characterSpaceToSpectrum a ψ
⊢ Continuous ⇑φ

case refine_2
A : Type u_1
inst✝¹ : CStarAlgebra A
a : A
inst✝ : IsStarNormal a
φ ψ : ↑(characterSpace ℂ ↥(elemental ℂ a))
h : characterSpaceToSpectrum a φ = characterSpaceToSpectrum a ψ
⊢ Continuous ⇑ψ

case refine_3
A : Type u_1
inst✝¹ : CStarAlgebra A
a : A
inst✝ : IsStarNormal a
φ ψ : ↑(characterSpace ℂ ↥(elemental ℂ a))
h : characterSpaceToSpectrum a φ = characterSpaceToSpectrum a ψ
⊢ φ ⟨a, ⋯⟩ = ψ ⟨a, ⋯⟩

case refine_4
A : Type u_1
inst✝¹ : CStarAlgebra A
a : A
inst✝ : IsStarNormal a
⊢ Function.Surjective (characterSpaceToSpectrum a)

Proof state:
case refine_1
A : Type u_1
inst✝¹ : CStarAlgebra A
a : A
inst✝ : IsStarNormal a
φ ψ : ↑(characterSpace ℂ ↥(elemental ℂ a))
h : characterSpaceToSpectrum a φ = characterSpaceToSpectrum a ψ
⊢ Continuous ⇑φ

Tactic:
exact (map_continuous φ)

Result:
no goals

Proof state:
case refine_2
A : Type u_1
inst✝¹ : CStarAlgebra A
a : A
inst✝ : IsStarNormal a
φ ψ : ↑(characterSpace ℂ ↥(elemental ℂ a))
h : characterSpaceToSpectrum a φ = characterSpaceToSpectrum a ψ
⊢ Continuous ⇑ψ

Tactic:
exact (map_continuous ψ)

Result:
no goals

Proof state:
case refine_4.mk
A : Type u_1
inst✝¹ : CStarAlgebra A
a : A
inst✝ : IsStarNormal a
z : ℂ
hz : z ∈ spectrum ℂ a
hz' : ∃ f, f ⟨a, ⋯⟩ = z
⊢ ∃ a_1, characterSpaceToSpectrum a a_1 = ⟨z, hz⟩

Tactic:
obtain ⟨φ, rfl⟩ := hz'

Result:
case refine_4.mk.intro
A : Type u_1
inst✝¹ : CStarAlgebra A
a : A
inst✝ : IsStarNormal a
φ : ↑(characterSpace ℂ ↥(elemental ℂ a))
hz : φ ⟨a, ⋯⟩ ∈ spectrum ℂ a
⊢ ∃ a_1, characterSpaceToSpectrum a a_1 = ⟨φ ⟨a, ⋯⟩, hz⟩

Proof state:
case refine_3
A : Type u_1
inst✝¹ : CStarAlgebra A
a : A
inst✝ : IsStarNormal a
φ ψ : ↑(characterSpace ℂ ↥(elemental ℂ a))
h : characterSpaceToSpectrum a φ = characterSpaceToSpectrum a ψ
⊢ φ ⟨a, ⋯⟩ = ψ ⟨a, ⋯⟩

Tactic:
simpa only [characterSpaceToSpectrum, Subtype.mk_eq_mk,
  ContinuousMap.coe_mk] using h

Result:
no goals

Proof state:
case refine_4
A : Type u_1
inst✝¹ : CStarAlgebra A
a : A
inst✝ : IsStarNormal a
⊢ Function.Surjective (characterSpaceToSpectrum a)

Tactic:
rintro ⟨z, hz⟩

Result:
case refine_4.mk
A : Type u_1
inst✝¹ : CStarAlgebra A
a : A
inst✝ : IsStarNormal a
z : ℂ
hz : z ∈ spectrum ℂ a
⊢ ∃ a_1, characterSpaceToSpectrum a a_1 = ⟨z, hz⟩