chore: targeted manual golf in Probability/Martingale + TripleLawDropInfo (#112)

Eight LSP-verified proof-body shrinks in the files that the bulk autoGolf
run in PR #16 never reached. Each site was probed individually rather
than via `exact?` (which timed out on these measure-heavy goals).

* `Crossings/Pathwise.lean:54` `up_neg_flip_eq_down`:
  body collapses to `rfl` — `downcrossingsBefore` is definitionally
  `upcrossingsBefore (-b) (-a) (negProcess X)`, so both sides of the
  lemma unfold to the same `⨆ N, ...` term.
* `Crossings/Pathwise.lean:123` `upcrossingsBefore_congr`:
  four lines (`simp only`/`congr`/`ext`/`rw`) collapse to
  `simp [upcrossingsBefore, upperCrossingTime_congr h]`.
* `Reverse.lean:80` `revCEFinite_martingale`:
  inline the local `have : 𝔽 (N-i) ≤ 𝔽 (N-j)` into the final
  `condExp_condExp_of_le` call.
* `Crossings/Bounds.lean:45` `hL1_bdd`:
  drop the `simp only [revCEFinite]`; `eLpNorm_one_condExp_le_eLpNorm`
  unifies definitionally.
* `Crossings/AntitoneLimit.lean:350` `h_tower`:
  rewrite as a term-mode `fun n => condExp_condExp_of_le (iInf_le 𝔽 n)
  (h_le n)`.
* `Crossings/AntitoneLimit.lean:368` `hL1_conv_Xn`:
  six-line `have`/`simp_rw`/`exact` collapses to a single
  `simpa [hXn_def, eLpNorm_sub_comm] using hL1_conv`.
* `TripleLawDropInfo/PairLawHelpers.lean:40` `marginal_law_eq_of_pair_law`:
  five lines (two `have`s + final `rw`) become a single
  `simpa [Measure.map_map …] using congrArg (Measure.map Prod.snd) h_law`.
* `TripleLawDropInfo/DropInfo.lean:211` final square-zero step:
  the trailing `have : ... = 0; linarith` two-liner collapses to a single
  `nlinarith [sq_nonneg (μ₂ ω - μ₁ ω)]`.

Net: 6 files, +11 / −30 (−19 lines).

Author: cameronfreer

Exchangeability/Probability/Martingale/Crossings/AntitoneLimit.lean

@@ -347,10 +347,8 @@ lemma ae_limit_is_condexp_iInf
   set F_inf := iInf 𝔽 with hF_inf_def
 
   -- Tower property: For every n, μ[μ[f | 𝔽 n] | F_inf] = μ[f | F_inf]
-  have h_tower : ∀ n, μ[μ[f | 𝔽 n] | F_inf] =ᵐ[μ] μ[f | F_inf] := by
-    intro n
-    have : F_inf ≤ 𝔽 n := iInf_le 𝔽 n
-    exact condExp_condExp_of_le this (h_le n)
+  have h_tower : ∀ n, μ[μ[f | 𝔽 n] | F_inf] =ᵐ[μ] μ[f | F_inf] :=
+    fun n => condExp_condExp_of_le (iInf_le 𝔽 n) (h_le n)
 
   -- Final identification: Xlim = μ[f | F_inf]
   -- Strategy: Use L¹-continuity of condExp (non-circular approach)
@@ -366,12 +364,7 @@ lemma ae_limit_is_condexp_iInf
 
   -- First, relate hL1_conv to Xn notation
   have hL1_conv_Xn : Tendsto (fun n => eLpNorm (Xlim - Xn n) 1 μ) atTop (𝓝 0) := by
-    have : ∀ n, eLpNorm (Xlim - Xn n) 1 μ = eLpNorm (μ[f | 𝔽 n] - Xlim) 1 μ := by
-      intro n
-      simp only [hXn_def]
-      rw [eLpNorm_sub_comm]
-    simp only [this]
-    exact hL1_conv
+    simpa [hXn_def, eLpNorm_sub_comm] using hL1_conv
 
   -- Key inequality: ‖μ[Xlim | F_inf] - Y‖₁ ≤ ‖Xlim - Xn n‖₁ for all n
   have h_bound (n : ℕ) : eLpNorm (μ[Xlim | F_inf] - Y) 1 μ ≤ eLpNorm (Xlim - Xn n) 1 μ := by

Exchangeability/Probability/Martingale/Crossings/Bounds.lean

@@ -44,7 +44,6 @@ lemma upcrossings_bdd_uniform
   -- The L¹ norm of revCEFinite is uniformly bounded by ‖f‖₁
   have hL1_bdd : ∀ N n, eLpNorm (revCEFinite (μ := μ) f 𝔽 N n) 1 μ ≤ eLpNorm f 1 μ := by
     intro N n
-    simp only [revCEFinite]
     exact eLpNorm_one_condExp_le_eLpNorm f
 
   -- For each N, revCEFinite is a martingale, hence a submartingale

Exchangeability/Probability/Martingale/Crossings/Pathwise.lean

@@ -52,8 +52,7 @@ noncomputable def downcrossings {Ω : Type*} (a b : ℝ) (X : ℕ → Ω → ℝ
 /-- **Identity 1:** Upcrossings of negated process = downcrossings of original.
 Negation flips crossing direction: up(-b, -a, -X) = down(a, b, X). -/
 lemma up_neg_flip_eq_down {Ω : Type*} (a b : ℝ) (X : ℕ → Ω → ℝ) :
-  upcrossings (-b) (-a) (negProcess X) = downcrossings a b X := by
-  funext ω; simp [upcrossings, downcrossings, downcrossingsBefore]
+  upcrossings (-b) (-a) (negProcess X) = downcrossings a b X := rfl
 
 /-- Double negation is identity (used by `simp` below). -/
 @[simp] private lemma negProcess_negProcess {Ω : Type*} (X : ℕ → Ω → ℝ) :
@@ -123,11 +122,7 @@ private lemma upperCrossingTime_congr {Ω : Type*} {a b : ℝ} {f g : ℕ → Ω
 lemma upcrossingsBefore_congr {Ω : Type*} {a b : ℝ} {f g : ℕ → Ω → ℝ} {N : ℕ} {ω : Ω}
     (h : ∀ n ≤ N, f n ω = g n ω) :
     upcrossingsBefore a b f N ω = upcrossingsBefore a b g N ω := by
-  simp only [upcrossingsBefore]
-  congr 1
-  ext k
-  simp only [Set.mem_setOf_eq]
-  rw [upperCrossingTime_congr h]
+  simp [upcrossingsBefore, upperCrossingTime_congr h]
 
 /-- Index is bounded by completion time when upperCrossingTime < N.
 If the n-th crossing completes before time N, then n < N. -/

Exchangeability/Probability/Martingale/Reverse.lean

@@ -76,10 +76,7 @@ lemma revCEFinite_martingale
     intro i j hij
     simp only [revCEFinite, revFiltration]
     -- Tower: E[μ[f | 𝔽_{N-j}] | 𝔽_{N-i}] = μ[f | 𝔽_{N-i}]
-    -- Need: 𝔽_{N-i} ≤ 𝔽_{N-j} (since i ≤ j ⟹ N-j ≤ N-i ⟹ 𝔽(N-i) ≤ 𝔽(N-j))
-    have : 𝔽 (N - i) ≤ 𝔽 (N - j) := by
-      have : N - j ≤ N - i := tsub_le_tsub_left hij N
-      exact h_antitone this
-    exact condExp_condExp_of_le this (h_le (N - j))
+    -- 𝔽_{N-i} ≤ 𝔽_{N-j} since i ≤ j ⟹ N-j ≤ N-i and 𝔽 is antitone.
+    exact condExp_condExp_of_le (h_antitone (tsub_le_tsub_left hij N)) (h_le (N - j))
 
 end Exchangeability.Probability

Exchangeability/Probability/TripleLawDropInfo/DropInfo.lean

@@ -209,6 +209,5 @@ lemma condExp_indicator_eq_of_law_eq_of_comap_le
 
   -- (μ₂ - μ₁)² = 0 implies μ₂ = μ₁
   filter_upwards [h_diff_zero] with ω hω
-  have : μ₂ ω - μ₁ ω = 0 := by nlinarith [sq_nonneg (μ₂ ω - μ₁ ω)]
-  linarith
+  nlinarith [sq_nonneg (μ₂ ω - μ₁ ω)]
 

Exchangeability/Probability/TripleLawDropInfo/PairLawHelpers.lean

@@ -38,11 +38,9 @@ lemma marginal_law_eq_of_pair_law
     (hX : Measurable X) (hW : Measurable W) (hW' : Measurable W')
     (h_law : Measure.map (fun ω => (X ω, W ω)) μ = Measure.map (fun ω => (X ω, W' ω)) μ) :
     Measure.map W μ = Measure.map W' μ := by
-  have h1 : Measure.map W μ = Measure.map Prod.snd (Measure.map (fun ω => (X ω, W ω)) μ) := by
-    rw [Measure.map_map measurable_snd (hX.prodMk hW)]; rfl
-  have h2 : Measure.map W' μ = Measure.map Prod.snd (Measure.map (fun ω => (X ω, W' ω)) μ) := by
-    rw [Measure.map_map measurable_snd (hX.prodMk hW')]; rfl
-  rw [h1, h_law, ← h2]
+  simpa [Measure.map_map measurable_snd (hX.prodMk hW),
+         Measure.map_map measurable_snd (hX.prodMk hW')] using
+    congrArg (Measure.map Prod.snd) h_law
 
 /-- Helper for Kallenberg 1.3: Square integrals are equal via Doob-Dynkin factorization.