∀ {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} {Y : Ω → ENNReal} (hm : mΩ ≤ mΩ₀) {P : MeasureTheory.Measure Ω}
  [hσ : MeasureTheory.SigmaFinite (P.trim hm)] (X : Ω → ENNReal),
  AEMeasurable Y (P.trim hm) →
    (∀ (s : Set Ω), MeasurableSet s → ∫⁻ (ω : Ω) in s, Y ω ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P) → Y =ᵐ[P] P⁻[X|mΩ]