awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
neg : LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A) → 0 ≤ a
neg₁ : 0 ≤ a → LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A)
⊢ LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A) ↔ 0 ≤ a

Tactic:
refine ⟨?_, ?_⟩
-- 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:
fun h ↦ (ha ?_).elim

Premises used: False.elim
-- 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
neg : ∀ (h : LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A)), IsSelfAdjoint a
⊢ LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A) → 0 ≤ a

Tactic:
refine fun h ↦ (ha ?_).elim

Premises used: False.elim
-- 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
⊢ 0 ≤ a → LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A)

Tactic:
fun h ↦ (ha ?_).elim

Premises used: False.elim
-- 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
neg : ∀ (h : 0 ≤ a), IsSelfAdjoint a
⊢ 0 ≤ a → LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A)

Tactic:
refine fun h ↦ (ha ?_).elim

Premises used: False.elim
-- 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
h : LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A)
⊢ IsSelfAdjoint a

Tactic:
isSelfAdjoint_inr (R := ℂ) |>.mp <| .of_nonneg h

Premises used: Unitization.isSelfAdjoint_inr, IsSelfAdjoint.of_nonneg, Iff.mp
-- 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
h : LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A)
⊢ IsSelfAdjoint a

Tactic:
exact isSelfAdjoint_inr (R := ℂ) |>.mp <| .of_nonneg h

Premises used: Unitization.isSelfAdjoint_inr, Iff.mp
-- 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
h : 0 ≤ a
⊢ IsSelfAdjoint a

Tactic:
.of_nonneg h

Premises used: IsSelfAdjoint.of_nonneg
-- 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
h : 0 ≤ a
⊢ IsSelfAdjoint a

Tactic:
exact .of_nonneg h
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
f : A → A
s : Set A
hf : ∀ (x : A), IsSelfAdjoint (f x)
hf₂ : ConvexOn ℝ (β := Unitization ℂ A) s (inr ∘ f)
⊢ ConvexOn ℝ s f

Tactic:
⟨hf₂.1, ?_⟩

Premises used: And.left, And.intro, ConvexOn
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
f : A → A
s : Set A
hf : ∀ (x : A), IsSelfAdjoint (f x)
hf₂ : ConvexOn ℝ (β := Unitization ℂ A) s (inr ∘ f)
refine :
  ∀ ⦃x : A⦄, x ∈ s → ∀ ⦃y : A⦄, y ∈ s → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y
⊢ ConvexOn ℝ s f

Tactic:
refine ⟨hf₂.1, ?_⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
f : A → A
s : Set A
hf : ∀ (x : A), IsSelfAdjoint (f x)
hf₂ : ConvexOn ℝ (β := Unitization ℂ A) s (inr ∘ f)
x : A
hx : x ∈ s
y : A
hy : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
rw : LE.le (α := Unitization ℂ A) (↑(f (a • x + b • y)) : Unitization ℂ A) (↑(a • f x + b • f y) : Unitization ℂ A)
⊢ f (a • x + b • y) ≤ a • f x + b • f y

Tactic:
rw [← Unitization.inr_le_iff _ _]

Premises used: Unitization.inr_le_iff
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
f : A → A
s : Set A
hf : ∀ (x : A), IsSelfAdjoint (f x)
hf₂ : ConvexOn ℝ (β := Unitization ℂ A) s (inr ∘ f)
x : A
hx : x ∈ s
y : A
hy : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ LE.le (α := Unitization ℂ A) (↑(f (a • x + b • y)) : Unitization ℂ A) (↑(a • f x + b • f y) : Unitization ℂ A)

Tactic:
simpa using hf₂.2 hx hy ha hb hab

Premises used: And.right
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
f : A → A
s : Set A
hf : ∀ (x : A), IsSelfAdjoint (f x)
hf₂ : ConcaveOn ℝ (β := Unitization ℂ A) s (inr ∘ f)
⊢ ConcaveOn ℝ s f

Tactic:
⟨hf₂.1, ?_⟩

Premises used: And.left, And.intro, ConcaveOn
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
f : A → A
s : Set A
hf : ∀ (x : A), IsSelfAdjoint (f x)
hf₂ : ConcaveOn ℝ (β := Unitization ℂ A) s (inr ∘ f)
refine :
  ∀ ⦃x : A⦄, x ∈ s → ∀ ⦃y : A⦄, y ∈ s → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • f x + b • f y ≤ f (a • x + b • y)
⊢ ConcaveOn ℝ s f

Tactic:
refine ⟨hf₂.1, ?_⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
f : A → A
s : Set A
hf : ∀ (x : A), IsSelfAdjoint (f x)
hf₂ : ConcaveOn ℝ (β := Unitization ℂ A) s (inr ∘ f)
x : A
hx : x ∈ s
y : A
hy : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
rw : LE.le (α := Unitization ℂ A) (↑(a • f x + b • f y) : Unitization ℂ A) (↑(f (a • x + b • y)) : Unitization ℂ A)
⊢ a • f x + b • f y ≤ f (a • x + b • y)

