no goals
α : Type u_1
β : Type ?u.257361
E : Type u_2
F : Type ?u.257367
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
C : ℝ
hs : ↑↑μ s < ⊤
hsm : MeasurableSet s
hC : ∀ᵐ (x : α) ∂μ, x ∈ s → ‖f x‖ ≤ C
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ s, ‖f x‖ ≤ C
rwa [ae_restrict_eq hsm, eventually_inf_principal]