no goals
α : Type u_1
β : Type ?u.3496438
γ : Type ?u.3496441
δ : Type ?u.3496444
ι : Type ?u.3496447
R : Type ?u.3496450
R' : Type ?u.3496453
m m0 : MeasurableSpace α
μ✝ : Measure α
s : Set α
μ : Measure α
hm : m ≤ m0
⊢ ↑(trim μ hm) = OuterMeasure.trim ↑μ
rw [Measure.trim, toMeasure_toOuterMeasure (ms := m)]