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
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)) * (↑b : A) * (↑b : A) ^ (-(1 / 2)) = 1

Tactic:
conjugate_rpow_neg_one_half (b : A)

Premises used: Units.val, CFC.conjugate_rpow_neg_one_half
-- 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)) ≤ 1

Tactic:
calc
      _ ≤ ↑b ^ (-(1 / 2) : ℝ) * (b : A) * ↑b ^ (-(1 / 2) : ℝ) :=
        IsSelfAdjoint.of_nonneg rpow_nonneg |>.conjugate_le_conjugate h
      _ = 1 := conjugate_rpow_neg_one_half (b : A)

Premises used: Units.val, HDiv.hDiv, IsSelfAdjoint.conjugate_le_conjugate, IsSelfAdjoint.of_nonneg, OfNat.ofNat, Neg.neg, CFC.conjugate_rpow_neg_one_half
-- 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 : (↑b : A) ^ (-(1 / 2)) * a * (↑b : A) ^ (-(1 / 2)) ≤ 1
simp : a = (↑b : A) ^ (1 / 2 + -(1 / 2)) * a * (↑b : A) ^ (-(1 / 2) + 1 / 2)
⊢ a = sqrt (↑b : A) * (↑b : A) ^ (-(1 / 2)) * a * ((↑b : A) ^ (-(1 / 2)) * sqrt (↑b : A))

Tactic:
simp only [CFC.sqrt_eq_rpow .., ← CFC.rpow_add b.isUnit]

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

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 : 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 = HPow.hPow (β := ℝ) (↑b : A) 0 * a * HPow.hPow (β := ℝ) (↑b : A) 0

Tactic:
simp [CFC.rpow_zero (b : A)]

Premises used: Units.val, 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 : 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
⊢ 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:
simp only [mul_assoc]

Premises used: mul_assoc
-- 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 : (↑b : A) ^ (-(1 / 2)) * a * (↑b : A) ^ (-(1 / 2)) ≤ 1
⊢ sqrt (↑b : A) * 1 * sqrt (↑b : A) ≤ (↑b : A)

Tactic:
simp [CFC.sqrt_mul_sqrt_self (b : A)]

Premises used: Units.val, CFC.sqrt_mul_sqrt_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 : 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₂ :
  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)
⊢ a ≤ (↑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)]

Premises used: HMul.hMul, CFC.sqrt, conjugate_le_conjugate_of_nonneg, HDiv.hDiv, HPow.hPow, LE.le.trans, CFC.sqrt_nonneg, OfNat.ofNat, Neg.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
b : Aˣ
ha : 0 ≤ a
hb : 0 ≤ (↑b : A)
⊢ Ne (α := ℝ) (-1) 0

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
b : Aˣ
ha : 0 ≤ a
hb : 0 ≤ (↑b : A)
rw : ‖sqrt a * (↑b : A) ^ (-(1 / 2))‖ ≤ 1 ↔ ‖sqrt a * (↑b : A) ^ (-1 * (1 / 2))‖ ≤ 1
⊢ a ≤ (↑b : A) ↔ ‖sqrt a * sqrt (↑b⁻¹ : A)‖ ≤ 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)]

Premises used: Units.val, CFC.sqrt_eq_rpow, CFC.rpow_rpow, CFC.rpow_neg_one_eq_inv, IsUnit.isStrictlyPositive, Units.isUnit, le_iff_norm_sqrt_mul_rpow
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
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)
⊢ ‖sqrt a * (↑b : A) ^ (-(1 / 2))‖ ≤ 1 ↔ ‖sqrt a * (↑b : A) ^ (-1 * (1 / 2))‖ ≤ 1

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 b : Aˣ
ha : 0 ≤ (↑a : A)
hab : (↑a : A) ≤ (↑b : A)
⊢ 0 ≤ (↑b : A)

