awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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)
⊢ 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
have 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
Tactic: rw [cfcₙ_nnreal_eq_real .., cfcₙ_nnreal_eq_real .., cfcₙ_nnreal_eq_real .., cfcₙ_congr this]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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)
⊢ 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
have refine_1 : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) (σₙ ℝ a)
Tactic: refine cfcₙ_sub _ _ a ?_ (by simpa) ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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)
⊢ 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
have refine_2 : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (↑(g x.toNNReal) : ℝ)) (σₙ ℝ a)
Tactic: refine cfcₙ_sub _ _ a ?_ (by simpa) ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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
⊢ LE.le (α := Unitization ℂ A) (↑a : Unitization ℂ A) (↑b : Unitization ℂ A) ↔ a ≤ b
have rw : (∀ x ∈ σₙ ℝ (b - a), 0 ≤ x) ↔ 0 ≤ b - a
Tactic: rw [← sub_nonneg, ← sub_nonneg (a := b), StarOrderedRing.nonneg_iff_spectrum_nonneg (R := ℝ) _,
    ← inr_sub ℂ b a, ← Unitization.quasispectrum_eq_spectrum_inr' ℝ ℂ]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
⊢ LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A) ↔ 0 ≤ a
have pos : ∀ (ha : IsSelfAdjoint a), LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A) ↔ 0 ≤ a
Tactic: by_cases ha : IsSelfAdjoint a
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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
⊢ LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A) ↔ 0 ≤ a
have neg : ∀ (ha : ¬IsSelfAdjoint a), LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A) ↔ 0 ≤ a
Tactic: by_cases ha : IsSelfAdjoint a
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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
have neg : LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A) → 0 ≤ a
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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
⊢ LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A) ↔ 0 ≤ a
have neg₁ : 0 ≤ a → LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A)
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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
have neg : ∀ (h : LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A)), IsSelfAdjoint a
Tactic: refine fun h ↦ (ha ?_).elim
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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)
have neg : ∀ (h : 0 ≤ a), IsSelfAdjoint a
Tactic: refine fun h ↦ (ha ?_).elim
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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
have 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
Tactic: refine ⟨hf₂.1, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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
⊢ f (a • x + b • y) ≤ a • f x + b • f y
have rw : LE.le (α := Unitization ℂ A) (↑(f (a • x + b • y)) : Unitization ℂ A) (↑(a • f x + b • f y) : Unitization ℂ A)
Tactic: rw [← Unitization.inr_le_iff _ _]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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
have 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)
Tactic: refine ⟨hf₂.1, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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
⊢ a • f x + b • f y ≤ f (a • x + b • y)
have rw : LE.le (α := Unitization ℂ A) (↑(a • f x + b • f y) : Unitization ℂ A) (↑(f (a • x + b • y)) : Unitization ℂ A)
Tactic: rw [← Unitization.inr_le_iff _ _]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
⊢ CFC.sqrt (↑a : Unitization ℂ A) = (↑(CFC.sqrt a) : Unitization ℂ A)
have pos : ∀ (ha : 0 ≤ a), CFC.sqrt (↑a : Unitization ℂ A) = (↑(CFC.sqrt a) : Unitization ℂ A)
Tactic: by_cases ha : 0 ≤ a
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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)
⊢ CFC.sqrt (↑a : Unitization ℂ A) = (↑(CFC.sqrt a) : Unitization ℂ A)
have neg : ∀ (ha : ¬0 ≤ a), CFC.sqrt (↑a : Unitization ℂ A) = (↑(CFC.sqrt a) : Unitization ℂ A)
Tactic: by_cases ha : 0 ≤ a
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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)
have rwa : ∀ (ha : LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A)), LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A)
Tactic: rwa [← Unitization.inr_nonneg_iff] at ha
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : 0 ≤ a
⊢ CFC.sqrt (↑a : Unitization ℂ A) = (↑(CFC.sqrt a) : Unitization ℂ A)
have ha' : LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A)
Tactic: have ha' := by rwa [← Unitization.inr_nonneg_iff] at ha
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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)
have rwa : ∀ (ha : ¬LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A)), ¬LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A)
Tactic: rwa [← Unitization.inr_nonneg_iff] at ha
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : ¬0 ≤ a
⊢ CFC.sqrt (↑a : Unitization ℂ A) = (↑(CFC.sqrt a) : Unitization ℂ A)
have ha' : ¬LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A)
Tactic: have ha' := by rwa [← Unitization.inr_nonneg_iff] at ha
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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)
⊢ CFC.sqrt (↑a : Unitization ℂ A) = (↑(CFC.sqrt a) : Unitization ℂ A)
have pos : HMul.hMul (α := Unitization ℂ A) (↑(CFC.sqrt a) : Unitization ℂ A) (↑(CFC.sqrt a) : Unitization ℂ A) =
  (↑a : Unitization ℂ A)
