-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean
lemma IsGreatest.nnnorm_cfc_nnreal [Nontrivial A] (f : ℝ≥0 → ℝ≥0) (a : A)
    (hf : ContinuousOn f (σ ℝ≥0 a)

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

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

Result:
no goals

Proof state:
case h.e'_3.h.mpr.intro.intro
A : Type u_1
inst✝⁷ : NormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedAlgebra ℝ A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : Nontrivial A
f : ℝ≥0 → ℝ≥0
a : A
hf : autoParam (ContinuousOn f (σ ℝ≥0 a)) _auto✝
ha : autoParam (0 ≤ a) _auto✝
ha' : SpectrumRestricts 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 h.e'_3
A : Type u_1
inst✝⁷ : NormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedAlgebra ℝ A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : Nontrivial A
f : ℝ≥0 → ℝ≥0
a : A
hf : autoParam (ContinuousOn f (σ ℝ≥0 a)) _auto✝
ha : autoParam (0 ≤ a) _auto✝
ha' : SpectrumRestricts 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✝⁷ : NormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedAlgebra ℝ A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : Nontrivial A
f : ℝ≥0 → ℝ≥0
a : A
hf : autoParam (ContinuousOn f (σ ℝ≥0 a)) _auto✝
ha : autoParam (0 ≤ a) _auto✝
ha' : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
x : ℝ≥0
⊢ x ∈ f '' σ ℝ≥0 a ↔ x ∈ (fun x => ‖↑(f x.toNNReal)‖₊) '' σ ℝ a

Proof state:
case intro
A : Type u_1
inst✝⁷ : NormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedAlgebra ℝ A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : Nontrivial A
f : ℝ≥0 → ℝ≥0
a : A
hf : autoParam (ContinuousOn f (σ ℝ≥0 a)) _auto✝
ha : autoParam (0 ≤ a) _auto✝
ha' : SpectrumRestricts 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

Result:
case h.e'_3
A : Type u_1
inst✝⁷ : NormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedAlgebra ℝ A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : Nontrivial A
f : ℝ≥0 → ℝ≥0
a : A
hf : autoParam (ContinuousOn f (σ ℝ≥0 a)) _auto✝
ha : autoParam (0 ≤ a) _auto✝
ha' : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
⊢ f '' σ ℝ≥0 a = (fun x => ‖↑(f x.toNNReal)‖₊) '' σ ℝ a

case hf_cont
A : Type u_1
inst✝⁷ : NormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedAlgebra ℝ A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : Nontrivial A
f : ℝ≥0 → ℝ≥0
a : A
hf : autoParam (ContinuousOn f (σ ℝ≥0 a)) _auto✝
ha : autoParam (0 ≤ a) _auto✝
ha' : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
⊢ ContinuousOn (fun x => ↑(f x.toNNReal)) (σ ℝ a)

Proof state:
case h.e'_3
A : Type u_1
inst✝⁷ : NormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedAlgebra ℝ A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : Nontrivial A
f : ℝ≥0 → ℝ≥0
a : A
hf : autoParam (ContinuousOn f (σ ℝ≥0 a)) _auto✝
ha : autoParam (0 ≤ a) _auto✝
ha' : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
⊢ f '' σ ℝ≥0 a = (fun x => ‖↑(f x.toNNReal)‖₊) '' σ ℝ a

case hf_cont
A : Type u_1
inst✝⁷ : NormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedAlgebra ℝ A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : Nontrivial A
f : ℝ≥0 → ℝ≥0
a : A
hf : autoParam (ContinuousOn f (σ ℝ≥0 a)) _auto✝
ha : autoParam (0 ≤ a) _auto✝
ha' : SpectrumRestricts 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✝⁷ : NormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedAlgebra ℝ A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : Nontrivial A
f : ℝ≥0 → ℝ≥0
a : A
hf : autoParam (ContinuousOn f (σ ℝ≥0 a)) _auto✝
ha : autoParam (0 ≤ a) _auto✝
ha' : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
⊢ f '' σ ℝ≥0 a = (fun x => ‖↑(f x.toNNReal)‖₊) '' σ ℝ a

Proof state:
A : Type u_1
inst✝⁷ : NormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedAlgebra ℝ A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : Nontrivial A
f : ℝ≥0 → ℝ≥0
a : A
hf : autoParam (ContinuousOn f (σ ℝ≥0 a)) _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✝⁷ : NormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedAlgebra ℝ A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : Nontrivial A
f : ℝ≥0 → ℝ≥0
a : A
hf : autoParam (ContinuousOn f (σ ℝ≥0 a)) _auto✝
ha : autoParam (0 ≤ a) _auto✝
⊢ IsGreatest (f '' σ ℝ≥0 a) ‖cfc (fun x => ↑(f x.toNNReal)) a‖₊