no goals
α : Type u_1
β : Type ?u.1818394
γ : Type ?u.1818397
δ : Type ?u.1818400
ι : Type ?u.1818403
R : Type ?u.1818406
R' : Type ?u.1818409
inst✝ : MeasureSpace α
s✝ t s : Set α
hs : MeasurableSet s
⊢ Measure.map Subtype.val volume = Measure.restrict volume s
rw [volume_set_coe_def, (MeasurableEmbedding.subtype_coe hs).map_comap volume, Subtype.range_coe]