-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.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✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
f g : R → R
a : A
hf : ContinuousOn f (σₙ R a)
hf0 : { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯ } 0 = 0
ha : p a
hg : ContinuousOn g (σₙ R a)
hg0 : { toFun := (σₙ R a).restrict g, continuous_toFun := ⋯ } 0 = 0
x✝ : p a
⊢ (fun x => Commute ((cfcₙHom ha) { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := hf0 }) x)
    ((cfcₙHom x✝) { toFun := (σₙ R a).restrict g, continuous_toFun := ⋯, map_zero' := hg0 })

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✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus 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✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
f g : R → R
a : A
hf : ContinuousOn f (σₙ R a)
hf0 : { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯ } 0 = 0
ha : p a
⊢ (fun x => Commute ((cfcₙHom ha) { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := hf0 }) x) 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
f g : R → R
a : A
hf : ContinuousOn f (σₙ R a)
hf0 : { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯ } 0 = 0
ha : p a
⊢ (fun x => Commute x (cfcₙ g a))
    ((cfcₙHom ha) { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := hf0 })

Tactic:
refine cfcₙ_cases (fun x ↦ Commute _ x) a g (by simp) fun hg hg0 _ ↦ ?_

Result:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
f g : R → R
a : A
hf : ContinuousOn f (σₙ R a)
hf0 : { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯ } 0 = 0
ha : p a
hg : ContinuousOn g (σₙ R a)
hg0 : { toFun := (σₙ R a).restrict g, continuous_toFun := ⋯ } 0 = 0
x✝ : p a
⊢ (fun x => Commute ((cfcₙHom ha) { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := hf0 }) x)
    ((cfcₙHom x✝) { toFun := (σₙ R a).restrict g, continuous_toFun := ⋯, map_zero' := hg0 })

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus 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 hf0 ha ↦ ?_

Result:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
f g : R → R
a : A
hf : ContinuousOn f (σₙ R a)
hf0 : { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯ } 0 = 0
ha : p a
⊢ (fun x => Commute x (cfcₙ g a))
    ((cfcₙHom ha) { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := hf0 })