chore: delete sigma-finite trim wrappers (incl. ForMathlib library) (−80 lines)

[cameronfreer]

Summary

The two local lemmas asserting SigmaFinite (μ.trim hm) for finite μ are now redundant: mathlib provides isFiniteMeasure_trim as an instance, and IsFiniteMeasure.toSigmaFinite chains automatically. inferInstance finds SigmaFinite (μ.trim hm) at every former call site without help — verified empirically at each site.

Deleting the wrappers means the ForMathlib library is now empty, so this PR also removes the ForMathlib lean_lib entirely.

Net diff: 8 files, +10 / −90 (−80 lines). Build down from 3531 jobs to 3528.

Why this PR is bigger-shape than the others in the series

This is the item flagged by the audit as "touches local API/export shape." It does, in two ways:

1. Removes the export MeasureTheory.Measure (sigmaFinite_trim) re-export from Exchangeability.Probability.CondExp.lean.
2. Removes the entire ForMathlib lean_lib (lakefile defaultTargets entry, [[lean_lib]] block, and the ForMathlib.lean root + the single file it imported).

Both are appropriate now: the ForMathlib directory was a staging area for upstreaming candidates (per PR #13's blueprint), and the only file it ever contained has been superseded by mathlib instance inference. Keeping an empty staging library is worse than removing it.

What changed

Deleted lemmas (both were inferInstance chains)

• ForMathlib/MeasureTheory/Measure/TrimInstances.lean: sigmaFinite_trim (body inferInstance).
• Exchangeability/Probability/CondExpBasic.lean: sigmaFinite_trim_of_le (body (inferInstance : IsFiniteMeasure _).toSigmaFinite).

Call sites updated (5)

All become inferInstance:

• Exchangeability/Probability/CondExp.lean:333, 359, 611 (three haveI blocks)
• Exchangeability/Probability/CondIndep/KallenbergIndicator.lean:100
• Exchangeability/DeFinetti/ViaL2/AlphaIicCE.lean:287
• Exchangeability/DeFinetti/ViaMartingale/FutureFiltration.lean:111 (the local sigmaFinite_trim_tailSigma lemma — its body becomes a one-line inferInstance)

Library/build-shape

• Exchangeability/Probability/CondExp.lean: drop the import ForMathlib.MeasureTheory.Measure.TrimInstances, the export MeasureTheory.Measure (sigmaFinite_trim), and the corresponding module-docstring section ("SigmaFinite instances for trimmed measures" / "Main components" bullet for sigmaFinite_trim).
• Exchangeability/Probability/CondExpBasic.lean: drop the "σ-Finiteness" bullet from "Main components".
• ForMathlib.lean: deleted (one-line root, imported only the deleted file).
• ForMathlib/MeasureTheory/Measure/TrimInstances.lean: deleted.
• lakefile.toml: drop "ForMathlib" from defaultTargets and the [[lean_lib]] name = "ForMathlib" block. Project now has one lean_lib.

Verification

Check	Baseline (main = 9d14638)	This branch
lake build	clean (3531 jobs)	clean (3528 jobs; −3 from deletions)
Axioms (11 theorem decls)	standard only	standard only
Sorries (Exchangeability)	0	0
Sorries (ForMathlib)	0 across 0 files	n/a (deleted)
Proof-file churn	—	8 files, +10 / −90

Notes for review

• The empirical verification of inferInstance (rather than a custom lemma) was the load-bearing step: I tested at one call site first before deleting the wrappers, and the full build confirms it works at all five.
• This concludes the safe-subset cleanup sequence (refactor: delete dead local Kernel.IndepFun.comp duplicate (−41 lines) #22 → chore: safe-subset mathlib cleanup batch (bdd_mul, iterate, pi prob, indicator) (−31 lines) #23 → this). The next item from the broader follow-up menu would be cylinder/product-measure refactor, or the design PR for DirectingMeasureCore → IsCondKernelCDF.toKernel.