no goals
α : Type u_1
β : Type ?u.3496189
γ : Type ?u.3496192
δ : Type ?u.3496195
ι : Type ?u.3496198
R : Type ?u.3496201
R' : Type ?u.3496204
inst✝ : MeasurableSpace α
μ : Measure α
⊢ trim μ (_ : inst✝ ≤ inst✝) = μ
simp [Measure.trim]