no goals
α : Type u_1
β : Type ?u.122815
γ : Type ?u.122818
δ : Type ?u.122821
ι : Type u_2
R : Type ?u.122827
R' : Type ?u.122830
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
m : MeasurableSpace α
I : Finset ι
μ : ι → Measure α
s : Set α
⊢ ↑↑(∑ i in I, μ i) s = ∑ i in I, ↑↑(μ i) s
rw [coe_finset_sum, Finset.sum_apply]