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 : 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 > 0, ∀ x ∈ spectrum ℝ a, r ≤ x
have refine_2 : ∀ (r : ℝ) (hr : r ∈ spectrum ℝ a) (hr_min : IsMinOn id (spectrum ℝ a) r), ∃ r > 0, ∀ x ∈ spectrum ℝ a, r ≤ x
Tactic: obtain ⟨r, hr, hr_min⟩ := h_cpct.exists_isMinOn
      (ContinuousFunctionalCalculus.spectrum_nonempty a ha) continuousOn_id
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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‖
have pos : ∀ (nontriv : Nontrivial A), a ≤ (algebraMap ℝ A : (a : ℝ) → A) ‖a‖
Tactic: by_cases! nontriv : Nontrivial A
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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‖
⊢ a ≤ (algebraMap ℝ A : (a : ℝ) → A) ‖a‖
have neg : ∀ (nontriv : Subsingleton A), a ≤ (algebraMap ℝ A : (a : ℝ) → A) ‖a‖
Tactic: by_cases! nontriv : Nontrivial A
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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‖
have pos : ∀ (r : ℝ) (hr : r ∈ spectrum ℝ a), r ≤ ‖a‖
Tactic: refine le_algebraMap_of_spectrum_le fun r hr => ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
⊢ -(algebraMap ℝ A : (a : ℝ) → A) ‖a‖ ≤ a
have rw : -a ≤ (algebraMap ℝ A : (a : ℝ) → A) ‖-a‖
Tactic: rw [neg_le, ← norm_neg]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (hypothesis)
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) (HPow.hPow (β := ℕ) ‖a‖ 2)
have this : 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
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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‖
⊢ a * star a ≤ (algebraMap ℝ A : (a : ℝ) → A) (HPow.hPow (β := ℕ) ‖a‖ 2)
have rwa : ∀ (this : a * star a ≤ (algebraMap ℝ A : (a : ℝ) → A) (‖a‖ * ‖a‖)),
  a * star a ≤ (algebraMap ℝ A : (a : ℝ) → A) (HPow.hPow (β := ℕ) ‖a‖ 2)
Tactic: rwa [CStarRing.norm_self_mul_star, ← pow_two] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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)
⊢ a * star a ≤ (algebraMap ℝ A : (a : ℝ) → A) (HPow.hPow (β := ℕ) ‖a‖ 2)
have rwa₁ : ∀ (this : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (hypothesis)
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) (HPow.hPow (β := ℕ) ‖a‖ 2)
have this : 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
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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‖
⊢ star a * a ≤ (algebraMap ℝ A : (a : ℝ) → A) (HPow.hPow (β := ℕ) ‖a‖ 2)
have rwa : ∀ (this : star a * a ≤ (algebraMap ℝ A : (a : ℝ) → A) (‖a‖ * ‖a‖)),
  star a * a ≤ (algebraMap ℝ A : (a : ℝ) → A) (HPow.hPow (β := ℕ) ‖a‖ 2)
