∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → ENNReal} (μ ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ]
  [MeasureTheory.SigmaFinite ν],
  AEMeasurable f ν →
    (∀ᵐ (x : α) ∂ν, f x ≠ 0) →
      (∀ᵐ (x : α) ∂ν, f x ≠ ⊤) →
        (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᵐ[ν] μ.rnDeriv (ν.withDensity f)