-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
theorem cfcₙ_tsub {A : Type*} [TopologicalSpace A] [NonUnitalRing A] [PartialOrder A] [StarRing A]
    [StarOrderedRing A] [Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A]
    [IsTopologicalRing A] [T2Space A] [NonUnitalContinuousFunctionalCalculus ℝ
    (IsSelfAdjoint : A → Prop)] [NonnegSpectrumClass ℝ A] (f g : ℝ≥0 → ℝ≥0)
    (a : A) (hfg : ∀ x ∈ σₙ ℝ≥0 a, g x ≤ f x) (ha : 0 ≤ a

Proof state:
A : Type u_1
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : PartialOrder A
inst✝⁸ : StarRing A
inst✝⁷ : StarOrderedRing A
inst✝⁶ : Module ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsTopologicalRing A
inst✝² : T2Space A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ σₙ ℝ≥0 a, g x ≤ f x
ha : autoParam (0 ≤ a) _auto✝
hf : autoParam (ContinuousOn f (σₙ ℝ≥0 a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
hg : autoParam (ContinuousOn g (σₙ ℝ≥0 a)) _auto✝
hg0 : autoParam (g 0 = 0) _auto✝
ha' : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
this : Set.EqOn (fun x => ↑(f x.toNNReal - g x.toNNReal)) (fun x => ↑(f x.toNNReal) - ↑(g x.toNNReal)) (σₙ ℝ a)
⊢ ↑(f (Real.toNNReal 0)) = 0

Tactic:
simpa

Result:
no goals

Proof state:
case refine_2
A : Type u_1
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : PartialOrder A
inst✝⁸ : StarRing A
inst✝⁷ : StarOrderedRing A
inst✝⁶ : Module ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsTopologicalRing A
inst✝² : T2Space A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ σₙ ℝ≥0 a, g x ≤ f x
ha : autoParam (0 ≤ a) _auto✝
hf : autoParam (ContinuousOn f (σₙ ℝ≥0 a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
hg : autoParam (ContinuousOn g (σₙ ℝ≥0 a)) _auto✝
hg0 : autoParam (g 0 = 0) _auto✝
ha' : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
this : Set.EqOn (fun x => ↑(f x.toNNReal - g x.toNNReal)) (fun x => ↑(f x.toNNReal) - ↑(g x.toNNReal)) (σₙ ℝ a)
⊢ ContinuousOn (fun x => ↑(g 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✝¹¹ : TopologicalSpace A
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : PartialOrder A
inst✝⁸ : StarRing A
inst✝⁷ : StarOrderedRing A
inst✝⁶ : Module ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsTopologicalRing A
inst✝² : T2Space A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ σₙ ℝ≥0 a, g x ≤ f x
ha : autoParam (0 ≤ a) _auto✝
hf : autoParam (ContinuousOn f (σₙ ℝ≥0 a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
hg : autoParam (ContinuousOn g (σₙ ℝ≥0 a)) _auto✝
hg0 : autoParam (g 0 = 0) _auto✝
ha' : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
this : Set.EqOn (fun x => ↑(f x.toNNReal - g x.toNNReal)) (fun x => ↑(f x.toNNReal) - ↑(g x.toNNReal)) (σₙ ℝ 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

Tactic:
refine cfcₙ_sub _ _ a ?_ (by simpa) ?_

Result:
case refine_1
A : Type u_1
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : PartialOrder A
inst✝⁸ : StarRing A
inst✝⁷ : StarOrderedRing A
inst✝⁶ : Module ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsTopologicalRing A
inst✝² : T2Space A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ σₙ ℝ≥0 a, g x ≤ f x
ha : autoParam (0 ≤ a) _auto✝
hf : autoParam (ContinuousOn f (σₙ ℝ≥0 a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
hg : autoParam (ContinuousOn g (σₙ ℝ≥0 a)) _auto✝
hg0 : autoParam (g 0 = 0) _auto✝
ha' : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
this : Set.EqOn (fun x => ↑(f x.toNNReal - g x.toNNReal)) (fun x => ↑(f x.toNNReal) - ↑(g x.toNNReal)) (σₙ ℝ a)
⊢ ContinuousOn (fun x => ↑(f x.toNNReal)) (σₙ ℝ a)

case refine_2
A : Type u_1
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : PartialOrder A
inst✝⁸ : StarRing A
inst✝⁷ : StarOrderedRing A
inst✝⁶ : Module ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsTopologicalRing A
inst✝² : T2Space A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ σₙ ℝ≥0 a, g x ≤ f x
ha : autoParam (0 ≤ a) _auto✝
hf : autoParam (ContinuousOn f (σₙ ℝ≥0 a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
hg : autoParam (ContinuousOn g (σₙ ℝ≥0 a)) _auto✝
hg0 : autoParam (g 0 = 0) _auto✝
ha' : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
this : Set.EqOn (fun x => ↑(f x.toNNReal - g x.toNNReal)) (fun x => ↑(f x.toNNReal) - ↑(g x.toNNReal)) (σₙ ℝ a)
⊢ ContinuousOn (fun x => ↑(g x.toNNReal)) (σₙ ℝ a)

Proof state:
case refine_1
A : Type u_1
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : PartialOrder A
inst✝⁸ : StarRing A
inst✝⁷ : StarOrderedRing A
inst✝⁶ : Module ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsTopologicalRing A
inst✝² : T2Space A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ σₙ ℝ≥0 a, g x ≤ f x
ha : autoParam (0 ≤ a) _auto✝
hf : autoParam (ContinuousOn f (σₙ ℝ≥0 a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
hg : autoParam (ContinuousOn g (σₙ ℝ≥0 a)) _auto✝
hg0 : autoParam (g 0 = 0) _auto✝
ha' : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
this : Set.EqOn (fun x => ↑(f x.toNNReal - g x.toNNReal)) (fun x => ↑(f x.toNNReal) - ↑(g x.toNNReal)) (σₙ ℝ a)
⊢ ContinuousOn (fun x => ↑(f x.toNNReal)) (σₙ ℝ a)

case refine_2
A : Type u_1
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : PartialOrder A
inst✝⁸ : StarRing A
inst✝⁷ : StarOrderedRing A
inst✝⁶ : Module ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsTopologicalRing A
inst✝² : T2Space A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ σₙ ℝ≥0 a, g x ≤ f x
ha : autoParam (0 ≤ a) _auto✝
hf : autoParam (ContinuousOn f (σₙ ℝ≥0 a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
hg : autoParam (ContinuousOn g (σₙ ℝ≥0 a)) _auto✝
hg0 : autoParam (g 0 = 0) _auto✝
ha' : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
this : Set.EqOn (fun x => ↑(f x.toNNReal - g x.toNNReal)) (fun x => ↑(f x.toNNReal) - ↑(g x.toNNReal)) (σₙ ℝ a)
⊢ ContinuousOn (fun x => ↑(g x.toNNReal)) (σₙ ℝ a)

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

Result:
no goals