∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set ↑s},
  MeasureTheory.NullMeasurableSet s μ → MeasurableSet t → MeasureTheory.NullMeasurableSet (Subtype.val '' t) μ