-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean
/-- An element in a C⋆-algebra is selfadjoint if and only if it is normal and its spectrum is
contained in `ℝ`. -/
lemma isSelfAdjoint_iff_isStarNormal_and_spectrumRestricts {a : A} :
    IsSelfAdjoint a ↔ IsStarNormal a ∧ SpectrumRestricts a Complex.reCLM

Proof state:
case refine_2.intro
A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra ℂ A
inst✝ : ContinuousFunctionalCalculus ℂ IsStarNormal
a : A
ha₁ : IsStarNormal a
ha₂ : SpectrumRestricts a ⇑Complex.reCLM
⊢ IsSelfAdjoint a

Tactic:
rw [isSelfAdjoint_iff]

Result:
case refine_2.intro
A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra ℂ A
inst✝ : ContinuousFunctionalCalculus ℂ IsStarNormal
a : A
ha₁ : IsStarNormal a
ha₂ : SpectrumRestricts a ⇑Complex.reCLM
⊢ star a = a

Proof state:
case refine_1
A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra ℂ A
inst✝ : ContinuousFunctionalCalculus ℂ IsStarNormal
a : A
ha : IsSelfAdjoint a
x : ℂ
hx : x ∈ σ ℂ a
⊢ (algebraMap ℝ ℂ) (Complex.reCLM x) = x

Tactic:
have := eqOn_of_cfc_eq_cfc <| (cfc_star (id : ℂ → ℂ) a).symm ▸ (cfc_id ℂ a).symm ▸ ha.star_eq

Result:
case refine_1
A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra ℂ A
inst✝ : ContinuousFunctionalCalculus ℂ IsStarNormal
a : A
ha : IsSelfAdjoint a
x : ℂ
hx : x ∈ σ ℂ a
this : Set.EqOn (fun x => star (id x)) id (σ ℂ a)
⊢ (algebraMap ℝ ℂ) (Complex.reCLM x) = x

Proof state:
case refine_1
A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra ℂ A
inst✝ : ContinuousFunctionalCalculus ℂ IsStarNormal
a : A
ha : IsSelfAdjoint a
x : ℂ
hx : x ∈ σ ℂ a
this : Set.EqOn (fun x => star (id x)) id (σ ℂ a)
⊢ (algebraMap ℝ ℂ) (Complex.reCLM x) = x

Tactic:
exact Complex.conj_eq_iff_re.mp (by simpa using this hx)

Result:
no goals

Proof state:
A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra ℂ A
inst✝ : ContinuousFunctionalCalculus ℂ IsStarNormal
a : A
ha : IsSelfAdjoint a
x : ℂ
hx : x ∈ σ ℂ a
this : Set.EqOn (fun x => star (id x)) id (σ ℂ a)
⊢ (starRingEnd ℂ) x = x

Tactic:
simpa using this hx

Result:
no goals

Proof state:
case refine_2.intro
A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra ℂ A
inst✝ : ContinuousFunctionalCalculus ℂ IsStarNormal
a : A
ha₁ : IsStarNormal a
ha₂ : SpectrumRestricts a ⇑Complex.reCLM
x : ℂ
hx : x ∈ σ ℂ a
⊢ star x = id x

Tactic:
obtain ⟨x, -, rfl⟩ := ha₂.algebraMap_image.symm ▸ hx

Result:
case refine_2.intro.intro.intro
A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra ℂ A
inst✝ : ContinuousFunctionalCalculus ℂ IsStarNormal
a : A
ha₁ : IsStarNormal a
ha₂ : SpectrumRestricts a ⇑Complex.reCLM
x : ℝ
hx : (algebraMap ℝ ℂ) x ∈ σ ℂ a
⊢ star ((algebraMap ℝ ℂ) x) = id ((algebraMap ℝ ℂ) x)

Proof state:
case refine_2.intro
A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra ℂ A
inst✝ : ContinuousFunctionalCalculus ℂ IsStarNormal
a : A
ha₁ : IsStarNormal a
ha₂ : SpectrumRestricts a ⇑Complex.reCLM
⊢ star a = a

