feat: if Y = f(X) then Y is X-measurable (#39728)

If `g = h ∘ f`, then the sigma-algebra generated by `g` is smaller than the one generated by `f`.

Thanks to this lemma, if one wants to prove that the sigma-algebra generated by a random variable `Y` is smaller than the one generated by `X`, one can provide `f` and prove that `Y = f(X)`.

Co-authored-by: EtienneC30 <66847262+EtienneC30@users.noreply.github.com>
Co-authored-by: Etienne Marion <66847262+EtienneC30@users.noreply.github.com>

Author: mathlib-splicebot[bot]

Mathlib/MeasureTheory/MeasurableSpace/Basic.lean

@@ -183,6 +183,14 @@ theorem measurable_iff_comap_le {m₁ : MeasurableSpace α} {m₂ : MeasurableSp
 
 alias ⟨Measurable.comap_le, Measurable.of_comap_le⟩ := measurable_iff_comap_le
 
+/-- If `g = h ∘ f`, then the sigma-algebra generated by `g` is
+smaller than the one generated by `f`. -/
+lemma MeasurableSpace.comap_le_comap_of_eq_comp {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
+    {f : α → β} {g : α → γ} (h : β → γ) (mh : Measurable h) (heq : g = h ∘ f) :
+    mγ.comap g ≤ mβ.comap f := by
+  rw [heq, ← MeasurableSpace.comap_comp]
+  exact MeasurableSpace.comap_mono mh.comap_le
+
 theorem comap_measurable {m : MeasurableSpace β} (f : α → β) : Measurable[m.comap f] f :=
   fun s hs => ⟨s, hs, rfl⟩