no goals
ι✝ : Type ?u.12645175
𝕜 : Type ?u.12645178
E : Type u_2
F : Type ?u.12645184
A : Type ?u.12645187
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b : ℝ
f✝ g : ℝ → E
μ : MeasureTheory.Measure ℝ
ι : Type u_1
s : Finset ι
f : ι → ℝ → E
h : ∀ (i : ι), i ∈ s → IntervalIntegrable (f i) μ a b
⊢ (∫ (x : ℝ) in a..b, ∑ i in s, f i x ∂μ) = ∑ i in s, ∫ (x : ℝ) in a..b, f i x ∂μ
simp only [intervalIntegral_eq_integral_uIoc, integral_finset_sum s fun i hi => (h i hi).def,
  Finset.smul_sum]