no goals
α : Type u_1
β : Type ?u.952854
γ : Type ?u.952857
δ : Type ?u.952860
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
c : ℝ≥0∞
⊢ (∫⁻ (a : α), indicator s (fun x => c) a ∂μ) = c * ↑↑μ s
rw [lintegral_indicator _ hs, set_lintegral_const]