-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma cfc_sum {ι : Type*} (f : ι → R → R) (a : A) (s : Finset ι)
    (hf : ∀ i ∈ s, ContinuousOn (f i) (spectrum R a)

Proof state:
case pos
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : autoParam (∀ i ∈ s, ContinuousOn (f i) (spectrum R a)) _auto✝
ha : p a
hsum : s.sum f = fun z => ∑ i ∈ s, f i z
hf' : ContinuousOn (∑ i : { x // x ∈ s }, f ↑i) (spectrum R a)
⊢ (cfcHom ha) { toFun := (spectrum R a).restrict (∑ i : { x // x ∈ s }, f ↑i), continuous_toFun := ⋯ } =
    (cfcHom ?m.260115) (∑ x : { x // x ∈ s }, { toFun := (spectrum R a).restrict (f ↑x), continuous_toFun := ⋯ })

R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : autoParam (∀ i ∈ s, ContinuousOn (f i) (spectrum R a)) _auto✝
ha : p a
hsum : s.sum f = fun z => ∑ i ∈ s, f i z
hf' : ContinuousOn (∑ i : { x // x ∈ s }, f ↑i) (spectrum R a)
⊢ p a

Tactic:
congr 1

Result:
case pos.h.e_6.h
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : autoParam (∀ i ∈ s, ContinuousOn (f i) (spectrum R a)) _auto✝
ha : p a
hsum : s.sum f = fun z => ∑ i ∈ s, f i z
hf' : ContinuousOn (∑ i : { x // x ∈ s }, f ↑i) (spectrum R a)
⊢ { toFun := (spectrum R a).restrict (∑ i : { x // x ∈ s }, f ↑i), continuous_toFun := ⋯ } =
    ∑ x : { x // x ∈ s }, { toFun := (spectrum R a).restrict (f ↑x), continuous_toFun := ⋯ }

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : autoParam (∀ i ∈ s, ContinuousOn (f i) (spectrum R a)) _auto✝
ha : p a
⊢ s.sum f = fun z => ∑ i ∈ s, f i z

Tactic:
ext

Result:
case h
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : autoParam (∀ i ∈ s, ContinuousOn (f i) (spectrum R a)) _auto✝
ha : p a
x✝ : R
⊢ s.sum f x✝ = ∑ i ∈ s, f i x✝

Proof state:
case pos.h.e_6.h.h
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : autoParam (∀ i ∈ s, ContinuousOn (f i) (spectrum R a)) _auto✝
ha : p a
hsum : s.sum f = fun z => ∑ i ∈ s, f i z
hf' : ContinuousOn (∑ i : { x // x ∈ s }, f ↑i) (spectrum R a)
a✝ : ↑(spectrum R a)
⊢ { toFun := (spectrum R a).restrict (∑ i : { x // x ∈ s }, f ↑i), continuous_toFun := ⋯ } a✝ =
    (∑ x : { x // x ∈ s }, { toFun := (spectrum R a).restrict (f ↑x), continuous_toFun := ⋯ }) a✝

Tactic:
simp

Result:
no goals

Proof state:
case pos
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : autoParam (∀ i ∈ s, ContinuousOn (f i) (spectrum R a)) _auto✝
ha : p a
hsum : s.sum f = fun z => ∑ i ∈ s, f i z
hf' : ContinuousOn (∑ i : { x // x ∈ s }, f ↑i) (spectrum R a)
⊢ cfc (∑ i : { x // x ∈ s }, f ↑i) a = ∑ i : { x // x ∈ s }, cfc (f ↑i) a

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

Result:
case pos
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : autoParam (∀ i ∈ s, ContinuousOn (f i) (spectrum R a)) _auto✝
ha : p a
hsum : s.sum f = fun z => ∑ i ∈ s, f i z
hf' : ContinuousOn (∑ i : { x // x ∈ s }, f ↑i) (spectrum R a)
⊢ (cfcHom ha) { toFun := (spectrum R a).restrict (∑ i : { x // x ∈ s }, f ↑i), continuous_toFun := ⋯ } =
    (cfcHom ?m.260115) (∑ x : { x // x ∈ s }, { toFun := (spectrum R a).restrict (f ↑x), continuous_toFun := ⋯ })

R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : autoParam (∀ i ∈ s, ContinuousOn (f i) (spectrum R a)) _auto✝
ha : p a
hsum : s.sum f = fun z => ∑ i ∈ s, f i z
hf' : ContinuousOn (∑ i : { x // x ∈ s }, f ↑i) (spectrum R a)
⊢ p a

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : autoParam (∀ i ∈ s, ContinuousOn (f i) (spectrum R a)) _auto✝
ha : p a
hsum : s.sum f = fun z => ∑ i ∈ s, f i z
⊢ ContinuousOn (∑ i : { x // x ∈ s }, f ↑i) (spectrum R a)

Tactic:
rw [sum_coe_sort s, hsum]

Result:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : autoParam (∀ i ∈ s, ContinuousOn (f i) (spectrum R a)) _auto✝
ha : p a
hsum : s.sum f = fun z => ∑ i ∈ s, f i z
⊢ ContinuousOn (fun z => ∑ i ∈ s, f i z) (spectrum R a)

Proof state:
case neg
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : autoParam (∀ i ∈ s, ContinuousOn (f i) (spectrum R a)) _auto✝
ha : ¬p a
⊢ cfc (∑ i ∈ s, f i) a = ∑ i ∈ s, cfc (f i) a

Tactic:
simp [cfc_apply_of_not_predicate a ha]

Result:
no goals