diff --git a/Mathlib/MeasureTheory/MeasurableSpace/Constructions.lean b/Mathlib/MeasureTheory/MeasurableSpace/Constructions.lean
index 99dceda0cffb8e..af653b39b48858 100644
--- a/Mathlib/MeasureTheory/MeasurableSpace/Constructions.lean
+++ b/Mathlib/MeasureTheory/MeasurableSpace/Constructions.lean
@@ -586,6 +586,12 @@ theorem measurable_pi_lambda (f : α → ∀ a, X a) (hf : ∀ a, Measurable fun
     Measurable f :=
   measurable_pi_iff.mpr hf
 
+lemma MeasurableSpace.comap_process_pi (X : (a : δ) → β → X a) :
+    MeasurableSpace.comap (fun b a ↦ X a b) inferInstance =
+      ⨆ a, MeasurableSpace.comap (X a) inferInstance := by
+  simp_rw [MeasurableSpace.pi, MeasurableSpace.comap_iSup, MeasurableSpace.comap_comp]
+  rfl
+
 /-- The function `(f, x) ↦ update f a x : (Π a, X a) × X a → Π a, X a` is measurable. -/
 @[fun_prop]
 theorem measurable_update' {a : δ} [DecidableEq δ] :
diff --git a/Mathlib/Probability/Process/Filtration.lean b/Mathlib/Probability/Process/Filtration.lean
index 0a2d61a3547b4a..0ad8aa6fb16ea3 100644
--- a/Mathlib/Probability/Process/Filtration.lean
+++ b/Mathlib/Probability/Process/Filtration.lean
@@ -399,6 +399,11 @@ def natural (u : (i : ι) → Ω → β i) (hum : ∀ i, StronglyMeasurable (u i
     rintro j _ s ⟨t, ht, rfl⟩
     exact (hum j).measurable ht
 
+lemma natural_eq_comap (u : (i : ι) → Ω → β i) (hum : ∀ (i : ι), StronglyMeasurable (u i)) (i : ι) :
+    natural u hum i = .comap (fun ω (j : Set.Iic i) ↦ u j ω) inferInstance := by
+  simp_rw [natural, MeasurableSpace.comap_process_pi, iSup_subtype']
+  rfl
+
 section
 
 open MeasurableSpace