∀ {α : Type u_1} {m : MeasurableSpace α} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {μ ν : MeasureTheory.Measure α} [μ.HaveLebesgueDecomposition ν] [MeasureTheory.SigmaFinite μ] {f : α → E},
  μ.AbsolutelyContinuous ν →
    MeasureTheory.Integrable f μ → (ν.withDensityᵥ fun x => (μ.rnDeriv ν x).toReal • f x) = μ.withDensityᵥ f