awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_9 : UniqueHom R A
g f : R → R
a : A
ha : p a
hg : ContinuousOn g (f '' spectrum R a)
hf : ContinuousOn f (spectrum R a)
this : ContinuousOn (g ∘ f) (spectrum R a)
sp_eq :
  spectrum.{u_1, u_2} R (A := A)
      ((cfcHom (p := p) ⋯ : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
          { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
            C((↑(spectrum R a) : Type u_1), R) } :
        A) =
    f '' spectrum R a
⊢ ∀ (x : (↑(spectrum R a) : Type u_1)),
    Eq (α := R)
      (({ toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
              C((↑(spectrum R a) : Type u_1), R) } :
            (a : (↑(spectrum R a) : Type u_1)) → R)
          x :
        R)
      ((↑(({
                  toFun :=
                    Set.codRestrict ((spectrum R a).restrict (π := fun (a : R) ↦ R) f)
                      (spectrum.{u_1, u_2} R (A := A)
                        ((cfcHom (p := p) ⋯ : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
                            { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
                              C((↑(spectrum R a) : Type u_1), R) } :
                          A))
                      ⋯,
                  continuous_toFun := ⋯ } :
                (a_1 : (↑(spectrum R a) : Type u_1)) →
                  (↑(spectrum R
                        ((cfcHom ⋯ : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
                          { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ })) :
                    Type u_1))
              x) :
          R) :
        R)

Tactic:
exact fun _ ↦ rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_9 : UniqueHom R A
g f : R → R
a : A
hg : ContinuousOn g (f '' spectrum R a)
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ cfc (p := p) (fun (x : R) ↦ g (f x)) a = cfc (p := p) g (cfc (p := p) f a)

Tactic:
cfc_comp g f a

Premises used: cfc_comp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_9 : UniqueHom R A
f : R → R
n : ℕ
a : A
hf : ContinuousOn f ((fun (x : R) ↦ x ^ n) '' spectrum R a)
ha : p a
rw : cfc (p := p) f (cfc (p := p) (fun (x : R) ↦ x ^ n) a) = cfc (p := p) f (a ^ n)
rw₁ rw₂ : cfc (p := p) f (a ^ n) = cfc (p := p) f (a ^ n)
⊢ cfc (p := p) (fun (x : R) ↦ f (x ^ n)) a = cfc (p := p) f (a ^ n)

Tactic:
rw [cfc_comp' .., cfc_pow_id ..]

Premises used: cfc_comp', cfc_pow_id
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_9 : UniqueHom R A
S : Type u_3
inst_10 : SMul S R
inst_11 : ContinuousConstSMul S R
inst_12 : SMulZeroClass S A
inst_13 : IsScalarTower S R A
inst_14 : IsScalarTower S R (R → R)
s : S
f : R → R
a : A
hf : ContinuousOn f ((fun (x : R) ↦ s • x) '' spectrum R a)
ha : p a
rw : cfc (p := p) f (cfc (p := p) (HSMul.hSMul s) a) = cfc (p := p) f (s • a)
rw₁ rw₂ : cfc (p := p) f (s • a) = cfc (p := p) f (s • a)
⊢ cfc (p := p) (fun (x : R) ↦ f (s • x)) a = cfc (p := p) f (s • a)

Tactic:
rw [cfc_comp' .., cfc_smul_id ..]

Premises used: cfc_comp', cfc_smul_id
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_9 : UniqueHom R A
r : R
f : R → R
a : A
hf : ContinuousOn f ((fun (x : R) ↦ r * x) '' spectrum R a)
ha : p a
rw : cfc (p := p) f (cfc (p := p) (HMul.hMul r) a) = cfc (p := p) f (r • a)
rw₁ rw₂ : cfc (p := p) f (r • a) = cfc (p := p) f (r • a)
⊢ cfc (p := p) (fun (x : R) ↦ f (r * x)) a = cfc (p := p) f (r • a)

Tactic:
rw [cfc_comp' .., cfc_const_mul_id ..]

Premises used: cfc_comp', cfc_const_mul_id
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_9 : UniqueHom R A
f : R → R
a : A
hf : ContinuousOn f (star '' spectrum R a)
ha : p a
rw : cfc (p := p) f (cfc.{u_1, u_2} (R := R) (p := p) star a) = cfc (p := p) f (star a)
rw₁ rw₂ : cfc (p := p) f (star a) = cfc (p := p) f (star a)
⊢ cfc (p := p) (fun (x : R) ↦ f (star x)) a = cfc (p := p) f (star a)

Tactic:
rw [cfc_comp' .., cfc_star_id ..]

Premises used: cfc_comp', cfc_star_id
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_9 : UniqueHom R A
q : R[X]
f : R → R
a : A
hf : ContinuousOn f ((fun (x : R) ↦ Polynomial.eval x q) '' spectrum R a)
ha : p a
rw : cfc (p := p) f (cfc (p := p) (fun (x : R) ↦ Polynomial.eval x q) a) = cfc (p := p) f ((aeval a : (a : R[X]) → A) q)
rw₁ rw₂ : cfc (p := p) f ((aeval a : (a : R[X]) → A) q) = cfc (p := p) f ((aeval a : (a : R[X]) → A) q)
⊢ cfc (p := p) (fun (x : R) ↦ f (Polynomial.eval x q)) a = cfc (p := p) f ((aeval a : (a : R[X]) → A) q)

Tactic:
rw [cfc_comp' .., cfc_polynomial ..]

Premises used: cfc_comp', cfc_polynomial
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
a : A
r : R
h_spec : spectrum R a ⊆ {r}
ha : p a
x : R
hx : x ∈ spectrum R a
⊢ id x = (fun (x : R) ↦ r) x

Tactic:
simpa using h_spec hx
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
a : A
r : R
h_spec : spectrum R a ⊆ {r}
ha : p a
⊢ a = (algebraMap R A : (a : R) → A) r

Tactic:
simpa [cfc_id R a, cfc_const r a] using
    cfc_congr (f := id) (g := fun _ : R ↦ r) (a := a) fun x hx ↦ by simpa using h_spec hx

Premises used: cfc_const, cfc_id, cfc_congr
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
a : A
h_spec : spectrum R a ⊆ {0}
ha : p a
⊢ a = 0

Tactic:
simpa using eq_algebraMap_of_spectrum_subset_singleton a 0 h_spec

Premises used: OfNat.ofNat, CFC.eq_algebraMap_of_spectrum_subset_singleton
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
a : A
h_spec : spectrum R a ⊆ {1}
ha : p a
⊢ a = 1

Tactic:
simpa using eq_algebraMap_of_spectrum_subset_singleton a 1 h_spec

Premises used: OfNat.ofNat, CFC.eq_algebraMap_of_spectrum_subset_singleton
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
r : R
rw : Subset (α := Set R) ((fun (x : R) ↦ r) '' spectrum.{u_1, u_2} R (A := A) 0) {r}
⊢ spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A) ⊆ {r}

Tactic:
rw [← cfc_const r 0 (cfc_predicate_zero R),
    cfc_map_spectrum (fun _ ↦ r) 0 (cfc_predicate_zero R)]

Premises used: cfc_map_spectrum, cfc_const, cfc_predicate_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
r x : R
⊢ Membership.mem (γ := Set R) {r} ((fun (x : R) ↦ r) x)

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_9 : Nontrivial A
r : R
⊢ p 0

Tactic:
have hp : p 0 := cfc_predicate_zero R
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_9 : Nontrivial A
r : R
hp : p 0
rw : Eq (α := Set R) ((fun (x : R) ↦ r) '' spectrum.{u_1, u_2} R (A := A) 0) {r}
⊢ spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A) = {r}

Tactic:
rw [← cfc_const r 0 hp, cfc_map_spectrum (fun _ => r) 0 hp]

Premises used: cfc_map_spectrum, cfc_const, OfNat.ofNat
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_9 : Nontrivial A
r : R
hp : p 0
⊢ Eq (α := Set R) ((fun (x : R) ↦ r) '' spectrum.{u_1, u_2} R (A := A) 0) {r}

Tactic:
Set.Nonempty.image_const (⟨0, spectrum.zero_mem (R := R) not_isUnit_zero⟩) _

Premises used: spectrum.zero_mem, Set.Nonempty.image_const, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_9 : Nontrivial A
r : R
hp : p 0
⊢ Eq (α := Set R) ((fun (x : R) ↦ r) '' spectrum.{u_1, u_2} R (A := A) 0) {r}

Tactic:
exact Set.Nonempty.image_const (⟨0, spectrum.zero_mem (R := R) not_isUnit_zero⟩) _

Premises used: spectrum.zero_mem, Set.Nonempty.image_const, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_9 : Nontrivial A
⊢ Eq.{u_2 + 1} (α := A) (0 : A) ((algebraMap R A : (a : R) → A) 0 : A)

Tactic:
have : (0 : A) = algebraMap R A 0 := Eq.symm (map_zero (algebraMap R A))
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_9 : Nontrivial A
this : Eq.{u_2 + 1} (α := A) (0 : A) ((algebraMap R A : (a : R) → A) 0 : A)
rw : spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) 0 : A) = {0}
rw₁ rw₂ : Eq (α := Set R) {0} {0}
⊢ spectrum.{u_1, u_2} R (A := A) 0 = {0}

Tactic:
rw [this, spectrum_algebraMap_eq]

Premises used: CFC.spectrum_algebraMap_eq
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_9 : Nontrivial A
⊢ Eq.{u_2 + 1} (α := A) (1 : A) ((algebraMap R A : (a : R) → A) 1 : A)

Tactic:
have : (1 : A) = algebraMap R A 1 := Eq.symm (map_one (algebraMap R A))
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_9 : Nontrivial A
this : Eq.{u_2 + 1} (α := A) (1 : A) ((algebraMap R A : (a : R) → A) 1 : A)
rw : spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) 1 : A) = {1}
rw₁ rw₂ : Eq (α := Set R) {1} {1}
⊢ spectrum.{u_1, u_2} R (A := A) 1 = {1}

Tactic:
rw [this, spectrum_algebraMap_eq]

Premises used: CFC.spectrum_algebraMap_eq
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
r : R
f : R → R
⊢ ContinuousOn f (spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A))

Tactic:
have h₁ : ContinuousOn f (spectrum R (algebraMap R A r)) :=
  continuousOn_singleton _ _ |>.mono <| CFC.spectrum_algebraMap_subset r
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
r : R
f : R → R
h₁ : ContinuousOn f (spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A))
rw :
  Eq.{u_2 + 1} (α := A)
    ((cfcHom (p := p) ⋯ : (a : C((↑(spectrum R ((algebraMap R A : (a : R) → A) r)) : Type u_1), R)) → A)
        {
          toFun :=
            (spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A)).restrict (π := fun (a : R) ↦ R) f,
          continuous_toFun := ⋯ :
          C((↑(spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A)) : Type u_1), R) } :
      A)
    ((cfcHom (p := p) ⋯ : (a : C((↑(spectrum R ((algebraMap R A : (a : R) → A) r)) : Type u_1), R)) → A)
        ((algebraMap R C((↑(spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A)) : Type u_1), R) :
              (a : R) → C((↑(spectrum R ((algebraMap R A : (a : R) → A) r)) : Type u_1), R))
            (f r) :
          C((↑(spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A)) : Type u_1), R)) :
      A)
