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

Proof state:
case refine_2.intro
A : Type u_1
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ IsStarNormal
a : A
ha₁ : IsStarNormal a
ha₂ : QuasispectrumRestricts 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✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ IsStarNormal
a : A
ha₁ : IsStarNormal a
ha₂ : QuasispectrumRestricts a ⇑Complex.reCLM
⊢ cfcₙ (fun x => star x) a = cfcₙ id a

Proof state:
case refine_2.intro
A : Type u_1
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ IsStarNormal
a : A
ha₁ : IsStarNormal a
ha₂ : QuasispectrumRestricts 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✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ IsStarNormal
a : A
ha₁ : IsStarNormal a
ha₂ : QuasispectrumRestricts 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✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ IsStarNormal
a : A
ha₁ : IsStarNormal a
ha₂ : QuasispectrumRestricts 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✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ IsStarNormal
a : A
ha₁ : IsStarNormal a
ha₂ : QuasispectrumRestricts a ⇑Complex.reCLM
⊢ star a = cfcₙ id a

Proof state:
case refine_1
A : Type u_1
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ 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:
case refine_1
A : Type u_1
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ 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✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ 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:
A : Type u_1
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ IsStarNormal
a : A
⊢ IsSelfAdjoint a ↔ IsStarNormal a ∧ QuasispectrumRestricts a ⇑Complex.reCLM

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

Result:
case refine_1
A : Type u_1
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ 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✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ IsStarNormal
a : A
⊢ IsStarNormal a ∧ QuasispectrumRestricts a ⇑Complex.reCLM → IsSelfAdjoint a

Proof state:
case refine_2.intro
A : Type u_1
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ IsStarNormal
a : A
ha₁ : IsStarNormal a
ha₂ : QuasispectrumRestricts a ⇑Complex.reCLM
⊢ IsSelfAdjoint a

Tactic:
rw [isSelfAdjoint_iff]

Result:
case refine_2.intro
A : Type u_1
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ IsStarNormal
a : A
ha₁ : IsStarNormal a
ha₂ : QuasispectrumRestricts a ⇑Complex.reCLM
⊢ star a = a

Proof state:
case refine_2.intro.intro.intro
A : Type u_1
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ IsStarNormal
a : A
ha₁ : IsStarNormal a
ha₂ : QuasispectrumRestricts a ⇑Complex.reCLM
x : ℝ
hx : (algebraMap ℝ ℂ) x ∈ σₙ ℂ a
⊢ star ((algebraMap ℝ ℂ) x) = id ((algebraMap ℝ ℂ) x)

Tactic:
exact Complex.conj_ofReal _

Result:
no goals

Proof state:
A : Type u_1
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ 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✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ IsStarNormal
a : A
ha₁ : IsStarNormal a
ha₂ : QuasispectrumRestricts 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✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ IsStarNormal
a : A
ha₁ : IsStarNormal a
ha₂ : QuasispectrumRestricts a ⇑Complex.reCLM
x : ℂ
hx : x ∈ σₙ ℂ a
⊢ star x = id x