-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma cfc_neg : cfc (fun x ↦ - (f x)) a = - (cfc f a)

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommRing R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalRing R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R p
f : R → R
a : A
⊢ cfc (fun x => -f x) a = -cfc f a

Tactic:
by_cases h : p a ∧ ContinuousOn f (spectrum R a)

Result:
case pos
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommRing R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalRing R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R p
f : R → R
a : A
h : p a ∧ ContinuousOn f (spectrum R a)
⊢ cfc (fun x => -f x) a = -cfc f a

case neg
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommRing R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalRing R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R p
f : R → R
a : A
h : ¬(p a ∧ ContinuousOn f (spectrum R a))
⊢ cfc (fun x => -f x) a = -cfc f a

Proof state:
case neg.inl
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommRing R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalRing R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R p
f : R → R
a : A
h : ¬(p a ∧ ContinuousOn f (spectrum R a))
ha : ¬p a
⊢ cfc (fun x => -f x) a = -cfc f a

Tactic:
simp [cfc_apply_of_not_predicate a ha]

Result:
no goals

Proof state:
case neg.inr
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommRing R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalRing R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R p
f : R → R
a : A
h : ¬(p a ∧ ContinuousOn f (spectrum R a))
hf : ¬ContinuousOn f (spectrum R a)
⊢ cfc (fun x => -f x) a = -cfc f a

Tactic:
rw [cfc_apply_of_not_continuousOn a hf, cfc_apply_of_not_continuousOn, neg_zero]

Result:
case neg.inr.hf
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommRing R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalRing R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R p
f : R → R
a : A
h : ¬(p a ∧ ContinuousOn f (spectrum R a))
hf : ¬ContinuousOn f (spectrum R a)
⊢ ¬ContinuousOn (fun x => -f x) (spectrum R a)

Proof state:
case pos.intro
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommRing R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalRing R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R p
f : R → R
a : A
ha : p a
hf : ContinuousOn f (spectrum R a)
⊢ cfc (fun x => -f x) a = -cfc f a

Tactic:
rw [cfc_apply f a, ← map_neg, cfc_apply ..]

Result:
case pos.intro
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommRing R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalRing R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R p
f : R → R
a : A
ha : p a
hf : ContinuousOn f (spectrum R a)
⊢ (cfcHom ha) { toFun := (spectrum R a).restrict fun x => -f x, continuous_toFun := ⋯ } =
    (cfcHom ha) (-{ toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ })

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommRing R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalRing R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R p
f : R → R
a : A
h : ¬(p a ∧ ContinuousOn f (spectrum R a))
hf : ¬ContinuousOn f (spectrum R a)
hf_neg : ContinuousOn (fun x => -f x) (spectrum R a)
⊢ ContinuousOn f (spectrum R a)

Tactic:
simpa using hf_neg.neg

Result:
no goals

Proof state:
case neg.inr.hf
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommRing R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalRing R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R p
f : R → R
a : A
h : ¬(p a ∧ ContinuousOn f (spectrum R a))
hf : ¬ContinuousOn f (spectrum R a)
⊢ ¬ContinuousOn (fun x => -f x) (spectrum R a)

Tactic:
exact fun hf_neg ↦ hf <| by simpa using hf_neg.neg

Result:
no goals

Proof state:
case neg
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommRing R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalRing R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R p
f : R → R
a : A
h : ¬(p a ∧ ContinuousOn f (spectrum R a))
⊢ cfc (fun x => -f x) a = -cfc f a

Tactic:
obtain (ha | hf) := not_and_or.mp h

Result:
case neg.inl
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommRing R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalRing R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R p
f : R → R
a : A
h : ¬(p a ∧ ContinuousOn f (spectrum R a))
ha : ¬p a
⊢ cfc (fun x => -f x) a = -cfc f a

case neg.inr
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommRing R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalRing R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R p
f : R → R
a : A
h : ¬(p a ∧ ContinuousOn f (spectrum R a))
hf : ¬ContinuousOn f (spectrum R a)
⊢ cfc (fun x => -f x) a = -cfc f a

Proof state:
case pos
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommRing R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalRing R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R p
f : R → R
a : A
h : p a ∧ ContinuousOn f (spectrum R a)
⊢ cfc (fun x => -f x) a = -cfc f a

Tactic:
obtain ⟨ha, hf⟩ := h

Result:
case pos.intro
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommRing R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalRing R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R p
f : R → R
a : A
ha : p a
hf : ContinuousOn f (spectrum R a)
⊢ cfc (fun x => -f x) a = -cfc f a

Proof state:
case pos.intro
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommRing R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalRing R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R p
f : R → R
a : A
ha : p a
hf : ContinuousOn f (spectrum R a)
⊢ (cfcHom ha) { toFun := (spectrum R a).restrict fun x => -f x, continuous_toFun := ⋯ } =
    (cfcHom ha) (-{ toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ })

Tactic:
congr

Result:
no goals