no goals
α : Type u_1
β : Type ?u.336860
γ : Type ?u.336863
δ : Type ?u.336866
ι : Type u_2
R : Type ?u.336872
R' : Type ?u.336875
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μ : ι → Measure α
i : ι
s : Set α
hs : MeasurableSet s
⊢ ↑↑(μ i) s ≤ ↑↑(sum μ) s
simpa only [sum_apply μ hs] using ENNReal.le_tsum i