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
a : A
ha : 0 ≤ a
x : ℂ
hx : x ∈ σₙ ℂ a
⊢ x ∈ spectrum ℂ (A := Unitization ℂ A) (↑a : Unitization ℂ A)

Tactic:
rw [Unitization.quasispectrum_eq_spectrum_inr' ℂ ℂ a] at hx

Premises used: Unitization.quasispectrum_eq_spectrum_inr', Complex
-- 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 : 0 ≤ a
x : ℂ
hx : x ∈ spectrum ℂ (A := Unitization ℂ A) (↑a : Unitization ℂ A)
⊢ 0 ≤ x

Tactic:
spectrum_nonneg_of_nonneg (Unitization.inr_nonneg_iff.mpr ha) hx

Premises used: Iff.mpr, spectrum_nonneg_of_nonneg, 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 : 0 ≤ a
x : ℂ
hx : x ∈ spectrum ℂ (A := Unitization ℂ A) (↑a : Unitization ℂ A)
⊢ 0 ≤ x

Tactic:
exact spectrum_nonneg_of_nonneg (Unitization.inr_nonneg_iff.mpr ha) hx

Premises used: Iff.mpr, spectrum_nonneg_of_nonneg, 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 b : A
ha : 0 ≤ a
hab : a ≤ b
this : ∀ (a b : Unitization ℂ A), 0 ≤ a → a ≤ b → ‖a‖ ≤ ‖b‖
⊢ 0 ≤ b

Tactic:
have hb := ha.trans hab
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
ha : 0 ≤ a
hab : a ≤ b
this : ∀ (a b : Unitization ℂ A), 0 ≤ a → a ≤ b → ‖a‖ ≤ ‖b‖
hb : 0 ≤ b
⊢ LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A)

Tactic:
simpa
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
ha : 0 ≤ a
hab : a ≤ b
this : ∀ (a b : Unitization ℂ A), 0 ≤ a → a ≤ b → ‖a‖ ≤ ‖b‖
hb : 0 ≤ b
rwa rwa₁ rwa₂ rwa₃ : a ≤ b
⊢ LE.le (α := Unitization ℂ A) (↑a : Unitization ℂ A) (↑b : Unitization ℂ A)

Tactic:
rwa [Unitization.inr_le_iff a b]

Premises used: Unitization.inr_le_iff
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
ha : 0 ≤ a
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])

Premises used: ge_iff_le, Unitization.inr, Unitization.norm_inr
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
ha : 0 ≤ a
hab : a ≤ b
suffices : ∀ (a b : Unitization ℂ A), 0 ≤ a → a ≤ b → ‖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])
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a_1 b_1 : A
ha_1 : 0 ≤ a_1
hab_1 : a_1 ≤ b_1
a b : Unitization ℂ A
ha : 0 ≤ a
hab : a ≤ b
⊢ 0 ≤ b

Tactic:
have hb : 0 ≤ b := ha.trans hab
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a_1 b_1 : A
ha_1 : 0 ≤ a_1
hab_1 : a_1 ≤ b_1
a b : Unitization ℂ A
ha : 0 ≤ a
hab : a ≤ b
hb : 0 ≤ b
⊢ ‖a‖ ≤ ‖b‖

Tactic:
(norm_le_iff_le_algebraMap a (norm_nonneg _) ha).2 <| hab.trans <|
    IsSelfAdjoint.le_algebraMap_norm_self (.of_nonneg hb)

Premises used: Iff.mpr, IsSelfAdjoint.of_nonneg, CStarAlgebra.norm_le_iff_le_algebraMap, LE.le.trans, IsSelfAdjoint.le_algebraMap_norm_self, norm_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 b_1 : A
ha_1 : 0 ≤ a_1
hab_1 : a_1 ≤ b_1
a b : Unitization ℂ A
ha : 0 ≤ a
hab : a ≤ b
hb : 0 ≤ b
⊢ ‖a‖ ≤ ‖b‖

Tactic:
exact (norm_le_iff_le_algebraMap a (norm_nonneg _) ha).2 <| hab.trans <|
    IsSelfAdjoint.le_algebraMap_norm_self (.of_nonneg hb)

Premises used: Iff.mpr, IsSelfAdjoint.of_nonneg, CStarAlgebra.norm_le_iff_le_algebraMap, LE.le.trans, IsSelfAdjoint.le_algebraMap_norm_self, norm_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
ha : 0 ≤ a
hab : a ≤ b
⊢ ‖a‖₊ ≤ ‖b‖₊

