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 : 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:
exact hf.add_left hg

Premises used: Commute.add_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
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
mul :
  Commute
    (HMul.hMul (α := 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_mul]

Premises used: map_mul
-- 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
    (HMul.hMul (α := 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:
mul_left hf hg

Premises used: Commute.mul_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
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
    (HMul.hMul (α := 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:
exact mul_left hf hg

Premises used: Commute.mul_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
f : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀
hf :
  ∃ᶠ (g : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) in nhds f,
    Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) g) b
⊢ Continuous (Y := A) fun (x : A) ↦ x * 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 : 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 : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀
hf :
  ∃ᶠ (g : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) in nhds f,
    Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 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 : 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 : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀
hf :
  ∃ᶠ (g : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) in nhds f,
    Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) g) b
frequently :
  Membership.mem.{u_2, u_2} (α := A) (γ := Set A) (closure {y : A | y * b = b * y})
    ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) f : A)
⊢ Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 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 : 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 : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀
hf :
  ∃ᶠ (g : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) in nhds f,
    Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) g) b
frequently :
  Filter.Tendsto.{u_1, u_2} (β := A)
    ((⇑(cfcₙHom (p := p) ha) : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) :
      (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A)
    (nhds f) (nhds ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) f) : Filter A)
⊢ Membership.mem.{u_2, u_2} (α := A) (γ := Set A) (closure {y : A | y * b = b * y})
    ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 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 : 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 : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀
hf :
  ∃ᶠ (g : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) in nhds f,
    Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) g) b
⊢ Filter.Tendsto.{u_1, u_2} (β := A)
    ((⇑(cfcₙHom (p := p) ha) : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) :
      (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A)
    (nhds f) (nhds ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) f) : Filter A)

Tactic:
cfcₙHom_continuous ha |>.tendsto _

Premises used: Continuous.tendsto, cfcₙHom_continuous
-- 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 : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀
hf :
  ∃ᶠ (g : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) in nhds f,
    Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) g) b
⊢ Filter.Tendsto.{u_1, u_2} (β := A)
    ((⇑(cfcₙHom (p := p) ha) : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) :
      (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A)
    (nhds f) (nhds ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) f) : Filter A)

Tactic:
exact cfcₙHom_continuous ha |>.tendsto _

Premises used: Continuous.tendsto, cfcₙHom_continuous
-- 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 : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀
zero : Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) 0) b
smul :
  ∀ (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 ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) (r • f)) b
id :
  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
star_id :
  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
add :
  ∀ (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 ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) (f + g)) b
mul :
  ∀ (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 ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) (f * g)) b
frequently :
  ∀ (f : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀)
    (hf :
      ∃ᶠ (g : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) in nhds f,
        Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) g) b),
    Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) f) b
⊢ Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) f) b

Tactic:
induction f using ContinuousMapZero.induction_on_of_compact with
  | zero => simp
  | smul r f hf => rw [map_smul]; exact hf.smul_left r
  | id => rwa [cfcₙHom_id ha]
  | star_id => rwa [map_star, cfcₙHom_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 cfcₙHom_continuous ha |>.tendsto _

Premises used: cfcₙHom_id, commute_iff_eq, IsClosed.closure_eq, StarHomClass.map_star, map_add, id, Set.mem_setOf, Continuous.tendsto, map_mul, isClosed_eq, cfcₙHom_continuous, 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
ha' : IsSelfAdjoint a
hb : Commute a b
f : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀
⊢ Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) f) b

