no goals
α : Type u_1
β : Type u_2
γ : Type ?u.398294
δ : Type ?u.398297
ι : Type ?u.398300
R : Type ?u.398303
R' : Type ?u.398306
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
h : μ ≪ ν
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ ↑↑(map f ν) s = 0 → ↑↑(map f μ) s = 0
simpa [hf, hs] using @h _