∀ {α : Type u_1} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) {R : Type u_3} [inst_1 : LinearOrder R]
  [inst_2 : MeasurableSpace R] (ν : MeasureTheory.Measure R) [MeasureTheory.NoAtoms ν] (g : α → R),
  (fun t => μ {a | t ≤ g a}) =ᵐ[ν] fun t => μ {a | t < g a}