case h
α : Type u_1
β : Type ?u.347212
γ : Type ?u.347215
δ : Type ?u.347218
ι : Type ?u.347221
R : Type ?u.347224
R' : Type ?u.347227
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν✝ ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μ ν : ℕ → Measure α
s : Set α
hs : MeasurableSet s
⊢ ↑↑(sum μ + sum ν) s = ↑↑(sum fun n => μ n + ν n) s
α : Type u_1
β : Type ?u.347212
γ : Type ?u.347215
δ : Type ?u.347218
ι : Type ?u.347221
R : Type ?u.347224
R' : Type ?u.347227
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν✝ ν' ν₁ ν₂ : Measure α
s s' t : Set α
μ ν : ℕ → Measure α
⊢ sum μ + sum ν = sum fun n => μ n + ν n
ext1 s hs
no goals
case h
α : Type u_1
β : Type ?u.347212
γ : Type ?u.347215
δ : Type ?u.347218
ι : Type ?u.347221
R : Type ?u.347224
R' : Type ?u.347227
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν✝ ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μ ν : ℕ → Measure α
s : Set α
hs : MeasurableSet s
⊢ ↑↑(sum μ + sum ν) s = ↑↑(sum fun n => μ n + ν n) s
simp only [add_apply, sum_apply _ hs, Pi.add_apply, coe_add,
  tsum_add ENNReal.summable ENNReal.summable]