awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConvexOn ℝ (inr '' s) (cfc (p := IsSelfAdjoint) f)
inrl : A →ₗ[ℝ] Unitization ℂ A := inrHom ℝ ℂ A
hf₀ : f 0 = 0
pos : ConvexOn ℝ (β := Unitization ℂ A) s (inr ∘ cfcₙ (p := IsSelfAdjoint) f)
⊢ ConvexOn ℝ s (cfcₙ (p := IsSelfAdjoint) f)

Tactic:
refine convexOn_of_convexOn_inr_comp (fun _ => IsSelfAdjoint.cfcₙ) ?_

Premises used: Unitization.convexOn_of_convexOn_inr_comp, IsSelfAdjoint.cfcₙ
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConvexOn ℝ (inr '' s) (cfc (p := IsSelfAdjoint) f)
inrl : A →ₗ[ℝ] Unitization ℂ A := inrHom ℝ ℂ A
hf₀ : f 0 = 0
⊢ Eq (α := A → Unitization ℂ A) (inr ∘ cfcₙ (p := IsSelfAdjoint) f) fun (x : A) ↦
    (↑(cfcₙ (p := IsSelfAdjoint) f x) : Unitization ℂ A)

Tactic:
have h₁ : inr (R := ℂ) ∘ (cfcₙ f) = fun x : A => ((cfcₙ f x : A) : A⁺¹) := rfl
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConvexOn ℝ (inr '' s) (cfc (p := IsSelfAdjoint) f)
inrl : A →ₗ[ℝ] Unitization ℂ A := inrHom ℝ ℂ A
hf₀ : f 0 = 0
h₁ :
  Eq (α := A → Unitization ℂ A) (inr ∘ cfcₙ (p := IsSelfAdjoint) f) fun (x : A) ↦
    (↑(cfcₙ (p := IsSelfAdjoint) f x) : Unitization ℂ A)
h : ∀ (x : A), (↑(cfcₙ (p := IsSelfAdjoint) f x) : Unitization ℂ A) = cfc (p := IsSelfAdjoint) f (↑x : Unitization ℂ A)
⊢ Eq.{u_1 + 1} (α := (x : A) → Unitization ℂ A) (fun (x : A) ↦ (↑(cfcₙ (p := IsSelfAdjoint) f x) : Unitization ℂ A))
    fun (x : A) ↦ cfc (p := IsSelfAdjoint) f (↑x : Unitization ℂ A)

Tactic:
ext1
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConvexOn ℝ (inr '' s) (cfc (p := IsSelfAdjoint) f)
inrl : A →ₗ[ℝ] Unitization ℂ A := inrHom ℝ ℂ A
hf₀ : f 0 = 0
h₁ :
  Eq (α := A → Unitization ℂ A) (inr ∘ cfcₙ (p := IsSelfAdjoint) f) fun (x : A) ↦
    (↑(cfcₙ (p := IsSelfAdjoint) f x) : Unitization ℂ A)
x : A
h h₂ : cfc (p := IsSelfAdjoint) f (↑x : Unitization ℂ A) = cfc (p := IsSelfAdjoint) f (↑x : Unitization ℂ A)
⊢ (↑(cfcₙ (p := IsSelfAdjoint) f x) : Unitization ℂ A) = cfc (p := IsSelfAdjoint) f (↑x : Unitization ℂ A)

Tactic:
rw [real_cfcₙ_eq_cfc_inr ..]

Premises used: Unitization.real_cfcₙ_eq_cfc_inr
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConvexOn ℝ (inr '' s) (cfc (p := IsSelfAdjoint) f)
inrl : A →ₗ[ℝ] Unitization ℂ A := inrHom ℝ ℂ A
hf₀ : f 0 = 0
h₁ :
  Eq (α := A → Unitization ℂ A) (inr ∘ cfcₙ (p := IsSelfAdjoint) f) fun (x : A) ↦
    (↑(cfcₙ (p := IsSelfAdjoint) f x) : Unitization ℂ A)
⊢ Eq.{u_1 + 1} (α := (x : A) → Unitization ℂ A) (fun (x : A) ↦ (↑(cfcₙ (p := IsSelfAdjoint) f x) : Unitization ℂ A))
    fun (x : A) ↦ cfc (p := IsSelfAdjoint) f (↑x : Unitization ℂ A)

