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