ProbabilityTheory.Kernel.condKernel_compProd_ae_eq

lemma condKernel_compProd_ae_eq    (κ : Kernel T S) [IsFiniteKernel κ]    (η : Kernel (T × S) U) [IsMarkovKernel η] (μ : Measure T) :    condKernel (κ ⊗ₖ η) =ᵐ[μ ⊗ₘ κ] η := by  rw [Filter.EventuallyEq, ae_iff_of_countable]  intro x hx  rw [condKernel_compProd_apply]  rw [Measure.compProd_apply (.singleton _), lintegral_eq_tsum] at hx  simp only [ne_eq, ENNReal.summable.tsum_eq_zero_iff, mul_eq_zero, not_forall] at hx  obtain ⟨y, hy⟩ := hx  push Not at hy  classical  rw [← Prod.eta x, ← Set.singleton_prod_singleton, Set.mk_preimage_prod_right_eq_if] at hy  simp only [ne_eq, Set.mem_singleton_iff] at hy  by_cases hyx1 : y = x.1  · simp only [hyx1, ite_true] at hy    exact hy.2  · simp [hyx1] at hy