ProbabilityTheory.Kernel.AEFiniteKernelSupport.map

lemma AEFiniteKernelSupport.map [MeasurableSingletonClass U] {κ : Kernel T S} {μ : Measure T}    (hκ : AEFiniteKernelSupport κ μ) {f : S → U} :    AEFiniteKernelSupport (Kernel.map κ f) μ := by  by_cases hf : Measurable f  · filter_upwards [hκ] with t ⟨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]