Tagging lemmas in NullMeasurable with @[measurability]

Stream: mathlib4

[Luigi Massacci]

Is there any particular reason why none of the lemmas in docs#MeasureTheory.NullMeasurable are ever tagged with [measurability]? (though some are simp lemmas). I found myself proving some statements by doing just: apply simple_lemma_in_NullMeasurable; measurability. It's technically not in the description of measurability, but is seems like it could be within its scope, if I understand how the latter works correctly. Was this tried and it didn't work out?