∀ {Ω : Type u_1} {F : Type u_2} {m mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : Ω → F}
  [inst : TopologicalSpace F],
  m ≤ mΩ →
    MeasureTheory.AEStronglyMeasurable f μ →
      MeasureTheory.AEStronglyMeasurable (fun x => f x.2) (MeasureTheory.Measure.map (fun ω => (id ω, id ω)) μ)