∀ {α : Type u_1} {mα : MeasurableSpace α} {γ : Type u_4} {mγ : MeasurableSpace γ} (β : Type u_6)
  [inst : MeasurableSpace β] (κ : ProbabilityTheory.Kernel α γ) (b : β),
  (ProbabilityTheory.Kernel.prodMkRight β κ).sectL b = κ