ProbabilityTheory.condDistrib_const_unit

lemma condDistrib_const_unit (hX : Measurable X) (hY : Measurable Y)    (μ : Measure Ω) [IsFiniteMeasure μ] :    Kernel.condKernel (Kernel.const Unit (μ.map (fun ω ↦ (X ω, Y ω))))      =ᵐ[μ.map (fun ω ↦ ((), X ω))] Kernel.prodMkLeft Unit (condDistrib Y X μ) := by  rw [Filter.EventuallyEq, ae_iff_of_countable]  intro x hx  have : (fun a ↦ ((), X a)) ⁻¹' {x} = X ⁻¹' {x.2} := by    ext ω    simp only [Set.mem_preimage, Set.mem_singleton_iff]    rw [← Prod.eta x, Prod.mk_inj]    simp  rw [Measure.map_apply (measurable_const.prodMk hX) (.singleton _), this] at hx  ext s hs  rw [Kernel.condKernel_apply']  swap  · rw [Kernel.const_apply,      Measure.map_apply (hX.prodMk hY) (measurable_fst (.singleton _))]    exact hx  simp_rw [Kernel.const_apply,    Measure.map_apply (hX.prodMk hY) (measurable_fst (.singleton _)),    Measure.map_apply (hX.prodMk hY) ((measurableSet_singleton _).prod hs)]  rw [Kernel.prodMkLeft_apply', condDistrib_apply' hY hX _ _ hx hs]  rfl