awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) a
x : PartialOrder (Unitization ℂ A) := spectralOrder (Unitization ℂ A)
this_1 : StarOrderedRing.{u_1} (Unitization ℂ A)
this :
  Membership.mem (α := Unitization ℂ A) (γ := AddSubmonoid (Unitization ℂ A))
    (AddSubmonoid.closure
      (Set.range (ι := A)
        (Function.comp (β := A) (⇑(Unitization.inrNonUnitalStarAlgHom ℂ A) : (a : A) → Unitization ℂ A) fun (s : A) ↦
          star s * s)))
    ((Unitization.inrNonUnitalStarAlgHom ℂ A : (a : A) → Unitization ℂ A) a : Unitization ℂ A)
s : A
⊢ Eq (α := Unitization ℂ A) ((fun (s : Unitization ℂ A) ↦ star s * s) (↑s : Unitization ℂ A))
    (Function.comp (β := A) (⇑(Unitization.inrNonUnitalStarAlgHom ℂ A) : (a : A) → Unitization ℂ A)
      (fun (s : A) ↦ star s * s) s)

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) a
x : PartialOrder (Unitization ℂ A) := spectralOrder (Unitization ℂ A)
this_1 : StarOrderedRing.{u_1} (Unitization ℂ A)
this :
  Membership.mem (α := Unitization ℂ A) (γ := AddSubmonoid (Unitization ℂ A))
    (AddSubmonoid.closure
      (Set.range (ι := A)
        (Function.comp (β := A) (⇑(Unitization.inrNonUnitalStarAlgHom ℂ A) : (a : A) → Unitization ℂ A) fun (s : A) ↦
          star s * s)))
    ((Unitization.inrNonUnitalStarAlgHom ℂ A : (a : A) → Unitization ℂ A) a : Unitization ℂ A)
s : A
⊢ Membership.mem (γ := Set (Unitization ℂ A)) (Set.range fun (s : Unitization ℂ A) ↦ star s * s)
    (Function.comp (β := A) (⇑(Unitization.inrNonUnitalStarAlgHom ℂ A) : (a : A) → Unitization ℂ A)
      (fun (s : A) ↦ star s * s) s)

