-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean
lemma IsGreatest.nnnorm_cfcₙ_nnreal (f : ℝ≥0 → ℝ≥0) (a : A)
    (hf : ContinuousOn f (σₙ ℝ≥0 a)

Proof state:
case h.e'_3.h.mp
A : Type u_1
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
hf : autoParam (ContinuousOn f (σₙ ℝ≥0 a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
ha : autoParam (0 ≤ a) _auto✝
ha' : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
x : ℝ≥0
⊢ x ∈ f '' σₙ ℝ≥0 a → x ∈ (fun x => ‖↑(f x.toNNReal)‖₊) '' σₙ ℝ a

case h.e'_3.h.mpr
A : Type u_1
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
hf : autoParam (ContinuousOn f (σₙ ℝ≥0 a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
ha : autoParam (0 ≤ a) _auto✝
ha' : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
x : ℝ≥0
⊢ x ∈ (fun x => ‖↑(f x.toNNReal)‖₊) '' σₙ ℝ a → x ∈ f '' σₙ ℝ≥0 a

Tactic:
all_goals rintro ⟨x, hx, rfl⟩

Result:
case h.e'_3.h.mp.intro.intro
A : Type u_1
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
hf : autoParam (ContinuousOn f (σₙ ℝ≥0 a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
ha : autoParam (0 ≤ a) _auto✝
ha' : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
x : ℝ≥0
hx : x ∈ σₙ ℝ≥0 a
⊢ f x ∈ (fun x => ‖↑(f x.toNNReal)‖₊) '' σₙ ℝ a

case h.e'_3.h.mpr.intro.intro
A : Type u_1
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
hf : autoParam (ContinuousOn f (σₙ ℝ≥0 a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
ha : autoParam (0 ≤ a) _auto✝
ha' : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
x : ℝ
hx : x ∈ σₙ ℝ a
⊢ (fun x => ‖↑(f x.toNNReal)‖₊) x ∈ f '' σₙ ℝ≥0 a

Proof state:
case h.e'_3.h.mpr
A : Type u_1
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
hf : autoParam (ContinuousOn f (σₙ ℝ≥0 a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
ha : autoParam (0 ≤ a) _auto✝
ha' : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
x : ℝ≥0
⊢ x ∈ (fun x => ‖↑(f x.toNNReal)‖₊) '' σₙ ℝ a → x ∈ f '' σₙ ℝ≥0 a

Tactic:
rintro ⟨x, hx, rfl⟩

Result:
case h.e'_3.h.mpr.intro.intro
A : Type u_1
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
hf : autoParam (ContinuousOn f (σₙ ℝ≥0 a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
ha : autoParam (0 ≤ a) _auto✝
ha' : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
x : ℝ
hx : x ∈ σₙ ℝ a
⊢ (fun x => ‖↑(f x.toNNReal)‖₊) x ∈ f '' σₙ ℝ≥0 a

Proof state:
case h.e'_3.h.mp.intro.intro
A : Type u_1
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
hf : autoParam (ContinuousOn f (σₙ ℝ≥0 a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
ha : autoParam (0 ≤ a) _auto✝
ha' : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
x : ℝ≥0
hx : x ∈ σₙ ℝ≥0 a
⊢ f x ∈ (fun x => ‖↑(f x.toNNReal)‖₊) '' σₙ ℝ a

Tactic:
exact ⟨x, quasispectrum.algebraMap_mem ℝ hx, by simp⟩

Result:
no goals

Proof state:
A : Type u_1
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
hf : autoParam (ContinuousOn f (σₙ ℝ≥0 a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
ha : autoParam (0 ≤ a) _auto✝
ha' : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
x : ℝ
hx : x ∈ σₙ ℝ a
⊢ f x.toNNReal = (fun x => ‖↑(f x.toNNReal)‖₊) x

Tactic:
simp

Result:
no goals

Proof state:
A : Type u_1
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
hf : autoParam (ContinuousOn f (σₙ ℝ≥0 a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
ha : autoParam (0 ≤ a) _auto✝
ha' : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
x : ℝ≥0
hx : x ∈ σₙ ℝ≥0 a
⊢ (fun x => ‖↑(f x.toNNReal)‖₊) ↑x = f x

Tactic:
simp

Result:
no goals

Proof state:
A : Type u_1
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
hf : autoParam (ContinuousOn f (σₙ ℝ≥0 a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
ha : autoParam (0 ≤ a) _auto✝
⊢ IsGreatest (f '' σₙ ℝ≥0 a) ‖cfcₙ (fun x => ↑(f x.toNNReal)) a‖₊

Tactic:
obtain ⟨-, ha'⟩ := nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts.mp ha

Result:
case intro
A : Type u_1
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
hf : autoParam (ContinuousOn f (σₙ ℝ≥0 a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
ha : autoParam (0 ≤ a) _auto✝
ha' : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
⊢ IsGreatest (f '' σₙ ℝ≥0 a) ‖cfcₙ (fun x => ↑(f x.toNNReal)) a‖₊