case h
α : Type u_2
β : Type ?u.345987
γ : Type ?u.345990
δ : Type ?u.345993
ι : Type u_1
R : Type ?u.345999
R' : Type ?u.346002
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
s : Set ι
μ : ι → Measure α
t : Set α
ht : MeasurableSet t
⊢ ↑↑((sum fun i => μ ↑i) + sum fun i => μ ↑i) t = ↑↑(sum μ) t
α : Type u_2
β : Type ?u.345987
γ : Type ?u.345990
δ : Type ?u.345993
ι : Type u_1
R : Type ?u.345999
R' : Type ?u.346002
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
s : Set ι
μ : ι → Measure α
⊢ ((sum fun i => μ ↑i) + sum fun i => μ ↑i) = sum μ
ext1 t ht
case h
α : Type u_2
β : Type ?u.345987
γ : Type ?u.345990
δ : Type ?u.345993
ι : Type u_1
R : Type ?u.345999
R' : Type ?u.346002
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
s : Set ι
μ : ι → Measure α
t : Set α
ht : MeasurableSet t
⊢ ((∑' (i : ↑s), ↑↑(μ ↑i) t) + ∑' (i : ↑(sᶜ)), ↑↑(μ ↑i) t) = ∑' (i : ι), ↑↑(μ i) t
case h
α : Type u_2
β : Type ?u.345987
γ : Type ?u.345990
δ : Type ?u.345993
ι : Type u_1
R : Type ?u.345999
R' : Type ?u.346002
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
s : Set ι
μ : ι → Measure α
t : Set α
ht : MeasurableSet t
⊢ ↑↑((sum fun i => μ ↑i) + sum fun i => μ ↑i) t = ↑↑(sum μ) t
simp only [add_apply, sum_apply _ ht]
no goals
case h
α : Type u_2
β : Type ?u.345987
γ : Type ?u.345990
δ : Type ?u.345993
ι : Type u_1
R : Type ?u.345999
R' : Type ?u.346002
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
s : Set ι
μ : ι → Measure α
t : Set α
ht : MeasurableSet t
⊢ ((∑' (i : ↑s), ↑↑(μ ↑i) t) + ∑' (i : ↑(sᶜ)), ↑↑(μ ↑i) t) = ∑' (i : ι), ↑↑(μ i) t
exact @tsum_add_tsum_compl ℝ≥0∞ ι _ _ _ (fun i => μ i t) _ s ENNReal.summable ENNReal.summable