⊢ cfc (p := p) f ((algebraMap R A : (a : R) → A) r) = (algebraMap R A : (a : R) → A) (f r)

Tactic:
rw [cfc_apply f (algebraMap R A r) (cfc_predicate_algebraMap r),
    ← AlgHomClass.commutes (cfcHom (p := p) (cfc_predicate_algebraMap r)) (f r)]

Premises used: Algebra.algebraMap, cfcHom, AlgHomClass.commutes, cfc_apply, cfc_predicate_algebraMap, DFunLike.coe
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
r : R
f : R → R
h₁ : ContinuousOn f (spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A))
h :
  (spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A)).restrict (π := fun (a : R) ↦ R) f =
    fun (x : (↑(spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A)) : Type u_1)) ↦
    (algebraMap R R : (a : R) → R) (f r)
⊢ Eq.{u_2 + 1} (α := A)
    ((cfcHom (p := p) ⋯ : (a : C((↑(spectrum R ((algebraMap R A : (a : R) → A) r)) : Type u_1), R)) → A)
        {
          toFun :=
            (spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A)).restrict (π := fun (a : R) ↦ R) f,
          continuous_toFun := ⋯ :
          C((↑(spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A)) : Type u_1), R) } :
      A)
    ((cfcHom (p := p) ⋯ : (a : C((↑(spectrum R ((algebraMap R A : (a : R) → A) r)) : Type u_1), R)) → A)
        ((algebraMap R C((↑(spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A)) : Type u_1), R) :
              (a : R) → C((↑(spectrum R ((algebraMap R A : (a : R) → A) r)) : Type u_1), R))
            (f r) :
          C((↑(spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A)) : Type u_1), R)) :
      A)