Tactic:
have h₂ : (fun x : A => ((cfcₙ f x : A) : A⁺¹))
      = fun x : A => cfc f (x : A⁺¹) := by ext1; rw [real_cfcₙ_eq_cfc_inr ..]
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConvexOn ℝ (inr '' s) (cfc (p := IsSelfAdjoint) f)
inrl : A →ₗ[ℝ] Unitization ℂ A := inrHom ℝ ℂ A
hf₀ : f 0 = 0
h₁ :
  Eq (α := A → Unitization ℂ A) (inr ∘ cfcₙ (p := IsSelfAdjoint) f) fun (x : A) ↦
    (↑(cfcₙ (p := IsSelfAdjoint) f x) : Unitization ℂ A)
h₂ :
  Eq.{u_1 + 1} (α := (x : A) → Unitization ℂ A) (fun (x : A) ↦ (↑(cfcₙ (p := IsSelfAdjoint) f x) : Unitization ℂ A))
    fun (x : A) ↦ cfc (p := IsSelfAdjoint) f (↑x : Unitization ℂ A)
pos : ConvexOn ℝ (β := Unitization ℂ A) s fun (x : A) ↦ cfc (p := IsSelfAdjoint) f (↑x : Unitization ℂ A)
⊢ ConvexOn ℝ (β := Unitization ℂ A) s (inr ∘ cfcₙ (p := IsSelfAdjoint) f)

Tactic:
rw [h₁, h₂]
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConvexOn ℝ (inr '' s) (cfc (p := IsSelfAdjoint) f)
inrl : A →ₗ[ℝ] Unitization ℂ A := inrHom ℝ ℂ A
hf₀ : f 0 = 0
h₁ :
  Eq (α := A → Unitization ℂ A) (inr ∘ cfcₙ (p := IsSelfAdjoint) f) fun (x : A) ↦
    (↑(cfcₙ (p := IsSelfAdjoint) f x) : Unitization ℂ A)
h₂ :
  Eq.{u_1 + 1} (α := (x : A) → Unitization ℂ A) (fun (x : A) ↦ (↑(cfcₙ (p := IsSelfAdjoint) f x) : Unitization ℂ A))
    fun (x : A) ↦ cfc (p := IsSelfAdjoint) f (↑x : Unitization ℂ A)
⊢ ConvexOn ℝ (E := A)
    (Set.preimage (β := Unitization ℂ A) (⇑inrl : (a : A) → Unitization ℂ A) ((⇑inrl : (a : A) → Unitization ℂ A) '' s))
    (cfc (p := IsSelfAdjoint) f ∘ (⇑inrl : (a : A) → Unitization ℂ A))

