awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ClosedEmbeddingContinuousFunctionalCalculus R A p
inst_10 : ContinuousMapZero.UniqueHom R A
inst_11 : CompleteSpace R
a : A
ha : p a
⊢ IsClosedEmbedding.{u_1, u_2} (X := C((↑(σₙ R a) : Type u_1), R)₀) (Y := A)
    (⇑(cfcₙHom_of_cfcHom R (p := p) ha) : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)

Tactic:
exact isClosedEmbedding_cfcₙHom_of_cfcHom ha

Premises used: isClosedEmbedding_cfcₙHom_of_cfcHom
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : PartialOrder A
inst_3 : StarRing A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : IsTopologicalRing A
inst_7 : T2Space A
inst_8 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ spectrum ℝ≥0 a, g x ≤ f x
ha : 0 ≤ a
hf : ContinuousOn f (spectrum ℝ≥0 a)
hg : ContinuousOn g (spectrum ℝ≥0 a)
⊢ SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)

Tactic:
have ha' := SpectrumRestricts.nnreal_of_nonneg ha
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : PartialOrder A
inst_3 : StarRing A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : IsTopologicalRing A
inst_7 : T2Space A
inst_8 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ spectrum ℝ≥0 a, g x ≤ f x
ha : 0 ≤ a
hf : ContinuousOn f (spectrum ℝ≥0 a)
hg : ContinuousOn g (spectrum ℝ≥0 a)
ha' : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ Set.EqOn (β := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal - g x.toNNReal) : ℝ))
    (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ) - (↑(g x.toNNReal) : ℝ)) (spectrum ℝ 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
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : PartialOrder A
inst_3 : StarRing A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : IsTopologicalRing A
inst_7 : T2Space A
inst_8 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ spectrum ℝ≥0 a, g x ≤ f x
ha : 0 ≤ a
hf : ContinuousOn f (spectrum ℝ≥0 a)
hg : ContinuousOn g (spectrum ℝ≥0 a)
ha' : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
this :
  Set.EqOn (β := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal - g x.toNNReal) : ℝ))
    (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ) - (↑(g x.toNNReal) : ℝ)) (spectrum ℝ a)
rw :
  cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ) - (↑(g x.toNNReal) : ℝ)) a =
    cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) a -
      cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(g x.toNNReal) : ℝ)) a
⊢ cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ f x - g x) a =
    cfc (p := fun (x : A) ↦ 0 ≤ x) f a - cfc (p := fun (x : A) ↦ 0 ≤ x) g a

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

Premises used: cfc_nnreal_eq_real, cfc_congr
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : PartialOrder A
inst_3 : StarRing A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : IsTopologicalRing A
inst_7 : T2Space A
inst_8 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ spectrum ℝ≥0 a, g x ≤ f x
ha : 0 ≤ a
hf : ContinuousOn f (spectrum ℝ≥0 a)
hg : ContinuousOn g (spectrum ℝ≥0 a)
ha' : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
this :
  Set.EqOn (β := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal - g x.toNNReal) : ℝ))
    (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ) - (↑(g x.toNNReal) : ℝ)) (spectrum ℝ a)
⊢ cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ) - (↑(g x.toNNReal) : ℝ)) a =
    cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) a -
      cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(g x.toNNReal) : ℝ)) a

Tactic:
cfc_sub _ _ a ?_ ?_

Premises used: cfc_sub
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : PartialOrder A
inst_3 : StarRing A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : IsTopologicalRing A
inst_7 : T2Space A
inst_8 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ spectrum ℝ≥0 a, g x ≤ f x
ha : 0 ≤ a
hf : ContinuousOn f (spectrum ℝ≥0 a)
hg : ContinuousOn g (spectrum ℝ≥0 a)
ha' : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
this :
  Set.EqOn (β := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal - g x.toNNReal) : ℝ))
    (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ) - (↑(g x.toNNReal) : ℝ)) (spectrum ℝ a)
refine_1 : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) (spectrum ℝ a)
refine_2 : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (↑(g x.toNNReal) : ℝ)) (spectrum ℝ a)
⊢ cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ) - (↑(g x.toNNReal) : ℝ)) a =
    cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) a -
      cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(g x.toNNReal) : ℝ)) a

Tactic:
refine cfc_sub _ _ a ?_ ?_

Premises used: cfc_sub
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : PartialOrder A
inst_3 : StarRing A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : IsTopologicalRing A
inst_7 : T2Space A
inst_8 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ spectrum ℝ≥0 a, g x ≤ f x
ha : 0 ≤ a
hf : ContinuousOn f (spectrum ℝ≥0 a)
hg : ContinuousOn g (spectrum ℝ≥0 a)
ha' : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
this :
  Set.EqOn (β := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal - g x.toNNReal) : ℝ))
    (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ) - (↑(g x.toNNReal) : ℝ)) (spectrum ℝ a)
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) (spectrum ℝ a)

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

