ProbabilityTheory.swap_condDistrib_ae_eq

lemma swap_condDistrib_ae_eq (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z)    (μ : Measure Ω) [IsFiniteMeasure μ] :    Kernel.comap (condDistrib Y (fun a ↦ (X a, Z a)) μ) Prod.swap measurable_swap      =ᵐ[μ.map (fun ω ↦ (Z ω, X ω))] condDistrib Y (fun ω ↦ (Z ω, X ω)) μ := by  rw [Filter.EventuallyEq, ae_iff_of_countable]  intro x hx  ext A hA  rw [Kernel.comap_apply']  have h_swap : (fun a ↦ (X a, Z a)) ⁻¹' {Prod.swap x} = (fun a ↦ (Z a, X a)) ⁻¹' {x} := by    ext ω    simp only [Set.mem_preimage, Set.mem_singleton_iff]    rw [← Prod.eta x, Prod.swap_prod_mk, Prod.mk_inj, Prod.mk_inj, and_comm]  rw [condDistrib_apply' hY (hX.prodMk hZ) _ _ _ hA]  swap; · rwa [Measure.map_apply (hZ.prodMk hX) (.singleton _), ← h_swap] at hx  rw [condDistrib_apply' hY (hZ.prodMk hX) _ _ _ hA]  swap; · rwa [Measure.map_apply (hZ.prodMk hX) (.singleton _)] at hx  rw [h_swap]