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

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
⊢ (fun x => ↑(f x.toNNReal)) 0 = 0

Tactic:
simpa

Result:
no goals

Proof state:
case h.e'_3
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
⊢ f '' σₙ ℝ≥0 a = (fun x => ‖↑(f x.toNNReal)‖₊) '' σₙ ℝ a

Tactic:
ext x

Result:
case h.e'_3.h
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

Proof state:
case h.e'_3
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
⊢ f '' σₙ ℝ≥0 a = (fun x => ‖↑(f x.toNNReal)‖₊) '' σₙ ℝ a

case hf_cont
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
⊢ ContinuousOn (fun x => ↑(f x.toNNReal)) (σₙ ℝ a)

Tactic:
case hf_cont => exact continuous_subtype_val.comp_continuousOn <|
  ContinuousOn.comp ‹_› continuous_real_toNNReal.continuousOn <| ha'.image ▸ Set.mapsTo_image ..

Result:
case h.e'_3
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
⊢ f '' σₙ ℝ≥0 a = (fun x => ‖↑(f x.toNNReal)‖₊) '' σₙ ℝ a

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ₙ f a‖₊

Tactic:
rw [cfcₙ_nnreal_eq_real]

Result:
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‖₊

Proof state:
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

Tactic:
exact ⟨x.toNNReal, ha'.apply_mem hx, by simp⟩

Result:
no goals

Proof state:
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‖₊

Tactic:
convert IsGreatest.nnnorm_cfcₙ (fun x : ℝ ↦ (f x.toNNReal : ℝ)) a ?hf_cont (by simpa)

Result:
case h.e'_3
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
⊢ f '' σₙ ℝ≥0 a = (fun x => ‖↑(f x.toNNReal)‖₊) '' σₙ ℝ a

case hf_cont
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
⊢ ContinuousOn (fun x => ↑(f x.toNNReal)) (σₙ ℝ a)