awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
R : Type u_2
inst_1 : Semifield R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : Module R A
inst_7 : IsScalarTower R A A
inst_8 : SMulCommClass R A A
inst_9 : Algebra R ℂ
inst_10 : IsScalarTower R ℂ A
p : A → Prop
p' : Unitization ℂ A → Prop
inst_11 : NonUnitalContinuousFunctionalCalculus R A p
inst_12 : ContinuousFunctionalCalculus R (Unitization ℂ A) p'
inst_13 : ContinuousMapZero.UniqueHom.{u_2, u_1} R (Unitization ℂ A)
hp : ∀ {a : A}, p' (↑a : Unitization ℂ A) ↔ p a
a : A
f : R → R
hf₀ : f 0 = 0
h : ¬(ContinuousOn f (σₙ R a) ∧ p a)
hf : ¬ContinuousOn f (σₙ R a)
neg : (↑0 : Unitization ℂ A) = cfc (p := p') f (↑a : Unitization ℂ A)
neg₁ : 0 = cfc (p := p') f (↑a : Unitization ℂ A)
⊢ (↑(cfcₙ (p := p) f a) : Unitization ℂ A) = cfc (p := p') f (↑a : Unitization ℂ A)
have neg₂ : Eq.{u_1 + 1} (α := Unitization ℂ A) 0 0
Tactic: rw [cfcₙ_apply_of_not_continuousOn a hf, inr_zero,
        cfc_apply_of_not_continuousOn _ (quasispectrum_eq_spectrum_inr' R ℂ a ▸ hf)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
R : Type u_2
inst_1 : Semifield R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : Module R A
inst_7 : IsScalarTower R A A
inst_8 : SMulCommClass R A A
inst_9 : Algebra R ℂ
inst_10 : IsScalarTower R ℂ A
p : A → Prop
p' : Unitization ℂ A → Prop
inst_11 : NonUnitalContinuousFunctionalCalculus R A p
inst_12 : ContinuousFunctionalCalculus R (Unitization ℂ A) p'
inst_13 : ContinuousMapZero.UniqueHom.{u_2, u_1} R (Unitization ℂ A)
hp : ∀ {a : A}, p' (↑a : Unitization ℂ A) ↔ p a
a : A
f : R → R
hf₀ : f 0 = 0
h : ¬(ContinuousOn f (σₙ R a) ∧ p a)
ha : ¬p a
⊢ (↑(cfcₙ (p := p) f a) : Unitization ℂ A) = cfc (p := p') f (↑a : Unitization ℂ A)
have neg : (↑0 : Unitization ℂ A) = cfc (p := p') f (↑a : Unitization ℂ A)
Tactic: rw [cfcₙ_apply_of_not_predicate a ha, inr_zero,
        cfc_apply_of_not_predicate _ (not_iff_not.mpr hp |>.mpr ha)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
R : Type u_2
inst_1 : Semifield R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : Module R A
inst_7 : IsScalarTower R A A
inst_8 : SMulCommClass R A A
inst_9 : Algebra R ℂ
inst_10 : IsScalarTower R ℂ A
p : A → Prop
p' : Unitization ℂ A → Prop
inst_11 : NonUnitalContinuousFunctionalCalculus R A p
inst_12 : ContinuousFunctionalCalculus R (Unitization ℂ A) p'
inst_13 : ContinuousMapZero.UniqueHom.{u_2, u_1} R (Unitization ℂ A)
hp : ∀ {a : A}, p' (↑a : Unitization ℂ A) ↔ p a
a : A
f : R → R
hf₀ : f 0 = 0
h : ¬(ContinuousOn f (σₙ R a) ∧ p a)
ha : ¬p a
neg : (↑0 : Unitization ℂ A) = cfc (p := p') f (↑a : Unitization ℂ A)
⊢ (↑(cfcₙ (p := p) f a) : Unitization ℂ A) = cfc (p := p') f (↑a : Unitization ℂ A)
have neg₁ : 0 = cfc (p := p') f (↑a : Unitization ℂ A)
Tactic: rw [cfcₙ_apply_of_not_predicate a ha, inr_zero,
        cfc_apply_of_not_predicate _ (not_iff_not.mpr hp |>.mpr ha)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
R : Type u_2
inst_1 : Semifield R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : Module R A
inst_7 : IsScalarTower R A A
inst_8 : SMulCommClass R A A
inst_9 : Algebra R ℂ
inst_10 : IsScalarTower R ℂ A
p : A → Prop
p' : Unitization ℂ A → Prop
inst_11 : NonUnitalContinuousFunctionalCalculus R A p
inst_12 : ContinuousFunctionalCalculus R (Unitization ℂ A) p'
inst_13 : ContinuousMapZero.UniqueHom.{u_2, u_1} R (Unitization ℂ A)
hp : ∀ {a : A}, p' (↑a : Unitization ℂ A) ↔ p a
a : A
f : R → R
hf₀ : f 0 = 0
h : ¬(ContinuousOn f (σₙ R a) ∧ p a)
ha : ¬p a
neg : (↑0 : Unitization ℂ A) = cfc (p := p') f (↑a : Unitization ℂ A)
neg₁ : 0 = cfc (p := p') f (↑a : Unitization ℂ A)
⊢ (↑(cfcₙ (p := p) f a) : Unitization ℂ A) = cfc (p := p') f (↑a : Unitization ℂ A)
have neg₂ : Eq.{u_1 + 1} (α := Unitization ℂ A) 0 0
Tactic: rw [cfcₙ_apply_of_not_predicate a ha, inr_zero,
        cfc_apply_of_not_predicate _ (not_iff_not.mpr hp |>.mpr ha)]
-- 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
r : 𝕜
| Commute
    ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A)
      (ContinuousMap.const (↑(spectrum 𝕜 a) : Type u_1) r))
    b
have enter : ContinuousMap.const (↑(spectrum 𝕜 a) : Type u_1) r
Tactic: enter [1, 2]
-- 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
r : 𝕜
| Commute
    ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A)
      (ContinuousMap.const (↑(spectrum 𝕜 a) : Type u_1) r))
    b
have enter : ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A)
    (ContinuousMap.const (↑(spectrum 𝕜 a) : Type u_1) r) :
  A)
Tactic: enter [1, 2]
      equals algebraMap 𝕜 _ r => rfl
-- 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
r : 𝕜
enter :
  ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A)
      (ContinuousMap.const (↑(spectrum 𝕜 a) : Type u_1) r) :
    A)
| Commute
    ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A)
      (ContinuousMap.const (↑(spectrum 𝕜 a) : Type u_1) r))
    b
have enter₁ : ContinuousMap.const (↑(spectrum 𝕜 a) : Type u_1) r
Tactic: enter [1, 2]
      equals algebraMap 𝕜 _ r => rfl
-- 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
r : 𝕜
⊢ Commute
    ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A)
      (ContinuousMap.const (↑(spectrum 𝕜 a) : Type u_1) r))
    b
have const : Commute
  ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A)
    ((algebraMap 𝕜 C((↑(spectrum 𝕜 a) : Type u_1), 𝕜) : (a_1 : 𝕜) → C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) r :
      C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)))
  b
