refactor: delete comap_comp_le wrapper, route call site through mathlib (−21 lines)

[cameronfreer]

Summary

MartingaleHelpers.comap_comp_le proved comap (g ∘ f) m ≤ comap f m for measurable g. It had one real caller (RevFiltration.lean:109) and was a thin wrapper around the mathlib chain. Two other reference sites (open ...MartingaleHelpers (comap_comp_le) in InfraCore.lean:103 and KernelBridge.lean:31) were vestigial after PR #22 deleted the local Kernel.IndepFun.comp that had used it internally.

Net diff: 4 files, +2 / −23 (−21 lines).

What changed

Inline the call site against mathlib

DeFinetti/ViaMartingale/RevFiltration.lean:109:

-- before
exact comap_comp_le (shiftRV X m) (shiftSeq k) measurable_shiftSeq

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

MeasurableSpace.comap_comp is the mathlib equality comap g (comap f m) = comap (f ∘ g) m; combined with comap_mono and the target function's .comap_le, it does exactly what the wrapper did. Two lines instead of one, but no MartingaleHelpers indirection.

Delete the wrapper

DeFinetti/MartingaleHelpers.lean: delete the comap_comp_le lemma + its section ComapTools wrapper (-19 lines).

Drop vestigial open statements

DeFinetti/ViaKoopman/InfraCore.lean:103 and DeFinetti/ViaKoopman/KernelBridge.lean:31: drop the open Exchangeability.DeFinetti.MartingaleHelpers (comap_comp_le) lines. Verified by grep that neither file uses the name after the open.

Verification

Check	Baseline (main = 68f2c62)	This branch
lake build	clean (3527 jobs)	clean (3527 jobs)
Axioms (11 theorem decls)	standard only	standard only
Sorries (Exchangeability)	0	0
Proof-file churn	—	4 files, +2 / −23

This closes out the post-bump "small targeted cleanup" series. The remaining docket items are larger: cylinder/product-measure refactor, file-by-file Probability bridge triage, and the DirectingMeasureCore → IsCondKernelCDF.toKernel design PR.