awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
⊢ a * star a ≤ (algebraMap ℝ A : (a : ℝ) → A) ‖a * star a‖

Tactic:
have : a * star a ≤ algebraMap ℝ A ‖a * star a‖ := 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
this : a * star a ≤ (algebraMap ℝ A : (a : ℝ) → A) ‖a * star a‖
rwa :
  ∀ (this : a * star a ≤ (algebraMap ℝ A : (a : ℝ) → A) (‖a‖ * ‖a‖)),
    a * star a ≤ (algebraMap ℝ A : (a : ℝ) → A) (HPow.hPow (β := ℕ) ‖a‖ 2)
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (this : a * star a ≤ (algebraMap ℝ A : (a : ℝ) → A) (HPow.hPow (β := ℕ) ‖a‖ 2)),
    a * star a ≤ (algebraMap ℝ A : (a : ℝ) → A) (HPow.hPow (β := ℕ) ‖a‖ 2)
⊢ a * star a ≤ (algebraMap ℝ A : (a : ℝ) → A) (HPow.hPow (β := ℕ) ‖a‖ 2)

Tactic:
rwa [CStarRing.norm_self_mul_star, ← pow_two] at this

Premises used: pow_two, CStarRing.norm_self_mul_star
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
⊢ star a * a ≤ (algebraMap ℝ A : (a : ℝ) → A) ‖star a * a‖

Tactic:
have : star a * a ≤ algebraMap ℝ A ‖star a * a‖ := 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
this : star a * a ≤ (algebraMap ℝ A : (a : ℝ) → A) ‖star a * a‖
rwa :
  ∀ (this : star a * a ≤ (algebraMap ℝ A : (a : ℝ) → A) (‖a‖ * ‖a‖)),
    star a * a ≤ (algebraMap ℝ A : (a : ℝ) → A) (HPow.hPow (β := ℕ) ‖a‖ 2)
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (this : star a * a ≤ (algebraMap ℝ A : (a : ℝ) → A) (HPow.hPow (β := ℕ) ‖a‖ 2)),
    star a * a ≤ (algebraMap ℝ A : (a : ℝ) → A) (HPow.hPow (β := ℕ) ‖a‖ 2)
⊢ star a * a ≤ (algebraMap ℝ A : (a : ℝ) → A) (HPow.hPow (β := ℕ) ‖a‖ 2)

Tactic:
rwa [CStarRing.norm_star_mul_self, ← pow_two] at this

Premises used: pow_two, CStarRing.norm_star_mul_self
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
⊢ (spectralRadius ℝ a).toReal = ‖a‖

Tactic:
simp [ha.spectrumRestricts.spectralRadius_eq, ha.spectralRadius_eq_nnnorm]

Premises used: IsSelfAdjoint.spectrumRestricts, SpectrumRestricts.spectralRadius_eq, IsSelfAdjoint.spectralRadius_eq_nnnorm
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : Nontrivial A
a : A
ha : IsSelfAdjoint a
⊢ SpectrumRestricts (R := ℝ) (S := ℂ) a (⇑Complex.reCLM : (a : ℂ) → ℝ)

Tactic:
have ha' : SpectrumRestricts a Complex.reCLM := ha.spectrumRestricts
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : Nontrivial A
a : A
ha : IsSelfAdjoint a
ha' : SpectrumRestricts (R := ℝ) (S := ℂ) a (⇑Complex.reCLM : (a : ℂ) → ℝ)
rw : (spectralRadius ℝ a).toReal ∈ spectrum ℝ a ∨ -(spectralRadius ℝ a).toReal ∈ spectrum ℝ a
⊢ ‖a‖ ∈ spectrum ℝ a ∨ -‖a‖ ∈ spectrum ℝ a

Tactic:
rw [← ha.toReal_spectralRadius_eq_norm]

Premises used: IsSelfAdjoint.toReal_spectralRadius_eq_norm
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : Nontrivial A
a : A
ha : IsSelfAdjoint a
ha' : SpectrumRestricts (R := ℝ) (S := ℂ) a (⇑Complex.reCLM : (a : ℂ) → ℝ)
⊢ (spectralRadius ℝ a).toReal ∈ spectrum ℝ a ∨ -(spectralRadius ℝ a).toReal ∈ spectrum ℝ a

