∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} {κ η ξ : ProbabilityTheory.Kernel α γ}
  {f : α → γ → ENNReal} [inst : ProbabilityTheory.IsFiniteKernel η],
  κ = η.withDensity f + ξ →
    Measurable (Function.uncurry f) → ∀ (a : α), (ξ a).MutuallySingular (η a) → f a =ᵐ[η a] (κ a).rnDeriv (η a)