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
a : A
f g : R → R
hf : ContinuousOn f (spectrum R a)
hg : ContinuousOn g (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) fun (x : R) ↦ f x + g 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)
        ({ toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
            C((↑(spectrum R a) : Type u_1), R) } +
          { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) g, continuous_toFun := ⋯ :
            C((↑(spectrum R a) : Type u_1), R) }) :
      A)
⊢ cfc (p := p) (fun (x : R) ↦ f x + g x) a = cfc (p := p) f a + cfc (p := p) g a

Tactic:
rw [cfc_apply f a, cfc_apply g a, ← map_add, cfc_apply _ a]

Premises used: map_add, 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
a : A
f g : R → R
hf : ContinuousOn f (spectrum R a)
hg : ContinuousOn g (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) fun (x : R) ↦ f x + g 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)
        ({ toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
            C((↑(spectrum R a) : Type u_1), R) } +
          { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) g, 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
a : A
f g : R → R
hf : ContinuousOn f (spectrum R a)
hg : ContinuousOn g (spectrum R a)
ha : ¬p a
⊢ cfc (p := p) (fun (x : R) ↦ f x + g x) a = cfc (p := p) f a + cfc (p := p) g 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)
ha : p a
h : ∀ (x : R), r + f x = (fun (x : R) ↦ r) x + f x
⊢ Eq.{u_1 + 1} (α := (z : R) → R) (fun (z : R) ↦ r + f z) fun (z : R) ↦ (fun (x : R) ↦ r) z + f z

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
r : R
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
x : R
⊢ r + f x = (fun (x : R) ↦ r) x + f 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
r : R
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ Eq.{u_1 + 1} (α := (z : R) → R) (fun (z : R) ↦ r + f z) fun (z : R) ↦ (fun (x : R) ↦ r) z + f z

Tactic:
have : (fun z => r + f z) = (fun z => (fun _ => r) z + f z) := by ext; 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
r : R
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
this : Eq.{u_1 + 1} (α := (z : R) → R) (fun (z : R) ↦ r + f z) fun (z : R) ↦ (fun (x : R) ↦ r) z + f z
rw :
  cfc (p := p) (fun (z : R) ↦ (fun (x : R) ↦ r) z + f z) a =
    HAdd.hAdd (α := A) ((algebraMap R A : (a : R) → A) r : A) (cfc (p := p) f a)
rw₁ :
  cfc (p := p) (fun (x : R) ↦ r) a + cfc (p := p) f a =
    HAdd.hAdd (α := A) ((algebraMap R A : (a : R) → A) r : A) (cfc (p := p) f a)
rw₂ rw₃ :
  HAdd.hAdd (α := A) ((algebraMap R A : (a : R) → A) r : A) (cfc (p := p) f a) =
    HAdd.hAdd (α := A) ((algebraMap R A : (a : R) → A) r : A) (cfc (p := p) f a)
⊢ cfc (p := p) (fun (x : R) ↦ r + f x) a = HAdd.hAdd (α := A) ((algebraMap R A : (a : R) → A) r : A) (cfc (p := p) f a)

Tactic:
rw [this, cfc_add a _ _ (continuousOn_const (c := r)) hf, cfc_const r a ha]

Premises used: continuousOn_const, cfc_const, cfc_add
-- 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)
ha : p a
rw :
  cfc (p := p) (fun (x : R) ↦ f x + r) a = HAdd.hAdd (α := A) ((algebraMap R A : (a : R) → A) r : A) (cfc (p := p) f a)
⊢ cfc (p := p) (fun (x : R) ↦ f x + r) a = HAdd.hAdd (β := A) (cfc (p := p) f a) ((algebraMap R A : (a : R) → A) r : A)

Tactic:
rw [add_comm (cfc f a)]

Premises used: cfc, add_comm
-- 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)
ha : p a
simp : cfc (p := p) (fun (x : R) ↦ r + f x) a
| cfc (p := p) (fun (x : R) ↦ f x + r) a

Tactic:
simp only [add_comm]

Premises used: add_comm
-- 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)
ha : p a
conv_lhs :
  cfc (p := p) (fun (x : R) ↦ r + f x) a = HAdd.hAdd (α := A) ((algebraMap R A : (a : R) → A) r : A) (cfc (p := p) f a)
⊢ cfc (p := p) (fun (x : R) ↦ f x + r) a = HAdd.hAdd (α := A) ((algebraMap R A : (a : R) → A) r : A) (cfc (p := p) f a)

Tactic:
conv_lhs => simp only [add_comm]

