awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : Aˣ
ha : 0 ≤ (↑a : A)
hab : ‖star (sqrt (↑a : A) * sqrt (↑b⁻¹ : A)) * (sqrt (↑a : A) * sqrt (↑b⁻¹ : A))‖ ≤ 1
hb : 0 ≤ (↑b : A)
hb_inv : 0 ≤ (↑b⁻¹ : A)
ha_inv : 0 ≤ (↑a⁻¹ : A)
rwa :
  ∀ (hab : ‖star (sqrt (↑b⁻¹ : A)) * star (sqrt (↑a : A)) * (sqrt (↑a : A) * sqrt (↑b⁻¹ : A))‖ ≤ 1) (hb : 0 ≤ (↑b : A))
    (hb_inv : 0 ≤ (↑b⁻¹ : A)) (ha_inv : 0 ≤ (↑a⁻¹ : A)),
    ‖sqrt (↑b⁻¹ : A) * sqrt (↑a : A) * (star (sqrt (↑a : A)) * star (sqrt (↑b⁻¹ : A)))‖ ≤ 1
rwa₁ :
  ∀ (hab : ‖sqrt (↑b⁻¹ : A) * star (sqrt (↑a : A)) * (sqrt (↑a : A) * sqrt (↑b⁻¹ : A))‖ ≤ 1) (hb : 0 ≤ (↑b : A))
    (hb_inv : 0 ≤ (↑b⁻¹ : A)) (ha_inv : 0 ≤ (↑a⁻¹ : A)),
    ‖sqrt (↑b⁻¹ : A) * sqrt (↑a : A) * (sqrt (↑a : A) * star (sqrt (↑b⁻¹ : A)))‖ ≤ 1
⊢ ‖sqrt (↑b⁻¹ : A) * sqrt (↑a : A) * star (sqrt (↑b⁻¹ : A) * sqrt (↑a : A))‖ ≤ 1
have rwa₂ : ∀ (hab : ‖sqrt (↑b⁻¹ : A) * sqrt (↑a : A) * (sqrt (↑a : A) * sqrt (↑b⁻¹ : A))‖ ≤ 1) (hb : 0 ≤ (↑b : A))
  (hb_inv : 0 ≤ (↑b⁻¹ : A)) (ha_inv : 0 ≤ (↑a⁻¹ : A)),
  ‖sqrt (↑b⁻¹ : A) * sqrt (↑a : A) * (sqrt (↑a : A) * sqrt (↑b⁻¹ : A))‖ ≤ 1
Tactic: rwa [star_mul, IsSelfAdjoint.of_nonneg (sqrt_nonneg _),
    IsSelfAdjoint.of_nonneg (sqrt_nonneg _)] at hab ⊢
Cleared hypotheses: hab, hb, hb_inv, ha_inv
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
hab : a ≤ b
ha : IsStrictlyPositive a
⊢ HPow.hPow (β := ℝ) b (-1) ≤ HPow.hPow (β := ℝ) a (-1)
have lift : ∀ (b : Aˣ) (hab : a ≤ (↑b : A)), HPow.hPow (β := ℝ) (↑b : A) (-1) ≤ HPow.hPow (β := ℝ) a (-1)
Tactic: lift b to Aˣ using isUnit_of_le a hab
Cleared hypotheses: b, hab
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsStrictlyPositive a
b : Aˣ
hab : a ≤ (↑b : A)
⊢ HPow.hPow (β := ℝ) (↑b : A) (-1) ≤ HPow.hPow (β := ℝ) a (-1)
have lift : ∀ (a : Aˣ) (ha : IsStrictlyPositive (↑a : A)) (hab : (↑a : A) ≤ (↑b : A)),
  HPow.hPow (β := ℝ) (↑b : A) (-1) ≤ HPow.hPow (β := ℝ) (↑a : A) (-1)