Tactic:
congr
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
r : R
f : R → R
h₁ : ContinuousOn f (spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A))
h :
  ∀ (x : R) (hx : x ∈ spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A)),
    (spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A)).restrict (π := fun (a : R) ↦ R) f
        (Subtype.mk (p := fun (x : R) ↦ x ∈ spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A)) x
          hx) =
      (algebraMap R R : (a : R) → R) (f r)
⊢ (spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A)).restrict (π := fun (a : R) ↦ R) f =
    fun (x : (↑(spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A)) : Type u_1)) ↦
    (algebraMap R R : (a : R) → R) (f r)

Tactic:
ext ⟨x, hx⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
r : R
f : R → R
h₁ : ContinuousOn f (spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A))
x : R
hx : x ∈ spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A)
⊢ Membership.mem (γ := Set R) {r} x

Tactic:
apply CFC.spectrum_algebraMap_subset r at hx

Premises used: CFC.spectrum_algebraMap_subset
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
r : R
f : R → R
h₁ : ContinuousOn f (spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A))
x : R
hx_1 : x ∈ spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A)
hx : Membership.mem (γ := Set R) {r} x
⊢ (spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A)).restrict (π := fun (a : R) ↦ R) f
      (Subtype.mk (p := fun (x : R) ↦ x ∈ spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A)) x
        hx_1) =
    (algebraMap R R : (a : R) → R) (f r)

