-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PosPart.lean
lemma posPart_sub_negPart (a : A) (ha : IsSelfAdjoint a

Proof state:
case h.e'_17.h
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 : autoParam (IsSelfAdjoint a) _auto✝
x✝ : ℝ
⊢ x✝⁺ - x✝⁻ = id x✝

Tactic:
exact _root_.posPart_sub_negPart _

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
ha : autoParam (IsSelfAdjoint a) _auto✝
⊢ cfcₙ (fun x => x⁺ - x⁻) a = a

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

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
ha : autoParam (IsSelfAdjoint a) _auto✝
⊢ cfcₙ (fun x => x⁺ - x⁻) a = cfcₙ id 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
ha : autoParam (IsSelfAdjoint a) _auto✝
⊢ cfcₙ (fun x => x⁺) a - cfcₙ (fun x => x⁻) a = a

Tactic:
rw [← cfcₙ_sub _ _]

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
ha : autoParam (IsSelfAdjoint a) _auto✝
⊢ cfcₙ (fun x => x⁺ - x⁻) a = 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
ha : autoParam (IsSelfAdjoint a) _auto✝
⊢ cfcₙ (fun x => x⁺ - x⁻) a = cfcₙ id a

Tactic:
congr! 2 with

Result:
case h.e'_17.h
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 : autoParam (IsSelfAdjoint a) _auto✝
x✝ : ℝ
⊢ x✝⁺ - x✝⁻ = id 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
ha : autoParam (IsSelfAdjoint a) _auto✝
⊢ a⁺ - a⁻ = a

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
ha : autoParam (IsSelfAdjoint a) _auto✝
⊢ cfcₙ (fun x => x⁺) a - cfcₙ (fun x => x⁻) a = a