Tactic:
norm_le_norm_of_nonneg_of_le ha hab

Premises used: CStarAlgebra.norm_le_norm_of_nonneg_of_le
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
hb : IsSelfAdjoint b
this : ∀ (a b : Unitization ℂ A), IsSelfAdjoint b → star a * b * a ≤ ‖b‖ • (star a * a)
⊢ IsSelfAdjoint (star a * b * a)

Tactic:
aesop
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
hb : IsSelfAdjoint b
this : ∀ (a b : Unitization ℂ A), IsSelfAdjoint b → star a * b * a ≤ ‖b‖ • (star a * a)
rw : LE.le (α := Unitization ℂ A) (↑(star a * b * a) : Unitization ℂ A) (↑(‖b‖ • (star a * a)) : Unitization ℂ A)
⊢ star a * b * a ≤ ‖b‖ • (star a * a)

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

Premises used: IsSelfAdjoint.star_mul_self, Unitization.inr_le_iff, IsSelfAdjoint.smul, IsSelfAdjoint.all
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
hb : IsSelfAdjoint b
this : ∀ (a b : Unitization ℂ A), IsSelfAdjoint b → star a * b * a ≤ ‖b‖ • (star a * a)
⊢ LE.le (α := Unitization ℂ A) (↑(star a * b * a) : Unitization ℂ A) (↑(‖b‖ • (star a * a)) : Unitization ℂ A)

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

Premises used: IsSelfAdjoint.inr, Unitization.inr, Complex, Unitization.norm_inr
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
hb : IsSelfAdjoint b
suffices : ∀ (a b : Unitization ℂ A), IsSelfAdjoint b → star a * b * a ≤ ‖b‖ • (star a * a)
⊢ 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 ℂ
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a_1 b_1 : A
hb_1 : IsSelfAdjoint b_1
a b : Unitization ℂ A
hb : IsSelfAdjoint b
⊢ star a * b * a ≤
    HMul.hMul (β := Unitization ℂ A) (star a)
        ((algebraMap ℝ (Unitization ℂ A) : (a : ℝ) → Unitization ℂ A) ‖b‖ : Unitization ℂ A) *
      a

Tactic:
star_left_conjugate_le_conjugate hb.le_algebraMap_norm_self _

Premises used: star_left_conjugate_le_conjugate, IsSelfAdjoint.le_algebraMap_norm_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 b_1 : A
hb_1 : IsSelfAdjoint b_1
a b : Unitization ℂ A
hb : IsSelfAdjoint b
⊢ HMul.hMul (β := Unitization ℂ A) (star a)
        ((algebraMap ℝ (Unitization ℂ A) : (a : ℝ) → Unitization ℂ A) ‖b‖ : Unitization ℂ A) *
      a =
    ‖b‖ • (star a * a)