Tactic:
have h₃ : ConvexOn ℝ (inrl ⁻¹' inrl '' s) ((cfc f) ∘ inrl) :=
    ConvexOn.comp_linearMap (g := inrl) hf
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConvexOn ℝ (inr '' s) (cfc (p := IsSelfAdjoint) f)
inrl : A →ₗ[ℝ] Unitization ℂ A := inrHom ℝ ℂ A
hf₀ : f 0 = 0
h₁ :
  Eq (α := A → Unitization ℂ A) (inr ∘ cfcₙ (p := IsSelfAdjoint) f) fun (x : A) ↦
    (↑(cfcₙ (p := IsSelfAdjoint) f x) : Unitization ℂ A)
h₂ :
  Eq.{u_1 + 1} (α := (x : A) → Unitization ℂ A) (fun (x : A) ↦ (↑(cfcₙ (p := IsSelfAdjoint) f x) : Unitization ℂ A))
    fun (x : A) ↦ cfc (p := IsSelfAdjoint) f (↑x : Unitization ℂ A)
h₃ :
  ConvexOn ℝ (E := A)
    (Set.preimage (β := Unitization ℂ A) (⇑inrl : (a : A) → Unitization ℂ A) ((⇑inrl : (a : A) → Unitization ℂ A) '' s))
    (cfc (p := IsSelfAdjoint) f ∘ (⇑inrl : (a : A) → Unitization ℂ A))
pos pos₁ pos₂ pos₃ :
  ∀ (h₃ : ConvexOn ℝ s (cfc (p := IsSelfAdjoint) f ∘ (⇑inrl : (a : A) → Unitization ℂ A))),
    ConvexOn ℝ (β := Unitization ℂ A) s fun (x : A) ↦ cfc (p := IsSelfAdjoint) f (↑x : Unitization ℂ A)
⊢ ConvexOn ℝ (β := Unitization ℂ A) s fun (x : A) ↦ cfc (p := IsSelfAdjoint) f (↑x : Unitization ℂ A)

Tactic:
rwa [Set.preimage_image_eq _ inrHom_injective] at h₃

Premises used: Unitization.inrHom_injective, Set.preimage_image_eq
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConcaveOn ℝ (inr '' s) (cfc (p := IsSelfAdjoint) f)
rw : ConcaveOn ℝ s (-cfcₙ (p := IsSelfAdjoint) (-f))
⊢ ConcaveOn ℝ s (- -cfcₙ (p := IsSelfAdjoint) f)

Tactic:
rw [← cfcₙ_neg' f]

Premises used: cfcₙ_neg'
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConcaveOn ℝ (inr '' s) (cfc (p := IsSelfAdjoint) f)
⊢ ConcaveOn ℝ s (-cfcₙ (p := IsSelfAdjoint) (-f))

Tactic:
(convexOn_cfcₙ_of_convexOn_cfc ?_).neg

Premises used: ConvexOn.neg, CStarAlgebra.convexOn_cfcₙ_of_convexOn_cfc
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConcaveOn ℝ (inr '' s) (cfc (p := IsSelfAdjoint) f)
refine : ConvexOn ℝ (inr '' s) (cfc (p := IsSelfAdjoint) (-f))
⊢ ConcaveOn ℝ s (-cfcₙ (p := IsSelfAdjoint) (-f))

Tactic:
refine (convexOn_cfcₙ_of_convexOn_cfc ?_).neg

Premises used: ConvexOn.neg, CStarAlgebra.convexOn_cfcₙ_of_convexOn_cfc
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConcaveOn ℝ (inr '' s) (cfc (p := IsSelfAdjoint) f)
rw : ConvexOn ℝ (inr '' s) (-cfc (p := IsSelfAdjoint) f)
⊢ ConvexOn ℝ (inr '' s) (cfc (p := IsSelfAdjoint) (-f))

Tactic:
rw [cfc_neg']

Premises used: cfc_neg'
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConcaveOn ℝ (inr '' s) (cfc (p := IsSelfAdjoint) f)
⊢ ConvexOn ℝ (inr '' s) (-cfc (p := IsSelfAdjoint) f)

Tactic:
hf.neg

Premises used: ConcaveOn.neg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConcaveOn ℝ (inr '' s) (cfc (p := IsSelfAdjoint) f)
⊢ ConvexOn ℝ (inr '' s) (-cfc (p := IsSelfAdjoint) f)

Tactic:
exact hf.neg

Premises used: ConcaveOn.neg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConcaveOn ℝ (inr '' s) (cfc (p := IsSelfAdjoint) f)
⊢ ConcaveOn ℝ s (- -cfcₙ (p := IsSelfAdjoint) f)

Tactic:
have : ConcaveOn ℝ s (- -cfcₙ f) := by
    rw [← cfcₙ_neg' f]
    refine (convexOn_cfcₙ_of_convexOn_cfc ?_).neg
    rw [cfc_neg']
    exact hf.neg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConcaveOn ℝ (inr '' s) (cfc (p := IsSelfAdjoint) f)
this : ConcaveOn ℝ s (- -cfcₙ (p := IsSelfAdjoint) f)
⊢ ConcaveOn ℝ s (cfcₙ (p := IsSelfAdjoint) f)

Tactic:
simpa using this
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
simp : 0 ≤ x → (LE.le (α := Unitization ℂ A) (↑x : Unitization ℂ A) 1 ↔ ‖x‖ ≤ 1)
⊢ Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑x : Unitization ℂ A) ↔ 0 ≤ x ∧ ‖x‖ ≤ 1

Tactic:
simp only [mem_Icc, inr_nonneg_iff, and_congr_right_iff]

Premises used: and_congr_right_iff, Set.mem_Icc, Unitization.inr_nonneg_iff
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
rw :
  LE.le (α := Unitization ℂ A) 0 (↑x : Unitization ℂ A) →
    (norm (E := Unitization ℂ A) (↑x : Unitization ℂ A) ≤ 1 ↔ LE.le (α := Unitization ℂ A) (↑x : Unitization ℂ A) 1)
⊢ 0 ≤ x → (LE.le (α := Unitization ℂ A) (↑x : Unitization ℂ A) 1 ↔ ‖x‖ ≤ 1)

Tactic:
rw [← norm_inr (𝕜 := ℂ), ← inr_nonneg_iff, iff_comm]

Premises used: iff_comm, Unitization.norm_inr, Unitization.inr_nonneg_iff
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
⊢ LE.le (α := Unitization ℂ A) 0 (↑x : Unitization ℂ A) →
    (norm (E := Unitization ℂ A) (↑x : Unitization ℂ A) ≤ 1 ↔ LE.le (α := Unitization ℂ A) (↑x : Unitization ℂ A) 1)

Tactic:
(norm_le_one_iff_of_nonneg _ ·)

Premises used: Unitization.inr, CStarAlgebra.norm_le_one_iff_of_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
⊢ LE.le (α := Unitization ℂ A) 0 (↑x : Unitization ℂ A) →
    (norm (E := Unitization ℂ A) (↑x : Unitization ℂ A) ≤ 1 ↔ LE.le (α := Unitization ℂ A) (↑x : Unitization ℂ A) 1)

Tactic:
exact (norm_le_one_iff_of_nonneg _ ·)

Premises used: CStarAlgebra.norm_le_one_iff_of_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
⊢ Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑x : Unitization ℂ A) ↔ 0 ≤ x ∧ ‖x‖₊ ≤ 1

Tactic:
inr_mem_Icc_iff_norm_le

Premises used: CStarAlgebra.inr_mem_Icc_iff_norm_le
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
h :
  ∀ (x : A),
    Membership.mem (γ := Set A) (preimage (β := Unitization ℂ A) inr (Icc 0 1)) x ↔
      Membership.mem (γ := Set A) ({x : A | 0 ≤ x} ∩ closedBall 0 1) x
⊢ Eq.{u_1 + 1} (α := Set A) (preimage (β := Unitization ℂ A) inr (Icc 0 1)) ({x : A | 0 ≤ x} ∩ closedBall 0 1)

Tactic:
ext
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
⊢ Membership.mem (γ := Set A) (preimage (β := Unitization ℂ A) inr (Icc 0 1)) x ↔
    Membership.mem (γ := Set A) ({x : A | 0 ≤ x} ∩ closedBall 0 1) x

Tactic:
simp [-mem_Icc, inr_mem_Icc_iff_norm_le]

Premises used: CStarAlgebra.inr_mem_Icc_iff_norm_le, Set.mem_Icc
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : Membership.mem (γ := Set A) (Ici 0) a
⊢ Membership.mem (γ := Set (Unitization ℂ A)) (Ici 0) (↑a : Unitization ℂ A)

Tactic:
Unitization.inr_nonneg_iff.mpr ha

Premises used: Iff.mpr, Set.Ici, Set.Mem, setOf, Unitization.inr_nonneg_iff
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : Membership.mem (γ := Set A) (Ici 0) a
⊢ Membership.mem (γ := Set (Unitization ℂ A)) (Ici 0) (↑a : Unitization ℂ A)

Tactic:
exact Unitization.inr_nonneg_iff.mpr ha

Premises used: Iff.mpr, Unitization.inr_nonneg_iff
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a e : A
he : IsStarProjection e
ha : 0 ≤ a
hae : a ≤ e
this : a * e = a
⊢ e * a = a

Tactic:
simpa [ha.star_eq, he.isSelfAdjoint.star_eq] using congr(star $this)

Premises used: LE.le.star_eq, IsStarProjection.isSelfAdjoint, IsSelfAdjoint.star_eq
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a e : A
he : IsStarProjection e
ha : 0 ≤ a
hae : a ≤ e
suffices : a * e = a
⊢ a * e = a ∧ e * a = a

Tactic:
suffices a * e = a from
    ⟨this, by simpa [ha.star_eq, he.isSelfAdjoint.star_eq] using congr(star $this)⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a e : A
he : IsStarProjection e
ha : 0 ≤ a
hae : a ≤ e
suffices : ∀ (a e : Unitization ℂ A), IsStarProjection e → 0 ≤ a → a ≤ e → a * e = a
⊢ a * e = a

Tactic:
suffices ∀ a e : A⁺¹, IsStarProjection e → 0 ≤ a → a ≤ e → a * e = a from
    mod_cast this a e he.inr ha.inr (inr_le_iff a e |>.mpr hae)
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a_1 e_1 : A
he_1 : IsStarProjection e_1
ha_1 : 0 ≤ a_1
hae_1 : a_1 ≤ e_1
a e : Unitization ℂ A
he : IsStarProjection e
ha : 0 ≤ a
hae : a ≤ e
this : sqrt a * (1 - e) = 0
⊢ a * e = a

Tactic:
simpa [← mul_assoc, sqrt_mul_sqrt_self a, mul_sub, sub_eq_zero, eq_comm (a := a)]
      using congr(sqrt a * $this)

Premises used: mul_sub, CFC.sqrt, sub_eq_zero, mul_assoc, eq_comm, CFC.sqrt_mul_sqrt_self
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a_1 e_1 : A
he_1 : IsStarProjection e_1
ha_1 : 0 ≤ a_1
hae_1 : a_1 ≤ e_1
a e : Unitization ℂ A
he : IsStarProjection e
ha : 0 ≤ a
hae : a ≤ e
suffices : sqrt a * (1 - e) = 0
⊢ a * e = a

Tactic:
suffices sqrt a * (1 - e : A⁺¹) = 0 by
    simpa [← mul_assoc, sqrt_mul_sqrt_self a, mul_sub, sub_eq_zero, eq_comm (a := a)]
      using congr(sqrt a * $this)
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a_1 e_1 : A
he_1 : IsStarProjection e_1
ha_1 : 0 ≤ a_1
hae_1 : a_1 ≤ e_1
a e : Unitization ℂ A
he : IsStarProjection e
ha : 0 ≤ a
hae : a ≤ e
rw : star (1 - e) * a * (1 - e) = 0
⊢ sqrt a * (1 - e) = 0

Tactic:
rw [← norm_eq_zero, ← sq_eq_zero_iff, ← norm_star_mul_mul_self_of_nonneg, norm_eq_zero]

Premises used: norm_eq_zero, CFC.norm_star_mul_mul_self_of_nonneg, sq_eq_zero_iff
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a_1 e_1 : A
he_1 : IsStarProjection e_1
ha_1 : 0 ≤ a_1
hae_1 : a_1 ≤ e_1
a e : Unitization ℂ A
he : IsStarProjection e
ha : 0 ≤ a
hae : a ≤ e
⊢ star (1 - e) * a * (1 - e) = 0

Tactic:
le_antisymm ?_ <| star_left_conjugate_nonneg ha _

Premises used: le_antisymm, star_left_conjugate_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a_1 e_1 : A
he_1 : IsStarProjection e_1
ha_1 : 0 ≤ a_1
hae_1 : a_1 ≤ e_1
a e : Unitization ℂ A
he : IsStarProjection e
ha : 0 ≤ a
hae : a ≤ e
refine : star (1 - e) * a * (1 - e) ≤ 0
⊢ star (1 - e) * a * (1 - e) = 0

Tactic:
refine le_antisymm ?_ <| star_left_conjugate_nonneg ha _

Premises used: le_antisymm, star_left_conjugate_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a_1 e_1 : A
he_1 : IsStarProjection e_1
ha_1 : 0 ≤ a_1
hae_1 : a_1 ≤ e_1
a e : Unitization ℂ A
he : IsStarProjection e
ha : 0 ≤ a
hae : a ≤ e
grw : star (1 - e) * e * (1 - e) ≤ 0
grw₁ : star (1 - e) * (e * (1 - e)) ≤ 0
grw₂ : star (1 - e) * 0 ≤ 0
grw₃ grw₄ : LE.le.{u_1} (α := Unitization ℂ A) 0 0
⊢ star (1 - e) * a * (1 - e) ≤ 0

Tactic:
grw [star_left_conjugate_le_conjugate hae (1 - e), mul_assoc, he.mul_one_sub_self, mul_zero]

Premises used: mul_assoc, HSub.hSub, MulZeroClass.mul_zero, star_left_conjugate_le_conjugate, OfNat.ofNat, IsStarProjection.mul_one_sub_self
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a e : A
he : IsStarProjection e
ha : 0 ≤ a
hae : a ≤ e
⊢ e * a * e = a

Tactic:
grind [he.mul_right_and_mul_left_of_nonneg_of_le ha hae]

Premises used: IsStarProjection.mul_right_and_mul_left_of_nonneg_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 : 0 ≤ a
n : ℕ
rw : 0 ≤ cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x ^ n) a
⊢ 0 ≤ a ^ n

Tactic:
rw [← cfc_pow_id (R := ℝ≥0) a]

Premises used: cfc_pow_id
-- 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
n : ℕ
⊢ 0 ≤ cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x ^ n) a

Tactic:
cfc_nonneg_of_predicate

Premises used: cfc_nonneg_of_predicate
-- 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
n : ℕ
⊢ 0 ≤ cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x ^ n) a