Tactic:
rw [← Unitization.inr_le_iff _ _]

Premises used: Unitization.inr_le_iff
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
f : A → A
s : Set A
hf : ∀ (x : A), IsSelfAdjoint (f x)
hf₂ : ConcaveOn ℝ (β := Unitization ℂ A) s (inr ∘ f)
x : A
hx : x ∈ s
y : A
hy : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ LE.le (α := Unitization ℂ A) (↑(a • f x + b • f y) : Unitization ℂ A) (↑(f (a • x + b • y)) : Unitization ℂ A)

Tactic:
simpa using hf₂.2 hx hy ha hb hab

Premises used: And.right
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
f : ℝ≥0 → ℝ≥0
hf₀ : f 0 = 0
⊢ (↑(cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f a) : Unitization ℂ A) =
    cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) f (↑a : Unitization ℂ A)

Tactic:
cfcₙ_eq_cfc_inr inr_nonneg_iff ..

Premises used: Unitization.inl, Unitization.inlRingHom, Unitization.inr_nonneg_iff, Unitization.cfcₙ_eq_cfc_inr
-- 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 : 0 ≤ a), CFC.sqrt (↑a : Unitization ℂ A) = (↑(CFC.sqrt a) : Unitization ℂ A)
neg : ∀ (ha : ¬0 ≤ a), CFC.sqrt (↑a : Unitization ℂ A) = (↑(CFC.sqrt a) : Unitization ℂ A)
⊢ CFC.sqrt (↑a : Unitization ℂ A) = (↑(CFC.sqrt a) : Unitization ℂ A)

Tactic:
by_cases ha : 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 : 0 ≤ a
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (ha : LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A)), LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A)
⊢ LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A)

Tactic:
rwa [← Unitization.inr_nonneg_iff] at ha

Premises used: Unitization.inr_nonneg_iff
-- 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 : 0 ≤ a
⊢ LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A)

Tactic:
have ha' := by rwa [← Unitization.inr_nonneg_iff] at ha
-- 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 : ¬0 ≤ a
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (ha : ¬LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A)),
    ¬LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A)
⊢ ¬LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A)

Tactic:
rwa [← Unitization.inr_nonneg_iff] at ha

Premises used: Unitization.inr_nonneg_iff
-- 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 : ¬0 ≤ a
⊢ ¬LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A)

Tactic:
have ha' := by rwa [← Unitization.inr_nonneg_iff] at ha
-- 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 : 0 ≤ a
ha' : LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A)
pos :
  HMul.hMul (α := Unitization ℂ A) (↑(CFC.sqrt a) : Unitization ℂ A) (↑(CFC.sqrt a) : Unitization ℂ A) =
    (↑a : Unitization ℂ A)
pos₁ : Eq (α := Unitization ℂ A) (↑(CFC.sqrt a * CFC.sqrt a) : Unitization ℂ A) (↑a : Unitization ℂ A)
pos₂ pos₃ : Eq (α := Unitization ℂ A) (↑a : Unitization ℂ A) (↑a : Unitization ℂ A)
⊢ CFC.sqrt (↑a : Unitization ℂ A) = (↑(CFC.sqrt a) : Unitization ℂ A)

Tactic:
rw [CFC.sqrt_eq_iff .., ← inr_mul, CFC.sqrt_mul_sqrt_self a]

