ProbabilityTheory.map_compProd_condDistrib

lemma map_compProd_condDistrib [Nonempty S] (hX : Measurable X) (hZ : Measurable Z)    (μ : Measure Ω) [IsProbabilityMeasure μ] :    μ.map Z ⊗ₘ condDistrib X Z μ = μ.map (fun ω ↦ (Z ω, X ω)) := by  ext A hA  rw [Measure.map_apply (hZ.prodMk hX) hA, Measure.compProd_apply hA, lintegral_eq_tsum]  have : ∑' x : U, μ.map Z {x} * condDistrib X Z μ x (Prod.mk x ⁻¹' A)      = ∑' x : U, μ (Z ⁻¹' {x} ∩ (fun ω ↦ (x, X ω)) ⁻¹' A) := by    congr 1 with x    rw [Measure.map_apply hZ (.singleton _)]    by_cases hx : μ (Z ⁻¹' {x}) = 0    · simp [hx, measure_mono_null Set.inter_subset_left hx]    rw [condDistrib_apply' hX hZ _ _ hx]    swap; · exact (measurable_prodMk_left hA)    rw [← mul_assoc, ENNReal.mul_inv_cancel hx (measure_ne_top _ _), one_mul]    congr  rw [this]  have : (fun a ↦ (Z a, X a)) ⁻¹' A = ⋃ x, Z ⁻¹' {x} ∩ ((fun a ↦ (x, X a)) ⁻¹' A) := by    ext ω    simp  rw [this, measure_iUnion]  · intro i j hij    rw [Function.onFun]    refine Disjoint.mono Set.inter_subset_left Set.inter_subset_left ?_    rw [Set.disjoint_iff]    intro z    simp only [Set.mem_inter_iff, Set.mem_preimage, Set.mem_singleton_iff, Set.mem_empty_iff_false,      and_imp]    exact fun hi hj ↦ hij (hi.symm.trans hj)  intro u  exact (hZ (.singleton _)).inter (measurable_const.prodMk hX hA)