Tactic:
have hb := ha.trans hab
-- 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 : A)
hab : (↑a : A) ≤ (↑b : A)
hb : 0 ≤ (↑b : A)
⊢ 0 ≤ (↑b⁻¹ : A)

Tactic:
have hb_inv : (0 : A) ≤ b⁻¹ := inv_nonneg_of_nonneg b hb
-- 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 : A)
hab : (↑a : A) ≤ (↑b : A)
hb : 0 ≤ (↑b : A)
hb_inv : 0 ≤ (↑b⁻¹ : A)
⊢ 0 ≤ (↑a⁻¹ : A)

Tactic:
have ha_inv : (0 : A) ≤ a⁻¹ := inv_nonneg_of_nonneg a ha
-- 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 : A)
hab : (↑a : A) ≤ (↑b : A)
hb : 0 ≤ (↑b : A)
hb_inv : 0 ≤ (↑b⁻¹ : A)
ha_inv : 0 ≤ (↑a⁻¹ : A)
⊢ ‖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

Premises used: sq_le_one_iff₀, sq, CStarRing.norm_star_mul_self, norm_nonneg, le_iff_norm_sqrt_mul_sqrt_inv
-- 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 : A)
hab : (↑a : A) ≤ (↑b : A)
hb : 0 ≤ (↑b : A)
hb_inv : 0 ≤ (↑b⁻¹ : A)
ha_inv : 0 ≤ (↑a⁻¹ : A)
hab₁ : ‖star (sqrt (↑a : A) * sqrt (↑b⁻¹ : A)) * (sqrt (↑a : A) * sqrt (↑b⁻¹ : A))‖ ≤ 1
⊢ 0 ≤ (↑b : A)

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

Premises used: sq_le_one_iff₀, sq, CStarRing.norm_star_mul_self, norm_nonneg, le_iff_norm_sqrt_mul_sqrt_inv
-- 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 : A)
hab : (↑a : A) ≤ (↑b : A)
hb : 0 ≤ (↑b : A)
hb_inv : 0 ≤ (↑b⁻¹ : A)
ha_inv : 0 ≤ (↑a⁻¹ : A)
hab₁ : ‖star (sqrt (↑a : A) * sqrt (↑b⁻¹ : A)) * (sqrt (↑a : A) * sqrt (↑b⁻¹ : A))‖ ≤ 1
hb₁ : 0 ≤ (↑b : A)
⊢ 0 ≤ (↑b⁻¹ : A)

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

Premises used: sq_le_one_iff₀, sq, CStarRing.norm_star_mul_self, norm_nonneg, le_iff_norm_sqrt_mul_sqrt_inv
-- 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 : A)
hab : (↑a : A) ≤ (↑b : A)
hb : 0 ≤ (↑b : A)
hb_inv : 0 ≤ (↑b⁻¹ : A)
ha_inv : 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)
⊢ 0 ≤ (↑a⁻¹ : A)

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

Premises used: sq_le_one_iff₀, sq, CStarRing.norm_star_mul_self, norm_nonneg, le_iff_norm_sqrt_mul_sqrt_inv
-- 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 : 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)
rw : ‖sqrt (↑b⁻¹ : A) * sqrt (↑a : A) * star (sqrt (↑b⁻¹ : A) * sqrt (↑a : A))‖ ≤ 1
⊢ (↑b⁻¹ : A) ≤ (↑a⁻¹ : A)

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]

Premises used: sq_le_one_iff₀, sq, CStarRing.norm_self_mul_star, inv_inv, norm_nonneg, le_iff_norm_sqrt_mul_sqrt_inv
-- 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 : 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
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
rwa₂ rwa₃ rwa₄ rwa₅ :
  ∀ (hab : ‖sqrt (↑b⁻¹ : A) * 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) * sqrt (↑b⁻¹ : A))‖ ≤ 1
⊢ ‖sqrt (↑b⁻¹ : A) * sqrt (↑a : A) * star (sqrt (↑b⁻¹ : A) * sqrt (↑a : A))‖ ≤ 1

