∀ {α : Type u_1} {Ω : Type u_3} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω] [inst_2 : Nonempty Ω]
  {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst_3 : MeasureTheory.IsFiniteMeasure μ] (Y : α → Ω),
  ⇑(ProbabilityTheory.condDistrib Y Y μ) =ᵐ[MeasureTheory.Measure.map Y μ] ⇑ProbabilityTheory.Kernel.id