∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {κ : ProbabilityTheory.Kernel Ω 𝓧}
  {μ : MeasureTheory.Measure Ω} [inst : MeasureTheory.IsFiniteMeasure μ] [inst_1 : ProbabilityTheory.IsFiniteKernel κ]
  [inst_2 : StandardBorelSpace Ω] [inst_3 : Nonempty Ω] [inst_4 : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧],
  (∀ᵐ (ω : Ω) ∂μ, (κ ω).AbsolutelyContinuous (μ.bind ⇑κ)) →
    ∀ᵐ (p : Ω × 𝓧) ∂μ.prod (μ.bind ⇑κ),
      (ProbabilityTheory.posterior κ μ).rnDeriv (ProbabilityTheory.Kernel.const 𝓧 μ) p.2 p.1 =
        κ.rnDeriv (ProbabilityTheory.Kernel.const Ω (μ.bind ⇑κ)) p.1 p.2