Tactic: conv =>
      enter [1, 2]
      equals algebraMap 𝕜 _ r => rfl
-- 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
r : 𝕜
⊢ Commute
    ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A)
      ((algebraMap 𝕜 C((↑(spectrum 𝕜 a) : Type u_1), 𝕜) : (a_1 : 𝕜) → C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) r :
        C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)))
    b
have const : Commute ((algebraMap 𝕜 A : (a : 𝕜) → A) r) b
Tactic: rw [AlgHomClass.commutes]
-- 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
⊢ Commute
    ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A)
      (star (ContinuousMap.restrict (spectrum 𝕜 a) (ContinuousMap.id 𝕜))))
    b
have star_id : Commute
  (star
    ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A)
      (ContinuousMap.restrict (spectrum 𝕜 a) (ContinuousMap.id 𝕜))))
  b
Tactic: rwa [map_star, cfcHom_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 : 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 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
have add : Commute
  (HAdd.hAdd (α := A) (β := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A) f : A)
    ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 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 : 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 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
have mul : Commute
  (HMul.hMul (α := A) (β := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A) f : A)
    ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 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 : 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
⊢ Commute ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 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})
  ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 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 : 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
⊢ 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)
have 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)
Tactic: apply mem_closure_of_frequently_of_tendsto hf
-- 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: 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: 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: 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: 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: 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