Tactic:
hb.cfcₙHom ha (ha'.star_eq.symm ▸ hb) f

Premises used: Commute.cfcₙHom
-- 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
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 hf₀ ha ↦ hb₁.cfcₙHom ha hb₂ ⟨⟨_, hf.restrict⟩, hf₀⟩

Premises used: Commute.zero_left, ContinuousMap.mk, quasispectrum, Commute, Commute.cfcₙHom, ContinuousOn.restrict, ContinuousMapZero.mk, 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 : 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 : 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 : NonUnitalRing A
inst_1 : StarRing A
inst_2 : Module ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : IsTopologicalRing A
inst_8 : T2Space A
a b : A
hb : Commute a b
f : ℝ → ℝ
hf : ContinuousOn f (quasispectrum ℝ a)
hf0 :
  Eq (α := ℝ)
    (({ toFun := (quasispectrum ℝ a).restrict (π := fun (a : ℝ) ↦ ℝ) f, continuous_toFun := ⋯ :
            C((↑(quasispectrum ℝ a) : Type), ℝ) } :
          (a : (↑(quasispectrum ℝ a) : Type)) → ℝ)
        0 :
      ℝ)
    (0 : ℝ)
ha : IsSelfAdjoint a
rw : Commute (cfcₙ (p := IsSelfAdjoint) f a) b
⊢ Commute
    ((cfcₙHom (p := IsSelfAdjoint) ha : (a : ContinuousMapZero (↑(quasispectrum ℝ a) : Type) ℝ) → A)
      { toFun := (quasispectrum ℝ a).restrict (π := fun (a : ℝ) ↦ ℝ) f, continuous_toFun := ⋯, map_zero' := hf0 :
        ContinuousMapZero (↑(quasispectrum ℝ a) : Type) ℝ })
    b

Tactic:
rw [← cfcₙ_apply ..]

Premises used: cfcₙ_apply
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
Goal:
A : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : Module ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : IsTopologicalRing A
inst_8 : T2Space A
a b : A
hb : Commute a b
f : ℝ → ℝ
hf : ContinuousOn f (quasispectrum ℝ a)
hf0 :
  Eq (α := ℝ)
    (({ toFun := (quasispectrum ℝ a).restrict (π := fun (a : ℝ) ↦ ℝ) f, continuous_toFun := ⋯ :
            C((↑(quasispectrum ℝ a) : Type), ℝ) } :
          (a : (↑(quasispectrum ℝ a) : Type)) → ℝ)
        0 :
      ℝ)
    (0 : ℝ)
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 : NonUnitalRing A
inst_1 : StarRing A
inst_2 : Module ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : IsTopologicalRing A
inst_8 : T2Space A
a b : A
hb : Commute a b
f : ℝ → ℝ
hf : ContinuousOn f (quasispectrum ℝ a)
hf0 :
  Eq (α := ℝ)
    (({ toFun := (quasispectrum ℝ a).restrict (π := fun (a : ℝ) ↦ ℝ) f, continuous_toFun := ⋯ :
            C((↑(quasispectrum ℝ a) : Type), ℝ) } :
          (a : (↑(quasispectrum ℝ a) : Type)) → ℝ)
        0 :
      ℝ)
    (0 : ℝ)
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 : NonUnitalRing A
inst_1 : StarRing A
inst_2 : Module ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : IsTopologicalRing A
inst_8 : T2Space A
inst_9 : PartialOrder A
inst_10 : NonnegSpectrumClass ℝ A
inst_11 : 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 : NonUnitalRing A
inst_1 : StarRing A
inst_2 : Module ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : IsTopologicalRing A
inst_8 : T2Space A
inst_9 : PartialOrder A
inst_10 : NonnegSpectrumClass ℝ A
inst_11 : 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 : NonUnitalRing A
inst_1 : StarRing A
inst_2 : Module ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : IsTopologicalRing A
inst_8 : T2Space A
inst_9 : PartialOrder A
inst_10 : NonnegSpectrumClass ℝ A
inst_11 : 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 : NonUnitalRing A
inst_1 : StarRing A
inst_2 : Module ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : IsTopologicalRing A
inst_8 : T2Space A
inst_9 : PartialOrder A
inst_10 : NonnegSpectrumClass ℝ A
inst_11 : 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 : NonUnitalRing A
inst_1 : StarRing A
inst_2 : Module ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : IsTopologicalRing A
inst_8 : T2Space A
inst_9 : PartialOrder A
inst_10 : NonnegSpectrumClass ℝ A
inst_11 : 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.Continuity
Goal:
X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (spectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (spectrum R a)
inl :
  ∀ (h_tendsto : TendstoUniformlyOn F f ⊥ (spectrum R a)) (hF : ∀ᶠ (x : X) in ⊥, ContinuousOn (F x) (spectrum R a)),
    Tendsto (fun (x : X) ↦ cfc (p := p) (F x) a) ⊥ (𝓝 (cfc (p := p) f a))
inr : ∀ (hl : l.NeBot), Tendsto (fun (x : X) ↦ cfc (p := p) (F x) a) l (𝓝 (cfc (p := p) f a))
⊢ Tendsto (fun (x : X) ↦ cfc (p := p) (F x) a) l (𝓝 (cfc (p := p) f a))

Tactic:
obtain (rfl | hl) := l.eq_or_neBot

Premises used: Filter.eq_or_neBot, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f ⊥ (spectrum R a)
hF : ∀ᶠ (x : X) in ⊥, ContinuousOn (F x) (spectrum R a)
⊢ Tendsto (fun (x : X) ↦ cfc (p := p) (F x) a) ⊥ (𝓝 (cfc (p := p) f a))

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (spectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (spectrum R a)
hl : l.NeBot
⊢ ContinuousOn f (spectrum R a)

Tactic:
have hf := h_tendsto.continuousOn hF.frequently
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (spectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (spectrum R a)
hl : l.NeBot
hf : ContinuousOn f (spectrum R a)
pos : ∀ (ha : p a), Tendsto (fun (x : X) ↦ cfc (p := p) (F x) a) l (𝓝 (cfc (p := p) f a))
neg : ∀ (ha : ¬p a), Tendsto (fun (x : X) ↦ cfc (p := p) (F x) a) l (𝓝 (cfc (p := p) f a))
⊢ Tendsto (fun (x : X) ↦ cfc (p := p) (F x) a) l (𝓝 (cfc (p := p) f a))

Tactic:
by_cases ha : p a