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
a : A
ha : IsSelfAdjoint a
pos : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺ * x⁻) a = cfcₙ (R := ℝ) (p := IsSelfAdjoint) 0 a
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) a * cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) a = 0

Tactic:
rw [← cfcₙ_mul _ _, ← cfcₙ_zero ℝ a]

Premises used: cfcₙ_zero, Real, cfcₙ_mul
-- 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
a : A
ha : IsSelfAdjoint a
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺ * x⁻) a = cfcₙ (R := ℝ) (p := IsSelfAdjoint) 0 a

Tactic:
cfcₙ_congr (fun x _ ↦ ?_)

Premises used: cfcₙ_congr
-- 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
a : A
ha : IsSelfAdjoint a
pos : ∀ x ∈ quasispectrum ℝ a, x⁺ * x⁻ = 0 x
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺ * x⁻) a = cfcₙ (R := ℝ) (p := IsSelfAdjoint) 0 a

Tactic:
refine cfcₙ_congr (fun x _ ↦ ?_)

Premises used: cfcₙ_congr
-- 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
a : A
ha : IsSelfAdjoint a
x : ℝ
h : x ∈ quasispectrum ℝ a
⊢ max x 0 * max (-x) 0 = 0 x

Tactic:
simpa using le_total x 0

Premises used: le_total, OfNat.ofNat
-- 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
a : A
ha : ¬IsSelfAdjoint a
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) a * cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) a = 0

Tactic:
simp [cfcₙ_apply_of_not_predicate a ha]

Premises used: cfcₙ_apply_of_not_predicate
-- 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
a : A
rw : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) a * cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) a = 0
⊢ a⁻ * a⁺ = 0

Tactic:
rw [posPart_def, negPart_def]

Premises used: CFC.negPart_def, CFC.posPart_def
-- 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
a : A
pos :
  ∀ (ha : IsSelfAdjoint a),
    cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) a * cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) a = 0
neg :
  ∀ (ha : ¬IsSelfAdjoint a),
    cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) a * cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) a = 0
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) a * cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) a = 0

Tactic:
by_cases ha : IsSelfAdjoint a

Premises used: IsSelfAdjoint
-- 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
a : A
ha : IsSelfAdjoint a
pos : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻ * x⁺) a = cfcₙ (R := ℝ) (p := IsSelfAdjoint) 0 a
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) a * cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) a = 0

Tactic:
rw [← cfcₙ_mul _ _, ← cfcₙ_zero ℝ a]

Premises used: cfcₙ_zero, Real, cfcₙ_mul
-- 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
a : A
ha : IsSelfAdjoint a
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻ * x⁺) a = cfcₙ (R := ℝ) (p := IsSelfAdjoint) 0 a

Tactic:
cfcₙ_congr (fun x _ ↦ ?_)

Premises used: cfcₙ_congr
-- 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
a : A
ha : IsSelfAdjoint a
pos : ∀ x ∈ quasispectrum ℝ a, x⁻ * x⁺ = 0 x
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻ * x⁺) a = cfcₙ (R := ℝ) (p := IsSelfAdjoint) 0 a

Tactic:
refine cfcₙ_congr (fun x _ ↦ ?_)

Premises used: cfcₙ_congr
-- 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
a : A
ha : IsSelfAdjoint a
x : ℝ
h : x ∈ quasispectrum ℝ a
⊢ max (-x) 0 * max x 0 = 0 x

Tactic:
simpa using le_total 0 x

Premises used: le_total, OfNat.ofNat
-- 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
a : A
ha : ¬IsSelfAdjoint a
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) a * cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) a = 0

Tactic:
simp [cfcₙ_apply_of_not_predicate a ha]

Premises used: cfcₙ_apply_of_not_predicate
-- 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
a : A
ha : IsSelfAdjoint a
rw : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) a - cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) a = a
⊢ a⁺ - a⁻ = a

Tactic:
rw [posPart_def, negPart_def]

