diff --git a/Exchangeability/DeFinetti/MartingaleHelpers.lean b/Exchangeability/DeFinetti/MartingaleHelpers.lean
index 7f30f000..2fc32d3a 100644
--- a/Exchangeability/DeFinetti/MartingaleHelpers.lean
+++ b/Exchangeability/DeFinetti/MartingaleHelpers.lean
@@ -50,25 +50,6 @@ export PathSpace (tailCylinder tailCylinder_measurable cylinder finCylinder
 
 open MeasureTheory
 
-section ComapTools
-
-/-- If `g` is measurable, then `comap (g ∘ f) ≤ comap f`. -/
-@[nolint unusedArguments]
-lemma comap_comp_le
-    {X Y Z : Type*} [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace Z]
-    (f : X → Y) (g : Y → Z) (hg : Measurable g) :
-    MeasurableSpace.comap (g ∘ f) (inferInstance : MeasurableSpace Z)
-      ≤ MeasurableSpace.comap f (inferInstance : MeasurableSpace Y) := by
-  intro s hs
-  -- s is a set in the comap (g ∘ f) algebra, so s = (g ∘ f) ⁻¹' t for some t
-  obtain ⟨t, ht, rfl⟩ := hs
-  -- Show (g ∘ f) ⁻¹' t is in comap f
-  refine ⟨g ⁻¹' t, hg ht, ?_⟩
-  ext x
-  simp [Set.mem_preimage, Function.comp_apply]
-
-end ComapTools
-
 section SequenceShift
 
 variable {β : Type*} [MeasurableSpace β]
diff --git a/Exchangeability/DeFinetti/ViaKoopman/InfraCore.lean b/Exchangeability/DeFinetti/ViaKoopman/InfraCore.lean
index 2f227db7..42ad4c5c 100644
--- a/Exchangeability/DeFinetti/ViaKoopman/InfraCore.lean
+++ b/Exchangeability/DeFinetti/ViaKoopman/InfraCore.lean
@@ -100,7 +100,6 @@ namespace Exchangeability.DeFinetti.ViaKoopman
 open MeasureTheory Filter Topology ProbabilityTheory
 open Exchangeability.Ergodic
 open Exchangeability.PathSpace
-open Exchangeability.DeFinetti.MartingaleHelpers (comap_comp_le)
 open scoped BigOperators RealInnerProductSpace
 
 variable {α : Type*} [MeasurableSpace α]
diff --git a/Exchangeability/DeFinetti/ViaKoopman/KernelBridge.lean b/Exchangeability/DeFinetti/ViaKoopman/KernelBridge.lean
index da0f9b03..9b9da248 100644
--- a/Exchangeability/DeFinetti/ViaKoopman/KernelBridge.lean
+++ b/Exchangeability/DeFinetti/ViaKoopman/KernelBridge.lean
@@ -28,7 +28,6 @@ namespace Exchangeability.DeFinetti.ViaKoopman
 open MeasureTheory Filter Topology ProbabilityTheory
 open Exchangeability.Ergodic
 open Exchangeability.PathSpace
-open Exchangeability.DeFinetti.MartingaleHelpers (comap_comp_le)
 open scoped BigOperators
 
 variable {α : Type*} [MeasurableSpace α]
diff --git a/Exchangeability/DeFinetti/ViaMartingale/RevFiltration.lean b/Exchangeability/DeFinetti/ViaMartingale/RevFiltration.lean
index 71874aaa..6f4e08b5 100644
--- a/Exchangeability/DeFinetti/ViaMartingale/RevFiltration.lean
+++ b/Exchangeability/DeFinetti/ViaMartingale/RevFiltration.lean
@@ -105,7 +105,7 @@ lemma revFiltration_antitone (X : ℕ → Ω → α) :
     simp only [shiftRV, shiftSeq, Function.comp_apply]
     congr 1
     omega
-  rw [h_comp]
-  exact comap_comp_le (shiftRV X m) (shiftSeq k) measurable_shiftSeq
+  rw [h_comp, ← MeasurableSpace.comap_comp]
+  exact MeasurableSpace.comap_mono measurable_shiftSeq.comap_le
 
 end Exchangeability.DeFinetti.ViaMartingale