∀ {β : Type u_2} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (α : Type u_6)
  [inst : MeasurableSpace α] (κ : ProbabilityTheory.Kernel β γ) (a : α),
  (ProbabilityTheory.Kernel.prodMkLeft α κ).sectR a = κ