feat: the identity function is a.e.-strongly measurable w.r.t. the map by an a.e.-strongly measurable function (leanprover-community#39644)

If `AEStronglyMeasurable f µ` then `AEStronglyMeasurable id (µ.map f)`. Contrary to [aestronglyMeasurable_id](https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.html#aestronglyMeasurable_id) this does not require the identity to be defined over a second-countable space as `f` has a.e.-separable range.

Author: EtienneC30

Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean

@@ -135,6 +135,30 @@ theorem aestronglyMeasurable_zero_measure (f : α → β) :
 theorem SimpleFunc.aestronglyMeasurable (f : α →ₛ β) : AEStronglyMeasurable f μ :=
   f.stronglyMeasurable.aestronglyMeasurable
 
+/-- In a pseudometrizable space, if a measure `μ` is supported on
+a separable set then the identity function is `AEStronglyMeasurable` with respect to `μ`. -/
+lemma aestronglyMeasurable_id_of_isSeparable [TopologicalSpace α]
+    [TopologicalSpace.PseudoMetrizableSpace α] [OpensMeasurableSpace α]
+    {s : Set α} (h1 : TopologicalSpace.IsSeparable s) (h2 : μ sᶜ = 0) :
+    AEStronglyMeasurable id μ := by
+  nontriviality α
+  obtain ⟨a, -⟩ := exists_pair_ne α
+  classical
+  refine ⟨(closure s).piecewise id (fun _ ↦ a), ?_,
+    Filter.mem_of_superset h2 (fun x hx ↦ by simp [subset_closure hx])⟩
+  have h : StronglyMeasurable ((↑) : closure s → α) := by
+    have := h1.closure.secondCountableTopology
+    exact continuous_subtype_val.stronglyMeasurable
+  have : (closure s).piecewise id (fun _ ↦ a) =
+      ((↑) : closure s → α).extend ((↑) : closure s → α) (fun _ ↦ a) := by
+    ext x
+    by_cases hx : x ∈ closure s
+    · simp [Function.extend_val_apply, hx]
+    · simp [hx]
+  rw [this]
+  exact (MeasurableEmbedding.subtype_coe isClosed_closure.measurableSet).stronglyMeasurable_extend
+    h stronglyMeasurable_const
+
 namespace AEStronglyMeasurable
 
 @[fun_prop]
@@ -585,6 +609,17 @@ theorem isSeparable_ae_range (hf : AEStronglyMeasurable f μ) :
   filter_upwards [hf.ae_eq_mk] with x hx
   simp [hx]
 
+/-- If `μ : Measure α` and `f : α → β` is `AEStronglyMeasurable` where `β` is a pseudometrizable
+space and a Borel space, then the identity is a.e.-strongly measurable w.r.t. `μ.map f`. -/
+lemma aestronglyMeasurable_id_map {mβ : MeasurableSpace β}
+    [TopologicalSpace.PseudoMetrizableSpace β] [BorelSpace β]
+    {f : α → β} (hf : AEStronglyMeasurable f μ) :
+    AEStronglyMeasurable id (μ.map f) := by
+  obtain ⟨t, ht1, ht2⟩ := hf.isSeparable_ae_range
+  refine aestronglyMeasurable_id_of_isSeparable ht1.closure ?_
+  refine ae_map_iff hf.aemeasurable isClosed_closure.measurableSet |>.2 ?_
+  filter_upwards [ht2] with ω hω using subset_closure hω
+
 /-- A function is almost everywhere strongly measurable if and only if it is almost everywhere
 measurable, and up to a zero measure set its range is contained in a separable set. -/
 theorem _root_.aestronglyMeasurable_iff_aemeasurable_separable [PseudoMetrizableSpace β]