awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
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 = ψ
simp : LE.le (α := ℝ) (↑0 : ℝ) 0
⊢ Eq (α := ℝ) (({ toFun := fun (x : (↑s : Type)) ↦ (↑x : ℝ)⁺, continuous_toFun := ⋯ } : (a : (↑s : Type)) → ℝ) 0 : ℝ)
    (0 : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
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 = ψ
⊢ LE.le (α := ℝ) (↑0 : ℝ) 0

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
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 = ψ
⊢ LE.le (α := ℝ) (↑0 : ℝ) 0

Tactic:
exact le_rfl

Premises used: le_rfl
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
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 = ψ
f : C((↑s : Type), ℝ)₀ := { toFun := fun (x : (↑s : Type)) ↦ (↑x : ℝ)⁺, continuous_toFun := ⋯, map_zero' := ⋯ }
⊢ Eq (α := A)
    (((cfcₙHomSuperset (p := IsSelfAdjoint) ha (s := s) has : C((↑s : Type), ℝ)₀ →⋆ₙₐ[ℝ] A) :
          (a : C((↑s : Type), ℝ)₀) → A)
        f :
      A)
    ((ψ : (a : C((↑s : Type), ℝ)₀) → A) f : A)

Tactic:
replace key := congr($key f)
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
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
rw : cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) 1 = 1
⊢ Eq.{u_1 + 1} (α := A) 1⁺ 1

Tactic:
rw [CFC.posPart_def, cfcₙ_eq_cfc]

Premises used: cfcₙ_eq_cfc, CFC.posPart_def
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
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
⊢ cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) 1 = 1

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
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
rw : cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) 1 = 0
⊢ Eq.{u_1 + 1} (α := A) 1⁻ 0

Tactic:
rw [CFC.negPart_def, cfcₙ_eq_cfc]

Premises used: cfcₙ_eq_cfc, CFC.negPart_def
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
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
⊢ cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) 1 = 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
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 : ℝ
rw : cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) ((algebraMap ℝ A : (a : ℝ) → A) r) = (algebraMap ℝ A : (a : ℝ) → A) r⁺
⊢ Eq (α := A) (((algebraMap ℝ A : (a : ℝ) → A) r)⁺ : A) ((algebraMap ℝ A : (a : ℝ) → A) r⁺ : A)

Tactic:
rw [CFC.posPart_def, cfcₙ_eq_cfc]

Premises used: cfcₙ_eq_cfc, CFC.posPart_def
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
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 : ℝ
⊢ cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) ((algebraMap ℝ A : (a : ℝ) → A) r) = (algebraMap ℝ A : (a : ℝ) → A) r⁺

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
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 : ℝ
rw : cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) ((algebraMap ℝ A : (a : ℝ) → A) r) = (algebraMap ℝ A : (a : ℝ) → A) r⁻
⊢ Eq (α := A) (((algebraMap ℝ A : (a : ℝ) → A) r)⁻ : A) ((algebraMap ℝ A : (a : ℝ) → A) r⁻ : A)

Tactic:
rw [CFC.negPart_def, cfcₙ_eq_cfc]

Premises used: cfcₙ_eq_cfc, CFC.negPart_def
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
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 : ℝ
⊢ cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) ((algebraMap ℝ A : (a : ℝ) → A) r) = (algebraMap ℝ A : (a : ℝ) → A) r⁻

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
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
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 : ℝ)
⊢ Eq (α := A) (((algebraMap ℝ≥0 A : (a : ℝ≥0) → A) r)⁺ : A) ((algebraMap ℝ≥0 A : (a : ℝ≥0) → A) r : A)

Tactic:
rw [CFC.posPart_def, cfcₙ_eq_cfc, IsScalarTower.algebraMap_apply ℝ≥0 ℝ A]

Premises used: Real, cfcₙ_eq_cfc, NNReal, CFC.posPart_def, IsScalarTower.algebraMap_apply
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
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
⊢ 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:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
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)
rw₁ 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)

Tactic:
rw [← map_natCast (algebraMap ℝ≥0 A), posPart_algebraMap_nnreal]

Premises used: Algebra.algebraMap, CFC.posPart_algebraMap_nnreal, NNReal, map_natCast
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
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
rw₃ rw₄ : x = 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

Tactic:
rw [CFC.posPart_sub_negPart _ (ℜ x).2, ← smul_sub, CFC.posPart_sub_negPart _ (ℑ x).2,
    realPart_add_I_smul_imaginaryPart x]

Premises used: CFC.posPart_sub_negPart, imaginaryPart, realPart_add_I_smul_imaginaryPart, smul_sub, realPart, DFunLike.coe, Subtype.property
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
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}) ⊤

Tactic:
eq_top_iff.mpr fun x _ => ?_

Premises used: Iff.mpr, eq_top_iff
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
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
refine :
  ∀ (x : A), Membership.mem (γ := Submodule ℂ A) ⊤ x → Membership.mem (γ := Submodule ℂ A) (span ℂ {a : A | 0 ≤ a}) x
⊢ Eq.{u_1 + 1} (α := Submodule ℂ A) (span ℂ {a : A | 0 ≤ a}) ⊤

Tactic:
refine eq_top_iff.mpr fun x _ => ?_

Premises used: Iff.mpr, eq_top_iff
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
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
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)⁻))
⊢ Membership.mem (γ := Submodule ℂ A) (span ℂ {a : A | 0 ≤ a}) x

Tactic:
rw [← CStarAlgebra.linear_combination_nonneg x]

Premises used: CStarAlgebra.linear_combination_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
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)⁺
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)⁻))

Tactic:
apply_rules [sub_mem, Submodule.smul_mem, add_mem]

Premises used: sub_mem, AddMemClass.add_mem, Submodule.smul_mem
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
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)⁺

Tactic:
subset_span ?_

Premises used: Submodule.subset_span