feat: ae strongly measurable with respect to compProd (#22381)

Co-authored-by: EtienneC30 <66847262+EtienneC30@users.noreply.github.com>

Author: EtienneC30

Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean

@@ -180,6 +180,12 @@ lemma setLIntegral_compProd [SFinite μ] [IsSFiniteKernel κ]
   rw [compProd, Kernel.setLIntegral_compProd _ _ _ hf hs ht]
   simp
 
+lemma _root_.MeasureTheory.AEStronglyMeasurable.ae_of_compProd [SFinite μ] [IsSFiniteKernel κ]
+    {E : Type*} [NormedAddCommGroup E] {f : α → β → E}
+    (hf : AEStronglyMeasurable f.uncurry (μ ⊗ₘ κ)) :
+    ∀ᵐ x ∂μ, AEStronglyMeasurable (f x) (κ x) := by
+  simpa using hf.compProd_mk_left
+
 lemma integrable_compProd_iff [SFinite μ] [IsSFiniteKernel κ] {E : Type*} [NormedAddCommGroup E]
     {f : α × β → E} (hf : AEStronglyMeasurable f (μ ⊗ₘ κ)) :
     Integrable f (μ ⊗ₘ κ) ↔