Premises used: add_comm
-- 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)
ha : p a
⊢ cfc (p := p) (fun (x : R) ↦ r + f x) a = HAdd.hAdd (α := A) ((algebraMap R A : (a : R) → A) r : A) (cfc (p := p) f a)

Tactic:
cfc_const_add r f a hf ha

Premises used: cfc_const_add
-- 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)
ha : p a
⊢ cfc (p := p) (fun (x : R) ↦ r + f x) a = HAdd.hAdd (α := A) ((algebraMap R A : (a : R) → A) r : A) (cfc (p := p) f a)

Tactic:
exact cfc_const_add r f a hf ha

Premises used: cfc_const_add
-- 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
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (spectrum R a)
pos : ∀ (ha : p a), cfc.{u_1, u_2} (R := R) (p := p) (∑ i ∈ s, f i) a = ∑ i ∈ s, cfc (p := p) (f i) a
neg : ∀ (ha : ¬p a), cfc.{u_1, u_2} (R := R) (p := p) (∑ i ∈ s, f i) a = ∑ i ∈ s, cfc (p := p) (f i) a
⊢ cfc.{u_1, u_2} (R := R) (p := p) (∑ i ∈ s, f i) a = ∑ i ∈ s, cfc (p := p) (f i) a

Tactic:
by_cases ha : p 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
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (spectrum R a)
ha : p a
h : ∀ (x : R), s.sum f x = ∑ i ∈ s, f i x
⊢ s.sum f = fun (z : R) ↦ ∑ i ∈ s, f i z

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
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (spectrum R a)
ha : p a
x : R
⊢ s.sum f x = ∑ i ∈ s, f i 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
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (spectrum R a)
ha : p a
⊢ s.sum f = fun (z : R) ↦ ∑ i ∈ s, f i z

Tactic:
have hsum : s.sum f = fun z => ∑ i ∈ s, f i z := by ext; 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
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (spectrum R a)
ha : p a
hsum : s.sum f = fun (z : R) ↦ ∑ i ∈ s, f i z
rw : ContinuousOn (Y := R) (fun (z : R) ↦ ∑ i ∈ s, f i z) (spectrum R a)
⊢ ContinuousOn (Y := R) (∑ i : ↥s, f (↑i : ι)) (spectrum R a)

Tactic:
rw [sum_coe_sort s, hsum]

Premises used: Finset.sum_coe_sort
-- 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
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (spectrum R a)
ha : p a
hsum : s.sum f = fun (z : R) ↦ ∑ i ∈ s, f i z
⊢ ContinuousOn (Y := R) (fun (z : R) ↦ ∑ i ∈ s, f i z) (spectrum R a)

Tactic:
continuousOn_finsetSum s fun i hi => hf i hi

Premises used: continuousOn_finsetSum
-- 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
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (spectrum R a)
ha : p a
hsum : s.sum f = fun (z : R) ↦ ∑ i ∈ s, f i z
⊢ ContinuousOn (Y := R) (fun (z : R) ↦ ∑ i ∈ s, f i z) (spectrum R a)

Tactic:
exact continuousOn_finsetSum s fun i hi => hf i hi

Premises used: continuousOn_finsetSum
-- 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
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (spectrum R a)
ha : p a
hsum : s.sum f = fun (z : R) ↦ ∑ i ∈ s, f i z
⊢ ContinuousOn (Y := R) (∑ i : ↥s, f (↑i : ι)) (spectrum R a)

Tactic:
have hf' : ContinuousOn (∑ i : s, f i) (spectrum R a) := by
      rw [sum_coe_sort s, hsum]
      exact continuousOn_finsetSum s fun i hi => hf i hi
-- 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
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (spectrum R a)
ha : p a
hsum : s.sum f = fun (z : R) ↦ ∑ i ∈ s, f i z
hf' : ContinuousOn (Y := R) (∑ i : ↥s, f (↑i : ι)) (spectrum R a)
pos : cfc.{u_1, u_2} (R := R) (p := p) (∑ i : ↥s, f (↑i : ι)) a = ∑ i : ↥s, cfc (p := p) (f (↑i : ι)) a
⊢ cfc.{u_1, u_2} (R := R) (p := p) (∑ i ∈ s, f i) a = ∑ i ∈ s, cfc (p := p) (f i) a

Tactic:
rw [← sum_coe_sort s, ← sum_coe_sort s]

Premises used: Finset.sum_coe_sort
-- 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
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (spectrum R a)
ha : p a
hsum : s.sum f = fun (z : R) ↦ ∑ i ∈ s, f i z
hf' : ContinuousOn (Y := R) (∑ i : ↥s, f (↑i : ι)) (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) (∑ i : ↥s, f (↑i : ι)), 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)
        (∑ x : ↥s, { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) (f (↑x : ι)), continuous_toFun := ⋯ }) :
      A)