Tactic:
exact ⟨s, by simp⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
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
pos :
  ∀ (h : ContinuousOn f (σₙ R a) ∧ p a),
    (↑(cfcₙ (p := p) f a) : Unitization ℂ A) = cfc (p := p') f (↑a : Unitization ℂ A)
neg :
  ∀ (h : ¬(ContinuousOn f (σₙ R a) ∧ p a)),
    (↑(cfcₙ (p := p) f a) : Unitization ℂ A) = cfc (p := p') f (↑a : Unitization ℂ A)
⊢ (↑(cfcₙ (p := p) f a) : Unitization ℂ A) = cfc (p := p') f (↑a : Unitization ℂ A)

Tactic:
by_cases h : ContinuousOn f (σₙ R a) ∧ p a

Premises used: quasispectrum, ContinuousOn
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
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
⊢ ContinuousOn f (σₙ R a)

Tactic:
obtain ⟨hf, ha⟩ := h
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
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)
⊢ p a

Tactic:
obtain ⟨hf, ha⟩ := h
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
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
hf : ContinuousOn f (σₙ R a)
ha : p a
pos : (↑(cfcₙ (p := p) f a) : Unitization ℂ A) = cfcₙ (p := p') f (↑a : Unitization ℂ A)
⊢ (↑(cfcₙ (p := p) f a) : Unitization ℂ A) = cfc (p := p') f (↑a : Unitization ℂ A)

Tactic:
rw [← cfcₙ_eq_cfc (quasispectrum_inr_eq R ℂ a ▸ hf)]

Premises used: cfcₙ_eq_cfc
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
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
hf : ContinuousOn f (σₙ R a)
ha : p a
⊢ (↑(cfcₙ (p := p) f a) : Unitization ℂ A) = cfcₙ (p := p') f (↑a : Unitization ℂ A)

Tactic:
(inrNonUnitalStarAlgHom ℂ A).map_cfcₙ f a

Premises used: NonUnitalStarAlgHom.map_cfcₙ, Unitization.inr, Unitization.inrNonUnitalStarAlgHom, Complex
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
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
hf : ContinuousOn f (σₙ R a)
ha : p a
⊢ (↑(cfcₙ (p := p) f a) : Unitization ℂ A) = cfcₙ (p := p') f (↑a : Unitization ℂ A)

Tactic:
exact (inrNonUnitalStarAlgHom ℂ A).map_cfcₙ f a

Premises used: NonUnitalStarAlgHom.map_cfcₙ, Unitization.inrNonUnitalStarAlgHom, Complex
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
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)
neg :
  ∀ (hf : ¬ContinuousOn f (σₙ R a)), (↑(cfcₙ (p := p) f a) : Unitization ℂ A) = cfc (p := p') f (↑a : Unitization ℂ A)
neg₁ : ∀ (ha : ¬p a), (↑(cfcₙ (p := p) f a) : Unitization ℂ A) = cfc (p := p') f (↑a : Unitization ℂ A)
⊢ (↑(cfcₙ (p := p) f a) : Unitization ℂ A) = cfc (p := p') f (↑a : Unitization ℂ A)

Tactic:
obtain (hf | ha) := not_and_or.mp h

Premises used: not_and_or, Iff.mp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
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)
neg₂ neg₃ : Eq.{u_1 + 1} (α := Unitization ℂ A) 0 0
⊢ (↑(cfcₙ (p := p) f a) : Unitization ℂ A) = cfc (p := p') f (↑a : Unitization ℂ A)

Tactic:
rw [cfcₙ_apply_of_not_continuousOn a hf, inr_zero,
        cfc_apply_of_not_continuousOn _ (quasispectrum_eq_spectrum_inr' R ℂ a ▸ hf)]

Premises used: Unitization.inr_zero, cfc_apply_of_not_continuousOn, cfcₙ_apply_of_not_continuousOn
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
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)
neg₂ neg₃ : Eq.{u_1 + 1} (α := Unitization ℂ A) 0 0
⊢ (↑(cfcₙ (p := p) f a) : 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)]

Premises used: not_iff_not, Iff.mpr, cfcₙ_apply_of_not_predicate, cfc_apply_of_not_predicate, Unitization.inr_zero
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
a : A
f : ℂ → ℂ
hf₀ : f 0 = 0
⊢ (↑(cfcₙ (p := IsStarNormal) f a) : Unitization ℂ A) = cfc (p := IsStarNormal) f (↑a : Unitization ℂ A)

Tactic:
Unitization.cfcₙ_eq_cfc_inr isStarNormal_inr ..

Premises used: Unitization.isStarNormal_inr, Unitization.cfcₙ_eq_cfc_inr
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
a : A
f : ℝ → ℝ
hf₀ : f 0 = 0
⊢ (↑(cfcₙ (p := IsSelfAdjoint) f a) : Unitization ℂ A) = cfc (p := IsSelfAdjoint) f (↑a : Unitization ℂ A)

Tactic:
Unitization.cfcₙ_eq_cfc_inr isSelfAdjoint_inr ..

Premises used: Unitization.isSelfAdjoint_inr, Unitization.cfcₙ_eq_cfc_inr
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra 𝕜 A
inst_4 : TopologicalSpace A
inst_5 : ContinuousFunctionalCalculus 𝕜 A p
inst_6 : IsSemitopologicalRing A
inst_7 : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
r : 𝕜
enter : ContinuousMap.const (↑(spectrum 𝕜 a) : Type u_1) r
| Commute
    ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A)
      (ContinuousMap.const (↑(spectrum 𝕜 a) : Type u_1) r))
    b

Tactic:
enter [1, 2]
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra 𝕜 A
inst_4 : TopologicalSpace A
inst_5 : ContinuousFunctionalCalculus 𝕜 A p
inst_6 : IsSemitopologicalRing A
inst_7 : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
r : 𝕜
⊢ Eq (α := C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) (ContinuousMap.const (↑(spectrum 𝕜 a) : Type u_1) r)
    ((algebraMap 𝕜 C((↑(spectrum 𝕜 a) : Type u_1), 𝕜) : (a_1 : 𝕜) → C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) r)

Tactic:
rfl
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra 𝕜 A
inst_4 : TopologicalSpace A
inst_5 : ContinuousFunctionalCalculus 𝕜 A p
inst_6 : IsSemitopologicalRing A
inst_7 : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
r : 𝕜
enter :
  ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A)
      (ContinuousMap.const (↑(spectrum 𝕜 a) : Type u_1) r) :
    A)
enter₁ : ContinuousMap.const (↑(spectrum 𝕜 a) : Type u_1) r
| Commute
    ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A)
      (ContinuousMap.const (↑(spectrum 𝕜 a) : Type u_1) r))
    b

Tactic:
enter [1, 2]
      equals algebraMap 𝕜 _ r => rfl

Premises used: Algebra.algebraMap, DFunLike.coe
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra 𝕜 A
inst_4 : TopologicalSpace A
inst_5 : ContinuousFunctionalCalculus 𝕜 A p
inst_6 : IsSemitopologicalRing A
inst_7 : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
r : 𝕜
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
⊢ Commute
    ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A)
      (ContinuousMap.const (↑(spectrum 𝕜 a) : Type u_1) r))
    b

