no goals
α : Type u_1
β : Type u_2
γ : Type ?u.1222190
δ : Type ?u.1222193
ι : Type ?u.1222196
R : Type ?u.1222199
R' : Type ?u.1222202
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : MeasureTheory.Measure α
s t : Set β
ht : MeasurableSet t
⊢ ↑↑(Measure.restrict (Measure.map f μ) s) t = ↑↑(Measure.map f (Measure.restrict μ (f ⁻¹' s))) t
simp [hf.map_apply, ht, hf.measurable ht]