ProbabilityTheory.Kernel.FiniteKernelSupport.map

lemma FiniteKernelSupport.map [MeasurableSingletonClass U]    {κ : Kernel T S} (hκ : FiniteKernelSupport κ) (f : S → U) :    FiniteKernelSupport (map κ f) := by  by_cases hf : Measurable f  · intro t    rcases hκ t with ⟨A, hA⟩    classical    use Finset.image f A    rw [Kernel.map_apply' _ hf]    · refine measure_mono_null ?_ hA      intro s      simp only [Finset.coe_image, Set.preimage_compl, Set.mem_compl_iff, Set.mem_preimage,        Set.mem_image, SetLike.mem_coe, not_exists, not_and]      contrapose!; intro hs; use s    · apply MeasurableSet.compl      apply Set.Finite.measurableSet      exact Finset.finite_toSet (Finset.image f A)  · simp [map_of_not_measurable _ hf]