Tactic: lift a to Aˣ using ha.isUnit
Cleared hypotheses: a, ha, hab
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
b a : Aˣ
ha : IsStrictlyPositive (↑a : A)
hab : (↑a : A) ≤ (↑b : A)
⊢ HPow.hPow (β := ℝ) (↑b : A) (-1) ≤ HPow.hPow (β := ℝ) (↑a : A) (-1)
have rw : (↑b⁻¹ : A) ≤ (↑a⁻¹ : A)
Tactic: rw [rpow_neg_one_eq_inv a, rpow_neg_one_eq_inv b (ha.nonneg.trans hab)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : 1 ≤ a
⊢ HPow.hPow (β := ℝ) a (-1) ≤ 1
have lift : ∀ (a : Aˣ) (ha : 1 ≤ (↑a : A)), HPow.hPow (β := ℝ) (↑a : A) (-1) ≤ 1
Tactic: lift a to Aˣ using isUnit_of_le 1 ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : Aˣ
ha : 1 ≤ (↑a : A)
⊢ HPow.hPow (β := ℝ) (↑a : A) (-1) ≤ 1
have rw : (↑a⁻¹ : A) ≤ 1
Tactic: rw [rpow_neg_one_eq_inv a (zero_le_one.trans ha)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
⊢ Membership.mem (γ := Set A) {a : A | IsStrictlyPositive a} a →
    ∀ ⦃b : A⦄, Membership.mem (γ := Set A) {a : A | IsStrictlyPositive a} b → a ≤ b → Ring.inverse b ≤ Ring.inverse a
have IsStrictlyPositive : ∀ (apos : IsStrictlyPositive a) ⦃b : A⦄,
  Membership.mem (γ := Set A) {a : A | IsStrictlyPositive a} b → a ≤ b → Ring.inverse b ≤ Ring.inverse a
Tactic: (apos : IsStrictlyPositive a)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
apos : IsStrictlyPositive a
b : A
⊢ Membership.mem (γ := Set A) {a : A | IsStrictlyPositive a} b → a ≤ b → Ring.inverse b ≤ Ring.inverse a
have IsStrictlyPositive : ∀ (bpos : IsStrictlyPositive b), a ≤ b → Ring.inverse b ≤ Ring.inverse a
Tactic: (bpos : IsStrictlyPositive b)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
apos : IsStrictlyPositive a
b : A
bpos : IsStrictlyPositive b
hab : a ≤ b
⊢ Ring.inverse b ≤ Ring.inverse a
have rw : (↑sorry.unit⁻¹ : A) ≤ (↑sorry.unit⁻¹ : A)
Tactic: rw [Ring.inverse_of_isUnit (by grind), Ring.inverse_of_isUnit (by grind)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (hypothesis)
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
⊢ 0 ≤ x
have hx₁ : x ∈ spectrum ℂ (A := Unitization ℂ A) (↑a : Unitization ℂ A)
Tactic: rw [Unitization.quasispectrum_eq_spectrum_inr' ℂ ℂ a] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (hypothesis)
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‖
⊢ ‖a‖ ≤ ‖b‖
have hb : 0 ≤ b
Tactic: have hb := ha.trans hab
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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‖
have suffices : ∀ (a b : Unitization ℂ A), 0 ≤ a → 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])
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (hypothesis)
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
⊢ ‖a‖ ≤ ‖b‖
have hb : 0 ≤ b
Tactic: have hb : 0 ≤ b := ha.trans hab
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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)
⊢ star a * b * a ≤ ‖b‖ • (star a * a)
have rw : LE.le (α := Unitization ℂ A) (↑(star a * b * a) : Unitization ℂ A) (↑(‖b‖ • (star a * a)) : Unitization ℂ A)
Tactic: rw [← Unitization.inr_le_iff _ _ (by aesop) ((IsSelfAdjoint.all _).smul (.star_mul_self a))]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
hb : IsSelfAdjoint b
⊢ star a * b * a ≤ ‖b‖ • (star a * a)
have suffices : ∀ (a b : Unitization ℂ A), IsSelfAdjoint b → 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 ℂ
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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 ≤ ‖b‖ • (star a * a)
have star : HMul.hMul (β := Unitization ℂ A) (star a)
      ((algebraMap ℝ (Unitization ℂ A) : (a : ℝ) → Unitization ℂ A) ‖b‖ : Unitization ℂ A) *
    a =
  ‖b‖ • (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]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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 := A) {a : A | 0 ≤ a}
have rw : IsClosed.{u_1} (X := Unitization ℂ A) (Unitization.inr '' {a : A | 0 ≤ a})
Tactic: rw [Unitization.isometry_inr (𝕜 := ℂ) |>.isClosedEmbedding.isClosed_iff_image_isClosed]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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) (Unitization.inr '' {a : A | 0 ≤ a})
have h : Eq.{u_1 + 1} (α := Set (Unitization ℂ A)) (Unitization.inr '' {a : A | 0 ≤ a})
  ({a : Unitization ℂ A | 0 ≤ a} ∩ Set.range Unitization.inr)
Tactic: convert! this.inter <| (Unitization.isometry_inr (𝕜 := ℂ)).isClosedEmbedding.isClosed_range
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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}
⊢ Eq.{u_1 + 1} (α := Set (Unitization ℂ A)) (Unitization.inr '' {a : A | 0 ≤ a})
    ({a : Unitization ℂ A | 0 ≤ a} ∩ Set.range Unitization.inr)
