-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Basic.lean
lemma SpectrumRestricts.nnreal_iff_nnnorm {a : A} {t : ℝ≥0} (ha : IsSelfAdjoint a) (ht : ‖a‖₊ ≤ t) :
    SpectrumRestricts a ContinuousMap.realToNNReal ↔ ‖algebraMap ℝ A t - a‖₊ ≤ t

Proof state:
A : Type u_2
inst✝ : CStarAlgebra A
a : A
t : ℝ≥0
ha : IsSelfAdjoint a
ht : spectralRadius ℝ a ≤ ↑t
this : IsSelfAdjoint ((algebraMap ℝ A) ↑t - a)
⊢ SpectrumRestricts ((algebraMap ℝ A) ↑t - a) ⇑Complex.reCLM

A : Type u_2
inst✝ : CStarAlgebra A
a : A
t : ℝ≥0
ha : IsSelfAdjoint a
ht : spectralRadius ℂ a ≤ ↑t
this : IsSelfAdjoint ((algebraMap ℝ A) ↑t - a)
⊢ SpectrumRestricts a ⇑Complex.reCLM

A : Type u_2
inst✝ : CStarAlgebra A
a : A
t : ℝ≥0
ha : IsSelfAdjoint a
ht : spectralRadius ℂ a ≤ ↑t
this : IsSelfAdjoint ((algebraMap ℝ A) ↑t - a)
⊢ IsSelfAdjoint ((algebraMap ℝ A) ↑t - a)

A : Type u_2
inst✝ : CStarAlgebra A
a : A
t : ℝ≥0
ha : IsSelfAdjoint a
ht : ↑‖a‖₊ ≤ ↑t
this : IsSelfAdjoint ((algebraMap ℝ A) ↑t - a)
⊢ IsSelfAdjoint a

Tactic:
all_goals
  try apply IsSelfAdjoint.spectrumRestricts
  assumption

Result:
no goals

Proof state:
A : Type u_2
inst✝ : CStarAlgebra A
a : A
t : ℝ≥0
ha : IsSelfAdjoint a
ht : ‖a‖₊ ≤ t
⊢ SpectrumRestricts a ⇑ContinuousMap.realToNNReal ↔ ‖(algebraMap ℝ A) ↑t - a‖₊ ≤ t

Tactic:
have : IsSelfAdjoint (algebraMap ℝ A t - a) := IsSelfAdjoint.algebraMap A (.all (t : ℝ)) |>.sub ha

Result:
A : Type u_2
inst✝ : CStarAlgebra A
a : A
t : ℝ≥0
ha : IsSelfAdjoint a
ht : ‖a‖₊ ≤ t
this : IsSelfAdjoint ((algebraMap ℝ A) ↑t - a)
⊢ SpectrumRestricts a ⇑ContinuousMap.realToNNReal ↔ ‖(algebraMap ℝ A) ↑t - a‖₊ ≤ t

Proof state:
A : Type u_2
inst✝ : CStarAlgebra A
a : A
t : ℝ≥0
ha : IsSelfAdjoint a
ht : ‖a‖₊ ≤ t
this : IsSelfAdjoint ((algebraMap ℝ A) ↑t - a)
⊢ SpectrumRestricts a ⇑ContinuousMap.realToNNReal ↔ ‖(algebraMap ℝ A) ↑t - a‖₊ ≤ t

Tactic:
rw [← ENNReal.coe_le_coe, ← IsSelfAdjoint.spectralRadius_eq_nnnorm,
  ← SpectrumRestricts.spectralRadius_eq (f := Complex.reCLM)] at ht ⊢

Result:
A : Type u_2
inst✝ : CStarAlgebra A
a : A
t : ℝ≥0
ha : IsSelfAdjoint a
ht : spectralRadius ℝ a ≤ ↑t
this : IsSelfAdjoint ((algebraMap ℝ A) ↑t - a)
⊢ SpectrumRestricts a ⇑ContinuousMap.realToNNReal ↔ spectralRadius ℝ ((algebraMap ℝ A) ↑t - a) ≤ ↑t

