no goals
α : Type u_1
β : Type ?u.3498066
γ : Type ?u.3498069
δ : Type ?u.3498072
ι : Type ?u.3498075
R : Type ?u.3498078
R' : Type ?u.3498081
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : ↑↑(trim μ hm) s = 0
⊢ ↑↑(trim μ hm) (toMeasurable (trim μ hm) s) = 0
rwa [@measure_toMeasurable _ m]