Premises used: CFC.negPart_def, CFC.posPart_def
-- 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
a : A
ha : IsSelfAdjoint a
rw : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺ - x⁻) a = a
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) a - cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) a = a

Tactic:
rw [← cfcₙ_sub _ _]

Premises used: cfcₙ_sub
-- 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
a : A
ha : IsSelfAdjoint a
rw : cfcₙ (R := ℝ) (p := IsSelfAdjoint) id a
| a

Tactic:
rw [← cfcₙ_id ℝ a]

Premises used: Real, cfcₙ_id
-- 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
a : A
ha : IsSelfAdjoint a
conv_rhs : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺ - x⁻) a = cfcₙ (R := ℝ) (p := IsSelfAdjoint) id a
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺ - x⁻) a = a

Tactic:
conv_rhs => rw [← cfcₙ_id ℝ a]

Premises used: Real, cfcₙ_id
-- 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
a : A
ha : IsSelfAdjoint a
h : ∀ (x : ℝ), x⁺ - x⁻ = id x
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺ - x⁻) a = cfcₙ (R := ℝ) (p := IsSelfAdjoint) id a

Tactic:
congr! 2 with
-- 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
a : A
ha : IsSelfAdjoint a
x : ℝ
⊢ x⁺ - x⁻ = id x

Tactic:
_root_.posPart_sub_negPart _

Premises used: posPart_sub_negPart
-- 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
a : A
ha : IsSelfAdjoint a
x : ℝ
⊢ x⁺ - x⁻ = id x

Tactic:
exact _root_.posPart_sub_negPart _

Premises used: posPart_sub_negPart
-- 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 : T2Space A
a : A
pos : ∀ (ha : IsSelfAdjoint a), (-a)⁺ = a⁻
neg : ∀ (ha : ¬IsSelfAdjoint a), (-a)⁺ = a⁻
⊢ (-a)⁺ = a⁻

Tactic:
by_cases ha : IsSelfAdjoint a

Premises used: IsSelfAdjoint
-- 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 : T2Space A
a : A
ha : IsSelfAdjoint a
pos : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (-x)⁺) a = cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) a
⊢ (-a)⁺ = a⁻

Tactic:
rw [posPart_def, negPart_def, ← cfcₙ_comp_neg _ _]

Premises used: cfcₙ_comp_neg, CFC.negPart_def, CFC.posPart_def
-- 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 : T2Space A
a : A
ha : IsSelfAdjoint a
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (-x)⁺) a = cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) a

Tactic:
congr! 2
-- 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 : T2Space A
a : A
ha : ¬IsSelfAdjoint a
h : IsSelfAdjoint (-a)
⊢ IsSelfAdjoint a

Tactic:
simpa using h.neg

Premises used: IsSelfAdjoint.neg
-- 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 : T2Space A
a : A
ha : ¬IsSelfAdjoint a
⊢ ¬IsSelfAdjoint (-a)

Tactic:
have ha' : ¬ IsSelfAdjoint (-a) := fun h ↦ ha (by simpa using h.neg)
-- 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 : T2Space A
a : A
ha : ¬IsSelfAdjoint a
ha' : ¬IsSelfAdjoint (-a)
neg : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) (-a) = a⁻
neg₁ : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) (-a) = cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) a
neg₂ : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) (-a) = 0
neg₃ neg₄ : Eq.{u_1 + 1} (α := A) 0 0
⊢ (-a)⁺ = a⁻

