refactor(MeasureTheory): golf Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable (leanprover-community#38876)

- rewrites `memLp_trim_of_mem_lpMeasSubgroup` to use `hf.mk f` instead of unpacking `hf.choose`
- shortens the norm comparison to a direct rewrite with `eLpNorm_trim` and `hf.ae_eq_mk`

Extracted from leanprover-community#38104

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

Author: yuanyi-350

Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean

@@ -134,14 +134,9 @@ theorem memLp_trim_of_mem_lpMeasSubgroup (hm : m ≤ m0) (f : Lp F p μ)
     MemLp (mem_lpMeasSubgroup_iff_aestronglyMeasurable.mp hf_meas).choose p (μ.trim hm) := by
   have hf : AEStronglyMeasurable[m] f μ :=
     mem_lpMeasSubgroup_iff_aestronglyMeasurable.mp hf_meas
-  let g := hf.choose
-  obtain ⟨hg, hfg⟩ := hf.choose_spec
-  change MemLp g p (μ.trim hm)
-  refine ⟨hg.aestronglyMeasurable, ?_⟩
-  have h_eLpNorm_fg : eLpNorm g p (μ.trim hm) = eLpNorm f p μ := by
-    rw [eLpNorm_trim hm hg]
-    exact eLpNorm_congr_ae hfg.symm
-  rw [h_eLpNorm_fg]
+  change MemLp (hf.mk f) p (μ.trim hm)
+  refine ⟨hf.stronglyMeasurable_mk.aestronglyMeasurable, ?_⟩
+  rw [eLpNorm_trim hm hf.stronglyMeasurable_mk, eLpNorm_congr_ae hf.ae_eq_mk.symm]
   exact Lp.eLpNorm_lt_top f
 
 /-- If `f` belongs to `Lp` for the measure `μ.trim hm`, then it belongs to the subgroup