no goals
α : Type u_1
β : Type ?u.3496903
γ : Type ?u.3496906
δ : Type ?u.3496909
ι : Type ?u.3496912
R : Type ?u.3496915
R' : Type ?u.3496918
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
⊢ ↑↑(trim μ hm) s = ↑↑μ s
rw [Measure.trim, toMeasure_apply (ms := m) _ _ hs]