-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
lemma cfcₙ_sum {ι : Type*} (f : ι → R → R) (a : A) (s : Finset ι)
    (hf : ∀ i ∈ s, ContinuousOn (f i) (σₙ R a)

Proof state:
case pos
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : autoParam (∀ i ∈ s, ContinuousOn (f i) (σₙ R a)) _auto✝
hf0 : autoParam (∀ i ∈ s, f i 0 = 0) _auto✝
ha : p a
hsum : s.sum f = fun z => ∑ i ∈ s, f i z
hf' : ContinuousOn (∑ i : { x // x ∈ s }, f ↑i) (σₙ R a)
⊢ (cfcₙHom ha) { toFun := (σₙ R a).restrict (∑ i : { x // x ∈ s }, f ↑i), continuous_toFun := ⋯, map_zero' := ⋯ } =
    (cfcₙHom ?m.491068)
      (∑ x : { x // x ∈ s }, { toFun := (σₙ R a).restrict (f ↑x), continuous_toFun := ⋯, map_zero' := ⋯ })

R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : autoParam (∀ i ∈ s, ContinuousOn (f i) (σₙ R a)) _auto✝
hf0 : autoParam (∀ i ∈ s, f i 0 = 0) _auto✝
ha : p a
hsum : s.sum f = fun z => ∑ i ∈ s, f i z
hf' : ContinuousOn (∑ i : { x // x ∈ s }, f ↑i) (σₙ 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✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : autoParam (∀ i ∈ s, ContinuousOn (f i) (σₙ R a)) _auto✝
hf0 : autoParam (∀ i ∈ s, f i 0 = 0) _auto✝
ha : p a
hsum : s.sum f = fun z => ∑ i ∈ s, f i z
hf' : ContinuousOn (∑ i : { x // x ∈ s }, f ↑i) (σₙ R a)
⊢ { toFun := (σₙ R a).restrict (∑ i : { x // x ∈ s }, f ↑i), continuous_toFun := ⋯, map_zero' := ⋯ } =
    ∑ x : { x // x ∈ s }, { toFun := (σₙ R a).restrict (f ↑x), continuous_toFun := ⋯, map_zero' := ⋯ }

Proof state:
case pos
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : autoParam (∀ i ∈ s, ContinuousOn (f i) (σₙ R a)) _auto✝
hf0 : autoParam (∀ i ∈ s, f i 0 = 0) _auto✝
ha : p a
⊢ cfcₙ (∑ i ∈ s, f i) a = ∑ i ∈ s, cfcₙ (f i) a

Tactic:
have hsum : s.sum f = fun z => ∑ i ∈ s, f i z := by ext; simp

Result:
case pos
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : autoParam (∀ i ∈ s, ContinuousOn (f i) (σₙ R a)) _auto✝
hf0 : autoParam (∀ i ∈ s, f i 0 = 0) _auto✝
ha : p a
hsum : s.sum f = fun z => ∑ i ∈ s, f i z
⊢ cfcₙ (∑ i ∈ s, f i) a = ∑ i ∈ s, cfcₙ (f i) a

Proof state:
case neg
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : autoParam (∀ i ∈ s, ContinuousOn (f i) (σₙ R a)) _auto✝
hf0 : autoParam (∀ i ∈ s, f i 0 = 0) _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