no goals
α : Type u_1
β : Type ?u.889169
γ : Type ?u.889172
δ : Type ?u.889175
m : MeasurableSpace α
μ ν : Measure α
f : α →ₛ ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ lintegral (restrict f s) μ = lintegral f (Measure.restrict μ s)
rw [f.restrict_lintegral hs, lintegral_restrict]