no goals
α : Type u_2
β : Type ?u.33095
E : Type u_1
F : Type ?u.33101
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
⊢ (∫ (x : α) in univ, f x ∂μ) = ∫ (x : α), f x ∂μ
rw [Measure.restrict_univ]