no goals
α : Type u_1
β : Type ?u.3496586
γ : Type ?u.3496589
δ : Type ?u.3496592
ι : Type ?u.3496595
R : Type ?u.3496598
R' : Type ?u.3496601
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
⊢ trim 0 hm = 0
simp [Measure.trim, @OuterMeasure.toMeasure_zero _ m]