-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
lemma le_iff_norm_sqrt_mul_rpow {a b : A} (hbu : IsUnit b) (ha : 0 ≤ a) (hb : 0 ≤ (b : A)) :
    a ≤ b ↔ ‖sqrt a * (b : A) ^ (-(1 / 2) : ℝ)‖ ≤ 1

Proof state:
case intro.refine_2
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
b : Aˣ
hb : 0 ≤ ↑b
hbab : 0 ≤ ↑b ^ (-(1 / 2)) * a * ↑b ^ (-(1 / 2))
h : ↑b ^ (-(1 / 2)) * a * ↑b ^ (-(1 / 2)) ≤ 1
⊢ a ≤ ↑b

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.zero_not_mem_spectrum ℝ≥0)]
    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)]

Result:
no goals

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
b : Aˣ
hb : 0 ≤ ↑b
hbab : 0 ≤ ↑b ^ (-(1 / 2)) * a * ↑b ^ (-(1 / 2))
h : ↑b ^ (-(1 / 2)) * a * ↑b ^ (-(1 / 2)) ≤ 1
⊢ a = sqrt ↑b * ↑b ^ (-(1 / 2)) * a * (↑b ^ (-(1 / 2)) * sqrt ↑b)

Tactic:
simp only [CFC.sqrt_eq_rpow .., ← CFC.rpow_add (b.zero_not_mem_spectrum ℝ≥0)]

Result:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
b : Aˣ
hb : 0 ≤ ↑b
hbab : 0 ≤ ↑b ^ (-(1 / 2)) * a * ↑b ^ (-(1 / 2))
h : ↑b ^ (-(1 / 2)) * a * ↑b ^ (-(1 / 2)) ≤ 1
⊢ a = ↑b ^ (1 / 2 + -(1 / 2)) * a * ↑b ^ (-(1 / 2) + 1 / 2)

Proof state:
case intro
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
b : Aˣ
hb : 0 ≤ ↑b
hbab : 0 ≤ ↑b ^ (-(1 / 2)) * a * ↑b ^ (-(1 / 2))
⊢ a ≤ ↑b ↔ ‖sqrt a * ↑b ^ (-(1 / 2))‖ ≤ 1

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

Result:
case intro
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
b : Aˣ
hb : 0 ≤ ↑b
hbab : 0 ≤ ↑b ^ (-(1 / 2)) * a * ↑b ^ (-(1 / 2))
⊢ a ≤ ↑b ↔ ↑b ^ (-(1 / 2)) * a * ↑b ^ (-(1 / 2)) ≤ 1

Proof state:
case intro
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
b : Aˣ
hb : 0 ≤ ↑b
hbab : 0 ≤ ↑b ^ (-(1 / 2)) * a * ↑b ^ (-(1 / 2))
⊢ a ≤ ↑b ↔ ↑b ^ (-(1 / 2)) * a * ↑b ^ (-(1 / 2)) ≤ 1

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

Result:
case intro.refine_1
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
b : Aˣ
hb : 0 ≤ ↑b
hbab : 0 ≤ ↑b ^ (-(1 / 2)) * a * ↑b ^ (-(1 / 2))
h : a ≤ ↑b
⊢ ↑b ^ (-(1 / 2)) * a * ↑b ^ (-(1 / 2)) ≤ 1

case intro.refine_2
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
b : Aˣ
hb : 0 ≤ ↑b
hbab : 0 ≤ ↑b ^ (-(1 / 2)) * a * ↑b ^ (-(1 / 2))
h : ↑b ^ (-(1 / 2)) * a * ↑b ^ (-(1 / 2)) ≤ 1
⊢ a ≤ ↑b

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
b : Aˣ
hb : 0 ≤ ↑b
hbab : 0 ≤ ↑b ^ (-(1 / 2)) * a * ↑b ^ (-(1 / 2))
h : ↑b ^ (-(1 / 2)) * a * ↑b ^ (-(1 / 2)) ≤ 1
⊢ a = ↑b ^ (1 / 2 + -(1 / 2)) * a * ↑b ^ (-(1 / 2) + 1 / 2)

Tactic:
norm_num

Result:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
b : Aˣ
hb : 0 ≤ ↑b
hbab : 0 ≤ ↑b ^ (-(1 / 2)) * a * ↑b ^ (-(1 / 2))
h : ↑b ^ (-(1 / 2)) * a * ↑b ^ (-(1 / 2)) ≤ 1
⊢ a = ↑b ^ 0 * a * ↑b ^ 0

Proof state:
case intro.refine_1
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
b : Aˣ
hb : 0 ≤ ↑b
hbab : 0 ≤ ↑b ^ (-(1 / 2)) * a * ↑b ^ (-(1 / 2))
h : a ≤ ↑b
⊢ ↑b ^ (-(1 / 2)) * a * ↑b ^ (-(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.isUnit

Result:
no goals

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
b : Aˣ
hb : 0 ≤ ↑b
hbab : 0 ≤ ↑b ^ (-(1 / 2)) * a * ↑b ^ (-(1 / 2))
h : ↑b ^ (-(1 / 2)) * a * ↑b ^ (-(1 / 2)) ≤ 1
⊢ a = ↑b ^ 0 * a * ↑b ^ 0

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

Result:
no goals

Proof state:
case intro
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
b : Aˣ
hb : 0 ≤ ↑b
⊢ a ≤ ↑b ↔ ‖sqrt a * ↑b ^ (-(1 / 2))‖ ≤ 1

Tactic:
have hbab : 0 ≤ (b : A) ^ (-(1 / 2) : ℝ) * a * (b : A) ^ (-(1 / 2) : ℝ) :=
  conjugate_nonneg_of_nonneg ha rpow_nonneg

Result:
case intro
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
b : Aˣ
hb : 0 ≤ ↑b
hbab : 0 ≤ ↑b ^ (-(1 / 2)) * a * ↑b ^ (-(1 / 2))
⊢ a ≤ ↑b ↔ ‖sqrt a * ↑b ^ (-(1 / 2))‖ ≤ 1

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
b : Aˣ
hb : 0 ≤ ↑b
hbab : 0 ≤ ↑b ^ (-(1 / 2)) * a * ↑b ^ (-(1 / 2))
h : ↑b ^ (-(1 / 2)) * a * ↑b ^ (-(1 / 2)) ≤ 1
⊢ sqrt ↑b * 1 * sqrt ↑b ≤ ↑b

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

Result:
no goals

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
b : Aˣ
hb : 0 ≤ ↑b
hbab : 0 ≤ ↑b ^ (-(1 / 2)) * a * ↑b ^ (-(1 / 2))
h : ↑b ^ (-(1 / 2)) * a * ↑b ^ (-(1 / 2)) ≤ 1
⊢ sqrt ↑b * ↑b ^ (-(1 / 2)) * a * (↑b ^ (-(1 / 2)) * sqrt ↑b) =
    sqrt ↑b * (↑b ^ (-(1 / 2)) * a * ↑b ^ (-(1 / 2))) * sqrt ↑b

Tactic:
simp only [mul_assoc]

Result:
no goals

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hbu : IsUnit b
ha : 0 ≤ a
hb : 0 ≤ b
⊢ a ≤ b ↔ ‖sqrt a * b ^ (-(1 / 2))‖ ≤ 1

Tactic:
lift b to Aˣ using hbu

Result:
case intro
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
b : Aˣ
hb : 0 ≤ ↑b
⊢ a ≤ ↑b ↔ ‖sqrt a * ↑b ^ (-(1 / 2))‖ ≤ 1