∀ {Ω : Type u_1} {E : Type u_2} [inst : MeasurableSpace E] {m : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω}
  {μ : MeasureTheory.Measure E} [MeasureTheory.SigmaFinite μ] {X : Ω → E} [MeasureTheory.HasPDF X ℙ μ]
  (f : E → ENNReal),
  AEMeasurable f μ → (MeasureTheory.Measure.map X ℙ = μ.withDensity f ↔ MeasureTheory.pdf X ℙ μ =ᵐ[μ] f)