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

Exchangeability/DeFinetti/ViaL2/AlphaIicCE.lean

@@ -283,8 +283,7 @@ lemma alphaIicCE_right_continuous_at
   have hm_le : TailSigma.tailSigma X ≤ (inferInstance : MeasurableSpace Ω) :=
     TailSigma.tailSigma_le X hX_meas
   haveI h_fact : Fact (TailSigma.tailSigma X ≤ (inferInstance : MeasurableSpace Ω)) := ⟨hm_le⟩
-  haveI h_sf : SigmaFinite (μ.trim hm_le) :=
-    Exchangeability.Probability.sigmaFinite_trim μ hm_le
+  haveI h_sf : SigmaFinite (μ.trim hm_le) := inferInstance
 
   -- Step 1: Get decreasing rational sequence u_n → t with u_n > t
   obtain ⟨u, u_anti, u_gt, u_tendsto⟩ := Real.exists_seq_rat_strictAnti_tendsto t

Exchangeability/DeFinetti/ViaMartingale/FutureFiltration.lean

@@ -105,10 +105,8 @@ case requires manual construction of spanning sets and is a mathlib gap. -/
 lemma sigmaFinite_trim_tailSigma {Ω α : Type*} {m₀ : MeasurableSpace Ω} [MeasurableSpace α]
     {μ : @Measure Ω m₀} [IsFiniteMeasure μ]
     (X : ℕ → Ω → α) (hX : ∀ n, Measurable (X n)) :
-    SigmaFinite (μ.trim (tailSigma_le X hX)) := by
-  classical
-  -- Use the infrastructure from CondExp.lean
-  exact Exchangeability.Probability.sigmaFinite_trim μ (tailSigma_le X hX)
+    SigmaFinite (μ.trim (tailSigma_le X hX)) :=
+  inferInstance
 
 /-! ### Helper lemmas for futureFiltration properties -/
 

Exchangeability/Probability/CondExp.lean

@@ -6,7 +6,6 @@ Authors: Cameron Freer
 import Exchangeability.Probability.CondExpBasic
 import Exchangeability.Probability.CondProb
 import Exchangeability.Probability.IntegrationHelpers
-import ForMathlib.MeasureTheory.Measure.TrimInstances
 import Mathlib.Probability.Independence.Basic
 import Mathlib.Probability.Independence.Conditional
 import Mathlib.Probability.Martingale.Basic
@@ -65,10 +64,6 @@ This file centralizes these patterns to keep the main proofs clean and maintaina
   - **Purpose**: Avoids typeclass metavariable issues in `μ[f | m]`
   - **Used in**: ViaMartingale finite-future sigma algebras
 
-- **`sigmaFinite_trim`**: Trimmed measure is sigma-finite (when base is finite)
-  - **Used in**: ViaMartingale, multiple sub-σ-algebra constructions
-  - **Note**: `isFiniteMeasure_trim` is now in mathlib as an instance
-
 ## Design Philosophy
 
 **Extract patterns that:**
@@ -299,19 +294,6 @@ lemma condExp_indicator_mul_indicator_of_condIndep
 These wrappers provide explicit instance management for conditional expectations
 with sub-σ-algebras, working around Lean 4 typeclass inference issues. -/
 
-/-! ### SigmaFinite instances for trimmed measures
-
-When working with conditional expectations on sub-σ-algebras, we need `SigmaFinite (μ.trim hm)`.
-For probability measures (or finite measures), this follows from showing the trimmed measure
-is still finite.
-
-These lemmas are now in `ForMathlib.MeasureTheory.Measure.TrimInstances` and re-exported here
-for backward compatibility. -/
-
--- Re-export from ForMathlib for backward compatibility
--- Note: isFiniteMeasure_trim is now in mathlib (as an instance), only sigmaFinite_trim is local
-export MeasureTheory.Measure (sigmaFinite_trim)
-
 /-! ### Stable conditional expectation wrapper
 
 This wrapper manages typeclass instances to avoid metavariable issues
@@ -330,7 +312,7 @@ def condExpWith {Ω : Type*} {m₀ : MeasurableSpace Ω}
   classical
   haveI : IsFiniteMeasure μ := inferInstance
   -- IsFiniteMeasure (μ.trim _hm) is now automatic via mathlib instance
-  haveI : SigmaFinite (μ.trim _hm) := sigmaFinite_trim μ _hm
+  haveI : SigmaFinite (μ.trim _hm) := inferInstance
   exact μ[f | m]
 
 /-! ### Bridge lemma for indicator factorization
