From 06955a93e225b3a64d91171a632db28d373c44b6 Mon Sep 17 00:00:00 2001
From: Cameron Freer <freer@mit.edu>
Date: Mon, 18 May 2026 15:03:13 +0000
Subject: [PATCH] refactor: delete comap_comp_le wrapper, route call site
 through mathlib
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The local `MartingaleHelpers.comap_comp_le` lemma had one real caller
(`RevFiltration.lean:109`) and was a thin wrapper around the mathlib
chain `MeasurableSpace.comap_comp` (equality) + `comap_mono` + the
target function's `.comap_le`. Inline at the call site:

  rw [← MeasurableSpace.comap_comp]
  exact MeasurableSpace.comap_mono measurable_shiftSeq.comap_le

The other two references to the lemma — `open ...MartingaleHelpers
(comap_comp_le)` in `ViaKoopman/InfraCore.lean:103` and
`ViaKoopman/KernelBridge.lean:31` — were vestigial after PR #22 (which
deleted the local `Kernel.IndepFun.comp` that had used `comap_comp_le`
internally). Dropped.

- DeFinetti/MartingaleHelpers.lean: delete the lemma + its
  `section ComapTools` wrapper (-19 lines).
- DeFinetti/ViaMartingale/RevFiltration.lean: inline the call (-0 lines
  net; 2 lines for 1).
- DeFinetti/ViaKoopman/{InfraCore,KernelBridge}.lean: drop the
  vestigial `open` statements (-1 line each).

Net -21 lines across 4 files. Build clean (3527 jobs), axioms standard,
0 sorries.
---
 .../DeFinetti/MartingaleHelpers.lean          | 19 -------------------
 .../DeFinetti/ViaKoopman/InfraCore.lean       |  1 -
 .../DeFinetti/ViaKoopman/KernelBridge.lean    |  1 -
 .../ViaMartingale/RevFiltration.lean          |  4 ++--
 4 files changed, 2 insertions(+), 23 deletions(-)

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