Premises used: Continuous.continuousOn, continuous_subtype_val, Continuous.comp_continuousOn, ContinuousOn.comp, continuous_real_toNNReal, NNReal.toReal
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : PartialOrder A
inst_3 : StarRing A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : IsTopologicalRing A
inst_7 : T2Space A
inst_8 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ spectrum ℝ≥0 a, g x ≤ f x
ha : 0 ≤ a
hf : ContinuousOn f (spectrum ℝ≥0 a)
hg : ContinuousOn g (spectrum ℝ≥0 a)
ha' : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
this :
  Set.EqOn (β := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal - g x.toNNReal) : ℝ))
    (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ) - (↑(g x.toNNReal) : ℝ)) (spectrum ℝ a)
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) (spectrum ℝ a)

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

Premises used: Continuous.continuousOn, continuous_subtype_val, Continuous.comp_continuousOn, ContinuousOn.comp, continuous_real_toNNReal
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : PartialOrder A
inst_3 : StarRing A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : IsTopologicalRing A
inst_7 : T2Space A
inst_8 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ spectrum ℝ≥0 a, g x ≤ f x
ha : 0 ≤ a
hf : ContinuousOn f (spectrum ℝ≥0 a)
hg : ContinuousOn g (spectrum ℝ≥0 a)
ha' : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
this :
  Set.EqOn (β := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal - g x.toNNReal) : ℝ))
    (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ) - (↑(g x.toNNReal) : ℝ)) (spectrum ℝ a)
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (↑(g x.toNNReal) : ℝ)) (spectrum ℝ a)

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

Premises used: Continuous.continuousOn, continuous_subtype_val, Continuous.comp_continuousOn, ContinuousOn.comp, continuous_real_toNNReal, NNReal.toReal
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : PartialOrder A
inst_3 : StarRing A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : IsTopologicalRing A
inst_7 : T2Space A
inst_8 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ spectrum ℝ≥0 a, g x ≤ f x
ha : 0 ≤ a
hf : ContinuousOn f (spectrum ℝ≥0 a)
hg : ContinuousOn g (spectrum ℝ≥0 a)
ha' : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
this :
  Set.EqOn (β := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal - g x.toNNReal) : ℝ))
    (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ) - (↑(g x.toNNReal) : ℝ)) (spectrum ℝ a)
⊢ ContinuousOn (Y := ℝ) (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 ..

Premises used: Continuous.continuousOn, continuous_subtype_val, Continuous.comp_continuousOn, ContinuousOn.comp, continuous_real_toNNReal
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : PartialOrder A
inst_3 : StarRing A
inst_4 : StarOrderedRing A
inst_5 : Module ℝ A
inst_6 : IsScalarTower ℝ A A
inst_7 : SMulCommClass ℝ A A
inst_8 : IsTopologicalRing A
inst_9 : T2Space A
inst_10 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_11 : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ σₙ ℝ≥0 a, g x ≤ f x
ha : 0 ≤ a
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 : f 0 = 0
hg : ContinuousOn g (σₙ ℝ≥0 a)
hg0 : g 0 = 0
⊢ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)

Tactic:
have ha' := QuasispectrumRestricts.nnreal_of_nonneg ha
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : PartialOrder A
inst_3 : StarRing A
inst_4 : StarOrderedRing A
inst_5 : Module ℝ A
inst_6 : IsScalarTower ℝ A A
inst_7 : SMulCommClass ℝ A A
inst_8 : IsTopologicalRing A
inst_9 : T2Space A
inst_10 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_11 : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ σₙ ℝ≥0 a, g x ≤ f x
ha : 0 ≤ a
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 : f 0 = 0
hg : ContinuousOn g (σₙ ℝ≥0 a)
hg0 : g 0 = 0
ha' : QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ Set.EqOn (β := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal - g x.toNNReal) : ℝ))
    (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ) - (↑(g x.toNNReal) : ℝ)) (σₙ ℝ a)

Tactic:
have : (σₙ ℝ 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
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : PartialOrder A
inst_3 : StarRing A
inst_4 : StarOrderedRing A
inst_5 : Module ℝ A
inst_6 : IsScalarTower ℝ A A
inst_7 : SMulCommClass ℝ A A
inst_8 : IsTopologicalRing A
inst_9 : T2Space A
inst_10 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_11 : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ σₙ ℝ≥0 a, g x ≤ f x
ha : 0 ≤ a
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 : f 0 = 0
hg : ContinuousOn g (σₙ ℝ≥0 a)
hg0 : g 0 = 0
ha' : QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
this :
  Set.EqOn (β := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal - g x.toNNReal) : ℝ))
    (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ) - (↑(g x.toNNReal) : ℝ)) (σₙ ℝ a)
