no goals
α : Type u_2
β : Type ?u.1492993
E : Type u_1
F : Type ?u.1492999
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
s : Set α
μ : Measure α
C : ℝ
hs : ↑↑μ s < ⊤
hf : ∀ᵐ (x : α) ∂Measure.restrict μ s, ‖f x‖ ≤ C
⊢ ↑↑(Measure.restrict μ s) univ < ⊤
rwa [Measure.restrict_apply_univ]