-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
theorem cfc_tsub {A : Type*} [TopologicalSpace A] [Ring A] [PartialOrder A] [StarRing A]
    [StarOrderedRing A] [Algebra ℝ A] [IsTopologicalRing A] [T2Space A]
    [ContinuousFunctionalCalculus ℝ (IsSelfAdjoint : A → Prop)]
    [NonnegSpectrumClass ℝ A] (f g : ℝ≥0 → ℝ≥0)
    (a : A) (hfg : ∀ x ∈ spectrum ℝ≥0 a, g x ≤ f x) (ha : 0 ≤ a

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

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

Tactic:
all_goals
  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✝⁹ : TopologicalSpace A
inst✝⁸ : Ring A
inst✝⁷ : PartialOrder A
inst✝⁶ : StarRing A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : IsTopologicalRing A
inst✝² : T2Space A
inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ spectrum ℝ≥0 a, g x ≤ f x
ha : autoParam (0 ≤ a) _auto✝
hf : autoParam (ContinuousOn f (spectrum ℝ≥0 a)) _auto✝
hg : autoParam (ContinuousOn g (spectrum ℝ≥0 a)) _auto✝
⊢ cfc (fun x => f x - g x) a = cfc f a - cfc g a

Tactic:
have ha' := SpectrumRestricts.nnreal_of_nonneg ha

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

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

Tactic:
have : (spectrum ℝ a).EqOn (fun x ↦ ((f x.toNNReal - g x.toNNReal : ℝ≥0) : ℝ))
    (fun x ↦ f x.toNNReal - g x.toNNReal) :=
  fun x hx ↦ NNReal.coe_sub <| hfg _ <| ha'.apply_mem hx

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

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

Tactic:
rw [cfc_nnreal_eq_real, cfc_nnreal_eq_real, cfc_nnreal_eq_real, cfc_congr this]

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

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

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

Result:
no goals