case h
α : Type u_2
β : Type ?u.340429
γ : Type ?u.340432
δ : Type ?u.340435
ι : Type u_3
R : Type ?u.340441
R' : Type ?u.340444
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
ι' : Type u_1
μ : ι → ι' → Measure α
s : Set α
hs : MeasurableSet s
⊢ ↑↑(sum fun n => sum (μ n)) s = ↑↑(sum fun m => sum fun n => μ n m) s
α : Type u_2
β : Type ?u.340429
γ : Type ?u.340432
δ : Type ?u.340435
ι : Type u_3
R : Type ?u.340441
R' : Type ?u.340444
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
ι' : Type u_1
μ : ι → ι' → Measure α
⊢ (sum fun n => sum (μ n)) = sum fun m => sum fun n => μ n m
ext1 s hs
case h
α : Type u_2
β : Type ?u.340429
γ : Type ?u.340432
δ : Type ?u.340435
ι : Type u_3
R : Type ?u.340441
R' : Type ?u.340444
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
ι' : Type u_1
μ : ι → ι' → Measure α
s : Set α
hs : MeasurableSet s
⊢ (∑' (i : ι) (i_1 : ι'), ↑↑(μ i i_1) s) = ∑' (i : ι') (i_1 : ι), ↑↑(μ i_1 i) s
case h
α : Type u_2
β : Type ?u.340429
γ : Type ?u.340432
δ : Type ?u.340435
ι : Type u_3
R : Type ?u.340441
R' : Type ?u.340444
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
ι' : Type u_1
μ : ι → ι' → Measure α
s : Set α
hs : MeasurableSet s
⊢ ↑↑(sum fun n => sum (μ n)) s = ↑↑(sum fun m => sum fun n => μ n m) s
simp_rw [sum_apply _ hs]
no goals
case h
α : Type u_2
β : Type ?u.340429
γ : Type ?u.340432
δ : Type ?u.340435
ι : Type u_3
R : Type ?u.340441
R' : Type ?u.340444
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
ι' : Type u_1
μ : ι → ι' → Measure α
s : Set α
hs : MeasurableSet s
⊢ (∑' (i : ι) (i_1 : ι'), ↑↑(μ i i_1) s) = ∑' (i : ι') (i_1 : ι), ↑↑(μ i_1 i) s
rw [ENNReal.tsum_comm]