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
S : Type u_3
inst_9 : SMul S R
inst_10 : ContinuousConstSMul S R
inst_11 : SMulZeroClass S A
inst_12 : IsScalarTower S R A
inst_13 : IsScalarTower S R (R → R)
s : S
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
pos :
  (cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
      { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) (HSMul.hSMul (β := R) s 1 • f), continuous_toFun := ⋯ :
        C((↑(spectrum R a) : Type u_1), R) } =
    HSMul.hSMul (β := A) (HSMul.hSMul (β := R) s 1)
      ((cfcHom (p := p) ha : (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)
⊢ (cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
      { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) fun (x : R) ↦ s • f x, continuous_toFun := ⋯ :
        C((↑(spectrum R a) : Type u_1), R) } =
    HSMul.hSMul (β := A) s
      ((cfcHom (p := p) ha : (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)

Tactic:
simp_rw [← Pi.smul_def, ← smul_one_smul R s _]

Premises used: smul_one_smul, Pi.smul_def
-- 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
S : Type u_3
inst_9 : SMul S R
inst_10 : ContinuousConstSMul S R
inst_11 : SMulZeroClass S A
inst_12 : IsScalarTower S R A
inst_13 : IsScalarTower S R (R → R)
s : S
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
pos :
  Eq.{u_2 + 1} (α := A)
    ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
        { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) (HSMul.hSMul (β := R) s 1 • f),
          continuous_toFun := ⋯ : C((↑(spectrum R a) : Type u_1), R) } :
      A)
    ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
        (HSMul.hSMul (β := R) s 1 •
          { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
            C((↑(spectrum R a) : Type u_1), R) }) :
      A)
⊢ (cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
      { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) (HSMul.hSMul (β := R) s 1 • f), continuous_toFun := ⋯ :
        C((↑(spectrum R a) : Type u_1), R) } =
    HSMul.hSMul (β := A) (HSMul.hSMul (β := R) s 1)
      ((cfcHom (p := p) ha : (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)

Tactic:
rw [← map_smul]

Premises used: map_smul
-- 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
S : Type u_3
inst_9 : SMul S R
inst_10 : ContinuousConstSMul S R
inst_11 : SMulZeroClass S A
inst_12 : IsScalarTower S R A
inst_13 : IsScalarTower S R (R → R)
s : S
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ Eq.{u_2 + 1} (α := A)
    ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
        { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) (HSMul.hSMul (β := R) s 1 • f),
          continuous_toFun := ⋯ : C((↑(spectrum R a) : Type u_1), R) } :
      A)
    ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
        (HSMul.hSMul (β := R) s 1 •
          { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
            C((↑(spectrum 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
S : Type u_3
inst_9 : SMul S R
inst_10 : ContinuousConstSMul S R
inst_11 : SMulZeroClass S A
inst_12 : IsScalarTower S R A
inst_13 : IsScalarTower S R (R → R)
s : S
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
ha : ¬p a
⊢ cfc (p := p) (fun (x : R) ↦ s • f x) a = s • cfc (p := p) f a

Tactic:
simp [cfc_apply_of_not_predicate a ha]

Premises used: cfc_apply_of_not_predicate
-- 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
a : A
hf : ContinuousOn f (spectrum R a)
⊢ cfc (p := p) (fun (x : R) ↦ r * f x) a = r • cfc (p := p) f a

Tactic:
cfc_smul r f a

Premises used: cfc_smul
-- 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
a : A
pos : ∀ (h : p a ∧ ContinuousOn f (spectrum R a)), cfc (p := p) (fun (x : R) ↦ star (f x)) a = star (cfc (p := p) f a)
neg :
  ∀ (h : ¬(p a ∧ ContinuousOn f (spectrum R a))), cfc (p := p) (fun (x : R) ↦ star (f x)) a = star (cfc (p := p) f a)
⊢ cfc (p := p) (fun (x : R) ↦ star (f x)) a = star (cfc (p := p) f a)

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

Premises used: spectrum, ContinuousOn
-- 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
a : A
h : p a ∧ ContinuousOn f (spectrum R a)
⊢ p a

Tactic:
obtain ⟨ha, hf⟩ := h
-- 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
a : A
h : p a ∧ ContinuousOn f (spectrum R a)
ha : p a
⊢ ContinuousOn f (spectrum R a)

Tactic:
obtain ⟨ha, hf⟩ := h
-- 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
a : A
ha : p a
hf : ContinuousOn f (spectrum R a)
pos :
  Eq.{u_2 + 1} (α := A)
    ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
        { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) fun (x : R) ↦ star (f x), continuous_toFun := ⋯ :
          C((↑(spectrum R a) : Type u_1), R) } :
      A)
    ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
        (star
          { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
            C((↑(spectrum R a) : Type u_1), R) }) :
      A)
⊢ cfc (p := p) (fun (x : R) ↦ star (f x)) a = star (cfc (p := p) f a)

Tactic:
rw [cfc_apply f a, ← map_star, cfc_apply _ a]

Premises used: StarHomClass.map_star, cfc_apply
-- 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
a : A
ha : p a
hf : ContinuousOn f (spectrum R a)
⊢ Eq.{u_2 + 1} (α := A)
    ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
        { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) fun (x : R) ↦ star (f x), continuous_toFun := ⋯ :
          C((↑(spectrum R a) : Type u_1), R) } :
      A)
    ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
        (star
          { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
            C((↑(spectrum 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
f : R → R
a : A
h : ¬(p a ∧ ContinuousOn f (spectrum R a))
neg : ∀ (ha : ¬p a), cfc (p := p) (fun (x : R) ↦ star (f x)) a = star (cfc (p := p) f a)
neg₁ : ∀ (hf : ¬ContinuousOn f (spectrum R a)), cfc (p := p) (fun (x : R) ↦ star (f x)) a = star (cfc (p := p) f a)
⊢ cfc (p := p) (fun (x : R) ↦ star (f x)) a = star (cfc (p := p) f a)

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

Premises used: not_and_or, Iff.mp
-- 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
a : A
h : ¬(p a ∧ ContinuousOn f (spectrum R a))
ha : ¬p a
⊢ cfc (p := p) (fun (x : R) ↦ star (f x)) a = star (cfc (p := p) f a)

Tactic:
simp [cfc_apply_of_not_predicate a ha]

Premises used: cfc_apply_of_not_predicate
-- 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
a : A
h : ¬(p a ∧ ContinuousOn f (spectrum R a))
hf : ¬ContinuousOn f (spectrum R a)
neg : ¬ContinuousOn (Y := R) (fun (x : R) ↦ star (f x)) (spectrum R a)
⊢ cfc (p := p) (fun (x : R) ↦ star (f x)) a = star (cfc (p := p) f a)

Tactic:
rw [cfc_apply_of_not_continuousOn a hf, cfc_apply_of_not_continuousOn, star_zero]

Premises used: star_zero, cfc_apply_of_not_continuousOn
-- 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
a : A
h : ¬(p a ∧ ContinuousOn f (spectrum R a))
hf : ¬ContinuousOn f (spectrum R a)
hf_star : ContinuousOn (Y := R) (fun (x : R) ↦ star (f x)) (spectrum R a)
⊢ ContinuousOn f (spectrum R a)

Tactic:
simpa using hf_star.star

Premises used: ContinuousOn.star
-- 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
a : A
h : ¬(p a ∧ ContinuousOn f (spectrum R a))
hf : ¬ContinuousOn f (spectrum R a)
⊢ ¬ContinuousOn (Y := R) (fun (x : R) ↦ star (f x)) (spectrum R a)

Tactic:
exact fun hf_star ↦ hf <| by simpa using hf_star.star
-- 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
n : ℕ
ha : p a
rw : cfc (p := p) (fun (x : R) ↦ x) a ^ n = a ^ n
rw₁ rw₂ : a ^ n = a ^ n
⊢ cfc (p := p) (fun (x : R) ↦ x ^ n) a = a ^ n

Tactic:
rw [cfc_pow .., cfc_id' ..]

Premises used: cfc_pow, cfc_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
S : Type u_3
inst_9 : SMul S R
inst_10 : ContinuousConstSMul S R
inst_11 : SMulZeroClass S A
inst_12 : IsScalarTower S R A
inst_13 : IsScalarTower S R (R → R)
s : S
a : A
ha : p a
rw : s • cfc (p := p) (fun (x : R) ↦ x) a = s • a
rw₁ rw₂ : s • a = s • a
⊢ cfc (p := p) (fun (x : R) ↦ s • x) a = s • a

Tactic:
rw [cfc_smul .., cfc_id' ..]

Premises used: cfc_id', cfc_smul
-- 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
a : A
ha : p a
⊢ cfc (p := p) (fun (x : R) ↦ r * x) a = r • a

Tactic:
cfc_smul_id r a

Premises used: 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
a : A
ha : p a
rw : star (cfc (p := p) (fun (x : R) ↦ x) a) = star a
rw₁ rw₂ : star a = star a
⊢ cfc (p := p) (fun (x : R) ↦ star x) a = star a

Tactic:
rw [cfc_star .., cfc_id' ..]

Premises used: cfc_id', cfc_star
-- 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 : StarModule R A
a : A
ha : p a
h :
  ∀ (x : A),
    Membership.mem (γ := Set A) (Set.range fun (x : R → R) ↦ cfc (p := p) x a) x ↔
      x ∈ (↑(StarAlgHom.range (A := C((↑(spectrum R a) : Type u_1), R)) (cfcHom (p := p) ha)) : Set A)
⊢ (Set.range fun (x : R → R) ↦ cfc (p := p) x a) =
    (↑(StarAlgHom.range (A := C((↑(spectrum R a) : Type u_1), R)) (cfcHom (p := p) ha)) : Set A)

Tactic:
ext
-- 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 : StarModule R A
a : A
ha : p a
x : A
h :
  Membership.mem (γ := Set A) (Set.range fun (x : R → R) ↦ cfc (p := p) x a) x →
    x ∈ (↑(StarAlgHom.range (A := C((↑(spectrum R a) : Type u_1), R)) (cfcHom (p := p) ha)) : Set A)
h₁ :
  x ∈ (↑(StarAlgHom.range (A := C((↑(spectrum R a) : Type u_1), R)) (cfcHom (p := p) ha)) : Set A) →
    Membership.mem (γ := Set A) (Set.range fun (x : R → R) ↦ cfc (p := p) x a) x
⊢ Membership.mem (γ := Set A) (Set.range fun (x : R → R) ↦ cfc (p := p) x a) x ↔
    x ∈ (↑(StarAlgHom.range (A := C((↑(spectrum R a) : Type u_1), R)) (cfcHom (p := p) ha)) : Set A)

Tactic:
constructor
-- 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 : StarModule R A
a : A
ha : p a
f : R → R
⊢ (fun (x : R → R) ↦ cfc (p := p) x a) f ∈
    (↑(StarAlgHom.range (A := C((↑(spectrum R a) : Type u_1), R)) (cfcHom (p := p) ha)) : Set A)

Tactic:
cfc_cases _ a f (zero_mem _) fun hf ha ↦ ⟨_, rfl⟩

Premises used: spectrum, Set.Mem, ContinuousMap.mk, ContinuousOn.restrict, Exists.intro, ZeroMemClass.zero_mem, Set.restrict, cfc_cases, 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 : StarModule R A
a : A
ha : p a
f : R → R
⊢ (fun (x : R → R) ↦ cfc (p := p) x a) f ∈
    (↑(StarAlgHom.range (A := C((↑(spectrum R a) : Type u_1), R)) (cfcHom (p := p) ha)) : Set A)

Tactic:
exact cfc_cases _ a f (zero_mem _) fun hf ha ↦ ⟨_, 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 : StarModule R A
a : A
ha : p a
f : C((↑(spectrum R a) : Type u_1), R)
⊢ Membership.mem.{u_2, u_2} (α := A) (γ := Set A) (Set.range fun (x : R → R) ↦ cfc (p := p) x a)
    ((AlgHom.toRingHom (↑(cfcHom (p := p) ha) : C((↑(spectrum R a) : Type u_1), R) →ₐ[R] A) :
          (a : C((↑(spectrum R a) : Type u_1), R)) → A)
        f :
      A)

Tactic:
⟨Subtype.val.extend f 0, cfcHom_eq_cfc_extend _ ha _ |>.symm⟩

Premises used: Set.Mem, setOf, Function.extend, cfcHom_eq_cfc_extend, Exists.intro, Set.range, OfNat.ofNat, Eq.symm, Subtype.val, 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
inst_9 : StarModule R A
a : A
ha : p a
f : C((↑(spectrum R a) : Type u_1), R)
⊢ Membership.mem.{u_2, u_2} (α := A) (γ := Set A) (Set.range fun (x : R → R) ↦ cfc (p := p) x a)
    ((AlgHom.toRingHom (↑(cfcHom (p := p) ha) : C((↑(spectrum R a) : Type u_1), R) →ₐ[R] A) :
          (a : C((↑(spectrum R a) : Type u_1), R)) → A)
        f :
      A)

Tactic:
exact ⟨Subtype.val.extend f 0, cfcHom_eq_cfc_extend _ ha _ |>.symm⟩
-- 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
ha : p a
⊢ cfc (p := p) (fun (x : R) ↦ Polynomial.eval x X) a = a

Tactic:
simpa using cfc_id R a

Premises used: cfc_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
r : R
a : A
ha : p a
⊢ cfc (p := p) (fun (x : R) ↦ Polynomial.eval x ((Polynomial.C : (a : R) → R[X]) r)) a =
    (algebraMap R A : (a : R) → A) r

Tactic:
simp [cfc_const r a]

Premises used: cfc_const
-- 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
a : A
ha : p a
hf : ContinuousOn f (spectrum R a)
r : R
⊢ cfc (p := p) (fun (x : R) ↦ Polynomial.eval (f x) ((Polynomial.C : (a : R) → R[X]) r)) a =
    (aeval (cfc (p := p) f a) : (a : R[X]) → A) ((Polynomial.C : (a : R) → R[X]) r : R[X])

Tactic:
simp [cfc_const r a]

Premises used: cfc_const
-- 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
a : A
ha : p a
hf : ContinuousOn f (spectrum R a)
q₁ q₂ : R[X]
hq₁ : cfc (p := p) (fun (x : R) ↦ Polynomial.eval (f x) q₁) a = (aeval (cfc (p := p) f a) : (a : R[X]) → A) q₁
hq₂ : cfc (p := p) (fun (x : R) ↦ Polynomial.eval (f x) q₂) a = (aeval (cfc (p := p) f a) : (a : R[X]) → A) q₂
⊢ cfc (p := p) (fun (x : R) ↦ Polynomial.eval (f x) (q₁ + q₂)) a = (aeval (cfc (p := p) f a) : (a : R[X]) → A) (q₁ + q₂)

Tactic:
simp only [eval_add, map_add, ← hq₁, ← hq₂, cfc_add a (q₁.eval <| f ·) (q₂.eval <| f ·)]

Premises used: Polynomial.eval, map_add, Polynomial.eval_add, cfc_add