ProbabilityTheory.Kernel.aefiniteKernelSupport_of_cond

lemma aefiniteKernelSupport_of_cond {κ : Kernel T (S × U)} [hU : Nonempty U]    [MeasurableSingletonClass S] [MeasurableSingletonClass T]    [MeasurableSingletonClass U] [Countable U] [Countable S] [Countable T]    (μ : Measure T) (hκ : AEFiniteKernelSupport κ μ) [IsFiniteKernel κ] :    AEFiniteKernelSupport (condKernel κ) (μ ⊗ₘ (Kernel.fst κ)) := by  rw [AEFiniteKernelSupport, ae_iff_of_countable] at hκ ⊢  intro (t, s) hts  simp only [compProd_apply_singleton, ne_eq, mul_eq_zero, not_or] at hts  push Not at hts  rcases hκ t hts.2 with ⟨A, hA⟩  classical  use Finset.image Prod.snd A  rw [condKernel_apply']; swap  · rw [Kernel.fst_apply' _ _ (.singleton _)] at hts    exact hts.1  simp only [Finset.coe_image, Set.singleton_prod, mul_eq_zero, ENNReal.inv_eq_zero]  right  refine measure_mono_null ?_ hA  intro x  simp only [Set.mem_image, Set.mem_compl_iff, Finset.mem_coe, Prod.exists, exists_eq_right,    not_exists, forall_exists_index, and_imp]  intro y h hsyx  rw [← hsyx]  exact h s