no goals
α : Type u_2
β : Type ?u.342451
γ : Type ?u.342454
δ : Type ?u.342457
ι : Type u_1
R : Type ?u.342463
R' : Type ?u.342466
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
s : Finset ι
μ : ι → Measure α
⊢ (sum fun i => μ ↑i) = ∑ i in s, μ i
rw [sum_fintype, Finset.sum_coe_sort s μ]