Tactic:
simp_all
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
f : R → R
⊢ cfc (p := p) f 0 = (algebraMap R A : (a : R) → A) (f 0)

Tactic:
simpa using cfc_algebraMap (A := A) 0 f

Premises used: OfNat.ofNat, cfc_algebraMap
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
f : R → R
⊢ cfc (p := p) f 1 = (algebraMap R A : (a : R) → A) (f 1)

Tactic:
simpa using cfc_algebraMap (A := A) 1 f

Premises used: OfNat.ofNat, cfc_algebraMap
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
f_1 g : R → R
a_1 : A
ha : p a_1
hf : ContinuousOn f_1 (spectrum R a_1)
hg : ContinuousOn g (spectrum R a_1)
f : R → R
a : A
pos :
  ∀ (h : ContinuousOn f (spectrum R a)),
    star (cfc (p := p) f a) * cfc (p := p) f a = cfc (p := p) f a * star (cfc (p := p) f a)
neg :
  ∀ (h : ¬ContinuousOn f (spectrum R a)),
    star (cfc (p := p) f a) * cfc (p := p) f a = cfc (p := p) f a * star (cfc (p := p) f a)
⊢ star (cfc (p := p) f a) * cfc (p := p) f a = cfc (p := p) f a * star (cfc (p := p) f a)

Tactic:
by_cases h : ContinuousOn f (spectrum R a)

Premises used: spectrum, ContinuousOn