Tactic:
simp [Algebra.algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a_1 b_1 : A
hb_1 : IsSelfAdjoint b_1
a b : Unitization ℂ A
hb : IsSelfAdjoint b
star :
  HMul.hMul (β := Unitization ℂ A) (Star.star a)
        ((algebraMap ℝ (Unitization ℂ A) : (a : ℝ) → Unitization ℂ A) ‖b‖ : Unitization ℂ A) *
      a =
    ‖b‖ • (Star.star a * a)
⊢ Star.star a * b * a ≤ ‖b‖ • (Star.star a * a)

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

Premises used: Norm.norm, Real, HMul.hMul, Algebra.algebraMap, star_left_conjugate_le_conjugate, Unitization, Complex, DFunLike.coe, IsSelfAdjoint.le_algebraMap_norm_self, Star.star
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
hb : IsSelfAdjoint b
⊢ a * b * star a ≤ ‖b‖ • (a * star a)

Tactic:
simpa using star_left_conjugate_le_norm_smul (a := star a)

Premises used: CStarAlgebra.star_left_conjugate_le_norm_smul
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
this : IsClosed.{u_1} (X := Unitization ℂ A) {a : Unitization ℂ A | 0 ≤ a}
rw : IsClosed.{u_1} (X := Unitization ℂ A) (Unitization.inr '' {a : A | 0 ≤ a})
⊢ IsClosed.{u_1} (X := A) {a : A | 0 ≤ a}

Tactic:
rw [Unitization.isometry_inr (𝕜 := ℂ) |>.isClosedEmbedding.isClosed_iff_image_isClosed]

Premises used: Unitization.isometry_inr, Topology.IsClosedEmbedding.isClosed_iff_image_isClosed, Isometry.isClosedEmbedding
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
this : IsClosed.{u_1} (X := Unitization ℂ A) {a : Unitization ℂ A | 0 ≤ a}
⊢ IsClosed.{u_1} (X := Unitization ℂ A) ({a : Unitization ℂ A | 0 ≤ a} ∩ Set.range Unitization.inr)

Tactic:
this.inter <| (Unitization.isometry_inr (𝕜 := ℂ)).isClosedEmbedding.isClosed_range

Premises used: Unitization.isometry_inr, Isometry.isClosedEmbedding, IsClosed.inter, Topology.IsClosedEmbedding.isClosed_range
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
this : IsClosed.{u_1} (X := Unitization ℂ A) {a : Unitization ℂ A | 0 ≤ a}
h :
  Eq.{u_1 + 1} (α := Set (Unitization ℂ A)) (Unitization.inr '' {a : A | 0 ≤ a})
    ({a : Unitization ℂ A | 0 ≤ a} ∩ Set.range Unitization.inr)
⊢ IsClosed.{u_1} (X := Unitization ℂ A) (Unitization.inr '' {a : A | 0 ≤ a})

Tactic:
convert! this.inter <| (Unitization.isometry_inr (𝕜 := ℂ)).isClosedEmbedding.isClosed_range

Premises used: Unitization.isometry_inr, Isometry.isClosedEmbedding, IsClosed.inter, Topology.IsClosedEmbedding.isClosed_range
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
this : IsClosed.{u_1} (X := Unitization ℂ A) {a : Unitization ℂ A | 0 ≤ a}
h :
  ∀ (a : Unitization ℂ A),
    Membership.mem (γ := Set (Unitization ℂ A)) (Unitization.inr '' {a : A | 0 ≤ a}) a ↔
      Membership.mem (γ := Set (Unitization ℂ A)) ({a : Unitization ℂ A | 0 ≤ a} ∩ Set.range Unitization.inr) a
⊢ Eq.{u_1 + 1} (α := Set (Unitization ℂ A)) (Unitization.inr '' {a : A | 0 ≤ a})
    ({a : Unitization ℂ A | 0 ≤ a} ∩ Set.range Unitization.inr)

Tactic:
ext a
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
this : IsClosed.{u_1} (X := Unitization ℂ A) {a : Unitization ℂ A | 0 ≤ a}
a : Unitization ℂ A
h : (∃ (x : A), 0 ≤ x ∧ (↑x : Unitization ℂ A) = a) ↔ ∃ (x : A), 0 ≤ a ∧ (↑x : Unitization ℂ A) = a
⊢ Membership.mem (γ := Set (Unitization ℂ A)) (Unitization.inr '' {a : A | 0 ≤ a}) a ↔
    Membership.mem (γ := Set (Unitization ℂ A)) ({a : Unitization ℂ A | 0 ≤ a} ∩ Set.range Unitization.inr) a

Tactic:
simp only [Set.mem_image, Set.mem_setOf_eq, Set.mem_inter_iff, Set.mem_range, ← exists_and_left]

Premises used: Set.mem_range, Set.mem_inter_iff, Set.mem_image, exists_and_left, Set.mem_setOf_eq
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
this : IsClosed.{u_1} (X := Unitization ℂ A) {a : Unitization ℂ A | 0 ≤ a}
a : Unitization ℂ A
h : ∀ (x : A), 0 ≤ x ∧ (↑x : Unitization ℂ A) = a ↔ 0 ≤ a ∧ (↑x : Unitization ℂ A) = a
⊢ (∃ (x : A), 0 ≤ x ∧ (↑x : Unitization ℂ A) = a) ↔ ∃ (x : A), 0 ≤ a ∧ (↑x : Unitization ℂ A) = a

Tactic:
congr! 2 with x
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
this : IsClosed.{u_1} (X := Unitization ℂ A) {a : Unitization ℂ A | 0 ≤ a}
a : Unitization ℂ A
x : A
h : (↑x : Unitization ℂ A) = a
⊢ 0 ≤ x ↔ 0 ≤ a

Tactic:
simp [← h]
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
this : IsClosed.{u_1} (X := Unitization ℂ A) {a : Unitization ℂ A | 0 ≤ a}
a : Unitization ℂ A
x : A
⊢ 0 ≤ x ∧ (↑x : Unitization ℂ A) = a ↔ 0 ≤ a ∧ (↑x : Unitization ℂ A) = a

Tactic:
exact and_congr_left fun h ↦ by simp [← h]

Premises used: and_congr_left
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
suffices : IsClosed.{u_1} (X := Unitization ℂ A) {a : Unitization ℂ A | 0 ≤ a}
⊢ IsClosed.{u_1} (X := A) {a : A | 0 ≤ a}

Tactic:
suffices IsClosed {a : A⁺¹ | 0 ≤ a} by
    rw [Unitization.isometry_inr (𝕜 := ℂ) |>.isClosedEmbedding.isClosed_iff_image_isClosed]
    convert! this.inter <| (Unitization.isometry_inr (𝕜 := ℂ)).isClosedEmbedding.isClosed_range
    ext a
    simp only [Set.mem_image, Set.mem_setOf_eq, Set.mem_inter_iff, Set.mem_range, ← exists_and_left]
    congr! 2 with x
    exact and_congr_left fun h ↦ by simp [← h]
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
simp :
  IsClosed.{u_1} (X := Unitization ℂ A)
    ({a : Unitization ℂ A | IsSelfAdjoint a} ∩
      {a : Unitization ℂ A |
        ‖HSub.hSub (α := Unitization ℂ A)
              ((algebraMap ℝ (Unitization ℂ A) : (a : ℝ) → Unitization ℂ A) (↑‖a‖₊ : ℝ) : Unitization ℂ A) a‖₊ ≤
          ‖a‖₊})
⊢ IsClosed.{u_1} (X := Unitization ℂ A) {a : Unitization ℂ A | 0 ≤ a}

Tactic:
simp only [nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts,
    and_congr_right (SpectrumRestricts.nnreal_iff_nnnorm · le_rfl), Set.setOf_and]

Premises used: Set.setOf_and, le_rfl, and_congr_right, nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts, SpectrumRestricts.nnreal_iff_nnnorm
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
⊢ IsClosed.{u_1} (X := Unitization ℂ A)
    ({a : Unitization ℂ A | IsSelfAdjoint a} ∩
      {a : Unitization ℂ A |
        ‖HSub.hSub (α := Unitization ℂ A)
              ((algebraMap ℝ (Unitization ℂ A) : (a : ℝ) → Unitization ℂ A) (↑‖a‖₊ : ℝ) : Unitization ℂ A) a‖₊ ≤
          ‖a‖₊})

Tactic:
isClosed_eq ?_ ?_ |>.inter <| isClosed_le ?_ ?_

Premises used: IsSelfAdjoint, setOf, isClosed_le, isClosed_eq, IsClosed.inter
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
refine_1 : Continuous.{u_1, u_1} (X := Unitization ℂ A) star
refine_2 : Continuous (Y := Unitization ℂ A) fun (a : Unitization ℂ A) ↦ a
refine_3 :
  Continuous (Y := ℝ≥0) fun (a : Unitization ℂ A) ↦
    ‖HSub.hSub (α := Unitization ℂ A)
        ((algebraMap ℝ (Unitization ℂ A) : (a : ℝ) → Unitization ℂ A) (↑‖a‖₊ : ℝ) : Unitization ℂ A) a‖₊
refine_4 : Continuous.{u_1, 0} (X := Unitization ℂ A) nnnorm
⊢ IsClosed.{u_1} (X := Unitization ℂ A)
    ({a : Unitization ℂ A | IsSelfAdjoint a} ∩
      {a : Unitization ℂ A |
        ‖HSub.hSub (α := Unitization ℂ A)
              ((algebraMap ℝ (Unitization ℂ A) : (a : ℝ) → Unitization ℂ A) (↑‖a‖₊ : ℝ) : Unitization ℂ A) a‖₊ ≤
          ‖a‖₊})

Tactic:
refine isClosed_eq ?_ ?_ |>.inter <| isClosed_le ?_ ?_

Premises used: isClosed_le, isClosed_eq, IsClosed.inter
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
⊢ Continuous.{u_1, u_1} (X := Unitization ℂ A) star

Tactic:
fun_prop
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
⊢ Continuous (Y := Unitization ℂ A) fun (a : Unitization ℂ A) ↦ a

Tactic:
fun_prop
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
⊢ Continuous (Y := ℝ≥0) fun (a : Unitization ℂ A) ↦
    ‖HSub.hSub (α := Unitization ℂ A)
        ((algebraMap ℝ (Unitization ℂ A) : (a : ℝ) → Unitization ℂ A) (↑‖a‖₊ : ℝ) : Unitization ℂ A) a‖₊

Tactic:
fun_prop
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
⊢ Continuous.{u_1, 0} (X := Unitization ℂ A) nnnorm

Tactic:
fun_prop
-- 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
pos : ∀ (hf₀ : f 0 = 0), ConvexOn ℝ s (cfcₙ (p := IsSelfAdjoint) f)
by_cases : ∀ (hf₀ : ¬f 0 = 0), ConvexOn ℝ s (cfcₙ (p := IsSelfAdjoint) f)
⊢ ConvexOn ℝ s (cfcₙ (p := IsSelfAdjoint) f)

Tactic:
by_cases hf₀ : f 0 = 0

Premises used: OfNat.ofNat
-- 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 : ∀ (x : A), cfcₙ (p := IsSelfAdjoint) f x = 0
⊢ cfcₙ (p := IsSelfAdjoint) f = fun (x : A) ↦ 0

Tactic:
ext x
-- 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
x : A
⊢ cfcₙ (p := IsSelfAdjoint) f x = 0

Tactic:
simp [cfcₙ_apply_of_not_map_zero _ hf₀]

Premises used: cfcₙ_apply_of_not_map_zero
-- 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
⊢ cfcₙ (p := IsSelfAdjoint) f = fun (x : A) ↦ 0

Tactic:
have : (cfcₙ f : A → A) = fun _ => 0 := by
      ext x
      simp [cfcₙ_apply_of_not_map_zero _ 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
this : cfcₙ (p := IsSelfAdjoint) f = fun (x : A) ↦ 0
rw : ConvexOn ℝ (β := A) s fun (x : A) ↦ 0
⊢ ConvexOn ℝ s (cfcₙ (p := IsSelfAdjoint) f)

Tactic:
rw [this]
-- 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
this : cfcₙ (p := IsSelfAdjoint) f = fun (x : A) ↦ 0
⊢ ConvexOn ℝ (β := A) s fun (x : A) ↦ 0

Tactic:
convexOn_const _ ?_

Premises used: convexOn_const
-- 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
this : cfcₙ (p := IsSelfAdjoint) f = fun (x : A) ↦ 0
refine : Convex ℝ s
⊢ ConvexOn ℝ (β := A) s fun (x : A) ↦ 0

Tactic:
refine convexOn_const _ ?_

Premises used: convexOn_const
-- 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
this : cfcₙ (p := IsSelfAdjoint) f = fun (x : A) ↦ 0
⊢ Convex ℝ (E := A)
    (Set.preimage (β := Unitization ℂ A) (⇑inrl : (a : A) → Unitization ℂ A) ((⇑inrl : (a : A) → Unitization ℂ A) '' s))

Tactic:
have : Convex ℝ (inrl ⁻¹' inrl '' s) := Convex.linear_preimage hf.1 _
-- 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
this_1 : cfcₙ (p := IsSelfAdjoint) f = fun (x : A) ↦ 0
this :
  Convex ℝ (E := A)
    (Set.preimage (β := Unitization ℂ A) (⇑inrl : (a : A) → Unitization ℂ A) ((⇑inrl : (a : A) → Unitization ℂ A) '' s))
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : Convex ℝ s), Convex ℝ s
⊢ Convex ℝ s

Tactic:
rwa [Set.preimage_image_eq _ inrHom_injective] at this

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 : ConvexOn ℝ (inr '' s) (cfc (p := IsSelfAdjoint) f)
inrl : A →ₗ[ℝ] Unitization ℂ A := inrHom ℝ ℂ A
hf₀ : ¬f 0 = 0
⊢ ConvexOn ℝ s (cfcₙ (p := IsSelfAdjoint) f)

Tactic:
case neg =>
    have : (cfcₙ f : A → A) = fun _ => 0 := by
      ext x
      simp [cfcₙ_apply_of_not_map_zero _ hf₀]
    rw [this]
    refine convexOn_const _ ?_
    have : Convex ℝ (inrl ⁻¹' inrl '' s) := Convex.linear_preimage hf.1 _
    rwa [Set.preimage_image_eq _ inrHom_injective] at this

Premises used: Unitization.inrHom_injective, Set.preimage_image_eq, convexOn_const
-- 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
⊢ ConvexOn ℝ s (cfcₙ (p := IsSelfAdjoint) f)

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

Premises used: Unitization.convexOn_of_convexOn_inr_comp, IsSelfAdjoint.cfcₙ