no goals
α : Type u_1
β : Type ?u.1494574
E : Type u_2
F : Type ?u.1494580
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
⊢ IntegrableOn f univ ↔ Integrable f
rw [IntegrableOn, Measure.restrict_univ]