-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
lemma norm_le_norm_of_nonneg_of_le {a b : A} (ha : 0 ≤ a

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a✝ b✝ : A
ha✝ : autoParam (0 ≤ a✝) _auto✝
hab✝ : a✝ ≤ b✝
a b : Unitization ℂ A
ha : 0 ≤ a
hab : a ≤ b
hb : 0 ≤ b
this✝ : IsSelfAdjoint a
this : IsSelfAdjoint b
⊢ cfc id a ≤ cfc (fun x => ‖b‖) a

Tactic:
calc _ = a := by rw [cfc_id ℝ a]
  _ ≤ cfc id b := (cfc_id ℝ b) ▸ hab
  _ ≤ cfc (fun _ => ‖b‖) b := by
      refine cfc_mono fun x hx => ?_
      calc x = ‖x‖ := (Real.norm_of_nonneg (spectrum_nonneg_of_nonneg hb hx)).symm
        _ ≤ ‖b‖ := spectrum.norm_le_norm_of_mem hx
  _ = _ := by rw [cfc_const _ _, cfc_const _ _]

Result:
no goals

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a✝ b✝ : A
ha✝ : autoParam (0 ≤ a✝) _auto✝
hab✝ : a✝ ≤ b✝
a b : Unitization ℂ A
ha : 0 ≤ a
hab : a ≤ b
hb : 0 ≤ b
this✝ : IsSelfAdjoint a
this : IsSelfAdjoint b
h₂ : ∀ x ∈ spectrum ℝ a, id x ≤ ‖b‖
⊢ ‖a‖ ≤ ‖b‖

Tactic:
exact h₂ ‖a‖ <| norm_mem_spectrum_of_nonneg ha

Result:
no goals

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a✝ b✝ : A
ha✝ : autoParam (0 ≤ a✝) _auto✝
hab✝ : a✝ ≤ b✝
a b : Unitization ℂ A
ha : 0 ≤ a
hab : a ≤ b
hb : 0 ≤ b
this✝ : IsSelfAdjoint a
this : IsSelfAdjoint b
x : ℝ
hx : x ∈ spectrum ℝ b
⊢ id x ≤ ‖b‖

Tactic:
calc x = ‖x‖ := (Real.norm_of_nonneg (spectrum_nonneg_of_nonneg hb hx)).symm
  _ ≤ ‖b‖ := spectrum.norm_le_norm_of_mem hx

Result:
no goals

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
ha : autoParam (0 ≤ a) _auto✝
hab : a ≤ b
⊢ ‖a‖ ≤ ‖b‖

Tactic:
suffices ∀ a b : A⁺¹, 0 ≤ a → a ≤ b → ‖a‖ ≤ ‖b‖ by
  have hb := ha.trans hab
  simpa only [ge_iff_le, Unitization.norm_inr] using
    this a b (by simpa) (by rwa [Unitization.inr_le_iff a b])

Result:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
ha : autoParam (0 ≤ a) _auto✝
hab : a ≤ b
⊢ ∀ (a b : Unitization ℂ A), 0 ≤ a → a ≤ b → ‖a‖ ≤ ‖b‖

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a✝ b✝ : A
ha✝ : autoParam (0 ≤ a✝) _auto✝
hab✝ : a✝ ≤ b✝
a b : Unitization ℂ A
ha : 0 ≤ a
hab : a ≤ b
hb : 0 ≤ b
this✝ : IsSelfAdjoint a
this : IsSelfAdjoint b
⊢ cfc (fun x => ‖b‖) b = cfc (fun x => ‖b‖) a

Tactic:
rw [cfc_const _ _, cfc_const _ _]

Result:
no goals

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

Tactic:
simpa

Result:
no goals

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a✝ b✝ : A
ha✝ : autoParam (0 ≤ a✝) _auto✝
hab✝ : a✝ ≤ b✝
a b : Unitization ℂ A
ha : 0 ≤ a
hab : a ≤ b
hb : 0 ≤ b
this✝ : IsSelfAdjoint a
this : IsSelfAdjoint b
⊢ cfc id a = a

Tactic:
rw [cfc_id ℝ a]

Result:
no goals

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a✝ b✝ : A
ha✝ : autoParam (0 ≤ a✝) _auto✝
hab✝ : a✝ ≤ b✝
a b : Unitization ℂ A
ha : 0 ≤ a
hab : a ≤ b
hb : 0 ≤ b
this✝ : IsSelfAdjoint a
this : IsSelfAdjoint b
⊢ cfc id b ≤ cfc (fun x => ‖b‖) b

Tactic:
refine cfc_mono fun x hx => ?_

Result:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a✝ b✝ : A
ha✝ : autoParam (0 ≤ a✝) _auto✝
hab✝ : a✝ ≤ b✝
a b : Unitization ℂ A
ha : 0 ≤ a
hab : a ≤ b
hb : 0 ≤ b
this✝ : IsSelfAdjoint a
this : IsSelfAdjoint b
x : ℝ
hx : x ∈ spectrum ℝ b
⊢ id x ≤ ‖b‖

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

Tactic:
simpa only [ge_iff_le, Unitization.norm_inr] using
  this a b (by simpa) (by rwa [Unitization.inr_le_iff a b])

Result:
no goals

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a✝ b✝ : A
ha✝ : autoParam (0 ≤ a✝) _auto✝
hab✝ : a✝ ≤ b✝
a b : Unitization ℂ A
ha : 0 ≤ a
hab : a ≤ b
hb : 0 ≤ b
⊢ ‖a‖ ≤ ‖b‖

Tactic:
have := IsSelfAdjoint.of_nonneg ha

Result:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a✝ b✝ : A
ha✝ : autoParam (0 ≤ a✝) _auto✝
hab✝ : a✝ ≤ b✝
a b : Unitization ℂ A
ha : 0 ≤ a
hab : a ≤ b
hb : 0 ≤ b
this : IsSelfAdjoint a
⊢ ‖a‖ ≤ ‖b‖

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a✝ b✝ : A
ha✝ : autoParam (0 ≤ a✝) _auto✝
hab✝ : a✝ ≤ b✝
a b : Unitization ℂ A
ha : 0 ≤ a
hab : a ≤ b
hb : 0 ≤ b
this : IsSelfAdjoint a
⊢ ‖a‖ ≤ ‖b‖

Tactic:
have := IsSelfAdjoint.of_nonneg hb

Result:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a✝ b✝ : A
ha✝ : autoParam (0 ≤ a✝) _auto✝
hab✝ : a✝ ≤ b✝
a b : Unitization ℂ A
ha : 0 ≤ a
hab : a ≤ b
hb : 0 ≤ b
this✝ : IsSelfAdjoint a
this : IsSelfAdjoint b
⊢ ‖a‖ ≤ ‖b‖

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

Tactic:
rwa [Unitization.inr_le_iff a b]

Result:
no goals

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
ha : autoParam (0 ≤ a) _auto✝
hab : a ≤ b
⊢ ∀ (a b : Unitization ℂ A), 0 ≤ a → a ≤ b → ‖a‖ ≤ ‖b‖

Tactic:
intro a b ha hab

Result:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a✝ b✝ : A
ha✝ : autoParam (0 ≤ a✝) _auto✝
hab✝ : a✝ ≤ b✝
a b : Unitization ℂ A
ha : 0 ≤ a
hab : a ≤ b
⊢ ‖a‖ ≤ ‖b‖

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a✝ b✝ : A
ha✝ : autoParam (0 ≤ a✝) _auto✝
hab✝ : a✝ ≤ b✝
a b : Unitization ℂ A
ha : 0 ≤ a
hab : a ≤ b
hb : 0 ≤ b
this✝ : IsSelfAdjoint a
this : IsSelfAdjoint b
h₂ : cfc id a ≤ cfc (fun x => ‖b‖) a
⊢ ‖a‖ ≤ ‖b‖

Tactic:
rw [cfc_le_iff id (fun _ => ‖b‖) a] at h₂

Result:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a✝ b✝ : A
ha✝ : autoParam (0 ≤ a✝) _auto✝
hab✝ : a✝ ≤ b✝
a b : Unitization ℂ A
ha : 0 ≤ a
hab : a ≤ b
hb : 0 ≤ b
this✝ : IsSelfAdjoint a
this : IsSelfAdjoint b
h₂ : ∀ x ∈ spectrum ℝ a, id x ≤ ‖b‖
⊢ ‖a‖ ≤ ‖b‖

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
ha : autoParam (0 ≤ a) _auto✝
hab : a ≤ b
this : ∀ (a b : Unitization ℂ A), 0 ≤ a → a ≤ b → ‖a‖ ≤ ‖b‖
⊢ ‖a‖ ≤ ‖b‖

Tactic:
have hb := ha.trans hab

Result:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
ha : autoParam (0 ≤ a) _auto✝
hab : a ≤ b
this : ∀ (a b : Unitization ℂ A), 0 ≤ a → a ≤ b → ‖a‖ ≤ ‖b‖
hb : 0 ≤ b
⊢ ‖a‖ ≤ ‖b‖

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a✝ b✝ : A
ha✝ : autoParam (0 ≤ a✝) _auto✝
hab✝ : a✝ ≤ b✝
a b : Unitization ℂ A
ha : 0 ≤ a
hab : a ≤ b
⊢ ‖a‖ ≤ ‖b‖

Tactic:
have hb : 0 ≤ b := ha.trans hab

Result:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a✝ b✝ : A
ha✝ : autoParam (0 ≤ a✝) _auto✝
hab✝ : a✝ ≤ b✝
a b : Unitization ℂ A
ha : 0 ≤ a
hab : a ≤ b
hb : 0 ≤ b
⊢ ‖a‖ ≤ ‖b‖