-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma cfc_commute_cfc (f g : R → R) (a : A) : Commute (cfc f a) (cfc g a)

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
f g : R → R
a : A
⊢ (fun x => Commute x (cfc g a)) 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
f g : R → R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ (fun x => Commute x (cfc g a)) ((cfcHom ha) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ })

Tactic:
refine cfc_cases (fun x ↦ Commute _ x) a g (by simp) fun hg _ ↦ ?_

Result:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
f g : R → R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
hg : ContinuousOn g (spectrum R a)
x✝ : p a
⊢ (fun x => Commute ((cfcHom ha) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ }) x)
    ((cfcHom x✝) { toFun := (spectrum R a).restrict g, continuous_toFun := ⋯ })

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
f g : R → R
a : A
⊢ Commute (cfc f a) (cfc g a)

Tactic:
refine cfc_cases (fun x ↦ Commute x (cfc g a)) a f (by simp) fun hf ha ↦ ?_

Result:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
f g : R → R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ (fun x => Commute x (cfc g a)) ((cfcHom ha) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ })

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
f g : R → R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
hg : ContinuousOn g (spectrum R a)
x✝ : p a
⊢ (fun x => Commute ((cfcHom ha) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ }) x)
    ((cfcHom x✝) { toFun := (spectrum R a).restrict g, continuous_toFun := ⋯ })

Tactic:
exact Commute.all _ _ |>.map _

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
f g : R → R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ (fun x => Commute ((cfcHom ha) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ }) x) 0

Tactic:
simp

Result:
no goals