diff --git a/Exchangeability/DeFinetti/ViaL2/AlphaConvergence/EndpointCommon.lean b/Exchangeability/DeFinetti/ViaL2/AlphaConvergence/EndpointCommon.lean
index f5da9a79..e2e1d0d6 100644
--- a/Exchangeability/DeFinetti/ViaL2/AlphaConvergence/EndpointCommon.lean
+++ b/Exchangeability/DeFinetti/ViaL2/AlphaConvergence/EndpointCommon.lean
@@ -104,8 +104,7 @@ lemma ae_tendsto_const_of_ae_convergent_of_L1_const
     exact h_int_zero
   -- Combine: hf_ae gives Tendsto _ (𝓝 (L ω)); h_abs_zero gives L ω = c a.e.
   filter_upwards [hf_ae, h_abs_zero] with ω h_ae h_eq
-  have h_diff_zero : L ω - c = 0 := by simpa using h_eq
-  have : L ω = c := by linarith
-  rwa [this] at h_ae
+  have : L ω = c := sub_eq_zero.mp (abs_eq_zero.mp h_eq)
+  simpa [this] using h_ae
 
 end Exchangeability.DeFinetti.ViaL2
diff --git a/Exchangeability/Probability/Martingale/Crossings/AntitoneLimit.lean b/Exchangeability/Probability/Martingale/Crossings/AntitoneLimit.lean
index 80f1e069..16d7a61f 100644
--- a/Exchangeability/Probability/Martingale/Crossings/AntitoneLimit.lean
+++ b/Exchangeability/Probability/Martingale/Crossings/AntitoneLimit.lean
@@ -62,9 +62,7 @@ lemma condExp_exists_ae_limit_antitone
     · -- Measurability
       exact stronglyMeasurable_condExp.measurable.mono (h_le n) le_rfl
     · -- Bound
-      calc eLpNorm (μ[f | 𝔽 n]) 1 μ
-          ≤ eLpNorm f 1 μ := hL1_bdd n
-        _ = R := hR
+      simpa [hR] using hL1_bdd n
 
   -- Step 2: Show finite upcrossings using L¹-boundedness. The expected number of
   -- upcrossings on `[a, b]` is bounded by a finite constant via
@@ -101,8 +99,7 @@ lemma condExp_exists_ae_limit_antitone
 
       -- Recognize that revProcess of condExp = revCEFinite
       have h_rev_eq : negProcess (revProcess (fun n => μ[f | 𝔽 n]) N)
-                    = negProcess (fun n => revCEFinite (μ := μ) f 𝔽 N n) := by
-        ext n ω'; simp [negProcess, revProcess, revCEFinite]
+                    = negProcess (fun n => revCEFinite (μ := μ) f 𝔽 N n) := rfl
 
       -- Pick index (N+1) from the supremum definition of upcrossings
       have h_to_iSup :
@@ -155,16 +152,8 @@ lemma condExp_exists_ae_limit_antitone
                       simp only [negProcess, revCEFinite]
                       exact (condExp_neg f (𝔽 (N - n))).symm
                     filter_upwards [h_ae_eq] with ω hω
-                    -- upcrossings = ⨆ M, upcrossingsBefore M. Use that upcrossingsBefore_congr
-                    -- gives equality when processes agree pointwise.
-                    unfold upcrossings
-                    congr 1
-                    ext M
-                    congr 1
-                    -- Apply upcrossingsBefore_congr: need ∀ k ≤ M, processes agree
-                    apply upcrossingsBefore_congr
-                    intro k _
-                    exact hω k
+                    simp [MeasureTheory.upcrossings,
+                          upcrossingsBefore_congr (fun k _ => hω k)]
               _ ≤ C_down := hC_down N
               _ ≤ C := le_max_right C_up C_down
 
@@ -235,9 +224,7 @@ lemma condExp_exists_ae_limit_antitone
         have : StronglyMeasurable[𝔽 n] (μ[f | 𝔽 n]) := stronglyMeasurable_condExp
         exact this.mono (h_le n) |>.aestronglyMeasurable
       · filter_upwards [h_ae_conv] with ω hω
-        simp only [Xlim]
-        rw [dif_pos hω]
-        exact Classical.choose_spec hω
+        simpa [Xlim, hω] using Classical.choose_spec hω
 
     -- By Fatou: ‖Xlim‖₁ ≤ liminf ‖μ[f | 𝔽 n]‖₁ ≤ ‖f‖₁ < ∞
     have hXlim_norm : HasFiniteIntegral Xlim μ := by
@@ -245,9 +232,7 @@ lemma condExp_exists_ae_limit_antitone
       -- Apply Fatou for ofReal ‖·‖
       have h_ae_tendsto : ∀ᵐ ω ∂μ, Tendsto (fun n => μ[f | 𝔽 n] ω) atTop (𝓝 (Xlim ω)) := by
         filter_upwards [h_ae_conv] with ω hω
-        simp only [Xlim]
-        rw [dif_pos hω]
-        exact Classical.choose_spec hω
+        simpa [Xlim, hω] using Classical.choose_spec hω
       -- Measurability proofs (separated to avoid timeout)
       have hmeas_n : ∀ n, AEMeasurable (fun ω => ENNReal.ofReal ‖μ[f | 𝔽 n] ω‖) μ := fun n =>
         ((stronglyMeasurable_condExp (f := f) (m := 𝔽 n) (μ := μ)).mono (h_le n)).norm.measurable.ennreal_ofReal.aemeasurable
@@ -279,9 +264,7 @@ lemma condExp_exists_ae_limit_antitone
 
   · -- A.e. convergence to Xlim
     filter_upwards [h_ae_conv] with ω hω
-    simp only [Xlim]
-    rw [dif_pos hω]
-    exact Classical.choose_spec hω
+    simpa [Xlim, hω] using Classical.choose_spec hω
 
 /-- **Key lemma: A.e. limit of adapted sequence for antitone filtration is F_inf-AEStronglyMeasurable.**
 
diff --git a/Exchangeability/Probability/Martingale/Crossings/Bounds.lean b/Exchangeability/Probability/Martingale/Crossings/Bounds.lean
index 1dca4313..c87f15fb 100644
--- a/Exchangeability/Probability/Martingale/Crossings/Bounds.lean
+++ b/Exchangeability/Probability/Martingale/Crossings/Bounds.lean
@@ -67,11 +67,9 @@ lemma upcrossings_bdd_uniform
                     simp only [le_abs_self, max_le_iff, abs_nonneg, and_self]
               _ ≤ |revCEFinite (μ := μ) f 𝔽 N M ω| + |a| := abs_sub _ _
       _ = ∫⁻ ω, (ENNReal.ofReal |revCEFinite (μ := μ) f 𝔽 N M ω| + ENNReal.ofReal |a|) ∂μ := by
-            congr 1; ext ω
-            exact ENNReal.ofReal_add (abs_nonneg _) (abs_nonneg _)
+            simp [ENNReal.ofReal_add]
       _ = ∫⁻ ω, ENNReal.ofReal |revCEFinite (μ := μ) f 𝔽 N M ω| ∂μ + ENNReal.ofReal |a| := by
-            rw [lintegral_add_right _ measurable_const, lintegral_const]
-            simp [IsProbabilityMeasure.measure_univ]
+            simp [lintegral_add_right, lintegral_const, IsProbabilityMeasure.measure_univ]
       _ ≤ ENNReal.ofReal (eLpNorm f 1 μ).toReal + ENNReal.ofReal |a| := by
             gcongr
             -- Convert lintegral to eLpNorm and use hL1_bdd