case h
α : Type u_2
β : Type ?u.341463
γ : Type ?u.341466
δ : Type ?u.341469
ι : Type u_1
R : Type ?u.341475
R' : Type ?u.341478
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : Fintype ι
μ : ι → Measure α
s : Set α
hs : MeasurableSet s
⊢ ↑↑(sum μ) s = ↑↑(∑ i : ι, μ i) s
α : Type u_2
β : Type ?u.341463
γ : Type ?u.341466
δ : Type ?u.341469
ι : Type u_1
R : Type ?u.341475
R' : Type ?u.341478
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : Fintype ι
μ : ι → Measure α
⊢ sum μ = ∑ i : ι, μ i
ext1 s hs
no goals
case h
α : Type u_2
β : Type ?u.341463
γ : Type ?u.341466
δ : Type ?u.341469
ι : Type u_1
R : Type ?u.341475
R' : Type ?u.341478
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : Fintype ι
μ : ι → Measure α
s : Set α
hs : MeasurableSet s
⊢ ↑↑(sum μ) s = ↑↑(∑ i : ι, μ i) s
simp only [sum_apply, finset_sum_apply, hs, tsum_fintype]