Tactic:
Real.spectralRadius_mem_spectrum_or (ha'.image ▸ (spectrum.nonempty a).image _)

Premises used: Eq.rec, Real.spectralRadius_mem_spectrum_or, spectrum.nonempty, Set.Nonempty.image, SpectrumRestricts.image
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : Nontrivial A
a : A
ha : IsSelfAdjoint a
ha' : SpectrumRestricts (R := ℝ) (S := ℂ) a (⇑Complex.reCLM : (a : ℂ) → ℝ)
⊢ (spectralRadius ℝ a).toReal ∈ spectrum ℝ a ∨ -(spectralRadius ℝ a).toReal ∈ spectrum ℝ a

Tactic:
exact Real.spectralRadius_mem_spectrum_or (ha'.image ▸ (spectrum.nonempty a).image _)

Premises used: Real.spectralRadius_mem_spectrum_or
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
inst_3 : Nontrivial A
a : A
ha : 0 ≤ a
⊢ IsSelfAdjoint a

Tactic:
have : IsSelfAdjoint a := .of_nonneg ha
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
inst_3 : Nontrivial A
a : A
ha : 0 ≤ a
this : IsSelfAdjoint a
⊢ (spectralRadius ℝ a).toNNReal ∈ spectrum ℝ≥0 a

Tactic:
NNReal.spectralRadius_mem_spectrum (a := a) ?_ (.nnreal_of_nonneg ha)

Premises used: SpectrumRestricts.nnreal_of_nonneg, NNReal.spectralRadius_mem_spectrum
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
inst_3 : Nontrivial A
a : A
ha : 0 ≤ a
this : IsSelfAdjoint a
h : ‖a‖₊ = (spectralRadius ℝ a).toNNReal
convert! : (spectrum ℝ a).Nonempty
⊢ ‖a‖₊ ∈ spectrum ℝ≥0 a

Tactic:
convert! NNReal.spectralRadius_mem_spectrum (a := a) ?_ (.nnreal_of_nonneg ha)

Premises used: SpectrumRestricts.nnreal_of_nonneg, NNReal.spectralRadius_mem_spectrum
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
inst_3 : Nontrivial A
a : A
ha : 0 ≤ a
this : IsSelfAdjoint a
⊢ ‖a‖₊ = (spectralRadius ℝ a).toNNReal

Tactic:
simp [this.spectrumRestricts.spectralRadius_eq, this.spectralRadius_eq_nnnorm]

Premises used: IsSelfAdjoint.spectrumRestricts, SpectrumRestricts.spectralRadius_eq, IsSelfAdjoint.spectralRadius_eq_nnnorm
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
inst_3 : Nontrivial A
a : A
ha : 0 ≤ a
this : IsSelfAdjoint a
⊢ (spectrum ℝ a).Nonempty

Tactic:
this.spectrumRestricts.image ▸ (spectrum.nonempty a).image _

Premises used: Eq.rec, IsSelfAdjoint.spectrumRestricts, spectrum.nonempty, Set.Nonempty.image, SpectrumRestricts.image
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
inst_3 : Nontrivial A
a : A
ha : 0 ≤ a
this : IsSelfAdjoint a
⊢ (spectrum ℝ a).Nonempty

Tactic:
exact this.spectrumRestricts.image ▸ (spectrum.nonempty a).image _
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
inst_3 : Nontrivial A
a : A
ha : 0 ≤ a
⊢ ‖a‖ ∈ spectrum ℝ a

Tactic:
simpa using spectrum.algebraMap_mem ℝ <| nnnorm_mem_spectrum_of_nonneg ha

Premises used: Real, spectrum.algebraMap_mem, CStarAlgebra.nnnorm_mem_spectrum_of_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
r : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
rw : ‖a‖ ≤ r ↔ ∀ x ∈ spectrum ℝ a, x ≤ r
⊢ ‖a‖ ≤ r ↔ a ≤ (algebraMap ℝ A : (a : ℝ) → A) r

Tactic:
rw [le_algebraMap_iff_spectrum_le]

Premises used: le_algebraMap_iff_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
r : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
inl : ∀ (h : Subsingleton A), ‖a‖ ≤ r ↔ ∀ x ∈ spectrum ℝ a, x ≤ r
inr : Nontrivial A → (‖a‖ ≤ r ↔ ∀ x ∈ spectrum ℝ a, x ≤ r)
⊢ ‖a‖ ≤ r ↔ ∀ x ∈ spectrum ℝ a, x ≤ r

Tactic:
obtain (h | _) := subsingleton_or_nontrivial A

Premises used: subsingleton_or_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
r : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
h : Subsingleton A
⊢ ‖a‖ ≤ r ↔ ∀ x ∈ spectrum ℝ a, x ≤ r

Tactic:
simp [Subsingleton.elim a 0, hr]

Premises used: Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
r : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
h : Nontrivial A
⊢ ‖a‖ ≤ r ↔ ∀ x ∈ spectrum ℝ a, x ≤ r

Tactic:
⟨fun h x hx ↦ Real.le_norm_self x |>.trans (spectrum.norm_le_norm_of_mem hx) |>.trans h,
      fun h ↦ h ‖a‖ <| norm_mem_spectrum_of_nonneg⟩

Premises used: Norm.norm, spectrum.norm_le_norm_of_mem, Real.le_norm_self, Iff.intro, LE.le.trans, CStarAlgebra.norm_mem_spectrum_of_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
r : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
h : Nontrivial A
⊢ ‖a‖ ≤ r ↔ ∀ x ∈ spectrum ℝ a, x ≤ r

Tactic:
exact ⟨fun h x hx ↦ Real.le_norm_self x |>.trans (spectrum.norm_le_norm_of_mem hx) |>.trans h,
      fun h ↦ h ‖a‖ <| norm_mem_spectrum_of_nonneg⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
r : ℝ≥0
ha : 0 ≤ a
⊢ (↑‖a‖₊ : ℝ) ≤ (↑r : ℝ) ↔ a ≤ (algebraMap ℝ≥0 A : (a : ℝ≥0) → A) r

Tactic:
norm_le_iff_le_algebraMap a r.2

Premises used: CStarAlgebra.norm_le_iff_le_algebraMap, NNReal.toReal, Subtype.property
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
r : ℝ≥0
ha : 0 ≤ a
⊢ (↑‖a‖₊ : ℝ) ≤ (↑r : ℝ) ↔ a ≤ (algebraMap ℝ≥0 A : (a : ℝ≥0) → A) r

Tactic:
exact norm_le_iff_le_algebraMap a r.2

Premises used: CStarAlgebra.norm_le_iff_le_algebraMap, Subtype.property
-- 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 : 0 ≤ a
⊢ ‖a‖ ≤ 1 ↔ a ≤ 1

Tactic:
simpa using norm_le_iff_le_algebraMap a zero_le_one

Premises used: zero_le_one, CStarAlgebra.norm_le_iff_le_algebraMap
-- 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 : 0 ≤ a
⊢ (↑‖a‖₊ : ℝ) ≤ (↑1 : ℝ) ↔ a ≤ 1

Tactic:
norm_le_one_iff_of_nonneg a

Premises used: CStarAlgebra.norm_le_one_iff_of_nonneg, NNReal.toReal
-- 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 : 0 ≤ a
⊢ (↑‖a‖₊ : ℝ) ≤ (↑1 : ℝ) ↔ a ≤ 1

Tactic:
exact norm_le_one_iff_of_nonneg a

Premises used: CStarAlgebra.norm_le_one_iff_of_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
n : ℕ
ha : 0 ≤ a
⊢ ‖a‖ ≤ (↑n : ℝ) ↔ a ≤ (↑n : A)

Tactic:
simpa using norm_le_iff_le_algebraMap a n.cast_nonneg

Premises used: Nat.cast_nonneg, CStarAlgebra.norm_le_iff_le_algebraMap
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
n : ℕ
ha : 0 ≤ a
⊢ ‖a‖₊ ≤ (↑n : ℝ≥0) ↔ a ≤ (↑n : A)

Tactic:
simpa using nnnorm_le_iff_of_nonneg a n

Premises used: CStarAlgebra.nnnorm_le_iff_of_nonneg, Nat.cast
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
r : ℝ
hr : 0 ≤ r
rw : 0 ≤ x → (‖x‖ ≤ r ↔ x ≤ (algebraMap ℝ A : (a : ℝ) → A) r)
⊢ Membership.mem (γ := Set A) (Icc 0 ((algebraMap ℝ A : (a : ℝ) → A) r) : Set A) x ↔ 0 ≤ x ∧ ‖x‖ ≤ r

Tactic:
rw [mem_Icc, and_congr_right_iff, iff_comm]

Premises used: iff_comm, and_congr_right_iff, Set.mem_Icc
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
r : ℝ
hr : 0 ≤ r
⊢ 0 ≤ x → (‖x‖ ≤ r ↔ x ≤ (algebraMap ℝ A : (a : ℝ) → A) r)

Tactic:
(norm_le_iff_le_algebraMap _ hr ·)

Premises used: CStarAlgebra.norm_le_iff_le_algebraMap
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
r : ℝ
hr : 0 ≤ r
⊢ 0 ≤ x → (‖x‖ ≤ r ↔ x ≤ (algebraMap ℝ A : (a : ℝ) → A) r)

Tactic:
exact (norm_le_iff_le_algebraMap _ hr ·)

Premises used: CStarAlgebra.norm_le_iff_le_algebraMap
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
r : ℝ≥0
⊢ Membership.mem (γ := Set A) (Icc 0 ((algebraMap ℝ≥0 A : (a : ℝ≥0) → A) r) : Set A) x ↔ 0 ≤ x ∧ ‖x‖₊ ≤ r

Tactic:
mem_Icc_algebraMap_iff_norm_le (hr := r.2)

Premises used: CStarAlgebra.mem_Icc_algebraMap_iff_norm_le, Set.Mem, NNReal.toReal, Subtype.property
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
⊢ Membership.mem (γ := Set A) (Icc 0 1) x ↔ 0 ≤ x ∧ ‖x‖ ≤ 1

Tactic:
simpa only [map_one] using mem_Icc_algebraMap_iff_norm_le zero_le_one (A := A)

Premises used: CStarAlgebra.mem_Icc_algebraMap_iff_norm_le, zero_le_one, map_one
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
⊢ Membership.mem (γ := Set A) (Icc 0 1) x ↔ 0 ≤ x ∧ ‖x‖₊ ≤ 1

Tactic:
mem_Icc_iff_norm_le_one

Premises used: CStarAlgebra.mem_Icc_iff_norm_le_one
-- 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 : IsStrictlyPositive a
⊢ IsUnit a

Tactic:
ha.isUnit

Premises used: IsStrictlyPositive.isUnit
-- 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 : IsStrictlyPositive a
lift : ∀ (a : Aˣ) (ha : IsStrictlyPositive (↑a : A)), (↑a : A) ^ (-(1 / 2)) * (↑a : A) * (↑a : A) ^ (-(1 / 2)) = 1
⊢ a ^ (-(1 / 2)) * a * a ^ (-(1 / 2)) = 1

Tactic:
lift a to Aˣ using ha.isUnit

Premises used: IsStrictlyPositive.isUnit
-- 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 : IsStrictlyPositive (↑a : A)
nth_rw : (↑a : A) ^ (-(1 / 2)) * HPow.hPow (β := ℝ) (↑a : A) 1 * (↑a : A) ^ (-(1 / 2)) = 1
⊢ (↑a : A) ^ (-(1 / 2)) * (↑a : A) * (↑a : A) ^ (-(1 / 2)) = 1

Tactic:
nth_rw 2 [← rpow_one (a : A)]

Premises used: Units.val, CFC.rpow_one
-- 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 : IsStrictlyPositive (↑a : A)
simp : (↑a : A) ^ (-(1 / 2) + 1 + -(1 / 2)) = 1
⊢ (↑a : A) ^ (-(1 / 2)) * HPow.hPow (β := ℝ) (↑a : A) 1 * (↑a : A) ^ (-(1 / 2)) = 1

Tactic:
simp only [← rpow_add a.isUnit]

Premises used: CFC.rpow_add, Units.isUnit
-- 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 : IsStrictlyPositive (↑a : A)
norm_num : HPow.hPow (β := ℝ) (↑a : A) 0 = 1
⊢ (↑a : A) ^ (-(1 / 2) + 1 + -(1 / 2)) = 1

Tactic:
norm_num
-- 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 : IsStrictlyPositive (↑a : A)
⊢ HPow.hPow (β := ℝ) (↑a : A) 0 = 1

Tactic:
rpow_zero _

Premises used: CFC.rpow_zero
-- 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 : IsStrictlyPositive (↑a : A)
⊢ HPow.hPow (β := ℝ) (↑a : A) 0 = 1

Tactic:
exact rpow_zero _

Premises used: CFC.rpow_zero
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
hab : a ≤ b
h : IsStrictlyPositive a
⊢ Nontrivial A

Tactic:
nontriviality A
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
hab : a ≤ b
h : IsStrictlyPositive a
h_1 : Nontrivial A
rw : 0 ∉ spectrum ℝ b
⊢ IsUnit b

Tactic:
rw [← spectrum.zero_notMem_iff ℝ]

Premises used: Real, spectrum.zero_notMem_iff
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
hab : a ≤ b
h : IsStrictlyPositive a
h_1 : Nontrivial A
⊢ ∃ r > 0, (algebraMap ℝ A : (a : ℝ) → A) r ≤ a

Tactic:
(exists_pos_algebraMap_le_iff h.isSelfAdjoint).2 fun x hx ↦ h.spectrum_pos hx

Premises used: Iff.mpr, CFC.exists_pos_algebraMap_le_iff, IsStrictlyPositive.spectrum_pos, IsStrictlyPositive.isSelfAdjoint
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
hab : a ≤ b
h : IsStrictlyPositive a
h_1 : Nontrivial A
obtain : ∀ (r : ℝ) (hr : r > 0) (hr_le : (algebraMap ℝ A : (a : ℝ) → A) r ≤ a), 0 ∉ spectrum ℝ b
⊢ 0 ∉ spectrum ℝ b

Tactic:
obtain ⟨r, hr, hr_le⟩ : ∃ r > 0, (algebraMap ℝ A) r ≤ a :=
    (exists_pos_algebraMap_le_iff h.isSelfAdjoint).2 fun x hx ↦ h.spectrum_pos hx

Premises used: Iff.mpr, CFC.exists_pos_algebraMap_le_iff, IsStrictlyPositive.spectrum_pos, IsStrictlyPositive.isSelfAdjoint
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
hab : a ≤ b
h : IsStrictlyPositive a
h_1 : Nontrivial A
r : ℝ
hr : r > 0
hr_le : (algebraMap ℝ A : (a : ℝ) → A) r ≤ a
⊢ 0 ∉ spectrum ℝ b

Tactic:
fun h0 ↦ not_le_of_gt hr <| (algebraMap_le_iff_le_spectrum <| .of_nonneg <|
    h.nonneg.trans hab).1 (hr_le.trans hab) 0 h0

Premises used: algebraMap_le_iff_le_spectrum, Iff.mp, LE.le.trans, not_le_of_gt, OfNat.ofNat, Not
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
hab : a ≤ b
h : IsStrictlyPositive a
h_1 : Nontrivial A
r : ℝ
hr : r > 0
hr_le : (algebraMap ℝ A : (a : ℝ) → A) r ≤ a
⊢ 0 ∉ spectrum ℝ b

Tactic:
exact fun h0 ↦ not_le_of_gt hr <| (algebraMap_le_iff_le_spectrum <| .of_nonneg <|
    h.nonneg.trans hab).1 (hr_le.trans hab) 0 h0

Premises used: algebraMap_le_iff_le_spectrum, Iff.mp, LE.le.trans, not_le_of_gt, OfNat.ofNat
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
ha : 0 ≤ a
hb : IsStrictlyPositive b
⊢ IsUnit b

Tactic:
hb.isUnit

Premises used: IsStrictlyPositive.isUnit
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
ha : 0 ≤ a
hb : IsStrictlyPositive b
lift : ∀ (b : Aˣ) (hb : IsStrictlyPositive (↑b : A)), a ≤ (↑b : A) ↔ ‖sqrt a * (↑b : A) ^ (-(1 / 2))‖ ≤ 1
⊢ a ≤ b ↔ ‖sqrt a * b ^ (-(1 / 2))‖ ≤ 1

Tactic:
lift b to Aˣ using hb.isUnit

Premises used: IsStrictlyPositive.isUnit
-- 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 : 0 ≤ a
b : Aˣ
hb : IsStrictlyPositive (↑b : A)
⊢ 0 ≤ (↑b : A) ^ (-(1 / 2)) * a * (↑b : A) ^ (-(1 / 2))

Tactic:
have hbab : 0 ≤ (b : A) ^ (-(1 / 2) : ℝ) * a * (b : A) ^ (-(1 / 2) : ℝ) :=
    conjugate_nonneg_of_nonneg ha rpow_nonneg
-- 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 : 0 ≤ a
b : Aˣ
hb : IsStrictlyPositive (↑b : A)
hbab : 0 ≤ (↑b : A) ^ (-(1 / 2)) * a * (↑b : A) ^ (-(1 / 2))
rw : (↑b : A) ^ (-(1 / 2)) * a * (↑b : A) ^ (-(1 / 2)) ≤ 1
| ‖sqrt a * (↑b : A) ^ (-(1 / 2))‖ ≤ 1

Tactic:
rw [← sq_le_one_iff₀ (norm_nonneg _), sq, ← CStarRing.norm_star_mul_self, star_mul,
      IsSelfAdjoint.of_nonneg (sqrt_nonneg a), IsSelfAdjoint.of_nonneg rpow_nonneg,
      ← mul_assoc, mul_assoc _ _ (sqrt a), sqrt_mul_sqrt_self a,
      CStarAlgebra.norm_le_one_iff_of_nonneg _ hbab]

Premises used: CFC.sqrt, mul_assoc, sq_le_one_iff₀, sq, IsSelfAdjoint.of_nonneg, CStarRing.norm_star_mul_self, StarMul.star_mul, CStarAlgebra.norm_le_one_iff_of_nonneg, CFC.sqrt_nonneg, CFC.sqrt_mul_sqrt_self, norm_nonneg
-- 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 : 0 ≤ a
b : Aˣ
hb : IsStrictlyPositive (↑b : A)
hbab : 0 ≤ (↑b : A) ^ (-(1 / 2)) * a * (↑b : A) ^ (-(1 / 2))
conv_rhs : a ≤ (↑b : A) ↔ (↑b : A) ^ (-(1 / 2)) * a * (↑b : A) ^ (-(1 / 2)) ≤ 1
⊢ a ≤ (↑b : A) ↔ ‖sqrt a * (↑b : A) ^ (-(1 / 2))‖ ≤ 1

Tactic:
conv_rhs =>
    rw [← sq_le_one_iff₀ (norm_nonneg _), sq, ← CStarRing.norm_star_mul_self, star_mul,
      IsSelfAdjoint.of_nonneg (sqrt_nonneg a), IsSelfAdjoint.of_nonneg rpow_nonneg,
      ← mul_assoc, mul_assoc _ _ (sqrt a), sqrt_mul_sqrt_self a,
      CStarAlgebra.norm_le_one_iff_of_nonneg _ hbab]

Premises used: CFC.sqrt, mul_assoc, sq_le_one_iff₀, sq, IsSelfAdjoint.of_nonneg, CStarRing.norm_star_mul_self, StarMul.star_mul, CStarAlgebra.norm_le_one_iff_of_nonneg, CFC.sqrt_nonneg, CFC.sqrt_mul_sqrt_self, norm_nonneg
-- 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 : 0 ≤ a
b : Aˣ
hb : IsStrictlyPositive (↑b : A)
hbab : 0 ≤ (↑b : A) ^ (-(1 / 2)) * a * (↑b : A) ^ (-(1 / 2))
⊢ a ≤ (↑b : A) ↔ (↑b : A) ^ (-(1 / 2)) * a * (↑b : A) ^ (-(1 / 2)) ≤ 1

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

Premises used: Iff.intro
-- 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 : 0 ≤ a
b : Aˣ
hb : IsStrictlyPositive (↑b : A)
hbab : 0 ≤ (↑b : A) ^ (-(1 / 2)) * a * (↑b : A) ^ (-(1 / 2))
refine_1 : ∀ (h : a ≤ (↑b : A)), (↑b : A) ^ (-(1 / 2)) * a * (↑b : A) ^ (-(1 / 2)) ≤ 1
refine_2 : ∀ (h : (↑b : A) ^ (-(1 / 2)) * a * (↑b : A) ^ (-(1 / 2)) ≤ 1), a ≤ (↑b : A)
⊢ a ≤ (↑b : A) ↔ (↑b : A) ^ (-(1 / 2)) * a * (↑b : A) ^ (-(1 / 2)) ≤ 1

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- 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 : 0 ≤ a
b : Aˣ
hb : IsStrictlyPositive (↑b : A)
hbab : 0 ≤ (↑b : A) ^ (-(1 / 2)) * a * (↑b : A) ^ (-(1 / 2))
h : a ≤ (↑b : A)
⊢ (↑b : A) ^ (-(1 / 2)) * a * (↑b : A) ^ (-(1 / 2)) ≤ (↑b : A) ^ (-(1 / 2)) * (↑b : A) * (↑b : A) ^ (-(1 / 2))

Tactic:
IsSelfAdjoint.of_nonneg rpow_nonneg |>.conjugate_le_conjugate h

Premises used: IsSelfAdjoint.conjugate_le_conjugate, IsSelfAdjoint.of_nonneg