-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
lemma conjugate_le_norm_smul {a b : A} (hb : IsSelfAdjoint b

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hb : autoParam (IsSelfAdjoint b) _auto✝
this : ∀ (a b : Unitization ℂ A), IsSelfAdjoint b → star a * b * a ≤ ‖b‖ • (star a * a)
⊢ star a * b * a ≤ ‖b‖ • (star a * a)

Tactic:
rw [← Unitization.inr_le_iff _ _ (by aesop) ((IsSelfAdjoint.all _).smul (.star_mul_self a))]

Result:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hb : autoParam (IsSelfAdjoint b) _auto✝
this : ∀ (a b : Unitization ℂ A), IsSelfAdjoint b → star a * b * a ≤ ‖b‖ • (star a * a)
⊢ ↑(star a * b * a) ≤ ↑(‖b‖ • (star a * a))

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hb : autoParam (IsSelfAdjoint b) _auto✝
⊢ ∀ (a b : Unitization ℂ A), IsSelfAdjoint b → star a * b * a ≤ ‖b‖ • (star a * a)

Tactic:
intro a b hb

Result:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a✝ b✝ : A
hb✝ : autoParam (IsSelfAdjoint b✝) _auto✝
a b : Unitization ℂ A
hb : IsSelfAdjoint b
⊢ star a * b * a ≤ ‖b‖ • (star a * a)

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hb : autoParam (IsSelfAdjoint b) _auto✝
⊢ star a * b * a ≤ ‖b‖ • (star a * a)

Tactic:
suffices ∀ a b : A⁺¹, IsSelfAdjoint b → star a * b * a ≤ ‖b‖ • (star a * a) by
  rw [← Unitization.inr_le_iff _ _ (by aesop) ((IsSelfAdjoint.all _).smul (.star_mul_self a))]
  simpa [Unitization.norm_inr] using this a b <| hb.inr ℂ

Result:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hb : autoParam (IsSelfAdjoint b) _auto✝
⊢ ∀ (a b : Unitization ℂ A), IsSelfAdjoint b → star a * b * a ≤ ‖b‖ • (star a * a)

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hb : autoParam (IsSelfAdjoint b) _auto✝
this : ∀ (a b : Unitization ℂ A), IsSelfAdjoint b → star a * b * a ≤ ‖b‖ • (star a * a)
⊢ IsSelfAdjoint (star a * b * a)

Tactic:
aesop

Result:
no goals

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a✝ b✝ : A
hb✝ : autoParam (IsSelfAdjoint b✝) _auto✝
a b : Unitization ℂ A
hb : IsSelfAdjoint b
⊢ star a * (algebraMap ℝ (Unitization ℂ A)) ‖b‖ * a = ‖b‖ • (star a * a)

Tactic:
simp [Algebra.algebraMap_eq_smul_one]

Result:
no goals

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hb : autoParam (IsSelfAdjoint b) _auto✝
this : ∀ (a b : Unitization ℂ A), IsSelfAdjoint b → star a * b * a ≤ ‖b‖ • (star a * a)
⊢ ↑(star a * b * a) ≤ ↑(‖b‖ • (star a * a))

Tactic:
simpa [Unitization.norm_inr] using this a b <| hb.inr ℂ

Result:
no goals

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a✝ b✝ : A
hb✝ : autoParam (IsSelfAdjoint b✝) _auto✝
a b : Unitization ℂ A
hb : IsSelfAdjoint b
⊢ star a * b * a ≤ ‖b‖ • (star a * a)

Tactic:
calc
  star a * b * a ≤ star a * (algebraMap ℝ A⁺¹ ‖b‖) * a :=
    conjugate_le_conjugate hb.le_algebraMap_norm_self _
  _ = ‖b‖ • (star a * a) := by simp [Algebra.algebraMap_eq_smul_one]

Result:
no goals