feat: add lemmas nullMeasurableSet_lt' and nullMeasurableSet_le (#10074)

Prior to this commit the state of Mathlib was:
```lean
import Mathlib

#check measurableSet_lt  -- Exists
#check measurableSet_lt' -- Exists
#check measurableSet_le  -- Exists

#check nullMeasurableSet_lt  -- Exists
#check nullMeasurableSet_lt' -- Missing
#check nullMeasurableSet_le  -- Missing
```

Co-authored-by: teorth <tao@math.ucla.edu>

Author: ocfnash

Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

@@ -643,6 +643,15 @@ theorem nullMeasurableSet_lt [SecondCountableTopology α] {μ : Measure δ} {f g
   (hf.prod_mk hg).nullMeasurable measurableSet_lt'
 #align null_measurable_set_lt nullMeasurableSet_lt
 
+theorem nullMeasurableSet_lt' [SecondCountableTopology α] {μ : Measure (α × α)} :
+    NullMeasurableSet { p : α × α | p.1 < p.2 } μ :=
+  measurableSet_lt'.nullMeasurableSet
+
+theorem nullMeasurableSet_le [SecondCountableTopology α] {μ : Measure δ}
+    {f g : δ → α} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
+    NullMeasurableSet { a | f a ≤ g a } μ :=
+  (hf.prod_mk hg).nullMeasurable measurableSet_le'
+
 theorem Set.OrdConnected.measurableSet (h : OrdConnected s) : MeasurableSet s := by
   let u := ⋃ (x ∈ s) (y ∈ s), Ioo x y
   have huopen : IsOpen u := isOpen_biUnion fun _ _ => isOpen_biUnion fun _ _ => isOpen_Ioo