Tactic:
rw [posPart_def, negPart_def, cfcₙ_apply_of_not_predicate a ha,
      cfcₙ_apply_of_not_predicate _ ha']

Premises used: cfcₙ_apply_of_not_predicate, CFC.negPart_def, CFC.posPart_def
-- 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 : T2Space A
a : A
rw : a⁺ = (-a)⁻
rw₁ : a⁺ - (-a)⁻ = 0
rw₂ : a⁺ - (- -a)⁺ = 0
rw₃ : a⁺ - a⁺ = 0
rw₄ rw₅ : Eq.{u_1 + 1} (α := A) 0 0
⊢ (-a)⁻ = a⁺

Tactic:
rw [← eq_comm, ← sub_eq_zero, ← posPart_neg, neg_neg, sub_self]

Premises used: sub_self, sub_eq_zero, neg_neg, eq_comm, CFC.posPart_neg
-- 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 : T2Space A
inst_8 : StarModule ℝ A
r : ℝ≥0
a : A
pos : ∀ (ha : IsSelfAdjoint a), (r • a)⁺ = r • a⁺
neg : ∀ (ha : ¬IsSelfAdjoint a), (r • a)⁺ = r • a⁺
⊢ (r • a)⁺ = r • a⁺

Tactic:
by_cases ha : IsSelfAdjoint a

Premises used: IsSelfAdjoint
-- 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 : T2Space A
inst_8 : StarModule ℝ A
r : ℝ≥0
a : A
ha : IsSelfAdjoint a
pos :
  cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) ((↑r : ℝ) • a) =
    (↑r : ℝ) • cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) a
⊢ (r • a)⁺ = r • a⁺

Tactic:
simp only [CFC.posPart_def, NNReal.smul_def]

Premises used: NNReal.smul_def, CFC.posPart_def
-- 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 : T2Space A
inst_8 : StarModule ℝ A
r : ℝ≥0
a : A
ha : IsSelfAdjoint a
pos :
  cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ ((↑r : ℝ) • x)⁺) a =
    cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑r : ℝ) • x⁺) a
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) ((↑r : ℝ) • a) =
    (↑r : ℝ) • cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) a

Tactic:
rw [← cfcₙ_comp_smul .., ← cfcₙ_smul ..]

Premises used: cfcₙ_comp_smul, cfcₙ_smul
-- 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 : T2Space A
inst_8 : StarModule ℝ A
r : ℝ≥0
a : A
ha : IsSelfAdjoint a
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ ((↑r : ℝ) • x)⁺) a =
    cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑r : ℝ) • x⁺) a

Tactic:
cfcₙ_congr fun x hx ↦ ?_

Premises used: cfcₙ_congr
-- 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 : T2Space A
inst_8 : StarModule ℝ A
r : ℝ≥0
a : A
ha : IsSelfAdjoint a
pos : ∀ (x : ℝ) (hx : x ∈ quasispectrum ℝ a), ((↑r : ℝ) • x)⁺ = (↑r : ℝ) • x⁺
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ ((↑r : ℝ) • x)⁺) a =
    cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑r : ℝ) • x⁺) a

Tactic:
refine cfcₙ_congr fun x hx ↦ ?_

Premises used: cfcₙ_congr
-- 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 : T2Space A
inst_8 : StarModule ℝ A
r : ℝ≥0
a : A
ha : IsSelfAdjoint a
x : ℝ
hx : x ∈ quasispectrum ℝ a
⊢ ((↑r : ℝ) • x)⁺ = (↑r : ℝ) • x⁺

Tactic:
simp [_root_.posPart_def, mul_max_of_nonneg]

Premises used: posPart_def, mul_max_of_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 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : T2Space A
inst_8 : StarModule ℝ A
r : ℝ≥0
a : A
ha : ¬IsSelfAdjoint a
neg : (HSMul.hSMul (α := ℝ≥0) 0 a)⁺ = HSMul.hSMul (α := ℝ≥0) 0 a⁺
neg₁ : ∀ (hr : r ≠ 0), (r • a)⁺ = r • a⁺
⊢ (r • a)⁺ = r • a⁺

Tactic:
obtain (rfl | hr) := eq_or_ne r 0

