ProbabilityTheory.Kernel.disintegration

lemma disintegration (κ : Kernel T (S × U)) [IsFiniteKernel κ] :    κ = (Kernel.fst κ) ⊗ₖ (condKernel κ) := by  ext x s hs  rw [compProd_apply hs, lintegral_fst]  swap; · exact measurable_kernel_prodMk_left' hs x  rw [lintegral_eq_tsum, ENNReal.tsum_prod']  change κ x s = ∑' a : S, ∑' b : U, κ x {(a, b)} * condKernel κ (x, a) (Prod.mk a ⁻¹' s)  simp_rw [ENNReal.tsum_mul_right, ← measure_preimage_fst_singleton_eq_tsum (κ x)]  have : ∑' a : S, (κ x (Prod.fst ⁻¹' {a})) * condKernel κ (x, a) (Prod.mk a ⁻¹' s)      = ∑' a : S, κ x (Prod.fst ⁻¹' {a} ∩ {su | (a, su.2) ∈ s}) := by    congr with a    by_cases ha : κ x (Prod.fst ⁻¹' {a}) = 0    · simp only [ha, zero_mul]      exact (measure_mono_null Set.inter_subset_left ha).symm    · rw [condKernel_apply' κ _ ha, ← mul_assoc,      ENNReal.mul_inv_cancel ha (measure_ne_top _ _), one_mul]      congr  simp_rw [this]  have : ⋃ a, Prod.fst ⁻¹' {a} ∩ {su | (a, su.2) ∈ s} = s := by ext a; simp  conv_lhs => rw [← this]  rw [measure_iUnion]  · intro a a' haa'    rw [Function.onFun, Set.disjoint_iff]    intro su    simp only [Set.mem_inter_iff, Set.mem_preimage, Set.mem_singleton_iff, Set.mem_setOf_eq,      Set.mem_empty_iff_false, and_imp]    intro h1 _ h1' _    exact haa' (h1.symm.trans h1')  · refine fun _ ↦ (measurable_fst (.singleton _)).inter ?_    exact measurable_prodMk_left.comp measurable_snd hs