Tactic:
rwa [star_mul, IsSelfAdjoint.of_nonneg (sqrt_nonneg _),
    IsSelfAdjoint.of_nonneg (sqrt_nonneg _)] at hab ⊢

Premises used: IsSelfAdjoint.of_nonneg, StarMul.star_mul
-- 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 : A)
hb : 0 ≤ (↑b : A)
⊢ (↑a⁻¹ : A) ≤ (↑b⁻¹ : A) ↔ (↑b : A) ≤ (↑a : A)

Tactic:
⟨CStarAlgebra.inv_le_inv (inv_nonneg_of_nonneg a ha), CStarAlgebra.inv_le_inv hb⟩

Premises used: CStarAlgebra.inv_le_inv, Iff.intro, CFC.inv_nonneg_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 b : Aˣ
ha : 0 ≤ (↑a : A)
hb : 0 ≤ (↑b : A)
⊢ (↑a⁻¹ : A) ≤ (↑b : A) ↔ (↑b⁻¹ : A) ≤ (↑a : A)

Tactic:
simpa using CStarAlgebra.inv_le_inv_iff ha (inv_nonneg_of_nonneg b hb)

Premises used: CStarAlgebra.inv_le_inv_iff, CFC.inv_nonneg_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 b : Aˣ
ha : 0 ≤ (↑a : A)
hb : 0 ≤ (↑b : A)
⊢ (↑a : A) ≤ (↑b⁻¹ : A) ↔ (↑b : A) ≤ (↑a⁻¹ : A)

Tactic:
simpa using CStarAlgebra.inv_le_inv_iff (inv_nonneg_of_nonneg a ha) hb

Premises used: CStarAlgebra.inv_le_inv_iff, CFC.inv_nonneg_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ˣ
ha : 0 ≤ (↑a : A)
⊢ LE.le.{u_1} (α := A) 0 (↑1 : 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 : 0 ≤ (↑a : A)
⊢ 1 ≤ (↑a⁻¹ : A) ↔ a ≤ 1

Tactic:
simpa using CStarAlgebra.le_inv_iff (a := 1) (by simp) ha

Premises used: CStarAlgebra.le_inv_iff
-- 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)
⊢ (↑a⁻¹ : A) ≤ 1 ↔ 1 ≤ a

Tactic:
simpa using CStarAlgebra.inv_le_iff ha (b := 1) (by simp)

Premises used: CStarAlgebra.inv_le_iff
-- 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 : 1 ≤ a
⊢ (↑a⁻¹ : A) ≤ 1

Tactic:
CStarAlgebra.inv_le_one_iff_one_le (zero_le_one.trans ha) |>.mpr ha

Premises used: Iff.mpr, zero_le_one, LE.le.trans, CStarAlgebra.inv_le_one_iff_one_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 : 1 ≤ (↑a⁻¹ : A)
⊢ (↑a : A) ≤ 1

Tactic:
simpa using CStarAlgebra.inv_le_one ha

Premises used: CStarAlgebra.inv_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 b : A
hab : a ≤ b
ha : IsStrictlyPositive a
⊢ IsUnit b

Tactic:
isUnit_of_le a hab

Premises used: CStarAlgebra.isUnit_of_le
-- 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
ha : IsStrictlyPositive a
lift : ∀ (b : Aˣ) (hab : a ≤ (↑b : A)), HPow.hPow (β := ℝ) (↑b : A) (-1) ≤ HPow.hPow (β := ℝ) a (-1)
⊢ HPow.hPow (β := ℝ) b (-1) ≤ HPow.hPow (β := ℝ) a (-1)

Tactic:
lift b to Aˣ using isUnit_of_le a hab