Tactic:
nth_rw 2 [← cfc_id ℂ a]

Result:
case refine_2.intro
A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra ℂ A
inst✝ : ContinuousFunctionalCalculus ℂ IsStarNormal
a : A
ha₁ : IsStarNormal a
ha₂ : SpectrumRestricts a ⇑Complex.reCLM
⊢ star a = cfc id a

Proof state:
case refine_2
A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra ℂ A
inst✝ : ContinuousFunctionalCalculus ℂ IsStarNormal
a : A
⊢ IsStarNormal a ∧ SpectrumRestricts a ⇑Complex.reCLM → IsSelfAdjoint a

Tactic:
rintro ⟨ha₁, ha₂⟩

Result:
case refine_2.intro
A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra ℂ A
inst✝ : ContinuousFunctionalCalculus ℂ IsStarNormal
a : A
ha₁ : IsStarNormal a
ha₂ : SpectrumRestricts a ⇑Complex.reCLM
⊢ IsSelfAdjoint a

Proof state:
case refine_2.intro.intro.intro
A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra ℂ A
inst✝ : ContinuousFunctionalCalculus ℂ IsStarNormal
a : A
ha₁ : IsStarNormal a
ha₂ : SpectrumRestricts a ⇑Complex.reCLM
x : ℝ
hx : (algebraMap ℝ ℂ) x ∈ σ ℂ a
⊢ star ((algebraMap ℝ ℂ) x) = id ((algebraMap ℝ ℂ) x)

Tactic:
exact Complex.conj_ofReal _

Result:
no goals

Proof state:
case refine_2.intro
A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra ℂ A
inst✝ : ContinuousFunctionalCalculus ℂ IsStarNormal
a : A
ha₁ : IsStarNormal a
ha₂ : SpectrumRestricts a ⇑Complex.reCLM
⊢ cfc (fun x => star x) a = cfc id a

Tactic:
refine cfc_congr fun x hx ↦ ?_

Result:
case refine_2.intro
A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra ℂ A
inst✝ : ContinuousFunctionalCalculus ℂ IsStarNormal
a : A
ha₁ : IsStarNormal a
ha₂ : SpectrumRestricts a ⇑Complex.reCLM
x : ℂ
hx : x ∈ σ ℂ a
⊢ star x = id x

Proof state:
A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra ℂ A
inst✝ : ContinuousFunctionalCalculus ℂ IsStarNormal
a : A
⊢ IsSelfAdjoint a ↔ IsStarNormal a ∧ SpectrumRestricts a ⇑Complex.reCLM

Tactic:
refine ⟨fun ha ↦ ⟨ha.isStarNormal, .of_rightInvOn Complex.ofReal_re fun x hx ↦ ?_⟩, ?_⟩

Result:
case refine_1
A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra ℂ A
inst✝ : ContinuousFunctionalCalculus ℂ IsStarNormal
a : A
ha : IsSelfAdjoint a
x : ℂ
hx : x ∈ σ ℂ a
⊢ (algebraMap ℝ ℂ) (Complex.reCLM x) = x

case refine_2
A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra ℂ A
inst✝ : ContinuousFunctionalCalculus ℂ IsStarNormal
a : A
⊢ IsStarNormal a ∧ SpectrumRestricts a ⇑Complex.reCLM → IsSelfAdjoint a

Proof state:
case refine_2.intro
A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra ℂ A
inst✝ : ContinuousFunctionalCalculus ℂ IsStarNormal
a : A
ha₁ : IsStarNormal a
ha₂ : SpectrumRestricts a ⇑Complex.reCLM
⊢ star a = cfc id a

Tactic:
rw [← cfc_star_id a (R := ℂ)]

Result:
case refine_2.intro
A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra ℂ A
inst✝ : ContinuousFunctionalCalculus ℂ IsStarNormal
a : A
ha₁ : IsStarNormal a
ha₂ : SpectrumRestricts a ⇑Complex.reCLM
⊢ cfc (fun x => star x) a = cfc id a