no goals
α : Type u_1
β : Type ?u.75567
γ : Type ?u.75570
δ : Type ?u.75573
m : MeasurableSpace α
μ ν : Measure α
s : Set α
c : ℝ≥0∞
⊢ (∫⁻ (x : α) in s, c ∂μ) = c * ↑↑μ s
rw [lintegral_const, Measure.restrict_apply_univ]