nullMeasurableSet_le missing

Stream: mathlib4

[Terence Tao]

The analogue of docs#nullMeasurableSet_lt for le appears to be missing from Mathlib viz.,

import Mathlib

theorem nullMeasurableSet_le {α : Type*} {δ : Type*} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderClosedTopology α] [SecondCountableTopology α] {μ : MeasureTheory.Measure δ} {f : δ → α} {g : δ → α} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) : NullMeasurableSet { a | f a ≤ g a } μ :=
  (hf.prod_mk hg).nullMeasurable measurableSet_le'

[Oliver Nash]

Thanks, it's great to get reports of gaps like this. I've just created #10074 to plug this.

[Kevin Buzzard]

@Terence Tao feel free to review the PR (i.e. just make a comment saying "yes please I need this and the proofs look sensible" or something) -- you don't have to be a maintainer to review a PR (many people seem to be under this misconception so it's always worth occasionally trying to dispel it).