Tactic:
conv =>
      enter [1, 2]
      equals algebraMap 𝕜 _ r => rfl

Premises used: Algebra.algebraMap, DFunLike.coe
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra 𝕜 A
inst_4 : TopologicalSpace A
inst_5 : ContinuousFunctionalCalculus 𝕜 A p
inst_6 : IsSemitopologicalRing A
inst_7 : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
r : 𝕜
const : Commute ((algebraMap 𝕜 A : (a : 𝕜) → A) r) b
⊢ 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:
rw [AlgHomClass.commutes]

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

Tactic:
Algebra.commute_algebraMap_left r b

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

Tactic:
exact Algebra.commute_algebraMap_left r b

Premises used: Algebra.commute_algebraMap_left
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra 𝕜 A
inst_4 : TopologicalSpace A
inst_5 : ContinuousFunctionalCalculus 𝕜 A p
inst_6 : IsSemitopologicalRing A
inst_7 : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
id id₁ id₂ id₃ : Commute a b
⊢ Commute
    ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A)
      (ContinuousMap.restrict (spectrum 𝕜 a) (ContinuousMap.id 𝕜)))
    b

Tactic:
rwa [cfcHom_id ha]

Premises used: cfcHom_id
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra 𝕜 A
inst_4 : TopologicalSpace A
inst_5 : ContinuousFunctionalCalculus 𝕜 A p
inst_6 : IsSemitopologicalRing A
inst_7 : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
star_id :
  Commute
    (star
      ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A)
        (ContinuousMap.restrict (spectrum 𝕜 a) (ContinuousMap.id 𝕜))))
    b
star_id₁ star_id₂ star_id₃ star_id₄ : 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

Tactic:
rwa [map_star, cfcHom_id]

Premises used: cfcHom_id, StarHomClass.map_star
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : 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
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
⊢ Commute ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A) (f + g)) b

Tactic:
rw [map_add]

Premises used: map_add
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : 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
    (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:
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 : 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
    (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:
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 : 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
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
⊢ Commute ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 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 : 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
    (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:
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 : 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
    (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:
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 : Ring A
inst_2 : StarRing A
inst_3 : Algebra 𝕜 A
inst_4 : TopologicalSpace A
inst_5 : ContinuousFunctionalCalculus 𝕜 A p
inst_6 : IsSemitopologicalRing A
inst_7 : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
f : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)
hf :
  ∃ᶠ (g : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) in nhds f,
    Commute ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A) g) b
⊢ Continuous (Y := A) fun (x : A) ↦ x * b

Tactic:
fun_prop