-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PosPart.lean
@[simp]
lemma posPart_neg (a : A) : (-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
inst✝ : T2Space A
a : A
⊢ (-a)⁺ = a⁻

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
inst✝ : T2Space A
a : A
ha : IsSelfAdjoint a
⊢ (-a)⁺ = a⁻

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
inst✝ : T2Space A
a : A
ha : ¬IsSelfAdjoint a
⊢ (-a)⁺ = a⁻

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

Tactic:
congr! 2

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
inst✝ : T2Space A
a : A
ha : ¬IsSelfAdjoint a
h : IsSelfAdjoint (-a)
⊢ IsSelfAdjoint a

Tactic:
simpa using h.neg

Result:
no goals

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
inst✝ : T2Space A
a : A
ha : ¬IsSelfAdjoint a
ha' : ¬IsSelfAdjoint (-a)
⊢ (-a)⁺ = a⁻

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

Result:
no goals

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
inst✝ : T2Space A
a : A
ha : ¬IsSelfAdjoint a
⊢ (-a)⁺ = a⁻

Tactic:
have ha' : ¬ IsSelfAdjoint (-a) := fun h ↦ ha (by simpa using h.neg)

Result:
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
inst✝ : T2Space A
a : A
ha : ¬IsSelfAdjoint a
ha' : ¬IsSelfAdjoint (-a)
⊢ (-a)⁺ = a⁻

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
inst✝ : T2Space A
a : A
ha : IsSelfAdjoint a
⊢ (-a)⁺ = a⁻

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

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