no goals
α : Type u_1
β : Type ?u.897363
γ : Type ?u.897366
δ : Type ?u.897369
m : MeasurableSpace α
μ ν : Measure α
c : ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ lintegral (restrict (const α c) s) μ = c * ↑↑μ s
rw [restrict_lintegral_eq_lintegral_restrict _ hs, const_lintegral_restrict]