awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra 𝕜 A
inst_4 : TopologicalSpace A
inst_5 : ContinuousFunctionalCalculus 𝕜 A p
inst_6 : IsSemitopologicalRing A
inst_7 : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
f : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)
hf :
  ∃ᶠ (g : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) in nhds f,
    Commute ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A) g) b
⊢ Continuous (X := A) (HMul.hMul b)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra 𝕜 A
inst_4 : TopologicalSpace A
inst_5 : ContinuousFunctionalCalculus 𝕜 A p
inst_6 : IsSemitopologicalRing A
inst_7 : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
f : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)
hf :
  ∃ᶠ (g : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) in nhds f,
    Commute ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A) g) b
frequently :
  Membership.mem.{u_2, u_2} (α := A) (γ := Set A) (closure {y : A | y * b = b * y})
    ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A) f : A)
⊢ Commute ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A) f) b

Tactic:
rw [commute_iff_eq, ← Set.mem_setOf (p := fun x => x * b = b * x),
      ← (isClosed_eq (by fun_prop) (by fun_prop)).closure_eq]

Premises used: commute_iff_eq, IsClosed.closure_eq, Set.mem_setOf, isClosed_eq
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra 𝕜 A
inst_4 : TopologicalSpace A
inst_5 : ContinuousFunctionalCalculus 𝕜 A p
inst_6 : IsSemitopologicalRing A
inst_7 : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
f : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)
hf :
  ∃ᶠ (g : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) in nhds f,
    Commute ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A) g) b
frequently :
  Filter.Tendsto.{u_1, u_2} (β := A)
    ((⇑(cfcHom (p := p) ha) : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A) :
      (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A)
    (nhds f) (nhds ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A) f) : Filter A)
⊢ Membership.mem.{u_2, u_2} (α := A) (γ := Set A) (closure {y : A | y * b = b * y})
    ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A) f : A)

Tactic:
apply mem_closure_of_frequently_of_tendsto hf

Premises used: mem_closure_of_frequently_of_tendsto
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra 𝕜 A
inst_4 : TopologicalSpace A
inst_5 : ContinuousFunctionalCalculus 𝕜 A p
inst_6 : IsSemitopologicalRing A
inst_7 : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
f : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)
hf :
  ∃ᶠ (g : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) in nhds f,
    Commute ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A) g) b
⊢ Filter.Tendsto.{u_1, u_2} (β := A)
    ((⇑(cfcHom (p := p) ha) : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A) :
      (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A)
    (nhds f) (nhds ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A) f) : Filter A)

Tactic:
cfcHom_continuous ha |>.tendsto _

Premises used: cfcHom_continuous, Continuous.tendsto
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra 𝕜 A
inst_4 : TopologicalSpace A
inst_5 : ContinuousFunctionalCalculus 𝕜 A p
inst_6 : IsSemitopologicalRing A
inst_7 : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
f : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)
hf :
  ∃ᶠ (g : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) in nhds f,
    Commute ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A) g) b
⊢ Filter.Tendsto.{u_1, u_2} (β := A)
    ((⇑(cfcHom (p := p) ha) : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A) :
      (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A)
    (nhds f) (nhds ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A) f) : Filter A)

Tactic:
exact cfcHom_continuous ha |>.tendsto _

Premises used: cfcHom_continuous, Continuous.tendsto
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra 𝕜 A
inst_4 : TopologicalSpace A
inst_5 : ContinuousFunctionalCalculus 𝕜 A p
inst_6 : IsSemitopologicalRing A
inst_7 : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
f : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)
const :
  ∀ (r : 𝕜),
    Commute
      ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A)
        (ContinuousMap.const (↑(spectrum 𝕜 a) : Type u_1) r))
      b
id :
  Commute
    ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A)
      (ContinuousMap.restrict (spectrum 𝕜 a) (ContinuousMap.id 𝕜)))
    b
star_id :
  Commute
    ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A)
      (star (ContinuousMap.restrict (spectrum 𝕜 a) (ContinuousMap.id 𝕜))))
    b
add :
  ∀ (f g : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜))
    (hf : Commute ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A) f) b)
    (hg : Commute ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A) g) b),
    Commute ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A) (f + g)) b
mul :
  ∀ (f g : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜))
    (hf : Commute ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A) f) b)
    (hg : Commute ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A) g) b),
    Commute ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A) (f * g)) b
frequently :
  ∀ (f : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜))
    (hf :
      ∃ᶠ (g : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) in nhds f,
        Commute ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A) g) b),
    Commute ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A) f) b
⊢ Commute ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A) f) b

