∀ {α : Type u_1} {mα : MeasurableSpace α} (Ω : Type u_5) [inst : Nonempty Ω] [inst_1 : MeasurableSpace Ω]
  [inst_2 : StandardBorelSpace Ω] (η : ProbabilityTheory.Kernel α ℝ) (a : α),
  (ProbabilityTheory.Kernel.borelMarkovFromReal Ω η) a =
    if (η a) (Set.range (MeasureTheory.embeddingReal Ω))ᶜ = 0 then
      MeasureTheory.Measure.comap (MeasureTheory.embeddingReal Ω) (η a)
    else MeasureTheory.Measure.comap (MeasureTheory.embeddingReal Ω) (MeasureTheory.Measure.dirac (Exists.choose ⋯))