no goals
α : Type u_1
β : Type ?u.1733020
γ : Type ?u.1733023
δ : Type ?u.1733026
m : MeasurableSpace α
μ ν : Measure α
inst✝ : MeasurableSingletonClass α
s : Finset α
f : α → ℝ≥0∞
⊢ (∫⁻ (x : α) in ↑s, f x ∂μ) = ∑ x in s, f x * ↑↑μ {x}
simp only [lintegral_countable _ s.countable_toSet, ← Finset.tsum_subtype']