∀ {Ω : Type u_1} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [inst : StandardBorelSpace Ω]
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {s : Set Ω},
  MeasurableSet s → Measurable fun ω => ((ProbabilityTheory.condExpKernel μ m) ω) s