-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
/-- `cfc_le_iff` only applies to a scalar ring where `R` is an actual `Ring`, and not a `Semiring`.
However, this theorem still holds for `ℝ≥0` as long as the algebra `A` itself is an `ℝ`-algebra. -/
lemma cfc_nnreal_le_iff {A : Type*} [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A]
    [StarOrderedRing A] [Algebra ℝ A] [IsTopologicalRing A] [NonnegSpectrumClass ℝ A]
    [T2Space A] [ContinuousFunctionalCalculus ℝ (IsSelfAdjoint : A → Prop)]
    (f : ℝ≥0 → ℝ≥0) (g : ℝ≥0 → ℝ≥0) (a : A)
    (ha_spec : SpectrumRestricts a ContinuousMap.realToNNReal)
    (hf : ContinuousOn f (spectrum ℝ≥0 a)

Proof state:
A : Type u_1
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Ring A
inst✝⁷ : StarRing A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : IsTopologicalRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : T2Space A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
f g : ℝ≥0 → ℝ≥0
a : A
ha_spec : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
hf : autoParam (ContinuousOn f (spectrum ℝ≥0 a)) _auto✝
hg : autoParam (ContinuousOn g (spectrum ℝ≥0 a)) _auto✝
ha : autoParam (0 ≤ a) _auto✝
hf' : ContinuousOn (fun x => ↑(f x.toNNReal)) (spectrum ℝ a)
⊢ cfc f a ≤ cfc g a ↔ ∀ x ∈ spectrum ℝ≥0 a, f x ≤ g x

Tactic:
have hg' := hg.ofReal_map_toNNReal <| ha_spec.image ▸ Set.mapsTo_image ..

Result:
A : Type u_1
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Ring A
inst✝⁷ : StarRing A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : IsTopologicalRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : T2Space A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
f g : ℝ≥0 → ℝ≥0
a : A
ha_spec : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
hf : autoParam (ContinuousOn f (spectrum ℝ≥0 a)) _auto✝
hg : autoParam (ContinuousOn g (spectrum ℝ≥0 a)) _auto✝
ha : autoParam (0 ≤ a) _auto✝
hf' : ContinuousOn (fun x => ↑(f x.toNNReal)) (spectrum ℝ a)
hg' : ContinuousOn (fun x => ↑(g x.toNNReal)) (spectrum ℝ a)
⊢ cfc f a ≤ cfc g a ↔ ∀ x ∈ spectrum ℝ≥0 a, f x ≤ g x

Proof state:
A : Type u_1
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Ring A
inst✝⁷ : StarRing A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : IsTopologicalRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : T2Space A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
f g : ℝ≥0 → ℝ≥0
a : A
ha_spec : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
hf : autoParam (ContinuousOn f (spectrum ℝ≥0 a)) _auto✝
hg : autoParam (ContinuousOn g (spectrum ℝ≥0 a)) _auto✝
ha : autoParam (0 ≤ a) _auto✝
⊢ cfc f a ≤ cfc g a ↔ ∀ x ∈ spectrum ℝ≥0 a, f x ≤ g x

Tactic:
have hf' := hf.ofReal_map_toNNReal <| ha_spec.image ▸ Set.mapsTo_image ..

Result:
A : Type u_1
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Ring A
inst✝⁷ : StarRing A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : IsTopologicalRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : T2Space A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
f g : ℝ≥0 → ℝ≥0
a : A
ha_spec : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
hf : autoParam (ContinuousOn f (spectrum ℝ≥0 a)) _auto✝
hg : autoParam (ContinuousOn g (spectrum ℝ≥0 a)) _auto✝
ha : autoParam (0 ≤ a) _auto✝
hf' : ContinuousOn (fun x => ↑(f x.toNNReal)) (spectrum ℝ a)
⊢ cfc f a ≤ cfc g a ↔ ∀ x ∈ spectrum ℝ≥0 a, f x ≤ g x

Proof state:
A : Type u_1
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Ring A
inst✝⁷ : StarRing A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : IsTopologicalRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : T2Space A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
f g : ℝ≥0 → ℝ≥0
a : A
ha_spec : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
hf : autoParam (ContinuousOn f (spectrum ℝ≥0 a)) _auto✝
hg : autoParam (ContinuousOn g (spectrum ℝ≥0 a)) _auto✝
ha : autoParam (0 ≤ a) _auto✝
hf' : ContinuousOn (fun x => ↑(f x.toNNReal)) (spectrum ℝ a)
hg' : ContinuousOn (fun x => ↑(g x.toNNReal)) (spectrum ℝ a)
⊢ cfc f a ≤ cfc g a ↔ ∀ x ∈ spectrum ℝ≥0 a, f x ≤ g x

Tactic:
rw [cfc_nnreal_eq_real, cfc_nnreal_eq_real, cfc_le_iff ..]

Result:
A : Type u_1
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Ring A
inst✝⁷ : StarRing A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : IsTopologicalRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : T2Space A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
f g : ℝ≥0 → ℝ≥0
a : A
ha_spec : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
hf : autoParam (ContinuousOn f (spectrum ℝ≥0 a)) _auto✝
hg : autoParam (ContinuousOn g (spectrum ℝ≥0 a)) _auto✝
ha : autoParam (0 ≤ a) _auto✝
hf' : ContinuousOn (fun x => ↑(f x.toNNReal)) (spectrum ℝ a)
hg' : ContinuousOn (fun x => ↑(g x.toNNReal)) (spectrum ℝ a)
⊢ (∀ x ∈ spectrum ℝ a, ↑(f x.toNNReal) ≤ ↑(g x.toNNReal)) ↔ ∀ x ∈ spectrum ℝ≥0 a, f x ≤ g x

Proof state:
A : Type u_1
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Ring A
inst✝⁷ : StarRing A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : IsTopologicalRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : T2Space A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
f g : ℝ≥0 → ℝ≥0
a : A
ha_spec : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
hf : autoParam (ContinuousOn f (spectrum ℝ≥0 a)) _auto✝
hg : autoParam (ContinuousOn g (spectrum ℝ≥0 a)) _auto✝
ha : autoParam (0 ≤ a) _auto✝
hf' : ContinuousOn (fun x => ↑(f x.toNNReal)) (spectrum ℝ a)
hg' : ContinuousOn (fun x => ↑(g x.toNNReal)) (spectrum ℝ a)
⊢ (∀ x ∈ spectrum ℝ a, ↑(f x.toNNReal) ≤ ↑(g x.toNNReal)) ↔ ∀ x ∈ spectrum ℝ≥0 a, f x ≤ g x

Tactic:
simp [NNReal.coe_le_coe, ← ha_spec.image]

Result:
no goals