⊢ cfc.{u_1, u_2} (R := R) (p := p) (∑ i : ↥s, f (↑i : ι)) a = ∑ i : ↥s, cfc (p := p) (f (↑i : ι)) a

Tactic:
rw [cfc_apply_pi _ a ha (fun ⟨i, hi⟩ => hf i hi), ← map_sum, cfc_apply _ a ha hf']

Premises used: map_sum, cfc_apply, cfc_apply_pi
-- 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
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (spectrum R a)
ha : p a
hsum : s.sum f = fun (z : R) ↦ ∑ i ∈ s, f i z
hf' : ContinuousOn (Y := R) (∑ i : ↥s, f (↑i : ι)) (spectrum R a)
pos :
  { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) (∑ i : ↥s, f (↑i : ι)), continuous_toFun := ⋯ :
      C((↑(spectrum R a) : Type u_1), R) } =
    ∑ x : ↥s, { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) (f (↑x : ι)), continuous_toFun := ⋯ }
⊢ 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) (∑ i : ↥s, f (↑i : ι)), 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)
        (∑ x : ↥s, { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) (f (↑x : ι)), continuous_toFun := ⋯ }) :
      A)

Tactic:
congr 1
-- 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
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (spectrum R a)
ha : p a
hsum : s.sum f = fun (z : R) ↦ ∑ i ∈ s, f i z
hf' : ContinuousOn (Y := R) (∑ i : ↥s, f (↑i : ι)) (spectrum R a)
pos :
  ∀ (a_1 : (↑(spectrum R a) : Type u_1)),
    Eq (α := R)
      (({ toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) (∑ i : ↥s, f (↑i : ι)), continuous_toFun := ⋯ :
              C((↑(spectrum R a) : Type u_1), R) } :
            (a : (↑(spectrum R a) : Type u_1)) → R)
          a_1 :
        R)
      ((∑ x : ↥s, { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) (f (↑x : ι)), continuous_toFun := ⋯ } :
            (a : (↑(spectrum R a) : Type u_1)) → R)
          a_1 :
        R)
⊢ { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) (∑ i : ↥s, f (↑i : ι)), continuous_toFun := ⋯ :
      C((↑(spectrum R a) : Type u_1), R) } =
    ∑ x : ↥s, { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) (f (↑x : ι)), continuous_toFun := ⋯ }

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
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (spectrum R a)
ha : p a
hsum : s.sum f = fun (z : R) ↦ ∑ i ∈ s, f i z
hf' : ContinuousOn (Y := R) (∑ i : ↥s, f (↑i : ι)) (spectrum R a)
a_1 : (↑(spectrum R a) : Type u_1)
⊢ Eq (α := R)
    (({ toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) (∑ i : ↥s, f (↑i : ι)), continuous_toFun := ⋯ :
            C((↑(spectrum R a) : Type u_1), R) } :
          (a : (↑(spectrum R a) : Type u_1)) → R)
        a_1 :
      R)
    ((∑ x : ↥s, { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) (f (↑x : ι)), continuous_toFun := ⋯ } :
          (a : (↑(spectrum R a) : Type u_1)) → R)
        a_1 :
      R)

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
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (spectrum R a)
ha : ¬p a
⊢ cfc.{u_1, u_2} (R := R) (p := p) (∑ i ∈ s, f i) a = ∑ i ∈ s, cfc (p := p) (f i) 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
ι : Type u_3
inst_9 : Fintype ι
f : ι → R → R
a : A
hf : ∀ (i : ι), ContinuousOn (f i) (spectrum R a)
⊢ cfc.{u_1, u_2} (R := R) (p := p) (∑ i : ι, f i) a = ∑ i : ι, cfc (p := p) (f i) a

Tactic:
cfc_sum f a _ fun i _ ↦ hf i

Premises used: cfc_sum
-- 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)
pos : ∀ (ha : p a), cfc (p := p) (fun (x : R) ↦ s • f x) a = s • cfc (p := p) f a
neg : ∀ (ha : ¬p a), cfc (p := p) (fun (x : R) ↦ s • f x) a = s • cfc (p := p) f a
⊢ cfc (p := p) (fun (x : R) ↦ s • f x) a = s • cfc (p := p) f a

Tactic:
by_cases ha : p 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
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) 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)
⊢ cfc (p := p) (fun (x : R) ↦ s • f x) a = s • cfc (p := p) f a

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

Premises used: cfc_apply