∀ {α : Type u_1} {β : Type u_2} {s : Set α} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (f : α → β)
  (μ : MeasureTheory.Measure β),
  MeasureTheory.NullMeasurableSet s (MeasureTheory.Measure.comap f μ) → (MeasureTheory.Measure.comap f μ) s ≤ μ (f '' s)