Tactic:
induction f using ContinuousMap.induction_on_of_compact with
  | const r =>
    conv =>
      enter [1, 2]
      equals algebraMap 𝕜 _ r => rfl
    rw [AlgHomClass.commutes]
    exact Algebra.commute_algebraMap_left r b
  | id => rwa [cfcHom_id ha]
  | star_id => rwa [map_star, cfcHom_id]
  | add f g hf hg => rw [map_add]; exact hf.add_left hg
  | mul f g hf hg => rw [map_mul]; exact mul_left hf hg
  | frequently f hf =>
    rw [commute_iff_eq, ← Set.mem_setOf (p := fun x => x * b = b * x),
      ← (isClosed_eq (by fun_prop) (by fun_prop)).closure_eq]
    apply mem_closure_of_frequently_of_tendsto hf
    exact cfcHom_continuous ha |>.tendsto _

Premises used: cfcHom_continuous, cfcHom_id, commute_iff_eq, IsClosed.closure_eq, StarHomClass.map_star, map_add, id, Set.mem_setOf, Continuous.tendsto, map_mul, isClosed_eq, AlgHomClass.commutes
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra 𝕜 A
inst_4 : TopologicalSpace A
inst_5 : ContinuousFunctionalCalculus 𝕜 A p
inst_6 : IsSemitopologicalRing A
inst_7 : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
f : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)
const :
  ∀ (r : 𝕜),
    Commute
      ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A)
        (ContinuousMap.const (↑(spectrum 𝕜 a) : Type u_1) r))
      b
id :
  Commute
    ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A)
      (ContinuousMap.restrict (spectrum 𝕜 a) (ContinuousMap.id 𝕜)))
    b
star_id :
  Commute
    ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A)
      (star (ContinuousMap.restrict (spectrum 𝕜 a) (ContinuousMap.id 𝕜))))
    b
add :
  ∀ (f g : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜))
    (hf : Commute ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A) f) b)
    (hg : Commute ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A) g) b),
    Commute ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A) (f + g)) b
mul :
  ∀ (f g : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜))
    (hf : Commute ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A) f) b)
    (hg : Commute ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A) g) b),
    Commute ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A) (f * g)) b
frequently :
  ∀ (f : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜))
    (hf :
      ∃ᶠ (g : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) in nhds f,
        Commute ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A) g) b),
    Commute ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A) f) b
⊢ Commute ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A) f) b

Tactic:
open scoped ContinuousFunctionalCalculus in
  induction f using ContinuousMap.induction_on_of_compact with
  | const r =>
    conv =>
      enter [1, 2]
      equals algebraMap 𝕜 _ r => rfl
    rw [AlgHomClass.commutes]
    exact Algebra.commute_algebraMap_left r b
  | id => rwa [cfcHom_id ha]
  | star_id => rwa [map_star, cfcHom_id]
  | add f g hf hg => rw [map_add]; exact hf.add_left hg
  | mul f g hf hg => rw [map_mul]; exact mul_left hf hg
  | frequently f hf =>
    rw [commute_iff_eq, ← Set.mem_setOf (p := fun x => x * b = b * x),
      ← (isClosed_eq (by fun_prop) (by fun_prop)).closure_eq]
    apply mem_closure_of_frequently_of_tendsto hf
    exact cfcHom_continuous ha |>.tendsto _

Premises used: cfcHom_continuous, cfcHom_id, commute_iff_eq, IsClosed.closure_eq, StarHomClass.map_star, map_add, id, Set.mem_setOf, Continuous.tendsto, map_mul, isClosed_eq, AlgHomClass.commutes, ContinuousFunctionalCalculus
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra 𝕜 A
inst_4 : TopologicalSpace A
inst_5 : ContinuousFunctionalCalculus 𝕜 A p
inst_6 : IsSemitopologicalRing A
inst_7 : T2Space A
a b : A
ha : p a
ha' : IsSelfAdjoint a
hb : Commute a b
f : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)
⊢ Commute ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A) f) b

