-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PosPart.lean
@[simp]
lemma negPart_mul_posPart (a : A) : a⁻ * a⁺ = 0

Proof state:
case neg
A : Type u_1
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarRing A
inst✝¹ : TopologicalSpace A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
a : A
ha : ¬IsSelfAdjoint a
⊢ cfcₙ (fun x => x⁻) a * cfcₙ (fun x => x⁺) a = 0

Tactic:
simp [cfcₙ_apply_of_not_predicate a ha]

Result:
no goals

Proof state:
A : Type u_1
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarRing A
inst✝¹ : TopologicalSpace A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
a : A
⊢ a⁻ * a⁺ = 0

Tactic:
rw [posPart_def, negPart_def]

Result:
A : Type u_1
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarRing A
inst✝¹ : TopologicalSpace A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
a : A
⊢ cfcₙ (fun x => x⁻) a * cfcₙ (fun x => x⁺) a = 0

Proof state:
case pos
A : Type u_1
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarRing A
inst✝¹ : TopologicalSpace A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
x : ℝ
x✝ : x ∈ quasispectrum ℝ a
⊢ (-x ⊔ 0) * (x ⊔ 0) = 0 x

Tactic:
simpa using le_total 0 x

Result:
no goals

Proof state:
case pos
A : Type u_1
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarRing A
inst✝¹ : TopologicalSpace A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
⊢ cfcₙ (fun x => x⁻) a * cfcₙ (fun x => x⁺) a = 0

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

Result:
case pos
A : Type u_1
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarRing A
inst✝¹ : TopologicalSpace A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
⊢ cfcₙ (fun x => x⁻ * x⁺) a = cfcₙ 0 a

Proof state:
A : Type u_1
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarRing A
inst✝¹ : TopologicalSpace A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
a : A
⊢ cfcₙ (fun x => x⁻) a * cfcₙ (fun x => x⁺) a = 0

Tactic:
by_cases ha : IsSelfAdjoint a

Result:
case pos
A : Type u_1
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarRing A
inst✝¹ : TopologicalSpace A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
⊢ cfcₙ (fun x => x⁻) a * cfcₙ (fun x => x⁺) a = 0

case neg
A : Type u_1
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarRing A
inst✝¹ : TopologicalSpace A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
a : A
ha : ¬IsSelfAdjoint a
⊢ cfcₙ (fun x => x⁻) a * cfcₙ (fun x => x⁺) a = 0

Proof state:
case pos
A : Type u_1
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarRing A
inst✝¹ : TopologicalSpace A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
⊢ cfcₙ (fun x => x⁻ * x⁺) a = cfcₙ 0 a

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

Result:
case pos
A : Type u_1
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarRing A
inst✝¹ : TopologicalSpace A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
x : ℝ
x✝ : x ∈ quasispectrum ℝ a
⊢ x⁻ * x⁺ = 0 x

Proof state:
case pos
A : Type u_1
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarRing A
inst✝¹ : TopologicalSpace A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
x : ℝ
x✝ : x ∈ quasispectrum ℝ a
⊢ x⁻ * x⁺ = 0 x

Tactic:
simp only [_root_.posPart_def, _root_.negPart_def]

Result:
case pos
A : Type u_1
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarRing A
inst✝¹ : TopologicalSpace A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
x : ℝ
x✝ : x ∈ quasispectrum ℝ a
⊢ (-x ⊔ 0) * (x ⊔ 0) = 0 x