A : Type u_2
inst✝ : CStarAlgebra A
a : A
t : ℝ≥0
ha : IsSelfAdjoint a
ht : spectralRadius ℝ a ≤ ↑t
this : IsSelfAdjoint ((algebraMap ℝ A) ↑t - a)
⊢ SpectrumRestricts ((algebraMap ℝ A) ↑t - a) ⇑Complex.reCLM

A : Type u_2
inst✝ : CStarAlgebra A
a : A
t : ℝ≥0
ha : IsSelfAdjoint a
ht : spectralRadius ℂ a ≤ ↑t
this : IsSelfAdjoint ((algebraMap ℝ A) ↑t - a)
⊢ SpectrumRestricts a ⇑Complex.reCLM

A : Type u_2
inst✝ : CStarAlgebra A
a : A
t : ℝ≥0
ha : IsSelfAdjoint a
ht : spectralRadius ℂ a ≤ ↑t
this : IsSelfAdjoint ((algebraMap ℝ A) ↑t - a)
⊢ IsSelfAdjoint ((algebraMap ℝ A) ↑t - a)

A : Type u_2
inst✝ : CStarAlgebra A
a : A
t : ℝ≥0
ha : IsSelfAdjoint a
ht : ↑‖a‖₊ ≤ ↑t
this : IsSelfAdjoint ((algebraMap ℝ A) ↑t - a)
⊢ IsSelfAdjoint a

Proof state:
A : Type u_2
inst✝ : CStarAlgebra A
a : A
t : ℝ≥0
ha : IsSelfAdjoint a
ht : spectralRadius ℂ a ≤ ↑t
this : IsSelfAdjoint ((algebraMap ℝ A) ↑t - a)
⊢ SpectrumRestricts a ⇑Complex.reCLM

Tactic:
try apply IsSelfAdjoint.spectrumRestricts

Result:
case ha
A : Type u_2
inst✝ : CStarAlgebra A
a : A
t : ℝ≥0
ha : IsSelfAdjoint a
ht : spectralRadius ℂ a ≤ ↑t
this : IsSelfAdjoint ((algebraMap ℝ A) ↑t - a)
⊢ IsSelfAdjoint a

Proof state:
A : Type u_2
inst✝ : CStarAlgebra A
a : A
t : ℝ≥0
ha : IsSelfAdjoint a
ht : spectralRadius ℝ a ≤ ↑t
this : IsSelfAdjoint ((algebraMap ℝ A) ↑t - a)
⊢ SpectrumRestricts a ⇑ContinuousMap.realToNNReal ↔ spectralRadius ℝ ((algebraMap ℝ A) ↑t - a) ≤ ↑t

Tactic:
exact SpectrumRestricts.nnreal_iff_spectralRadius_le ht

Result:
no goals

Proof state:
A : Type u_2
inst✝ : CStarAlgebra A
a : A
t : ℝ≥0
ha : IsSelfAdjoint a
ht : spectralRadius ℂ a ≤ ↑t
this : IsSelfAdjoint ((algebraMap ℝ A) ↑t - a)
⊢ SpectrumRestricts a ⇑Complex.reCLM

Tactic:
apply IsSelfAdjoint.spectrumRestricts

Result:
case ha
A : Type u_2
inst✝ : CStarAlgebra A
a : A
t : ℝ≥0
ha : IsSelfAdjoint a
ht : spectralRadius ℂ a ≤ ↑t
this : IsSelfAdjoint ((algebraMap ℝ A) ↑t - a)
⊢ IsSelfAdjoint a

Proof state:
A : Type u_2
inst✝ : CStarAlgebra A
a : A
t : ℝ≥0
ha : IsSelfAdjoint a
ht : ↑‖a‖₊ ≤ ↑t
this : IsSelfAdjoint ((algebraMap ℝ A) ↑t - a)
⊢ IsSelfAdjoint a

Tactic:
assumption

Result:
no goals