no goals
α : Type u_1
β : Type ?u.897125
γ : Type ?u.897128
δ : Type ?u.897131
m : MeasurableSpace α
μ ν : Measure α
c : ℝ≥0∞
s : Set α
⊢ lintegral (const α c) (Measure.restrict μ s) = c * ↑↑μ s
rw [const_lintegral, Measure.restrict_apply MeasurableSet.univ, univ_inter]