ProbabilityTheory.Kernel.FiniteKernelSupport.compProd

lemma FiniteKernelSupport.compProd [MeasurableSingletonClass S] [MeasurableSingletonClass U]    {κ : Kernel T S} {η : Kernel (T × S) U}    (hκ : FiniteKernelSupport κ) (hη : FiniteKernelSupport η) :    FiniteKernelSupport (κ ⊗ₖ η) := by  by_cases hκ' : IsSFiniteKernel κ; swap  · simp [compProd_of_not_isSFiniteKernel_left _ _ hκ']  by_cases hη' : IsSFiniteKernel η; swap  · simp [compProd_of_not_isSFiniteKernel_right _ _ hη']  intro t  rcases hκ t with ⟨A, hA⟩  rcases (local_support_of_finiteKernelSupport hη ({t} ×ˢ A)) with ⟨B, hB⟩  use A ×ˢ B  rw [Kernel.compProd_apply (by measurability), lintegral_eq_setLIntegral hA,    setLIntegral_eq_sum]  apply Finset.sum_eq_zero  intro s hs  simp only [Finset.coe_product, Set.preimage_compl, mul_eq_zero]  right  refine measure_mono_null ?_ (hB (t, s) (by simp [hs]))  intro u; simp; tauto