Premises used: CStarAlgebra.isUnit_of_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 : IsStrictlyPositive a
b : Aˣ
hab : a ≤ (↑b : 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
b : Aˣ
hab : a ≤ (↑b : A)
lift :
  ∀ (a : Aˣ) (ha : IsStrictlyPositive (↑a : A)) (hab : (↑a : A) ≤ (↑b : A)),
    HPow.hPow (β := ℝ) (↑b : A) (-1) ≤ HPow.hPow (β := ℝ) (↑a : A) (-1)
⊢ HPow.hPow (β := ℝ) (↑b : A) (-1) ≤ HPow.hPow (β := ℝ) a (-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
b a : Aˣ
ha : IsStrictlyPositive (↑a : A)
hab : (↑a : A) ≤ (↑b : A)
rw : (↑b⁻¹ : A) ≤ (↑a⁻¹ : A)
⊢ HPow.hPow (β := ℝ) (↑b : A) (-1) ≤ HPow.hPow (β := ℝ) (↑a : A) (-1)

Tactic:
rw [rpow_neg_one_eq_inv a, rpow_neg_one_eq_inv b (ha.nonneg.trans hab)]

Premises used: CFC.rpow_neg_one_eq_inv, LE.le.trans, IsStrictlyPositive.nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
b a : Aˣ
ha : IsStrictlyPositive (↑a : A)
hab : (↑a : A) ≤ (↑b : A)
⊢ (↑b⁻¹ : A) ≤ (↑a⁻¹ : A)

Tactic:
CStarAlgebra.inv_le_inv ha.nonneg hab

Premises used: CStarAlgebra.inv_le_inv, IsStrictlyPositive.nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
b a : Aˣ
ha : IsStrictlyPositive (↑a : A)
hab : (↑a : A) ≤ (↑b : A)
⊢ (↑b⁻¹ : A) ≤ (↑a⁻¹ : A)

Tactic:
exact CStarAlgebra.inv_le_inv ha.nonneg hab

Premises used: CStarAlgebra.inv_le_inv, IsStrictlyPositive.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 : 1 ≤ a
⊢ IsUnit a

Tactic:
isUnit_of_le 1 ha

Premises used: CStarAlgebra.isUnit_of_le, 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
ha : 1 ≤ a
lift : ∀ (a : Aˣ) (ha : 1 ≤ (↑a : A)), HPow.hPow (β := ℝ) (↑a : A) (-1) ≤ 1
⊢ HPow.hPow (β := ℝ) a (-1) ≤ 1

Tactic:
lift a to Aˣ using isUnit_of_le 1 ha

Premises used: CStarAlgebra.isUnit_of_le, 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ˣ
ha : 1 ≤ (↑a : A)
rw : (↑a⁻¹ : A) ≤ 1
⊢ HPow.hPow (β := ℝ) (↑a : A) (-1) ≤ 1

Tactic:
rw [rpow_neg_one_eq_inv a (zero_le_one.trans ha)]

Premises used: CFC.rpow_neg_one_eq_inv, zero_le_one, LE.le.trans
-- 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 : 1 ≤ (↑a : A)
⊢ (↑a⁻¹ : A) ≤ 1

Tactic:
inv_le_one ha

Premises used: CStarAlgebra.inv_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 : 1 ≤ (↑a : A)
⊢ (↑a⁻¹ : A) ≤ 1

Tactic:
exact inv_le_one ha

Premises used: CStarAlgebra.inv_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 b : A
ha : IsStrictlyPositive a
hab : a ≤ b
⊢ IsStrictlyPositive b

Tactic:
⟨ha.nonneg.trans hab, CStarAlgebra.isUnit_of_le a hab⟩

Premises used: CStarAlgebra.isUnit_of_le, And.intro, LE.le.trans, IsStrictlyPositive.nonneg, IsStrictlyPositive
-- 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 : IsStrictlyPositive a
hb : 0 ≤ b
⊢ IsStrictlyPositive (a + b)

Tactic:
IsStrictlyPositive.of_le ha ((le_add_iff_nonneg_right a).mpr hb)

Premises used: Iff.mpr, le_add_iff_nonneg_right, IsStrictlyPositive.of_le
-- 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
⊢ IsStrictlyPositive (a + b)

Tactic:
add_comm a b ▸ hb.add_nonneg ha

Premises used: Eq.rec, add_comm, Eq.symm, IsStrictlyPositive.add_nonneg
-- 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
h : IsStrictlyPositive a ∧ 0 ≤ b ∨ 0 ≤ a ∧ IsStrictlyPositive b
⊢ IsStrictlyPositive (a + b)

Tactic:
grind [IsStrictlyPositive.add_nonneg, IsStrictlyPositive.nonneg_add]

Premises used: IsStrictlyPositive.add_nonneg, IsStrictlyPositive.nonneg_add
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
IsStrictlyPositive :
  ∀ (apos : _root_.IsStrictlyPositive a) ⦃b : A⦄,
    Membership.mem (γ := Set A) {a : A | _root_.IsStrictlyPositive a} b → a ≤ b → Ring.inverse b ≤ Ring.inverse a
⊢ Membership.mem (γ := Set A) {a : A | _root_.IsStrictlyPositive a} a →
    ∀ ⦃b : A⦄,
      Membership.mem (γ := Set A) {a : A | _root_.IsStrictlyPositive a} b → a ≤ b → Ring.inverse b ≤ Ring.inverse a

Tactic:
(apos : IsStrictlyPositive a)
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
apos : _root_.IsStrictlyPositive a
b : A
IsStrictlyPositive : ∀ (bpos : _root_.IsStrictlyPositive b), a ≤ b → Ring.inverse b ≤ Ring.inverse a
⊢ Membership.mem (γ := Set A) {a : A | _root_.IsStrictlyPositive a} b → a ≤ b → Ring.inverse b ≤ Ring.inverse a

Tactic:
(bpos : IsStrictlyPositive b)
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
apos : IsStrictlyPositive a
b : A
bpos : IsStrictlyPositive b
hab : a ≤ b
⊢ IsUnit b

Tactic:
grind
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
apos : IsStrictlyPositive a
b : A
bpos : IsStrictlyPositive b
hab : a ≤ b
⊢ IsUnit a

Tactic:
grind
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
apos : IsStrictlyPositive a
b : A
bpos : IsStrictlyPositive b
hab : a ≤ b
rw : (↑⋯.unit⁻¹ : A) ≤ (↑⋯.unit⁻¹ : A)
⊢ Ring.inverse b ≤ Ring.inverse a

Tactic:
rw [Ring.inverse_of_isUnit (by grind), Ring.inverse_of_isUnit (by grind)]

Premises used: Ring.inverse_of_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
apos : IsStrictlyPositive a
b : A
bpos : IsStrictlyPositive b
hab : a ≤ b
⊢ (↑⋯.unit⁻¹ : A) ≤ (↑⋯.unit⁻¹ : A)

Tactic:
CStarAlgebra.inv_le_inv (Units.isStrictlyPositive_iff.mp apos) hab

Premises used: CStarAlgebra.inv_le_inv, Iff.mp, Units.isStrictlyPositive_iff
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
apos : IsStrictlyPositive a
b : A
bpos : IsStrictlyPositive b
hab : a ≤ b
⊢ (↑⋯.unit⁻¹ : A) ≤ (↑⋯.unit⁻¹ : A)

Tactic:
exact CStarAlgebra.inv_le_inv (Units.isStrictlyPositive_iff.mp apos) hab

Premises used: CStarAlgebra.inv_le_inv, Iff.mp, Units.isStrictlyPositive_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
ha : IsStrictlyPositive a
⊢ b⁻¹ʳ ≤ a⁻¹ʳ

Tactic:
antitoneOn_ringInverse ha (IsStrictlyPositive.of_le ha hab) hab

Premises used: CStarAlgebra.antitoneOn_ringInverse, IsStrictlyPositive.of_le