no goals
α : Type u_1
β : Type ?u.925545
γ : Type ?u.925548
δ : Type ?u.925551
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
⊢ (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
rw [Measure.restrict_univ]