no goals
α : Type u_3
β : Type u_2
γ : Type ?u.948084
δ : Type ?u.948087
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
ι : Type u_1
s : Finset ι
f : ι → α → β
hf : ∀ (i : ι), i ∈ s → Integrable (f i)
⊢ Integrable fun a => ∑ i in s, f i a
simpa only [← Finset.sum_apply] using integrable_finset_sum' s hf