no goals
α : Type u_1
β : Type u_2
γ : Type ?u.216218
δ : Type ?u.216221
ι : Type ?u.216224
R : Type ?u.216227
R' : Type ?u.216230
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
f : α → β
h : μ ≤ ν
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ ↑↑(map f μ) s ≤ ↑↑(map f ν) s
simp [hf.aemeasurable, hs, h _ (hf hs)]