rw :
  cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ) - (↑(g x.toNNReal) : ℝ)) a =
    cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) a -
      cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(g x.toNNReal) : ℝ)) a
⊢ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ f x - g x) a =
    cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f a - cfcₙ (p := fun (x : A) ↦ 0 ≤ x) g a

Tactic:
rw [cfcₙ_nnreal_eq_real .., cfcₙ_nnreal_eq_real .., cfcₙ_nnreal_eq_real .., cfcₙ_congr this]

Premises used: cfcₙ_congr, cfcₙ_nnreal_eq_real
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : PartialOrder A
inst_3 : StarRing A
inst_4 : StarOrderedRing A
inst_5 : Module ℝ A
inst_6 : IsScalarTower ℝ A A
inst_7 : SMulCommClass ℝ A A
inst_8 : IsTopologicalRing A
inst_9 : T2Space A
inst_10 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_11 : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ σₙ ℝ≥0 a, g x ≤ f x
ha : 0 ≤ a
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 : f 0 = 0
hg : ContinuousOn g (σₙ ℝ≥0 a)
hg0 : g 0 = 0
ha' : QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
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
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : PartialOrder A
inst_3 : StarRing A
inst_4 : StarOrderedRing A
inst_5 : Module ℝ A
inst_6 : IsScalarTower ℝ A A
inst_7 : SMulCommClass ℝ A A
inst_8 : IsTopologicalRing A
inst_9 : T2Space A
inst_10 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_11 : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ σₙ ℝ≥0 a, g x ≤ f x
ha : 0 ≤ a
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 : f 0 = 0
hg : ContinuousOn g (σₙ ℝ≥0 a)
hg0 : g 0 = 0
ha' : QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
this :
  Set.EqOn (β := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal - g x.toNNReal) : ℝ))
    (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ) - (↑(g x.toNNReal) : ℝ)) (σₙ ℝ a)
refine_1 : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) (σₙ ℝ a)
refine_2 : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (↑(g x.toNNReal) : ℝ)) (σₙ ℝ a)
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ) - (↑(g x.toNNReal) : ℝ)) a =
    cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) a -
      cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(g x.toNNReal) : ℝ)) a

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

Premises used: cfcₙ_sub
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : PartialOrder A
inst_3 : StarRing A
inst_4 : StarOrderedRing A
inst_5 : Module ℝ A
inst_6 : IsScalarTower ℝ A A
inst_7 : SMulCommClass ℝ A A
inst_8 : IsTopologicalRing A
inst_9 : T2Space A
inst_10 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_11 : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ σₙ ℝ≥0 a, g x ≤ f x
ha : 0 ≤ a
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 : f 0 = 0
hg : ContinuousOn g (σₙ ℝ≥0 a)
hg0 : g 0 = 0
ha' : QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
this :
  Set.EqOn (β := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal - g x.toNNReal) : ℝ))
    (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ) - (↑(g x.toNNReal) : ℝ)) (σₙ ℝ a)
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) (σₙ ℝ a)

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

Premises used: Continuous.continuousOn, continuous_subtype_val, Continuous.comp_continuousOn, ContinuousOn.comp, continuous_real_toNNReal, NNReal.toReal
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : PartialOrder A
inst_3 : StarRing A
inst_4 : StarOrderedRing A
inst_5 : Module ℝ A
inst_6 : IsScalarTower ℝ A A
inst_7 : SMulCommClass ℝ A A
inst_8 : IsTopologicalRing A
inst_9 : T2Space A
inst_10 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_11 : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ σₙ ℝ≥0 a, g x ≤ f x
ha : 0 ≤ a
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 : f 0 = 0
hg : ContinuousOn g (σₙ ℝ≥0 a)
hg0 : g 0 = 0
ha' : QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
this :
  Set.EqOn (β := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal - g x.toNNReal) : ℝ))
    (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ) - (↑(g x.toNNReal) : ℝ)) (σₙ ℝ a)
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) (σₙ ℝ a)

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

