no goals
α : Type u_1
β : Type ?u.1430585
γ : Type ?u.1430588
δ : Type ?u.1430591
ι : Type ?u.1430594
R : Type ?u.1430597
R' : Type ?u.1430600
m0 : MeasurableSpace α
s : Set α
hs : MeasurableSet s
μ : MeasureTheory.Measure α
⊢ Measure.map Subtype.val (Measure.comap Subtype.val μ) = Measure.restrict μ s
rw [(MeasurableEmbedding.subtype_coe hs).map_comap, Subtype.range_coe]