no goals
ι : Type ?u.4971036
α : Type u_1
β : Type ?u.4971042
γ : Type ?u.4971045
δ : Type u_2
R : Type ?u.4971051
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f✝ g : α → β
μ ν : Measure α
inst✝ : Zero β
f : α → δ
h : μ ≤ ν
hf : AEMeasurable f
s : Set δ
hs : MeasurableSet s
⊢ ↑↑(map f μ) s ≤ ↑↑(map f ν) s
simpa [hf, hs, hf.mono_measure h] using Measure.le_iff'.1 h (f ⁻¹' s)