Tactic: rwa [CStarRing.norm_star_mul_self, ← pow_two] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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)
⊢ star a * a ≤ (algebraMap ℝ A : (a : ℝ) → A) (HPow.hPow (β := ℕ) ‖a‖ 2)
have rwa₁ : ∀ (this : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : Nontrivial A
a : A
ha : IsSelfAdjoint a
⊢ ‖a‖ ∈ spectrum ℝ a ∨ -‖a‖ ∈ spectrum ℝ a
have ha' : SpectrumRestricts (R := ℝ) (S := ℂ) a (⇑Complex.reCLM : (a : ℂ) → ℝ)
Tactic: have ha' : SpectrumRestricts a Complex.reCLM := ha.spectrumRestricts
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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 : ℂ) → ℝ)
⊢ ‖a‖ ∈ spectrum ℝ a ∨ -‖a‖ ∈ spectrum ℝ a
have rw : (spectralRadius ℝ a).toReal ∈ spectrum ℝ a ∨ -(spectralRadius ℝ a).toReal ∈ spectrum ℝ a
Tactic: rw [← ha.toReal_spectralRadius_eq_norm]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (hypothesis)
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 ℝ≥0 a
have this : IsSelfAdjoint a
Tactic: have : IsSelfAdjoint a := .of_nonneg ha
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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‖₊ ∈ spectrum ℝ≥0 a
have h : ‖a‖₊ = (spectralRadius ℝ a).toNNReal
Tactic: convert! NNReal.spectralRadius_mem_spectrum (a := a) ?_ (.nnreal_of_nonneg ha)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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
⊢ ‖a‖₊ ∈ spectrum ℝ≥0 a
have convert! : (spectrum ℝ a).Nonempty
Tactic: convert! NNReal.spectralRadius_mem_spectrum (a := a) ?_ (.nnreal_of_nonneg ha)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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
⊢ ‖a‖ ≤ r ↔ a ≤ (algebraMap ℝ A : (a : ℝ) → A) r
have rw : ‖a‖ ≤ r ↔ ∀ x ∈ spectrum ℝ a, x ≤ r
Tactic: rw [le_algebraMap_iff_spectrum_le]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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
⊢ ‖a‖ ≤ r ↔ ∀ x ∈ spectrum ℝ a, x ≤ r
have inl : ∀ (h : Subsingleton A), ‖a‖ ≤ r ↔ ∀ x ∈ spectrum ℝ a, x ≤ r
Tactic: obtain (h | _) := subsingleton_or_nontrivial A
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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
⊢ ‖a‖ ≤ r ↔ ∀ x ∈ spectrum ℝ a, x ≤ r
have inr : Nontrivial A → (‖a‖ ≤ r ↔ ∀ x ∈ spectrum ℝ a, x ≤ r)
Tactic: obtain (h | _) := subsingleton_or_nontrivial A
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
r : ℝ
hr : 0 ≤ r
⊢ Membership.mem (γ := Set A) (Icc 0 ((algebraMap ℝ A : (a : ℝ) → A) r) : Set A) x ↔ 0 ≤ x ∧ ‖x‖ ≤ r
have rw : 0 ≤ x → (‖x‖ ≤ r ↔ x ≤ (algebraMap ℝ A : (a : ℝ) → A) r)
Tactic: rw [mem_Icc, and_congr_right_iff, iff_comm]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsStrictlyPositive a
⊢ a ^ (-(1 / 2)) * a * a ^ (-(1 / 2)) = 1
have lift : ∀ (a : Aˣ) (ha : IsStrictlyPositive (↑a : A)), (↑a : A) ^ (-(1 / 2)) * (↑a : A) * (↑a : A) ^ (-(1 / 2)) = 1
Tactic: lift a to Aˣ using ha.isUnit
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : Aˣ
ha : IsStrictlyPositive (↑a : A)
⊢ (↑a : A) ^ (-(1 / 2)) * (↑a : A) * (↑a : A) ^ (-(1 / 2)) = 1
have nth_rw : (↑a : A) ^ (-(1 / 2)) * HPow.hPow (β := ℝ) (↑a : A) 1 * (↑a : A) ^ (-(1 / 2)) = 1
Tactic: nth_rw 2 [← rpow_one (a : A)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : Aˣ
ha : IsStrictlyPositive (↑a : A)
⊢ (↑a : A) ^ (-(1 / 2)) * HPow.hPow (β := ℝ) (↑a : A) 1 * (↑a : A) ^ (-(1 / 2)) = 1
have simp : (↑a : A) ^ (-(1 / 2) + 1 + -(1 / 2)) = 1
Tactic: simp only [← rpow_add a.isUnit]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : Aˣ
ha : IsStrictlyPositive (↑a : A)
⊢ (↑a : A) ^ (-(1 / 2) + 1 + -(1 / 2)) = 1
have norm_num : HPow.hPow (β := ℝ) (↑a : A) 0 = 1
Tactic: norm_num
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (hypothesis)
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
⊢ IsUnit b
have a₁ : Nontrivial A
Tactic: nontriviality A
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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
⊢ IsUnit b
have rw : 0 ∉ spectrum ℝ b
Tactic: rw [← spectrum.zero_notMem_iff ℝ]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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
⊢ 0 ∉ spectrum ℝ b
have obtain : ∀ (r : ℝ) (hr : r > 0) (hr_le : (algebraMap ℝ A : (a : ℝ) → A) r ≤ a), 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
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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
⊢ a ≤ b ↔ ‖sqrt a * b ^ (-(1 / 2))‖ ≤ 1
have lift : ∀ (b : Aˣ) (hb : IsStrictlyPositive (↑b : A)), a ≤ (↑b : A) ↔ ‖sqrt a * (↑b : A) ^ (-(1 / 2))‖ ≤ 1
Tactic: lift b to Aˣ using hb.isUnit
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (hypothesis)
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)
⊢ a ≤ (↑b : A) ↔ ‖sqrt a * (↑b : A) ^ (-(1 / 2))‖ ≤ 1
have hbab : 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
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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))
| ‖sqrt a * (↑b : A) ^ (-(1 / 2))‖ ≤ 1
have rw : (↑b : A) ^ (-(1 / 2)) * 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]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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) ↔ ‖sqrt a * (↑b : A) ^ (-(1 / 2))‖ ≤ 1
have conv_rhs : a ≤ (↑b : A) ↔ (↑b : A) ^ (-(1 / 2)) * 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]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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
have refine_1 : ∀ (h : a ≤ (↑b : A)), (↑b : A) ^ (-(1 / 2)) * a * (↑b : A) ^ (-(1 / 2)) ≤ 1
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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
⊢ a ≤ (↑b : A) ↔ (↑b : A) ^ (-(1 / 2)) * a * (↑b : A) ^ (-(1 / 2)) ≤ 1
have refine_2 : ∀ (h : (↑b : A) ^ (-(1 / 2)) * a * (↑b : A) ^ (-(1 / 2)) ≤ 1), a ≤ (↑b : A)
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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 : (↑b : A) ^ (-(1 / 2)) * a * (↑b : A) ^ (-(1 / 2)) ≤ 1
⊢ a = sqrt (↑b : A) * (↑b : A) ^ (-(1 / 2)) * a * ((↑b : A) ^ (-(1 / 2)) * sqrt (↑b : A))
have simp : a = (↑b : A) ^ (1 / 2 + -(1 / 2)) * a * (↑b : A) ^ (-(1 / 2) + 1 / 2)
Tactic: simp only [CFC.sqrt_eq_rpow .., ← CFC.rpow_add b.isUnit]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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 : (↑b : A) ^ (-(1 / 2)) * a * (↑b : A) ^ (-(1 / 2)) ≤ 1
⊢ a = (↑b : A) ^ (1 / 2 + -(1 / 2)) * a * (↑b : A) ^ (-(1 / 2) + 1 / 2)
have norm_num : a = HPow.hPow (β := ℝ) (↑b : A) 0 * a * HPow.hPow (β := ℝ) (↑b : A) 0
Tactic: norm_num
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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 : (↑b : A) ^ (-(1 / 2)) * a * (↑b : A) ^ (-(1 / 2)) ≤ 1
⊢ a ≤ (↑b : A)
have a₁ : a = sqrt (↑b : A) * (↑b : A) ^ (-(1 / 2)) * a * ((↑b : A) ^ (-(1 / 2)) * sqrt (↑b : A))
Tactic: calc
      a = (sqrt ↑b * ↑b ^ (-(1 / 2) : ℝ)) * a * (↑b ^ (-(1 / 2) : ℝ) * sqrt ↑b) := by
        simp only [CFC.sqrt_eq_rpow .., ← CFC.rpow_add b.isUnit]
        norm_num
        simp [CFC.rpow_zero (b : A)]
      _ = sqrt ↑b * (↑b ^ (-(1 / 2) : ℝ) * a * ↑b ^ (-(1 / 2) : ℝ)) * sqrt ↑b := by
        simp only [mul_assoc]
      _ ≤ b := conjugate_le_conjugate_of_nonneg h (sqrt_nonneg _) |>.trans <| by
        simp [CFC.sqrt_mul_sqrt_self (b : A)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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 : (↑b : A) ^ (-(1 / 2)) * a * (↑b : A) ^ (-(1 / 2)) ≤ 1
a₁ : a = sqrt (↑b : A) * (↑b : A) ^ (-(1 / 2)) * a * ((↑b : A) ^ (-(1 / 2)) * sqrt (↑b : A))
⊢ a ≤ (↑b : A)
have a₂ : sqrt (↑b : A) * (↑b : A) ^ (-(1 / 2)) * a * ((↑b : A) ^ (-(1 / 2)) * sqrt (↑b : A)) =
  sqrt (↑b : A) * ((↑b : A) ^ (-(1 / 2)) * a * (↑b : A) ^ (-(1 / 2))) * sqrt (↑b : A)
Tactic: calc
      a = (sqrt ↑b * ↑b ^ (-(1 / 2) : ℝ)) * a * (↑b ^ (-(1 / 2) : ℝ) * sqrt ↑b) := by
        simp only [CFC.sqrt_eq_rpow .., ← CFC.rpow_add b.isUnit]
        norm_num
        simp [CFC.rpow_zero (b : A)]
      _ = sqrt ↑b * (↑b ^ (-(1 / 2) : ℝ) * a * ↑b ^ (-(1 / 2) : ℝ)) * sqrt ↑b := by
        simp only [mul_assoc]
      _ ≤ b := conjugate_le_conjugate_of_nonneg h (sqrt_nonneg _) |>.trans <| by
        simp [CFC.sqrt_mul_sqrt_self (b : A)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
b : Aˣ
ha : 0 ≤ a
hb : 0 ≤ (↑b : A)
⊢ a ≤ (↑b : A) ↔ ‖sqrt a * sqrt (↑b⁻¹ : A)‖ ≤ 1
have rw : ‖sqrt a * (↑b : A) ^ (-(1 / 2))‖ ≤ 1 ↔ ‖sqrt a * (↑b : A) ^ (-1 * (1 / 2))‖ ≤ 1
Tactic: rw [CFC.sqrt_eq_rpow (a := (↑b⁻¹ : A)), ← CFC.rpow_neg_one_eq_inv b,
    CFC.rpow_rpow (b : A) _ _ (by simp),
    le_iff_norm_sqrt_mul_rpow a (hb := b.isUnit.isStrictlyPositive hb)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : Aˣ
ha : 0 ≤ (↑a : A)
hab : (↑a : A) ≤ (↑b : A)
⊢ (↑b⁻¹ : A) ≤ (↑a⁻¹ : A)
have hb : 0 ≤ (↑b : A)
Tactic: have hb := ha.trans hab
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : Aˣ
ha : 0 ≤ (↑a : A)
hab : (↑a : A) ≤ (↑b : A)
hb : 0 ≤ (↑b : A)
⊢ (↑b⁻¹ : A) ≤ (↑a⁻¹ : A)
have hb_inv : 0 ≤ (↑b⁻¹ : A)
Tactic: have hb_inv : (0 : A) ≤ b⁻¹ := inv_nonneg_of_nonneg b hb
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : Aˣ
ha : 0 ≤ (↑a : A)
hab : (↑a : A) ≤ (↑b : A)
hb : 0 ≤ (↑b : A)
hb_inv : 0 ≤ (↑b⁻¹ : A)
⊢ (↑b⁻¹ : A) ≤ (↑a⁻¹ : A)
have ha_inv : 0 ≤ (↑a⁻¹ : A)
Tactic: have ha_inv : (0 : A) ≤ a⁻¹ := inv_nonneg_of_nonneg a ha
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : Aˣ
ha : 0 ≤ (↑a : A)
hab : (↑a : A) ≤ (↑b : A)
hb : 0 ≤ (↑b : A)
hb_inv : 0 ≤ (↑b⁻¹ : A)
ha_inv : 0 ≤ (↑a⁻¹ : A)
⊢ (↑b⁻¹ : A) ≤ (↑a⁻¹ : A)
have hab₁ : ‖star (sqrt (↑a : A) * sqrt (↑b⁻¹ : A)) * (sqrt (↑a : A) * sqrt (↑b⁻¹ : A))‖ ≤ 1
Tactic: rw [le_iff_norm_sqrt_mul_sqrt_inv ha hb, ← sq_le_one_iff₀ (norm_nonneg _), sq,
    ← CStarRing.norm_star_mul_self] at hab
Cleared hypotheses: hab, hb, hb_inv, ha_inv
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : Aˣ
ha : 0 ≤ (↑a : A)
hab : ‖star (sqrt (↑a : A) * sqrt (↑b⁻¹ : A)) * (sqrt (↑a : A) * sqrt (↑b⁻¹ : A))‖ ≤ 1
hb : 0 ≤ (↑b : A)
hb_inv : 0 ≤ (↑b⁻¹ : A)
ha_inv : 0 ≤ (↑a⁻¹ : A)
⊢ (↑b⁻¹ : A) ≤ (↑a⁻¹ : A)
have rw : ‖sqrt (↑b⁻¹ : A) * sqrt (↑a : A) * star (sqrt (↑b⁻¹ : A) * sqrt (↑a : A))‖ ≤ 1
Tactic: rw [le_iff_norm_sqrt_mul_sqrt_inv hb_inv ha_inv, inv_inv, ← sq_le_one_iff₀ (norm_nonneg _), sq,
    ← CStarRing.norm_self_mul_star]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : Aˣ
ha : 0 ≤ (↑a : A)
hab : ‖star (sqrt (↑a : A) * sqrt (↑b⁻¹ : A)) * (sqrt (↑a : A) * sqrt (↑b⁻¹ : A))‖ ≤ 1
hb : 0 ≤ (↑b : A)
hb_inv : 0 ≤ (↑b⁻¹ : A)
ha_inv : 0 ≤ (↑a⁻¹ : A)
⊢ ‖sqrt (↑b⁻¹ : A) * sqrt (↑a : A) * star (sqrt (↑b⁻¹ : A) * sqrt (↑a : A))‖ ≤ 1
have rwa : ∀ (hab : ‖star (sqrt (↑b⁻¹ : A)) * star (sqrt (↑a : A)) * (sqrt (↑a : A) * sqrt (↑b⁻¹ : A))‖ ≤ 1) (hb : 0 ≤ (↑b : A))
  (hb_inv : 0 ≤ (↑b⁻¹ : A)) (ha_inv : 0 ≤ (↑a⁻¹ : A)),
  ‖sqrt (↑b⁻¹ : A) * sqrt (↑a : A) * (star (sqrt (↑a : A)) * star (sqrt (↑b⁻¹ : A)))‖ ≤ 1
Tactic: rwa [star_mul, IsSelfAdjoint.of_nonneg (sqrt_nonneg _),
    IsSelfAdjoint.of_nonneg (sqrt_nonneg _)] at hab ⊢
Cleared hypotheses: hab, hb, hb_inv, ha_inv
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : Aˣ
ha : 0 ≤ (↑a : A)
hab : ‖star (sqrt (↑a : A) * sqrt (↑b⁻¹ : A)) * (sqrt (↑a : A) * sqrt (↑b⁻¹ : A))‖ ≤ 1
hb : 0 ≤ (↑b : A)
hb_inv : 0 ≤ (↑b⁻¹ : A)
ha_inv : 0 ≤ (↑a⁻¹ : A)
rwa :
  ∀ (hab : ‖star (sqrt (↑b⁻¹ : A)) * star (sqrt (↑a : A)) * (sqrt (↑a : A) * sqrt (↑b⁻¹ : A))‖ ≤ 1) (hb : 0 ≤ (↑b : A))
    (hb_inv : 0 ≤ (↑b⁻¹ : A)) (ha_inv : 0 ≤ (↑a⁻¹ : A)),
    ‖sqrt (↑b⁻¹ : A) * sqrt (↑a : A) * (star (sqrt (↑a : A)) * star (sqrt (↑b⁻¹ : A)))‖ ≤ 1
⊢ ‖sqrt (↑b⁻¹ : A) * sqrt (↑a : A) * star (sqrt (↑b⁻¹ : A) * sqrt (↑a : A))‖ ≤ 1
have rwa₁ : ∀ (hab : ‖sqrt (↑b⁻¹ : A) * star (sqrt (↑a : A)) * (sqrt (↑a : A) * sqrt (↑b⁻¹ : A))‖ ≤ 1) (hb : 0 ≤ (↑b : A))
  (hb_inv : 0 ≤ (↑b⁻¹ : A)) (ha_inv : 0 ≤ (↑a⁻¹ : A)),
  ‖sqrt (↑b⁻¹ : A) * sqrt (↑a : A) * (sqrt (↑a : A) * star (sqrt (↑b⁻¹ : A)))‖ ≤ 1
Tactic: rwa [star_mul, IsSelfAdjoint.of_nonneg (sqrt_nonneg _),
    IsSelfAdjoint.of_nonneg (sqrt_nonneg _)] at hab ⊢
Cleared hypotheses: hab, hb, hb_inv, ha_inv