awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
hc' : IsSelfAdjoint (-c)
ha : IsSelfAdjoint a
s : Set ℝ := σₙ ℝ a ∪ σₙ ℝ b ∪ σₙ ℝ (-c)
hs : CompactSpace (↑s : Type)
has : σₙ ℝ a ⊆ s
hbs : σₙ ℝ b ⊆ s
hcs : σₙ ℝ (-c) ⊆ s
this : Fact (0 ∈ s)
mul₁ :
  ∀ (f g : C((↑s : Type), ℝ)₀),
    HMul.hMul (α := A) (β := A)
        (((cfcₙHomSuperset (p := IsSelfAdjoint) hb' (s := s) hbs : C((↑s : Type), ℝ)₀ →⋆ₙₐ[ℝ] A) :
              (a : C((↑s : Type), ℝ)₀) → A)
            f :
          A)
        (((cfcₙHomSuperset (p := IsSelfAdjoint) hc' (s := s) hcs : C((↑s : Type), ℝ)₀ →⋆ₙₐ[ℝ] A) :
              (a : C((↑s : Type), ℝ)₀) → A)
            g :
          A) =
      0
mul₂ :
  ∀ (f g : C((↑s : Type), ℝ)₀),
    HMul.hMul (α := A) (β := A)
        (((cfcₙHomSuperset (p := IsSelfAdjoint) hc' (s := s) hcs : C((↑s : Type), ℝ)₀ →⋆ₙₐ[ℝ] A) :
              (a : C((↑s : Type), ℝ)₀) → A)
            f :
          A)
        (((cfcₙHomSuperset (p := IsSelfAdjoint) hb' (s := s) hbs : C((↑s : Type), ℝ)₀ →⋆ₙₐ[ℝ] A) :
              (a : C((↑s : Type), ℝ)₀) → A)
            g :
          A) =
      0
ψ : C((↑s : Type), ℝ)₀ →⋆ₙₐ[ℝ] A :=
  let __src :=
    HAdd.hAdd (α := C((↑s : Type), ℝ)₀ →ₗ[ℝ] A)
      (↑(cfcₙHomSuperset (p := IsSelfAdjoint) hb' (s := s) hbs : C((↑s : Type), ℝ)₀ →⋆ₙₐ[ℝ] A) :
        [inst_12 : FunLike (C((↑s : Type), ℝ)₀ →⋆ₙₐ[ℝ] A) C((↑s : Type), ℝ)₀ A] →
          [SemilinearMapClass (C((↑s : Type), ℝ)₀ →⋆ₙₐ[ℝ] A) (RingHom.id ℝ) C((↑s : Type), ℝ)₀ A] →
            C((↑s : Type), ℝ)₀ →ₗ[ℝ] A)
      (↑(cfcₙHomSuperset (p := IsSelfAdjoint) hc' (s := s) hcs : C((↑s : Type), ℝ)₀ →⋆ₙₐ[ℝ] A) :
        [inst_12 : FunLike (C((↑s : Type), ℝ)₀ →⋆ₙₐ[ℝ] A) C((↑s : Type), ℝ)₀ A] →
          [SemilinearMapClass (C((↑s : Type), ℝ)₀ →⋆ₙₐ[ℝ] A) (RingHom.id ℝ) C((↑s : Type), ℝ)₀ A] →
            C((↑s : Type), ℝ)₀ →ₗ[ℝ] A);
  {
    toFun :=
      HAdd.hAdd (α := (a : C((↑s : Type), ℝ)₀) → A)
        (⇑(cfcₙHomSuperset (p := IsSelfAdjoint) hb' (s := s) hbs : C((↑s : Type), ℝ)₀ →⋆ₙₐ[ℝ] A) :
          (a : C((↑s : Type), ℝ)₀) → A)
        (⇑(cfcₙHomSuperset (p := IsSelfAdjoint) hc' (s := s) hcs : C((↑s : Type), ℝ)₀ →⋆ₙₐ[ℝ] A) :
          (a : C((↑s : Type), ℝ)₀) → A),
    map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯, map_star' := ⋯ }
key : cfcₙHomSuperset (p := IsSelfAdjoint) ha (s := s) has = ψ
⊢ Eq (α := ℝ) (({ toFun := fun (x : (↑s : Type)) ↦ (↑x : ℝ)⁺, continuous_toFun := ⋯ } : (a : (↑s : Type)) → ℝ) 0 : ℝ)
    (0 : ℝ)
have simp : LE.le (α := ℝ) (↑0 : ℝ) 0
Tactic: simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : Ring A
inst_1 : Algebra ℝ A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_5 : T2Space A
⊢ Eq.{u_1 + 1} (α := A) 1⁺ 1
have rw : cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) 1 = 1
Tactic: rw [CFC.posPart_def, cfcₙ_eq_cfc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : Ring A
inst_1 : Algebra ℝ A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_5 : T2Space A
⊢ Eq.{u_1 + 1} (α := A) 1⁻ 0
have rw : cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) 1 = 0
Tactic: rw [CFC.negPart_def, cfcₙ_eq_cfc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : Ring A
inst_1 : Algebra ℝ A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_5 : T2Space A
r : ℝ
⊢ Eq (α := A) (((algebraMap ℝ A : (a : ℝ) → A) r)⁺ : A) ((algebraMap ℝ A : (a : ℝ) → A) r⁺ : A)
have rw : cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) ((algebraMap ℝ A : (a : ℝ) → A) r) = (algebraMap ℝ A : (a : ℝ) → A) r⁺
Tactic: rw [CFC.posPart_def, cfcₙ_eq_cfc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : Ring A
inst_1 : Algebra ℝ A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_5 : T2Space A
r : ℝ
⊢ Eq (α := A) (((algebraMap ℝ A : (a : ℝ) → A) r)⁻ : A) ((algebraMap ℝ A : (a : ℝ) → A) r⁻ : A)
have rw : cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) ((algebraMap ℝ A : (a : ℝ) → A) r) = (algebraMap ℝ A : (a : ℝ) → A) r⁻
Tactic: rw [CFC.negPart_def, cfcₙ_eq_cfc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : Ring A
inst_1 : Algebra ℝ A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_5 : T2Space A
r : ℝ≥0
⊢ Eq (α := A) (((algebraMap ℝ≥0 A : (a : ℝ≥0) → A) r)⁺ : A) ((algebraMap ℝ≥0 A : (a : ℝ≥0) → A) r : A)
have rw : cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺)
    ((algebraMap ℝ A : (a : ℝ) → A) ((algebraMap ℝ≥0 ℝ : (a : ℝ≥0) → ℝ) r : ℝ)) =
  (algebraMap ℝ A : (a : ℝ) → A) ((algebraMap ℝ≥0 ℝ : (a : ℝ≥0) → ℝ) r : ℝ)
Tactic: rw [CFC.posPart_def, cfcₙ_eq_cfc, IsScalarTower.algebraMap_apply ℝ≥0 ℝ A]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : Ring A
inst_1 : Algebra ℝ A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_5 : T2Space A
n : ℕ
⊢ Eq.{u_1 + 1} (α := A) (↑n : A)⁺ (↑n : A)
have rw : Eq (α := A) (((algebraMap ℝ≥0 A : (a : ℝ≥0) → A) (↑n : ℝ≥0))⁺ : A) ((algebraMap ℝ≥0 A : (a : ℝ≥0) → A) (↑n : ℝ≥0) : A)
Tactic: rw [← map_natCast (algebraMap ℝ≥0 A), posPart_algebraMap_nnreal]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : Ring A
inst_1 : Algebra ℝ A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_5 : T2Space A
n : ℕ
rw :
  Eq (α := A) (((algebraMap ℝ≥0 A : (a : ℝ≥0) → A) (↑n : ℝ≥0))⁺ : A) ((algebraMap ℝ≥0 A : (a : ℝ≥0) → A) (↑n : ℝ≥0) : A)
⊢ Eq.{u_1 + 1} (α := A) (↑n : A)⁺ (↑n : A)
have rw₁ : Eq (α := A) ((algebraMap ℝ≥0 A : (a : ℝ≥0) → A) (↑n : ℝ≥0) : A) ((algebraMap ℝ≥0 A : (a : ℝ≥0) → A) (↑n : ℝ≥0) : A)
Tactic: rw [← map_natCast (algebraMap ℝ≥0 A), posPart_algebraMap_nnreal]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℂ A
inst_2 : SMulCommClass ℂ A A
inst_3 : IsScalarTower ℂ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
x : A
⊢ HSub.hSub (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁺
        (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁻ +
      (HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁺ -
        HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁻) =
    x
have rw : (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
    (HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁺ -
      HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁻) =
  x
Tactic: rw [CFC.posPart_sub_negPart _ (ℜ x).2, ← smul_sub, CFC.posPart_sub_negPart _ (ℑ x).2,
    realPart_add_I_smul_imaginaryPart x]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℂ A
inst_2 : SMulCommClass ℂ A A
inst_3 : IsScalarTower ℂ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
x : A
rw :
  (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
      (HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁺ -
        HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁻) =
    x
⊢ HSub.hSub (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁺
        (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁻ +
      (HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁺ -
        HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁻) =
    x
have rw₁ : (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
    I •
      HSub.hSub (α := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁺
        (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁻ =
  x
Tactic: rw [CFC.posPart_sub_negPart _ (ℜ x).2, ← smul_sub, CFC.posPart_sub_negPart _ (ℑ x).2,
    realPart_add_I_smul_imaginaryPart x]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℂ A
inst_2 : SMulCommClass ℂ A A
inst_3 : IsScalarTower ℂ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
x : A
rw :
  (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
      (HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁺ -
        HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁻) =
    x
rw₁ :
  (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
      I •
        HSub.hSub (α := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁺
          (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁻ =
    x
⊢ HSub.hSub (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁺
        (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁻ +
      (HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁺ -
        HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁻) =
    x
have rw₂ : (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
    HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) =
  x
Tactic: rw [CFC.posPart_sub_negPart _ (ℜ x).2, ← smul_sub, CFC.posPart_sub_negPart _ (ℑ x).2,
    realPart_add_I_smul_imaginaryPart x]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℂ A
inst_2 : SMulCommClass ℂ A A
inst_3 : IsScalarTower ℂ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
x : A
rw :
  (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
      (HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁺ -
        HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁻) =
    x
rw₁ :
  (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
      I •
        HSub.hSub (α := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁺
          (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁻ =
    x
rw₂ :
  (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
      HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) =
    x
⊢ HSub.hSub (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁺
        (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁻ +
      (HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁺ -
        HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁻) =
    x
have rw₃ : x = x
Tactic: rw [CFC.posPart_sub_negPart _ (ℜ x).2, ← smul_sub, CFC.posPart_sub_negPart _ (ℑ x).2,
    realPart_add_I_smul_imaginaryPart x]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℂ A
inst_2 : SMulCommClass ℂ A A
inst_3 : IsScalarTower ℂ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : PartialOrder A
inst_9 : StarOrderedRing A
⊢ Eq.{u_1 + 1} (α := Submodule ℂ A) (span ℂ {a : A | 0 ≤ a}) ⊤
have refine : ∀ (x : A), Membership.mem (γ := Submodule ℂ A) ⊤ x → Membership.mem (γ := Submodule ℂ A) (span ℂ {a : A | 0 ≤ a}) x
Tactic: refine eq_top_iff.mpr fun x _ => ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℂ A
inst_2 : SMulCommClass ℂ A A
inst_3 : IsScalarTower ℂ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : PartialOrder A
inst_9 : StarOrderedRing A
x : A
h : Membership.mem (γ := Submodule ℂ A) ⊤ x
⊢ Membership.mem (γ := Submodule ℂ A) (span ℂ {a : A | 0 ≤ a}) x
have rw : Membership.mem (γ := Submodule ℂ A) (span ℂ {a : A | 0 ≤ a})
  (HSub.hSub (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁺
      (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁻ +
    (HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁺ -
      HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁻))
Tactic: rw [← CStarAlgebra.linear_combination_nonneg x]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℂ A
inst_2 : SMulCommClass ℂ A A
inst_3 : IsScalarTower ℂ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : PartialOrder A
inst_9 : StarOrderedRing A
x : A
h : Membership.mem (γ := Submodule ℂ A) ⊤ x
⊢ Membership.mem (γ := Submodule ℂ A) (span ℂ {a : A | 0 ≤ a})
    (HSub.hSub (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁺
        (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁻ +
      (HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁺ -
        HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁻))
have a : Membership.mem (γ := Submodule ℂ A) (span ℂ {a : A | 0 ≤ a})
  (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁺
Tactic: apply_rules [sub_mem, Submodule.smul_mem, add_mem]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℂ A
inst_2 : SMulCommClass ℂ A A
inst_3 : IsScalarTower ℂ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : PartialOrder A
inst_9 : StarOrderedRing A
x : A
h : Membership.mem (γ := Submodule ℂ A) ⊤ x
a :
  Membership.mem (γ := Submodule ℂ A) (span ℂ {a : A | 0 ≤ a})
    (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁺
⊢ Membership.mem (γ := Submodule ℂ A) (span ℂ {a : A | 0 ≤ a})
    (HSub.hSub (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁺
        (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁻ +
      (HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁺ -
        HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁻))
have a₁ : Membership.mem (γ := Submodule ℂ A) (span ℂ {a : A | 0 ≤ a})
  (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁻
Tactic: apply_rules [sub_mem, Submodule.smul_mem, add_mem]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℂ A
inst_2 : SMulCommClass ℂ A A
inst_3 : IsScalarTower ℂ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : PartialOrder A
inst_9 : StarOrderedRing A
x : A
h : Membership.mem (γ := Submodule ℂ A) ⊤ x
a :
  Membership.mem (γ := Submodule ℂ A) (span ℂ {a : A | 0 ≤ a})
    (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁺
a₁ :
  Membership.mem (γ := Submodule ℂ A) (span ℂ {a : A | 0 ≤ a})
    (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁻
⊢ Membership.mem (γ := Submodule ℂ A) (span ℂ {a : A | 0 ≤ a})
    (HSub.hSub (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁺
        (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁻ +
      (HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁺ -
        HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁻))
have a₂ : Membership.mem (γ := Submodule ℂ A) (span ℂ {a : A | 0 ≤ a})
  (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁺
Tactic: apply_rules [sub_mem, Submodule.smul_mem, add_mem]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℂ A
inst_2 : SMulCommClass ℂ A A
inst_3 : IsScalarTower ℂ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : PartialOrder A
inst_9 : StarOrderedRing A
x : A
h : Membership.mem (γ := Submodule ℂ A) ⊤ x
a :
  Membership.mem (γ := Submodule ℂ A) (span ℂ {a : A | 0 ≤ a})
    (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁺
a₁ :
  Membership.mem (γ := Submodule ℂ A) (span ℂ {a : A | 0 ≤ a})
    (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁻
a₂ :
  Membership.mem (γ := Submodule ℂ A) (span ℂ {a : A | 0 ≤ a})
    (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁺
⊢ Membership.mem (γ := Submodule ℂ A) (span ℂ {a : A | 0 ≤ a})
    (HSub.hSub (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁺
        (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁻ +
      (HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁺ -
        HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁻))
have a₃ : Membership.mem (γ := Submodule ℂ A) (span ℂ {a : A | 0 ≤ a})
  (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁻
Tactic: apply_rules [sub_mem, Submodule.smul_mem, add_mem]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℂ A
inst_2 : SMulCommClass ℂ A A
inst_3 : IsScalarTower ℂ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : PartialOrder A
inst_9 : StarOrderedRing A
x : A
h : Membership.mem (γ := Submodule ℂ A) ⊤ x
⊢ Membership.mem (γ := Submodule ℂ A) (span ℂ {a : A | 0 ≤ a})
    (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁺
have a : Membership.mem (γ := Set A) {a : A | 0 ≤ a} (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁺
Tactic: refine subset_span ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℂ A
inst_2 : SMulCommClass ℂ A A
inst_3 : IsScalarTower ℂ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : PartialOrder A
inst_9 : StarOrderedRing A
x : A
h : Membership.mem (γ := Submodule ℂ A) ⊤ x
⊢ Membership.mem (γ := Submodule ℂ A) (span ℂ {a : A | 0 ≤ a})
    (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁻
have a : Membership.mem (γ := Set A) {a : A | 0 ≤ a} (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁻
Tactic: refine subset_span ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℂ A
inst_2 : SMulCommClass ℂ A A
inst_3 : IsScalarTower ℂ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : PartialOrder A
inst_9 : StarOrderedRing A
x : A
h : Membership.mem (γ := Submodule ℂ A) ⊤ x
⊢ Membership.mem (γ := Submodule ℂ A) (span ℂ {a : A | 0 ≤ a})
    (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁺
have a : Membership.mem (γ := Set A) {a : A | 0 ≤ a} (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁺
Tactic: refine subset_span ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℂ A
inst_2 : SMulCommClass ℂ A A
inst_3 : IsScalarTower ℂ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : PartialOrder A
inst_9 : StarOrderedRing A
x : A
h : Membership.mem (γ := Submodule ℂ A) ⊤ x
⊢ Membership.mem (γ := Submodule ℂ A) (span ℂ {a : A | 0 ≤ a})
    (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁻
have a : Membership.mem (γ := Set A) {a : A | 0 ≤ a} (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁻
Tactic: refine subset_span ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric (goal)
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
⊢ ‖a⁺‖ ≤ ‖a‖
have pos : ∀ (ha : IsSelfAdjoint a), ‖a⁺‖ ≤ ‖a‖
Tactic: by_cases ha : IsSelfAdjoint a
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric (goal)
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
pos : ∀ (ha : IsSelfAdjoint a), ‖a⁺‖ ≤ ‖a‖
⊢ ‖a⁺‖ ≤ ‖a‖
have by_cases : ∀ (ha : ¬IsSelfAdjoint a), ‖a⁺‖ ≤ ‖a‖
Tactic: by_cases ha : IsSelfAdjoint a