Tactic:
exact cfc_nonneg_of_predicate

Premises used: cfc_nonneg_of_predicate
-- 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
⊢ 0 ≤ a

Tactic:
have ha' : 0 ≤ a := zero_le_one.trans ha
-- 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
ha' : 0 ≤ a
n m : ℕ
hnm : n ≤ m
simp : a ^ n ≤ a ^ m
⊢ LE.le.{u_1} (α := A) ((fun (x : ℕ) ↦ a ^ x) n) ((fun (x : ℕ) ↦ a ^ x) m)

Tactic:
simp only
-- 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
ha' : 0 ≤ a
n m : ℕ
hnm : n ≤ m
rw : ∀ x ∈ spectrum ℝ a, x ^ n ≤ x ^ m
⊢ a ^ n ≤ a ^ m

Tactic:
rw [← cfc_pow_id (R := ℝ) a, ← cfc_pow_id (R := ℝ) a, cfc_le_iff ..]

Premises used: cfc_le_iff, cfc_pow_id
-- 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
ha' : 0 ≤ a
n m : ℕ
hnm : n ≤ m
rw : ∀ (ha : ∀ x ∈ spectrum ℝ a, 1 ≤ x) (ha' : 0 ≤ a) ⦃n m : ℕ⦄ (hnm : n ≤ m), ∀ x ∈ spectrum ℝ a, x ^ n ≤ x ^ m
⊢ ∀ x ∈ spectrum ℝ a, x ^ n ≤ x ^ m

Tactic:
rw [CFC.one_le_iff (R := ℝ) a] at ha

Premises used: CFC.one_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 : ∀ x ∈ spectrum ℝ a, 1 ≤ x
ha' : 0 ≤ a
n m : ℕ
hnm : n ≤ m
h : ∀ (x : ℝ) (hx : x ∈ spectrum ℝ a) (this : 1 ≤ x), x ^ n ≤ x ^ m
⊢ ∀ x ∈ spectrum ℝ a, x ^ n ≤ x ^ m

Tactic:
peel ha with x hx _
-- 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 : ∀ x ∈ spectrum ℝ a, 1 ≤ x
ha' : 0 ≤ a
n m : ℕ
hnm : n ≤ m
x : ℝ
hx : x ∈ spectrum ℝ a
this : 1 ≤ x
⊢ x ^ n ≤ x ^ m

Tactic:
pow_le_pow_right₀ (ha x hx) hnm

Premises used: pow_le_pow_right₀
-- 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 : ∀ x ∈ spectrum ℝ a, 1 ≤ x
ha' : 0 ≤ a
n m : ℕ
hnm : n ≤ m
x : ℝ
hx : x ∈ spectrum ℝ a
this : 1 ≤ x
⊢ x ^ n ≤ x ^ m

Tactic:
exact pow_le_pow_right₀ (ha x hx) hnm

Premises used: pow_le_pow_right₀
-- 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
ha₁ : a ≤ 1
n m : ℕ
hnm : n ≤ m
simp : a ^ m ≤ a ^ n
⊢ LE.le.{u_1} (α := A) ((fun (x : ℕ) ↦ a ^ x) m) ((fun (x : ℕ) ↦ a ^ x) n)

Tactic:
simp only
-- 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
ha₁ : a ≤ 1
n m : ℕ
hnm : n ≤ m
rw : ∀ x ∈ spectrum ℝ a, x ^ m ≤ x ^ n
⊢ a ^ m ≤ a ^ n

Tactic:
rw [← cfc_pow_id (R := ℝ) a, ← cfc_pow_id (R := ℝ) a, cfc_le_iff ..]

Premises used: cfc_le_iff, cfc_pow_id
-- 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
ha₁ : a ≤ 1
n m : ℕ
hnm : n ≤ m
rw : ∀ (ha₁ : ∀ x ∈ spectrum ℝ a, x ≤ 1) ⦃n m : ℕ⦄ (hnm : n ≤ m), ∀ x ∈ spectrum ℝ a, x ^ m ≤ x ^ n
⊢ ∀ x ∈ spectrum ℝ a, x ^ m ≤ x ^ n

Tactic:
rw [CFC.le_one_iff (R := ℝ) a] at ha₁

Premises used: CFC.le_one_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
ha₁ : ∀ x ∈ spectrum ℝ a, x ≤ 1
n m : ℕ
hnm : n ≤ m
h : ∀ (x : ℝ) (hx : x ∈ spectrum ℝ a) (this : x ≤ 1), x ^ m ≤ x ^ n
⊢ ∀ x ∈ spectrum ℝ a, x ^ m ≤ x ^ n

Tactic:
peel ha₁ with x hx _