∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  AEMeasurable f μ →
    (∀ᵐ (x : α) ∂μ, f x ≠ 0) → (∀ᵐ (x : α) ∂μ, f x ≠ ⊤) → ((μ.withDensity f).withDensity fun x => (f x)⁻¹) = μ