no goals
α : Type u_1
β : Type u_2
γ : Type ?u.305334
δ : Type ?u.305337
ι : Type ?u.305340
R : Type ?u.305343
R' : Type ?u.305346
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
t : Set β
ht : MeasurableSet t
⊢ ↑↑(restrict (map f μ) s) t = ↑↑(map f (restrict μ (f ⁻¹' s))) t
simp [*, hf ht]