∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν κ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ]
  [MeasureTheory.SigmaFinite ν] [MeasureTheory.SigmaFinite κ],
  μ.AbsolutelyContinuous ν → μ.rnDeriv ν * ν.rnDeriv κ =ᵐ[κ] μ.rnDeriv κ