Premises used: eq_or_ne, OfNat.ofNat, 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 : T2Space A
inst_8 : StarModule ℝ A
a : A
ha : ¬IsSelfAdjoint a
⊢ (HSMul.hSMul (α := ℝ≥0) 0 a)⁺ = HSMul.hSMul (α := ℝ≥0) 0 a⁺

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 : T2Space A
inst_8 : StarModule ℝ A
r : ℝ≥0
a : A
ha : ¬IsSelfAdjoint a
hr : r ≠ 0
⊢ ¬IsSelfAdjoint (r • a)

Tactic:
have := (not_iff_not.mpr <| (IsSelfAdjoint.all r).smul_iff hr.isUnit (x := a)) |>.mpr ha
-- 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 : T2Space A
inst_8 : StarModule ℝ A
r : ℝ≥0
a : A
ha : ¬IsSelfAdjoint a
hr : r ≠ 0
this : ¬IsSelfAdjoint (r • a)
⊢ (r • a)⁺ = r • a⁺

Tactic:
simp [CFC.posPart_def, cfcₙ_apply_of_not_predicate a ha,
        cfcₙ_apply_of_not_predicate _ this]

Premises used: cfcₙ_apply_of_not_predicate, CFC.posPart_def
-- 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 : T2Space A
inst_8 : StarModule ℝ A
r : ℝ≥0
a : A
⊢ (r • a)⁻ = r • a⁻

Tactic:
simpa using posPart_smul (r := r) (a := -a)

Premises used: CFC.posPart_smul
-- 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 : T2Space A
inst_8 : StarModule ℝ A
r : ℝ
hr : 0 ≤ r
a : A
⊢ (r • a)⁺ = r • a⁺

Tactic:
posPart_smul (r := ⟨r, hr⟩)

Premises used: CFC.posPart_smul, NNReal.toReal
-- 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 : T2Space A
inst_8 : StarModule ℝ A
r : ℝ
hr : r ≤ 0
a : A
nth_rw : (- -r • a)⁺ = -r • a⁻
⊢ (r • a)⁺ = -r • a⁻

Tactic:
nth_rw 1 [← neg_neg r]

Premises used: neg_neg
-- 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 : T2Space A
inst_8 : StarModule ℝ A
r : ℝ
hr : r ≤ 0
a : A
rw : (-(-r • a))⁺ = -r • a⁻
rw₁ : (-r • -a)⁺ = -r • a⁻
rw₂ : -r • (-a)⁺ = -r • a⁻
rw₃ rw₄ : -r • a⁻ = -r • a⁻
⊢ (- -r • a)⁺ = -r • a⁻

Tactic:
rw [neg_smul, ← smul_neg, posPart_smul_of_nonneg (neg_nonneg.mpr hr), posPart_neg]

Premises used: Iff.mpr, neg_smul, smul_neg, neg_nonneg, CFC.posPart_smul_of_nonneg, CFC.posPart_neg
-- 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 : T2Space A
inst_8 : StarModule ℝ A
r : ℝ
hr : 0 ≤ r
a : A
⊢ -r ≤ 0

Tactic:
simpa
-- 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 : T2Space A
inst_8 : StarModule ℝ A
r : ℝ
hr : 0 ≤ r
a : A
rw : r • a⁻
| (r • a)⁻

Tactic:
rw [← neg_neg r, neg_smul, negPart_neg, posPart_smul_of_nonpos (by simpa), neg_neg]

Premises used: CFC.posPart_smul_of_nonpos, neg_smul, neg_neg, CFC.negPart_neg
-- 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 : T2Space A
inst_8 : StarModule ℝ A
r : ℝ
hr : 0 ≤ r
a : A
conv_lhs : (r • a)⁻ = r • a⁻
conv_lhs₁ : r • a⁻ = r • a⁻
⊢ (r • a)⁻ = r • a⁻

Tactic:
conv_lhs => rw [← neg_neg r, neg_smul, negPart_neg, posPart_smul_of_nonpos (by simpa), neg_neg]

Premises used: CFC.posPart_smul_of_nonpos, neg_smul, neg_neg, CFC.negPart_neg