awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute (goal)
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
⊢ Commute ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A) f) b
have 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
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 _
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute (goal)
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), 𝕜)
⊢ Commute ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A) f) b
have const : ∀ (r : 𝕜),
  Commute
    ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A)
      (ContinuousMap.const (↑(spectrum 𝕜 a) : Type u_1) r))
    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 _
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute (goal)
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
⊢ Commute ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A) f) b
have id : Commute
  ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A)
    (ContinuousMap.restrict (spectrum 𝕜 a) (ContinuousMap.id 𝕜)))
  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 _
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute (goal)
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
⊢ Commute ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A) f) b
have star_id : Commute
  ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A)
    (star (ContinuousMap.restrict (spectrum 𝕜 a) (ContinuousMap.id 𝕜))))
  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 _
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute (goal)
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
⊢ Commute ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A) f) b
have 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
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 _
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute (goal)
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
⊢ Commute ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A) f) b
have 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
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 _
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute (goal)
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
⊢ Commute ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A) f) b
have 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
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 _
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute (goal)
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)
    ((cfcHom (p := IsSelfAdjoint) ha : (a : C((↑(spectrum ℝ a) : Type), ℝ)) → A)
      { toFun := (spectrum ℝ a).restrict (π := fun (a : ℝ) ↦ ℝ) f, continuous_toFun := ⋯ :
        C((↑(spectrum ℝ a) : Type), ℝ) })
have rw : (fun (x : A) ↦ Commute x b) (cfc (p := IsSelfAdjoint) f a)
Tactic: rw [← cfc_apply ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute (goal)
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
⊢ Commute (cfc (p := fun (x : A) ↦ 0 ≤ x) f a) b
have pos : ∀ (ha : 0 ≤ a), Commute (cfc (p := fun (x : A) ↦ 0 ≤ x) f a) b
Tactic: by_cases ha : 0 ≤ a
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute (goal)
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
⊢ Commute (cfc (p := fun (x : A) ↦ 0 ≤ x) f a) b
have neg : ∀ (ha : ¬0 ≤ a), Commute (cfc (p := fun (x : A) ↦ 0 ≤ x) f a) b
Tactic: by_cases ha : 0 ≤ a
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute (goal)
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
have pos : Commute (cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) a) b
Tactic: rw [cfc_nnreal_eq_real ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute (goal)
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 ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) (r • f)) b
have smul : Commute (HSMul.hSMul (β := A) r ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) f : A)) b
Tactic: rw [map_smul]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute (goal)
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)
      (star (ContinuousMapZero.id (quasispectrum 𝕜 a)) : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀))
    b
have 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
Tactic: rwa [map_star, cfcₙHom_id]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute (goal)
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 ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) (f + g)) b
have 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
Tactic: rw [map_add]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute (goal)
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 ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) (f * g)) b
have 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
Tactic: rw [map_mul]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute (goal)
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
⊢ Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) f) b
have 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)
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]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute (goal)
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
⊢ 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)
have 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)
Tactic: apply mem_closure_of_frequently_of_tendsto hf