ProbabilityTheory.Kernel.condKernel_compProd_apply'

lemma condKernel_compProd_apply' (κ : Kernel T S) [IsFiniteKernel κ]    (η : Kernel (T × S) U) [IsMarkovKernel η]    (x : T × S) (hx : κ x.1 {x.2} ≠ 0) {s : Set U} (hs : MeasurableSet s) :    condKernel (κ ⊗ₖ η) x s = η x s := by  have hx' : (κ ⊗ₖ η) x.1 (Prod.fst ⁻¹' {x.2}) ≠ 0 := by    rwa [compProd_preimage_fst (.singleton _)]  rw [condKernel_apply' _ _ hx', compProd_apply ((measurableSet_singleton _).prod hs),    Kernel.compProd_apply, lintegral_eq_single _ x.2, lintegral_eq_single _ x.2]  · simp [Set.preimage_preimage, mul_comm]    simp [← mul_assoc, ENNReal.inv_mul_cancel hx (measure_ne_top (κ x.1) {x.2})]  · intro b hb    rw [Set.eq_empty_of_forall_notMem (s := _ ⁻¹' _) (by simp [hb]), measure_empty]  · intro b hb    simp [hb, Set.preimage_preimage]  · measurability