refactor(MeasureTheory): golf Mathlib/MeasureTheory/Integral/Marginal (#39176)

- refactors `Mathlib/MeasureTheory/Integral/Marginal` by shortening `Measurable.lmarginal`

Extracted from #38104

[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)

Author: yuanyi-350

Mathlib/MeasureTheory/Integral/Marginal.lean

@@ -89,13 +89,8 @@ notation "∫⋯∫⁻_" s ", " f => lmarginal (fun _ ↦ volume) s f
 variable (μ)
 
 theorem _root_.Measurable.lmarginal [∀ i, SigmaFinite (μ i)] (hf : Measurable f) :
-    Measurable (∫⋯∫⁻_s, f ∂μ) := by
-  refine Measurable.lintegral_prod_right ?_
-  refine hf.comp ?_
-  rw [measurable_pi_iff]; intro i
-  by_cases hi : i ∈ s
-  · simpa [hi, updateFinset] using measurable_pi_iff.1 measurable_snd _
-  · simpa [hi, updateFinset] using measurable_pi_iff.1 measurable_fst _
+    Measurable (∫⋯∫⁻_s, f ∂μ) :=
+  Measurable.lintegral_prod_right (hf.comp measurable_updateFinset')
 
 @[simp] theorem lmarginal_empty (f : (∀ i, X i) → ℝ≥0∞) : ∫⋯∫⁻_∅, f ∂μ = f := by
   ext1 x