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 : 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), 𝕜)₀
⊢ Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) f) b
have zero : Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) 0) 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 _
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 : 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
⊢ Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) f) b
have 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
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 _
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 : 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
⊢ Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) f) b
have 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
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 _
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 : 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
⊢ Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) f) b
have 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
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 _
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 : 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
⊢ Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) f) b
have 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
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 _
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 : 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
⊢ Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) f) b
have 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
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 _
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 : 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
⊢ Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) f) b
have 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
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 _
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 : 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), 𝕜)₀
⊢ Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) f) b
have zero : Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) 0) b
Tactic: open scoped NonUnitalContinuousFunctionalCalculus in
  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 _
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 : 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
⊢ Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) f) b
have 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
Tactic: open scoped NonUnitalContinuousFunctionalCalculus in
  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 _
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 : 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
⊢ Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) f) b
have 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
Tactic: open scoped NonUnitalContinuousFunctionalCalculus in
  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 _
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 : 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
⊢ Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) f) b
have 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
Tactic: open scoped NonUnitalContinuousFunctionalCalculus in
  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 _
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 : 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
⊢ Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) f) b
have 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
Tactic: open scoped NonUnitalContinuousFunctionalCalculus in
  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 _
Cleared hypotheses: f