@@ -356,7 +338,7 @@ lemma condexp_indicator_inter_bridge
      μ[B.indicator (fun _ => (1 : ℝ)) | m]) := by
   classical
   -- Install trimmed instances (IsFiniteMeasure is automatic via mathlib)
-  haveI : SigmaFinite (μ.trim hm) := sigmaFinite_trim μ hm
+  haveI : SigmaFinite (μ.trim hm) := inferInstance
   -- Forward to the proven lemma
   exact condExp_indicator_mul_indicator_of_condIndep hm hmF hmH hCI hA hB
 
@@ -608,7 +590,7 @@ lemma condExp_mul_pullout {Ω : Type*} {m₀ : MeasurableSpace Ω} {μ : Measure
   have hg_bound : ∀ᵐ ω ∂μ, ‖g ω‖ ≤ C := ae_of_all μ fun ω => (Real.norm_eq_abs _).le.trans (hC ω)
 
   -- Provide typeclass instances explicitly (IsFiniteMeasure is automatic via mathlib)
-  haveI : SigmaFinite (μ.trim hm) := sigmaFinite_trim μ hm
+  haveI : SigmaFinite (μ.trim hm) := inferInstance
 
   -- Now condExp_stronglyMeasurable_mul_of_bound can resolve instances
   have h := condExp_stronglyMeasurable_mul_of_bound hm hg_strong hf C hg_bound

Exchangeability/Probability/CondExpBasic.lean

@@ -17,9 +17,6 @@ improve compilation speed.
 
 ## Main components
 
-### σ-Finiteness
-- `sigmaFinite_trim_of_le`: Trimmed measure inherits σ-finiteness from finite measures
-
 ### Indicators
 - `indicator_iUnion_tsum_of_pairwise_disjoint`: Union of disjoint indicators equals their sum
 
@@ -40,14 +37,6 @@ to work with multiple measurable space structures (e.g., for trimmed measures).
 section variable `[MeasurableSpace Ω]` unused for those lemmas, requiring `set_option
 linter.unusedSectionVars false`. -/
 
-set_option linter.unusedSectionVars false in
-/-- If `μ` is finite, then any trim of `μ` is σ-finite. -/
-@[nolint unusedArguments]
-lemma sigmaFinite_trim_of_le {m m₀ : MeasurableSpace Ω}
-    (μ : Measure Ω) [IsFiniteMeasure μ] (hm : m ≤ m₀) :
-    SigmaFinite (μ.trim hm) :=
-  (inferInstance : IsFiniteMeasure (μ.trim hm)).toSigmaFinite
-
 set_option linter.unusedSectionVars false in
 /-- For pairwise disjoint sets, the indicator of the union equals
 the pointwise `tsum` of indicators (for ℝ-valued constants). -/

Exchangeability/Probability/CondIndep/KallenbergIndicator.lean

@@ -96,8 +96,9 @@ lemma condIndep_indicator_of_dropInfoY
     obtain ⟨S, hS_meas, rfl⟩ := hs
     exact hS_meas.preimage (hZ.prodMk hW)
 
-  -- SigmaFinite instance for trim (needed for condExp lemmas)
-  haveI hσZW : SigmaFinite (μ.trim hmZW_le) := sigmaFinite_trim_of_le μ hmZW_le
+  -- SigmaFinite instance for trim (needed for condExp lemmas); provided automatically
+  -- via mathlib's `isFiniteMeasure_trim` instance + `IsFiniteMeasure.toSigmaFinite`.
+  haveI hσZW : SigmaFinite (μ.trim hmZW_le) := inferInstance
 
   -- Integrability of indicators (bounded by 1)
   have hIndA_int : Integrable indA μ := (integrable_const 1).indicator (hA.preimage hY)

lakefile.toml

@@ -1,6 +1,6 @@
 name = "exchangeability"
 version = "0.1.0"
-defaultTargets = ["Exchangeability", "ForMathlib"]
+defaultTargets = ["Exchangeability"]
 
 [[require]]
 name = "mathlib"
@@ -11,8 +11,5 @@ rev = "v4.30.0-rc2"
 name = "checkdecls"
 git = "https://github.com/PatrickMassot/checkdecls.git"
 
-[[lean_lib]]
-name = "ForMathlib"
-
 [[lean_lib]]
 name = "Exchangeability"