Tactic:
hb.cfcHom ha (ha'.star_eq.symm ▸ hb) f

Premises used: Commute.cfcHom
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra 𝕜 A
inst_4 : TopologicalSpace A
inst_5 : ContinuousFunctionalCalculus 𝕜 A p
inst_6 : IsSemitopologicalRing A
inst_7 : T2Space A
a b : A
hb₁ : Commute a b
hb₂ : Commute (star a) b
f : 𝕜 → 𝕜
⊢ Commute (cfc (p := p) f a) b

Tactic:
cfc_cases (fun x ↦ Commute x b) a f (Commute.zero_left _)
    fun hf ha ↦ hb₁.cfcHom ha hb₂ ⟨_, hf.restrict⟩

Premises used: spectrum, Commute.zero_left, ContinuousMap.mk, Commute, Commute.cfcHom, ContinuousOn.restrict, Set.restrict, cfc_cases
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra 𝕜 A
inst_4 : TopologicalSpace A
inst_5 : ContinuousFunctionalCalculus 𝕜 A p
inst_6 : IsSemitopologicalRing A
inst_7 : T2Space A
a b : A
ha : IsSelfAdjoint a
hb₁ : Commute a b
f : 𝕜 → 𝕜
⊢ Commute (cfc (p := p) f a) b

Tactic:
hb₁.cfc (ha.star_eq.symm ▸ hb₁) f

Premises used: Commute.cfc
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
Goal:
A : Type u_2
inst : Ring A
inst_1 : StarRing A
inst_2 : Algebra ℝ A
inst_3 : TopologicalSpace A
inst_4 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_5 : IsTopologicalRing A
inst_6 : T2Space A
a b : A
hb : Commute a b
f : ℝ → ℝ
hf : ContinuousOn f (spectrum ℝ a)
ha : IsSelfAdjoint a
rw : Commute (cfc (p := IsSelfAdjoint) f a) b
⊢ Commute
    ((cfcHom (p := IsSelfAdjoint) ha : (a : C((↑(spectrum ℝ a) : Type), ℝ)) → A)
      { toFun := (spectrum ℝ a).restrict (π := fun (a : ℝ) ↦ ℝ) f, continuous_toFun := ⋯ :
        C((↑(spectrum ℝ a) : Type), ℝ) })
    b

Tactic:
rw [← cfc_apply ..]

Premises used: cfc_apply
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
Goal:
A : Type u_2
inst : Ring A
inst_1 : StarRing A
inst_2 : Algebra ℝ A
inst_3 : TopologicalSpace A
inst_4 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_5 : IsTopologicalRing A
inst_6 : T2Space A
a b : A
hb : Commute a b
f : ℝ → ℝ
hf : ContinuousOn f (spectrum ℝ a)
ha : IsSelfAdjoint a
⊢ (fun (x : A) ↦ Commute x b) (cfc (p := IsSelfAdjoint) f a)

Tactic:
hb.cfc (ha.star_eq.symm ▸ hb) _

Premises used: Commute.cfc
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
Goal:
A : Type u_2
inst : Ring A
inst_1 : StarRing A
inst_2 : Algebra ℝ A
inst_3 : TopologicalSpace A
inst_4 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_5 : IsTopologicalRing A
inst_6 : T2Space A
a b : A
hb : Commute a b
f : ℝ → ℝ
hf : ContinuousOn f (spectrum ℝ a)
ha : IsSelfAdjoint a
⊢ (fun (x : A) ↦ Commute x b) (cfc (p := IsSelfAdjoint) f a)

Tactic:
exact hb.cfc (ha.star_eq.symm ▸ hb) _

Premises used: Commute.cfc
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
Goal:
A : Type u_2
inst : Ring A
inst_1 : StarRing A
inst_2 : Algebra ℝ A
inst_3 : TopologicalSpace A
inst_4 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_5 : IsTopologicalRing A
inst_6 : T2Space A
inst_7 : PartialOrder A
inst_8 : NonnegSpectrumClass ℝ A
inst_9 : StarOrderedRing A
a b : A
hb : Commute a b
f : ℝ≥0 → ℝ≥0
pos : ∀ (ha : 0 ≤ a), Commute (cfc (p := fun (x : A) ↦ 0 ≤ x) f a) b
neg : ∀ (ha : ¬0 ≤ a), Commute (cfc (p := fun (x : A) ↦ 0 ≤ x) f a) b
⊢ Commute (cfc (p := fun (x : A) ↦ 0 ≤ x) f a) b

Tactic:
by_cases ha : 0 ≤ a
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
Goal:
A : Type u_2
inst : Ring A
inst_1 : StarRing A
inst_2 : Algebra ℝ A
inst_3 : TopologicalSpace A
inst_4 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_5 : IsTopologicalRing A
inst_6 : T2Space A
inst_7 : PartialOrder A
inst_8 : NonnegSpectrumClass ℝ A
inst_9 : StarOrderedRing A
a b : A
hb : Commute a b
f : ℝ≥0 → ℝ≥0
ha : 0 ≤ a
pos : Commute (cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) a) b
⊢ Commute (cfc (p := fun (x : A) ↦ 0 ≤ x) f a) b

Tactic:
rw [cfc_nnreal_eq_real ..]

