ProbabilityTheory.condKernel_condDistrib_ae_eq

lemma condKernel_condDistrib_ae_eq [Nonempty S]    (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (μ : Measure Ω)    [IsFiniteMeasure μ] :  Kernel.condKernel (condDistrib (fun a ↦ (X a, Y a)) Z μ) =ᵐ[μ.map (fun ω ↦ (Z ω, X ω))]    condDistrib Y (fun ω ↦ (Z ω, X ω)) μ := by  rw [Filter.EventuallyEq, ae_iff_of_countable]  intro x hx  rw [Measure.map_apply (hZ.prodMk hX) (.singleton _)] at hx  ext A hA  have hx1 : μ (Z ⁻¹' {x.1}) ≠ 0 := by    refine fun h_null ↦ hx (measure_mono_null ?_ h_null)    intro ω hω    simp only [Set.mem_preimage, Set.mem_singleton_iff] at hω ⊢    rw [← Prod.eta x, Prod.mk_inj] at hω    exact hω.1  rw [Kernel.condKernel_apply']  swap  · rw [condDistrib_apply' (hX.prodMk hY) hZ _ _ hx1]    swap    · exact measurable_fst (.singleton _)    simp only [ne_eq, mul_eq_zero, ENNReal.inv_eq_zero, measure_ne_top μ, false_or]    convert hx    ext ω    simp only [Set.mem_inter_iff, Set.mem_preimage, Set.mem_singleton_iff]    conv_rhs => rw [← Prod.eta x]    exact Prod.mk_inj.symm  rw [condDistrib_apply' (hX.prodMk hY) hZ _ _ hx1]  swap  · exact measurable_fst (.singleton _)  rw [condDistrib_apply' (hX.prodMk hY) hZ _ _ hx1]  swap  · exact (measurable_fst (.singleton _)).inter (measurable_snd hA)  rw [condDistrib_apply' hY (hZ.prodMk hX) _ _ hx hA]  have : (fun a ↦ (X a, Y a)) ⁻¹' (Prod.fst ⁻¹' {x.2}) = X ⁻¹' {x.2} := by rfl  simp_rw [this]  have : (fun a ↦ (X a, Y a)) ⁻¹' ({x.2} ×ˢ A) = X ⁻¹' {x.2} ∩ Y ⁻¹' A := by    ext y;    simp only [Set.singleton_prod, Set.mem_preimage, Set.mem_image, Prod.mk.injEq,      exists_eq_right_right, Set.mem_inter_iff, Set.mem_singleton_iff]    tauto  simp_rw [this]  have : (fun a ↦ (Z a, X a)) ⁻¹' {x} = Z ⁻¹' {x.1} ∩ X ⁻¹' {x.2} := by    ext y    simp only [Set.mem_preimage, Set.mem_singleton_iff, Set.mem_inter_iff]    conv_lhs => rw [← Prod.eta x, Prod.mk_inj]  rw [this, ENNReal.mul_inv (Or.inr (measure_ne_top _ _)), inv_inv]  swap; · left; simp [hx1]  calc (μ (Z ⁻¹' {x.1})) * (μ (Z ⁻¹' {x.1} ∩ X ⁻¹' {x.2}))⁻¹ *      ((μ (Z ⁻¹' {x.1}))⁻¹ * μ (Z ⁻¹' {x.1} ∩ (X ⁻¹' {x.2} ∩ Y ⁻¹' A)))    = (μ (Z ⁻¹' {x.1})) * (μ (Z ⁻¹' {x.1}))⁻¹ * (μ (Z ⁻¹' {x.1} ∩ X ⁻¹' {x.2}))⁻¹ *      μ (Z ⁻¹' {x.1} ∩ (X ⁻¹' {x.2} ∩ Y ⁻¹' A)) := by        ring  _ = (μ (Z ⁻¹' {x.1} ∩ X ⁻¹' {x.2}))⁻¹ * μ (Z ⁻¹' {x.1} ∩ X ⁻¹' {x.2} ∩ Y ⁻¹' A) := by        rw [ENNReal.mul_inv_cancel hx1 (measure_ne_top _ _), one_mul, Set.inter_assoc]