feat(MeasureTheory/MeasurableSpace/Basic): add map_comap_eq_of_surjective and measurable_comap_iff_right (#41090)

[We have nine map_comap_eq_of_surjective lemmas](https://loogle.lean-lang.org/?q=%22map_comap_eq_self_of_surjective%22) for `Submonoid`, `Subgroup`, `Subring`, etc., but were lacking one for `MeasurableSpace`.  This PR adds the analogous lemma; as an application it also establishes a dual version of `measurable_comap_iff` involving composition on the right rather than the left.

Co-authored-by: Terence Tao <tao@math.ucla.edu>

Author: teorth

Mathlib/MeasureTheory/MeasurableSpace/Basic.lean

@@ -152,6 +152,11 @@ theorem comap_map_le : (m.map f).comap f ≤ m :=
 theorem le_map_comap : m ≤ (m.comap g).map g :=
   (gc_comap_map g).le_u_l _
 
+theorem map_comap_eq_of_surjective (hg : Function.Surjective g) : (m.comap g).map g = m := by
+  refine le_antisymm (fun S hS => ?_) le_map_comap
+  rw [map_def, measurableSet_comap] at hS
+  aesop
+
 end Functors
 
 @[simp] theorem map_const {m} (b : β) : MeasurableSpace.map (fun _a : α ↦ b) m = ⊤ :=
@@ -200,6 +205,10 @@ lemma measurable_comap_iff {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
     {f : α → β} {g : β → γ} : Measurable[mα, mγ.comap g] f ↔ Measurable (g ∘ f) := by
   simp [measurable_iff_comap_le]
 
+lemma measurable_comap_iff_right {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {g : α → β}
+    {f : β → γ} (hg : Function.Surjective g) : Measurable f ↔ Measurable[mβ.comap g] (f ∘ g) := by
+  rw [measurable_iff_le_map, measurable_iff_le_map, ← map_comp, map_comap_eq_of_surjective hg]
+
 theorem Measurable.mono {ma ma' : MeasurableSpace α} {mb mb' : MeasurableSpace β} {f : α → β}
     (hf : @Measurable α β ma mb f) (ha : ma ≤ ma') (hb : mb' ≤ mb) : @Measurable α β ma' mb' f :=
   fun _t ht => ha _ <| hf <| hb _ ht