Premises used: Continuous.continuousOn, continuous_subtype_val, Continuous.comp_continuousOn, ContinuousOn.comp, continuous_real_toNNReal
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : PartialOrder A
inst_3 : StarRing A
inst_4 : StarOrderedRing A
inst_5 : Module ℝ A
inst_6 : IsScalarTower ℝ A A
inst_7 : SMulCommClass ℝ A A
inst_8 : IsTopologicalRing A
inst_9 : T2Space A
inst_10 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_11 : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ σₙ ℝ≥0 a, g x ≤ f x
ha : 0 ≤ a
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 : f 0 = 0
hg : ContinuousOn g (σₙ ℝ≥0 a)
hg0 : g 0 = 0
ha' : QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
this :
  Set.EqOn (β := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal - g x.toNNReal) : ℝ))
    (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ) - (↑(g x.toNNReal) : ℝ)) (σₙ ℝ a)
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (↑(g x.toNNReal) : ℝ)) (σₙ ℝ a)

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

Premises used: Continuous.continuousOn, continuous_subtype_val, Continuous.comp_continuousOn, ContinuousOn.comp, continuous_real_toNNReal, NNReal.toReal
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : PartialOrder A
inst_3 : StarRing A
inst_4 : StarOrderedRing A
inst_5 : Module ℝ A
inst_6 : IsScalarTower ℝ A A
inst_7 : SMulCommClass ℝ A A
inst_8 : IsTopologicalRing A
inst_9 : T2Space A
inst_10 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_11 : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ σₙ ℝ≥0 a, g x ≤ f x
ha : 0 ≤ a
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 : f 0 = 0
hg : ContinuousOn g (σₙ ℝ≥0 a)
hg0 : g 0 = 0
ha' : QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
this :
  Set.EqOn (β := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal - g x.toNNReal) : ℝ))
    (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ) - (↑(g x.toNNReal) : ℝ)) (σₙ ℝ a)
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (↑(g x.toNNReal) : ℝ)) (σₙ ℝ a)

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

Premises used: Continuous.continuousOn, continuous_subtype_val, Continuous.comp_continuousOn, ContinuousOn.comp, continuous_real_toNNReal
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
⊢ StarOrderedRing.{u_1} (Unitization ℂ A)

Tactic:
CStarAlgebra.spectralOrderedRing _

Premises used: CStarAlgebra.spectralOrderedRing
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
ha : IsSelfAdjoint a
hb : IsSelfAdjoint b
rw : (∀ x ∈ σₙ ℝ (b - a), 0 ≤ x) ↔ 0 ≤ b - a
⊢ LE.le (α := Unitization ℂ A) (↑a : Unitization ℂ A) (↑b : Unitization ℂ A) ↔ a ≤ b

Tactic:
rw [← sub_nonneg, ← sub_nonneg (a := b), StarOrderedRing.nonneg_iff_spectrum_nonneg (R := ℝ) _,
    ← inr_sub ℂ b a, ← Unitization.quasispectrum_eq_spectrum_inr' ℝ ℂ]

Premises used: Real, Unitization.inr_sub, Unitization.quasispectrum_eq_spectrum_inr', StarOrderedRing.nonneg_iff_spectrum_nonneg, Complex, sub_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
ha : IsSelfAdjoint a
hb : IsSelfAdjoint b
⊢ (∀ x ∈ σₙ ℝ (b - a), 0 ≤ x) ↔ 0 ≤ b - a

Tactic:
StarOrderedRing.nonneg_iff_quasispectrum_nonneg _ |>.symm

Premises used: StarOrderedRing.nonneg_iff_quasispectrum_nonneg, Iff.symm
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
ha : IsSelfAdjoint a
hb : IsSelfAdjoint b
⊢ (∀ x ∈ σₙ ℝ (b - a), 0 ≤ x) ↔ 0 ≤ b - a

Tactic:
exact StarOrderedRing.nonneg_iff_quasispectrum_nonneg _ |>.symm

Premises used: StarOrderedRing.nonneg_iff_quasispectrum_nonneg, Iff.symm
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
pos : ∀ (ha : IsSelfAdjoint a), LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A) ↔ 0 ≤ a
neg : ∀ (ha : ¬IsSelfAdjoint a), LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A) ↔ 0 ≤ a
⊢ LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A) ↔ 0 ≤ a

Tactic:
by_cases ha : IsSelfAdjoint a

Premises used: IsSelfAdjoint
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
⊢ LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A) ↔ 0 ≤ a

Tactic:
inr_zero ℂ (A := A) ▸ inr_le_iff 0 a

Premises used: Unitization.inr_le_iff, Eq.rec, Unitization.inr_zero, Complex, OfNat.ofNat
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
⊢ LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A) ↔ 0 ≤ a

Tactic:
exact inr_zero ℂ (A := A) ▸ inr_le_iff 0 a
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : ¬IsSelfAdjoint a
⊢ LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A) ↔ 0 ≤ a

Tactic:
⟨?_, ?_⟩

Premises used: Iff.intro