Tactic: rw [CFC.sqrt_eq_iff .., ← inr_mul, CFC.sqrt_mul_sqrt_self a]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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)
⊢ CFC.sqrt (↑a : Unitization ℂ A) = (↑(CFC.sqrt a) : Unitization ℂ A)
have pos₁ : Eq (α := Unitization ℂ A) (↑(CFC.sqrt a * CFC.sqrt a) : Unitization ℂ A) (↑a : Unitization ℂ A)
Tactic: rw [CFC.sqrt_eq_iff .., ← inr_mul, CFC.sqrt_mul_sqrt_self a]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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)
⊢ CFC.sqrt (↑a : Unitization ℂ A) = (↑(CFC.sqrt a) : Unitization ℂ A)
have pos₂ : Eq (α := Unitization ℂ A) (↑a : Unitization ℂ A) (↑a : Unitization ℂ A)
Tactic: rw [CFC.sqrt_eq_iff .., ← inr_mul, CFC.sqrt_mul_sqrt_self a]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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)
⊢ CFC.sqrt (↑a : Unitization ℂ A) = (↑(CFC.sqrt a) : Unitization ℂ A)
have neg : cfcₙ (R := ℝ≥0) (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (⇑NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (↑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]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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)
⊢ CFC.sqrt (↑a : Unitization ℂ A) = (↑(CFC.sqrt a) : Unitization ℂ A)
have 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)
Tactic: rw [CFC.sqrt, CFC.sqrt, cfcₙ_apply_of_not_predicate _ ha,
      cfcₙ_apply_of_not_predicate _ ha', inr_zero]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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)
⊢ CFC.sqrt (↑a : Unitization ℂ A) = (↑(CFC.sqrt a) : Unitization ℂ A)
have neg₂ : cfcₙ (R := ℝ≥0) (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (⇑NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (↑a : Unitization ℂ A) =
  (↑0 : Unitization ℂ A)
Tactic: rw [CFC.sqrt, CFC.sqrt, cfcₙ_apply_of_not_predicate _ ha,
      cfcₙ_apply_of_not_predicate _ ha', inr_zero]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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)
⊢ CFC.sqrt (↑a : Unitization ℂ A) = (↑(CFC.sqrt a) : Unitization ℂ A)
have neg₃ : Eq.{u_1 + 1} (α := Unitization ℂ A) 0 (↑0 : Unitization ℂ A)
Tactic: rw [CFC.sqrt, CFC.sqrt, cfcₙ_apply_of_not_predicate _ ha,
      cfcₙ_apply_of_not_predicate _ ha', inr_zero]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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)
⊢ CFC.sqrt (↑a : Unitization ℂ A) = (↑(CFC.sqrt a) : Unitization ℂ A)
have neg₄ : Eq.{u_1 + 1} (α := Unitization ℂ A) 0 0
Tactic: rw [CFC.sqrt, CFC.sqrt, cfcₙ_apply_of_not_predicate _ ha,
      cfcₙ_apply_of_not_predicate _ ha', inr_zero]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (hypothesis)
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
⊢ 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
have hf' : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) (spectrum ℝ a)
Tactic: have hf' := hf.ofReal_map_toNNReal <| ha_spec.image ▸ Set.mapsTo_image ..
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (hypothesis)
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)
⊢ 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
have hg' : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (↑(g x.toNNReal) : ℝ)) (spectrum ℝ a)
Tactic: have hg' := hg.ofReal_map_toNNReal <| ha_spec.image ▸ Set.mapsTo_image ..
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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)
⊢ 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
have rw : (∀ x ∈ spectrum ℝ a, (↑(f x.toNNReal) : ℝ) ≤ (↑(g x.toNNReal) : ℝ)) ↔ ∀ x ∈ spectrum ℝ≥0 a, f x ≤ g x
Tactic: rw [cfc_nnreal_eq_real .., cfc_nnreal_eq_real .., cfc_le_iff ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (hypothesis)
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
⊢ (∃ r > 0, (algebraMap ℝ A : (a : ℝ) → A) r ≤ a) ↔ ∀ x ∈ spectrum ℝ a, 0 < x
have h_cpct : IsCompact (spectrum ℝ a)
Tactic: have h_cpct : IsCompact (spectrum ℝ a) := isCompact_iff_compactSpace.mpr inferInstance
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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, (algebraMap ℝ A : (a : ℝ) → A) r ≤ a) ↔ ∀ x ∈ spectrum ℝ a, 0 < x
have simp_rw : (∃ r > 0, ∀ x ∈ spectrum ℝ a, r ≤ x) ↔ ∀ x ∈ spectrum ℝ a, 0 < x
Tactic: simp_rw [algebraMap_le_iff_le_spectrum (a := a)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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
have refine_1 : (∃ r > 0, ∀ x ∈ spectrum ℝ a, r ≤ x) → ∀ x ∈ spectrum ℝ a, 0 < x
Tactic: refine ⟨?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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
⊢ (∃ r > 0, ∀ x ∈ spectrum ℝ a, r ≤ x) ↔ ∀ x ∈ spectrum ℝ a, 0 < x
have refine_2 : ∀ (h : ∀ x ∈ spectrum ℝ a, 0 < x), ∃ r > 0, ∀ x ∈ spectrum ℝ a, r ≤ x
Tactic: refine ⟨?_, fun h ↦ ?_⟩