-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PosPart.lean
@[simp]
lemma posPart_mul_negPart (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:
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

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 ⊔ 0) * (-x ⊔ 0) = 0 x

Tactic:
simpa using le_total x 0

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
⊢ 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