Premises used: cfc_nnreal_eq_real
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
Goal:
A : Type u_2
inst : Ring A
inst_1 : StarRing A
inst_2 : Algebra ℝ A
inst_3 : TopologicalSpace A
inst_4 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_5 : IsTopologicalRing A
inst_6 : T2Space A
inst_7 : PartialOrder A
inst_8 : NonnegSpectrumClass ℝ A
inst_9 : StarOrderedRing A
a b : A
hb : Commute a b
f : ℝ≥0 → ℝ≥0
ha : 0 ≤ a
⊢ Commute (cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) a) b

Tactic:
hb.cfc_real _

Premises used: Commute.cfc_real
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
Goal:
A : Type u_2
inst : Ring A
inst_1 : StarRing A
inst_2 : Algebra ℝ A
inst_3 : TopologicalSpace A
inst_4 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_5 : IsTopologicalRing A
inst_6 : T2Space A
inst_7 : PartialOrder A
inst_8 : NonnegSpectrumClass ℝ A
inst_9 : StarOrderedRing A
a b : A
hb : Commute a b
f : ℝ≥0 → ℝ≥0
ha : 0 ≤ a
⊢ Commute (cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) a) b

Tactic:
exact hb.cfc_real _

Premises used: Commute.cfc_real
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
Goal:
A : Type u_2
inst : Ring A
inst_1 : StarRing A
inst_2 : Algebra ℝ A
inst_3 : TopologicalSpace A
inst_4 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_5 : IsTopologicalRing A
inst_6 : T2Space A
inst_7 : PartialOrder A
inst_8 : NonnegSpectrumClass ℝ A
inst_9 : StarOrderedRing A
a b : A
hb : Commute a b
f : ℝ≥0 → ℝ≥0
ha : ¬0 ≤ a
⊢ Commute (cfc (p := fun (x : A) ↦ 0 ≤ x) f a) b

Tactic:
simp [cfc_apply_of_not_predicate a ha]

Premises used: cfc_apply_of_not_predicate
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : TopologicalSpace A
inst_7 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst_8 : IsTopologicalRing A
inst_9 : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
⊢ Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) 0) b

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : TopologicalSpace A
inst_7 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst_8 : IsTopologicalRing A
inst_9 : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
r : 𝕜
f : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀
hf : Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) f) b
smul :
  Commute (HSMul.hSMul (β := A) r ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) f : A)) b
⊢ Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) (r • f)) b

Tactic:
rw [map_smul]

Premises used: map_smul
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : TopologicalSpace A
inst_7 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst_8 : IsTopologicalRing A
inst_9 : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
r : 𝕜
f : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀
hf : Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) f) b
⊢ Commute (HSMul.hSMul (β := A) r ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) f : A)) b

Tactic:
hf.smul_left r

Premises used: Commute.smul_left
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : TopologicalSpace A
inst_7 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst_8 : IsTopologicalRing A
inst_9 : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
r : 𝕜
f : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀
hf : Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) f) b
⊢ Commute (HSMul.hSMul (β := A) r ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) f : A)) b

Tactic:
exact hf.smul_left r

Premises used: Commute.smul_left
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : TopologicalSpace A
inst_7 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst_8 : IsTopologicalRing A
inst_9 : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
id id₁ id₂ id₃ : Commute a b
⊢ Commute
    ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A)
      (ContinuousMapZero.id (quasispectrum 𝕜 a) : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀))
    b

Tactic:
rwa [cfcₙHom_id ha]

Premises used: cfcₙHom_id
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : TopologicalSpace A
inst_7 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst_8 : IsTopologicalRing A
inst_9 : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
star_id :
  Commute
    (star
      ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A)
        (ContinuousMapZero.id (quasispectrum 𝕜 a) : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀)))
    b
star_id₁ star_id₂ star_id₃ star_id₄ : Commute (star a) b
⊢ Commute
    ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A)
      (star (ContinuousMapZero.id (quasispectrum 𝕜 a)) : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀))
    b

Tactic:
rwa [map_star, cfcₙHom_id]

Premises used: cfcₙHom_id, StarHomClass.map_star
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : TopologicalSpace A
inst_7 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst_8 : IsTopologicalRing A
inst_9 : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
f g : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀
hf : Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) f) b
hg : Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) g) b
add :
  Commute
    (HAdd.hAdd (α := A) (β := A) ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) f : A)
      ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) g : A))
    b
⊢ Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) (f + g)) b

Tactic:
rw [map_add]

Premises used: map_add
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : TopologicalSpace A
inst_7 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst_8 : IsTopologicalRing A
inst_9 : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
f g : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀
hf : Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) f) b
hg : Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) g) b
⊢ Commute
    (HAdd.hAdd (α := A) (β := A) ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) f : A)
      ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) g : A))
    b

Tactic:
hf.add_left hg

Premises used: Commute.add_left