-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean
lemma CFC.exists_sqrt_of_isSelfAdjoint_of_spectrumRestricts {A : Type*} [Ring A] [StarRing A]
    [TopologicalSpace A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ (IsSelfAdjoint : A → Prop)]
    {a : A} (ha₁ : IsSelfAdjoint a) (ha₂ : SpectrumRestricts a ContinuousMap.realToNNReal) :
    ∃ x : A, IsSelfAdjoint x ∧ SpectrumRestricts x ContinuousMap.realToNNReal ∧ x ^ 2 = a

Proof state:
A : Type u_1
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
a : A
ha₁ : IsSelfAdjoint a
ha₂ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
x : ℝ
hx : x ∈ σ ℝ a
⊢ √x ^ 2 = id x

Tactic:
rw [SpectrumRestricts.nnreal_iff] at ha₂

Result:
A : Type u_1
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
a : A
ha₁ : IsSelfAdjoint a
ha₂ : ∀ x ∈ σ ℝ a, 0 ≤ x
x : ℝ
hx : x ∈ σ ℝ a
⊢ √x ^ 2 = id x

Proof state:
A : Type u_1
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
a : A
ha₁ : IsSelfAdjoint a
ha₂ : ∀ x ∈ σ ℝ a, 0 ≤ x
x : ℝ
hx : x ∈ σ ℝ a
⊢ √x ^ 2 = id x

Tactic:
apply ha₂ x at hx

Result:
A : Type u_1
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
a : A
ha₁ : IsSelfAdjoint a
ha₂ : ∀ x ∈ σ ℝ a, 0 ≤ x
x : ℝ
hx : 0 ≤ x
⊢ √x ^ 2 = id x

Proof state:
case right.right
A : Type u_1
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
a : A
ha₁ : IsSelfAdjoint a
ha₂ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
⊢ cfc (fun x => √x ^ 2) a = a

Tactic:
nth_rw 2 [← cfc_id ℝ a]

Result:
case right.right
A : Type u_1
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
a : A
ha₁ : IsSelfAdjoint a
ha₂ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
⊢ cfc (fun x => √x ^ 2) a = cfc id a

Proof state:
case right.right
A : Type u_1
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
a : A
ha₁ : IsSelfAdjoint a
ha₂ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
⊢ cfc (fun x => √x ^ 2) a = cfc id a

Tactic:
apply cfc_congr fun x hx ↦ ?_

Result:
A : Type u_1
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
a : A
ha₁ : IsSelfAdjoint a
ha₂ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
x : ℝ
hx : x ∈ σ ℝ a
⊢ √x ^ 2 = id x

Proof state:
case right.left
A : Type u_1
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
a : A
ha₁ : IsSelfAdjoint a
ha₂ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
⊢ SpectrumRestricts (cfc Real.sqrt a) ⇑ContinuousMap.realToNNReal

Tactic:
simpa only [SpectrumRestricts.nnreal_iff, cfc_map_spectrum Real.sqrt a, Set.mem_image,
  forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] using fun x _ ↦ Real.sqrt_nonneg x

Result:
no goals

Proof state:
A : Type u_1
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
a : A
ha₁ : IsSelfAdjoint a
ha₂ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
⊢ ∃ x, IsSelfAdjoint x ∧ SpectrumRestricts x ⇑ContinuousMap.realToNNReal ∧ x ^ 2 = a

Tactic:
use cfc Real.sqrt a, cfc_predicate Real.sqrt a

Result:
case right
A : Type u_1
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
a : A
ha₁ : IsSelfAdjoint a
ha₂ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
⊢ SpectrumRestricts (cfc Real.sqrt a) ⇑ContinuousMap.realToNNReal ∧ cfc Real.sqrt a ^ 2 = a

Proof state:
case right
A : Type u_1
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
a : A
ha₁ : IsSelfAdjoint a
ha₂ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
⊢ SpectrumRestricts (cfc Real.sqrt a) ⇑ContinuousMap.realToNNReal ∧ cfc Real.sqrt a ^ 2 = a

Tactic:
constructor

Result:
case right.left
A : Type u_1
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
a : A
ha₁ : IsSelfAdjoint a
ha₂ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
⊢ SpectrumRestricts (cfc Real.sqrt a) ⇑ContinuousMap.realToNNReal

case right.right
A : Type u_1
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
a : A
ha₁ : IsSelfAdjoint a
ha₂ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
⊢ cfc Real.sqrt a ^ 2 = a

Proof state:
case right.right
A : Type u_1
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
a : A
ha₁ : IsSelfAdjoint a
ha₂ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
⊢ cfc Real.sqrt a ^ 2 = a

Tactic:
rw [← cfc_pow ..]

Result:
case right.right
A : Type u_1
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
a : A
ha₁ : IsSelfAdjoint a
ha₂ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
⊢ cfc (fun x => √x ^ 2) a = a

Proof state:
A : Type u_1
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
a : A
ha₁ : IsSelfAdjoint a
ha₂ : ∀ x ∈ σ ℝ a, 0 ≤ x
x : ℝ
hx : 0 ≤ x
⊢ √x ^ 2 = id x

Tactic:
simp [Real.sq_sqrt hx]

Result:
no goals