no goals
α : Type u_1
β : Type ?u.918292
γ : Type ?u.918295
δ : Type ?u.918298
m✝ : MeasurableSpace α
μ✝ ν✝ : Measure α
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
⊢ (∫⁻ (a : α), f a ∂μ + ν) = (∫⁻ (a : α), f a ∂μ) + ∫⁻ (a : α), f a ∂ν
simpa [tsum_fintype] using lintegral_sum_measure f fun b => cond b μ ν