no goals
α : Type u_1
β : Type ?u.1694799
γ : Type ?u.1694802
δ : Type ?u.1694805
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
c : ℝ≥0∞
⊢ (∑' (x : α), c) = c * ↑↑count univ
rw [← lintegral_count, lintegral_const]