Premises used: CFC.sqrt_eq_iff, Unitization.inr_mul, CFC.sqrt_mul_sqrt_self
-- 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 : ¬0 ≤ a
ha' : ¬LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A)
neg :
  cfcₙ (R := ℝ≥0) (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (⇑NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (↑a : Unitization ℂ A) =
    (↑(CFC.sqrt a) : Unitization ℂ A)
neg₁ :
  cfcₙ (R := ℝ≥0) (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (⇑NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (↑a : Unitization ℂ A) =
    (↑(cfcₙ (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) (⇑NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) a) : Unitization ℂ A)
neg₂ :
  cfcₙ (R := ℝ≥0) (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (⇑NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (↑a : Unitization ℂ A) =
    (↑0 : Unitization ℂ A)
neg₃ : Eq.{u_1 + 1} (α := Unitization ℂ A) 0 (↑0 : Unitization ℂ A)
neg₄ neg₅ : Eq.{u_1 + 1} (α := Unitization ℂ A) 0 0
⊢ CFC.sqrt (↑a : Unitization ℂ A) = (↑(CFC.sqrt a) : Unitization ℂ A)

Tactic:
rw [CFC.sqrt, CFC.sqrt, cfcₙ_apply_of_not_predicate _ ha,
      cfcₙ_apply_of_not_predicate _ ha', inr_zero]

Premises used: CFC.sqrt, cfcₙ_apply_of_not_predicate, Unitization.inr_zero
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : IsTopologicalRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : T2Space A
inst_9 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
f g : ℝ≥0 → ℝ≥0
a : A
ha_spec : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hf : ContinuousOn f (spectrum ℝ≥0 a)
hg : ContinuousOn g (spectrum ℝ≥0 a)
ha : 0 ≤ a
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) (spectrum ℝ a)

Tactic:
have hf' := hf.ofReal_map_toNNReal <| ha_spec.image ▸ Set.mapsTo_image ..
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : IsTopologicalRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : T2Space A
inst_9 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
f g : ℝ≥0 → ℝ≥0
a : A
ha_spec : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hf : ContinuousOn f (spectrum ℝ≥0 a)
hg : ContinuousOn g (spectrum ℝ≥0 a)
ha : 0 ≤ a
hf' : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) (spectrum ℝ a)
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (↑(g x.toNNReal) : ℝ)) (spectrum ℝ a)

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

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

Premises used: cfc_nnreal_eq_real, cfc_le_iff
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : IsTopologicalRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : T2Space A
inst_9 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
f g : ℝ≥0 → ℝ≥0
a : A
ha_spec : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hf : ContinuousOn f (spectrum ℝ≥0 a)
hg : ContinuousOn g (spectrum ℝ≥0 a)
ha : 0 ≤ a
hf' : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) (spectrum ℝ a)
hg' : ContinuousOn (Y := ℝ) (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]

Premises used: SpectrumRestricts.image, NNReal.coe_le_coe
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : NonnegSpectrumClass ℝ A
inst_7 : Nontrivial A
inst_8 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
⊢ IsCompact (spectrum ℝ a)

Tactic:
have h_cpct : IsCompact (spectrum ℝ a) := isCompact_iff_compactSpace.mpr inferInstance
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : NonnegSpectrumClass ℝ A
inst_7 : Nontrivial A
inst_8 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
h_cpct : IsCompact (spectrum ℝ a)
simp_rw : (∃ r > 0, ∀ x ∈ spectrum ℝ a, r ≤ x) ↔ ∀ x ∈ spectrum ℝ a, 0 < x
⊢ (∃ r > 0, (algebraMap ℝ A : (a : ℝ) → A) r ≤ a) ↔ ∀ x ∈ spectrum ℝ a, 0 < x

Tactic:
simp_rw [algebraMap_le_iff_le_spectrum (a := a)]

Premises used: algebraMap_le_iff_le_spectrum
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : NonnegSpectrumClass ℝ A
inst_7 : Nontrivial A
inst_8 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
h_cpct : IsCompact (spectrum ℝ a)
⊢ (∃ r > 0, ∀ x ∈ spectrum ℝ a, r ≤ x) ↔ ∀ x ∈ spectrum ℝ a, 0 < x

Tactic:
⟨?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : NonnegSpectrumClass ℝ A
inst_7 : Nontrivial A
inst_8 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
h_cpct : IsCompact (spectrum ℝ a)
refine_1 : (∃ r > 0, ∀ x ∈ spectrum ℝ a, r ≤ x) → ∀ x ∈ spectrum ℝ a, 0 < x
refine_2 : ∀ (h : ∀ x ∈ spectrum ℝ a, 0 < x), ∃ r > 0, ∀ x ∈ spectrum ℝ a, r ≤ x
⊢ (∃ r > 0, ∀ x ∈ spectrum ℝ a, r ≤ x) ↔ ∀ x ∈ spectrum ℝ a, 0 < x

Tactic:
refine ⟨?_, fun h ↦ ?_⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : NonnegSpectrumClass ℝ A
inst_7 : Nontrivial A
inst_8 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
h_cpct : IsCompact (spectrum ℝ a)
r : ℝ
hr : r > 0
hr_le : ∀ x ∈ spectrum ℝ a, r ≤ x
⊢ ∀ x ∈ spectrum ℝ a, 0 < x

Tactic:
(hr.trans_le <| hr_le · ·)

Premises used: LT.lt.trans_le
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : NonnegSpectrumClass ℝ A
inst_7 : Nontrivial A
inst_8 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
h_cpct : IsCompact (spectrum ℝ a)
r : ℝ
hr : r > 0
hr_le : ∀ x ∈ spectrum ℝ a, r ≤ x
⊢ ∀ x ∈ spectrum ℝ a, 0 < x

Tactic:
exact (hr.trans_le <| hr_le · ·)

Premises used: LT.lt.trans_le
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : NonnegSpectrumClass ℝ A
inst_7 : Nontrivial A
inst_8 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
h_cpct : IsCompact (spectrum ℝ a)
h : ∀ x ∈ spectrum ℝ a, 0 < x
refine_2 : ∀ (r : ℝ) (hr : r ∈ spectrum ℝ a) (hr_min : IsMinOn id (spectrum ℝ a) r), ∃ r > 0, ∀ x ∈ spectrum ℝ a, r ≤ x
⊢ ∃ r > 0, ∀ x ∈ spectrum ℝ a, r ≤ x

Tactic:
obtain ⟨r, hr, hr_min⟩ := h_cpct.exists_isMinOn
      (ContinuousFunctionalCalculus.spectrum_nonempty a ha) continuousOn_id

Premises used: IsCompact.exists_isMinOn, continuousOn_id, ContinuousFunctionalCalculus.spectrum_nonempty
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : NonnegSpectrumClass ℝ A
inst_7 : Nontrivial A
inst_8 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
h_cpct : IsCompact (spectrum ℝ a)
h : ∀ x ∈ spectrum ℝ a, 0 < x
r : ℝ
hr : r ∈ spectrum ℝ a
hr_min : IsMinOn id (spectrum ℝ a) r
⊢ ∃ r > 0, ∀ x ∈ spectrum ℝ a, r ≤ x

Tactic:
⟨r, h _ hr, hr_min⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : NonnegSpectrumClass ℝ A
inst_7 : Nontrivial A
inst_8 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
h_cpct : IsCompact (spectrum ℝ a)
h : ∀ x ∈ spectrum ℝ a, 0 < x
r : ℝ
hr : r ∈ spectrum ℝ a
hr_min : IsMinOn id (spectrum ℝ a) r
⊢ ∃ r > 0, ∀ x ∈ spectrum ℝ a, r ≤ x

Tactic:
exact ⟨r, h _ hr, hr_min⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
pos : ∀ (nontriv : Nontrivial A), a ≤ (algebraMap ℝ A : (a : ℝ) → A) ‖a‖
neg : ∀ (nontriv : Subsingleton A), a ≤ (algebraMap ℝ A : (a : ℝ) → A) ‖a‖
⊢ a ≤ (algebraMap ℝ A : (a : ℝ) → A) ‖a‖

Tactic:
by_cases! nontriv : Nontrivial A

Premises used: Nontrivial
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
nontriv : Nontrivial A
⊢ a ≤ (algebraMap ℝ A : (a : ℝ) → A) ‖a‖

Tactic:
le_algebraMap_of_spectrum_le fun r hr => ?_

Premises used: le_algebraMap_of_spectrum_le
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
nontriv : Nontrivial A
pos : ∀ (r : ℝ) (hr : r ∈ spectrum ℝ a), r ≤ ‖a‖
⊢ a ≤ (algebraMap ℝ A : (a : ℝ) → A) ‖a‖

Tactic:
refine le_algebraMap_of_spectrum_le fun r hr => ?_

Premises used: le_algebraMap_of_spectrum_le
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
nontriv : Nontrivial A
r : ℝ
hr : r ∈ spectrum ℝ a
⊢ r ≤ ‖r‖

Tactic:
Real.le_norm_self r

Premises used: Real.le_norm_self
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
nontriv : Nontrivial A
r : ℝ
hr : r ∈ spectrum ℝ a
⊢ ‖r‖ ≤ ‖a‖

Tactic:
spectrum.norm_le_norm_of_mem hr

Premises used: spectrum.norm_le_norm_of_mem
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
nontriv : Nontrivial A
r : ℝ
hr : r ∈ spectrum ℝ a
⊢ r ≤ ‖a‖

Tactic:
calc r ≤ ‖r‖ := Real.le_norm_self r
      _ ≤ ‖a‖ := spectrum.norm_le_norm_of_mem hr

Premises used: spectrum.norm_le_norm_of_mem, Real.le_norm_self
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
nontriv : Subsingleton A
⊢ a ≤ (algebraMap ℝ A : (a : ℝ) → A) ‖a‖

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
rw : -a ≤ (algebraMap ℝ A : (a : ℝ) → A) ‖-a‖
⊢ -(algebraMap ℝ A : (a : ℝ) → A) ‖a‖ ≤ a

Tactic:
rw [neg_le, ← norm_neg]

Premises used: neg_le, norm_neg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
⊢ -a ≤ (algebraMap ℝ A : (a : ℝ) → A) ‖-a‖

Tactic:
ha.neg.le_algebraMap_norm_self

Premises used: IsSelfAdjoint.neg, IsSelfAdjoint.le_algebraMap_norm_self
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
⊢ -a ≤ (algebraMap ℝ A : (a : ℝ) → A) ‖-a‖

Tactic:
exact ha.neg.le_algebraMap_norm_self

Premises used: IsSelfAdjoint.neg, IsSelfAdjoint.le_algebraMap_norm_self