have 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
Tactic: ext a
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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
⊢ 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
have h : (∃ (x : A), 0 ≤ x ∧ (↑x : Unitization ℂ A) = a) ↔ ∃ (x : A), 0 ≤ a ∧ (↑x : Unitization ℂ A) = a
Tactic: simp only [Set.mem_image, Set.mem_setOf_eq, Set.mem_inter_iff, Set.mem_range, ← exists_and_left]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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) ↔ ∃ (x : A), 0 ≤ a ∧ (↑x : Unitization ℂ A) = a
have h : ∀ (x : A), 0 ≤ x ∧ (↑x : Unitization ℂ A) = a ↔ 0 ≤ a ∧ (↑x : Unitization ℂ A) = a
Tactic: congr! 2 with x
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
⊢ IsClosed.{u_1} (X := A) {a : A | 0 ≤ a}
have suffices : IsClosed.{u_1} (X := Unitization ℂ A) {a : Unitization ℂ 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]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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 | 0 ≤ a}
have 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‖₊})
Tactic: simp only [nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts,
    and_congr_right (SpectrumRestricts.nnreal_iff_nnnorm · le_rfl), Set.setOf_and]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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‖₊})
have refine_1 : Continuous.{u_1, u_1} (X := Unitization ℂ A) star
Tactic: refine isClosed_eq ?_ ?_ |>.inter <| isClosed_le ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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
⊢ 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‖₊})
have refine_2 : Continuous (Y := Unitization ℂ A) fun (a : Unitization ℂ A) ↦ a
Tactic: refine isClosed_eq ?_ ?_ |>.inter <| isClosed_le ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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
⊢ 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‖₊})
have refine_3 : Continuous (Y := ℝ≥0) fun (a : Unitization ℂ A) ↦
  ‖HSub.hSub (α := Unitization ℂ A)
      ((algebraMap ℝ (Unitization ℂ A) : (a : ℝ) → Unitization ℂ A) (↑‖a‖₊ : ℝ) : Unitization ℂ A) a‖₊
Tactic: refine isClosed_eq ?_ ?_ |>.inter <| isClosed_le ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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‖₊
⊢ 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‖₊})
have refine_4 : Continuous.{u_1, 0} (X := Unitization ℂ A) nnnorm
Tactic: refine isClosed_eq ?_ ?_ |>.inter <| isClosed_le ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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
⊢ ConvexOn ℝ s (cfcₙ (p := IsSelfAdjoint) f)
have pos : ∀ (hf₀ : f 0 = 0), ConvexOn ℝ s (cfcₙ (p := IsSelfAdjoint) f)
Tactic: by_cases hf₀ : f 0 = 0
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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)
⊢ ConvexOn ℝ s (cfcₙ (p := IsSelfAdjoint) f)
have by_cases : ∀ (hf₀ : ¬f 0 = 0), ConvexOn ℝ s (cfcₙ (p := IsSelfAdjoint) f)
Tactic: by_cases hf₀ : f 0 = 0
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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
have h : ∀ (x : A), cfcₙ (p := IsSelfAdjoint) f x = 0
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (hypothesis)
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)
have this : 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₀]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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 ℝ s (cfcₙ (p := IsSelfAdjoint) f)
have rw : ConvexOn ℝ (β := A) s fun (x : A) ↦ 0
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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
have refine : Convex ℝ s
Tactic: refine convexOn_const _ ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (hypothesis)
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 ℝ s
have this₁ : 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 _
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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))
⊢ Convex ℝ s
have rwa : ∀ (this : Convex ℝ s), Convex ℝ s
Tactic: rwa [Set.preimage_image_eq _ inrHom_injective] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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)
have pos : ConvexOn ℝ (β := Unitization ℂ A) s (inr ∘ cfcₙ (p := IsSelfAdjoint) f)
Tactic: refine convexOn_of_convexOn_inr_comp (fun _ => IsSelfAdjoint.cfcₙ) ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (hypothesis)
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 ℝ (β := Unitization ℂ A) s (inr ∘ cfcₙ (p := IsSelfAdjoint) f)
have h₁ : 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
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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)
have h : ∀ (x : A), (↑(cfcₙ (p := IsSelfAdjoint) f x) : Unitization ℂ A) = cfc (p := IsSelfAdjoint) f (↑x : Unitization ℂ A)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
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
⊢ (↑(cfcₙ (p := IsSelfAdjoint) f x) : Unitization ℂ A) = cfc (p := IsSelfAdjoint) f (↑x : Unitization ℂ A)
have h : cfc (p := IsSelfAdjoint) f (↑x : Unitization ℂ A) = cfc (p := IsSelfAdjoint) f (↑x : Unitization ℂ A)
Tactic: rw [real_cfcₙ_eq_cfc_inr ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (hypothesis)
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)
⊢ ConvexOn ℝ (β := Unitization ℂ A) s (inr ∘ cfcₙ (p := IsSelfAdjoint) f)
have 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)
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 ..]