∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (γ : Type u_5)
  [inst : MeasurableSpace γ] (κ : ProbabilityTheory.Kernel α β),
  ProbabilityTheory.Kernel.prodMkRight γ κ = κ.comap Prod.fst ⋯