no goals
α : Type u_1
β : Type ?u.888288
γ : Type ?u.888291
δ : Type ?u.888294
m✝ : MeasurableSpace α
μ✝ ν : Measure α
m : MeasurableSpace α
f : α →ₛ ℝ≥0∞
s : Set α
μ : Measure α
⊢ lintegral f (Measure.restrict μ s) = ∑ y in SimpleFunc.range f, y * ↑↑μ (↑f ⁻¹' {y} ∩ s)
simp only [lintegral, Measure.restrict_apply, f.measurableSet_preimage]