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

Tactic:
simp

Result:
no goals

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

Tactic:
constructor

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

case h.e'_3.h.mpr
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 ∈ (fun x => ‖↑(f x.toNNReal)‖₊) '' σ ℝ a → x ∈ f '' σ ℝ≥0 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✝
ha' : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
⊢ ContinuousOn (fun x => ↑(f x.toNNReal)) (σ ℝ a)

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

Result:
no goals

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✝
ha' : SpectrumRestricts 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✝⁷ : 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‖₊

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

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

Proof state:
case h.e'_3.h.mp
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

case h.e'_3.h.mpr
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 ∈ (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✝⁷ : 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

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

Proof state:
case h.e'_3.h.mpr
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 ∈ (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✝⁷ : 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