ProbabilityTheory.Kernel.AEFiniteKernelSupport.compProd

lemma AEFiniteKernelSupport.compProd [Countable S] [MeasurableSingletonClass S]    [Countable T] [MeasurableSingletonClass T] [MeasurableSingletonClass U]    {κ : Kernel T S} {η : Kernel (T × S) U} {μ : Measure T} [SFinite μ]    (hκ : AEFiniteKernelSupport κ μ) (hη : AEFiniteKernelSupport η (μ ⊗ₘ κ)) :    AEFiniteKernelSupport (κ ⊗ₖ η) μ := 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η']  rw [aefiniteKernelSupport_iff]  refine ⟨hκ.mk ⊗ₖ hη.mk, ?_, ?_⟩  · exact hκ.finiteKernelSupport_mk.compProd hη.finiteKernelSupport_mk  · have h_meas_eq : μ ⊗ₘ hκ.mk = μ ⊗ₘ κ := Measure.compProd_congr hκ.ae_eq_mk.symm    refine compProd_congr_ae hκ.ae_eq_mk.symm ?_    convert hη.ae_eq_mk.symm