no goals
α✝ : Type ?u.268461
β : Type ?u.268464
E : Type u_2
F : Type ?u.268470
inst✝³ : MeasurableSpace α✝
inst✝² : NormedAddCommGroup E
f✝ g : α✝ → E
s✝ t : Set α✝
μ✝ ν : Measure α✝
l l' : Filter α✝
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → E
hf_meas : StronglyMeasurable f
s : Set α
hs : MeasurableSet s
⊢ (∫ (x : α) in s, f x ∂μ) = ∫ (x : α) in s, f x ∂Measure.trim μ hm
rwa [integral_trim hm hf_meas, restrict_trim hm μ]