diff --git a/Exchangeability/Contractability.lean b/Exchangeability/Contractability.lean
index 09580fcf..eaa21aae 100644
--- a/Exchangeability/Contractability.lean
+++ b/Exchangeability/Contractability.lean
@@ -335,9 +335,7 @@ lemma exists_perm_extending_strictMono {m n : ℕ} (k : Fin m → ℕ)
           ext; simp [ι]
       , right_inv := by
           intro i
-          cases i with
-          | mk i hi =>
-            simp [ι] }
+          rfl }
   -- Equivalence between the image of `k` and `Fin m`.
   -- For injectivity of k, we use that it's strictly monotone
   have hk_inj : Function.Injective kFin :=
@@ -409,11 +407,8 @@ lemma Contractable.shift_and_select {μ : Measure Ω} {X : ℕ → Ω → α}
 
 /-- For a permutation σ on Fin n, the range {σ(0), ..., σ(n-1)} equals {0, ..., n-1}. -/
 lemma perm_range_eq {n : ℕ} (σ : Equiv.Perm (Fin n)) :
-    Finset.image (fun i : Fin n => σ i) Finset.univ = Finset.univ := by
-  ext x
-  simp only [Finset.mem_image, Finset.mem_univ, true_and, iff_true]
-  use σ.symm x
-  simp
+    Finset.image (fun i : Fin n => σ i) Finset.univ = Finset.univ :=
+  Finset.image_univ_equiv σ
 
 /--
 Helper lemma: All values of a strictly monotone function are bounded by its last value plus one.
diff --git a/Exchangeability/Core.lean b/Exchangeability/Core.lean
index ab76cf98..081be12a 100644
--- a/Exchangeability/Core.lean
+++ b/Exchangeability/Core.lean
@@ -244,14 +244,7 @@ lemma cylinder_subset_prefixCylinders {s : Finset ℕ} {S : Set (∀ _ : s, α)}
   have hs_eq :
       MeasureTheory.cylinder (α:=fun _ : ℕ => α) s S =
         prefixCylinder (α:=α) (pull ⁻¹' S) := by
-    ext x
-    classical
-    have hpull : pull (prefixProj (α:=α) N x) = s.restrict x := by
-      funext y
-      rcases y with ⟨y, hy⟩
-      simp only [pull, prefixProj, Finset.restrict]
-      rfl
-    simp [MeasureTheory.cylinder, prefixCylinder, hpull]
+    rfl
   refine hs_eq ▸ prefixCylinder_mem_prefixCylinders (α:=α) ?_
   exact hpull_meas hS
 
@@ -438,8 +431,8 @@ lemma pathLaw_map_prefix_perm (μ : Measure Ω) (X : ℕ → Ω → α)
         rw [Measure.map_map (measurable_prefixProj (α:=α) (n:=n)) hreindex]
     _ = Measure.map (prefixProj (α:=α) n ∘ reindex (α:=α) π)
         (Measure.map (fun ω => fun i : ℕ => X i ω) μ) := by rw [pathLaw]
-    _ = Measure.map ((prefixProj (α:=α) n ∘ reindex (α:=α) π) ∘ fun ω => fun i : ℕ => X i ω) μ := by
-        exact Measure.map_map ((measurable_prefixProj (α:=α) (n:=n)).comp hreindex) (by fun_prop)
+    _ = Measure.map ((prefixProj (α:=α) n ∘ reindex (α:=α) π) ∘ fun ω => fun i : ℕ => X i ω) μ :=
+        Measure.map_map ((measurable_prefixProj (α:=α) (n:=n)).comp hreindex) (by fun_prop)
     _ = Measure.map (fun ω => fun i : Fin n => X (π i) ω) μ := rfl
 
 /--
@@ -539,10 +532,7 @@ def approxEquiv :
       ext
       simp
     · intro y
-      rcases y with ⟨y, hy⟩
-      rcases hy with ⟨j, hj⟩
-      ext
-      simp [hj]
+      norm_num
 
 /--
 A finite permutation of `Fin (permBound π n)` that agrees with `π` on `{0,...,n-1}`.
@@ -673,18 +663,7 @@ private lemma exchangeable_finite_marginals_eq_reindexed {μ : Measure Ω}
   have h2 := pathLaw_map_prefix_perm (α:=α) μ X hX π n
   have hperm := marginals_perm_eq (μ:=μ) (X:=X) hX hEx π n
   -- LHS equals the unpermed marginal
-  have hlhs :
-      Measure.map (prefixProj (α:=α) n) μX =
-        Measure.map (fun ω => fun i : Fin n => X i ω) μ := by
-    rwa [hμX]
-  -- RHS equals the permuted marginal
-  have hrhs :
-      Measure.map (prefixProj (α:=α) n)
-          (Measure.map (reindex (α:=α) π) μX) =
-        Measure.map (fun ω => fun i : Fin n => X (π i) ω) μ := by
-    rwa [hμX]
-  rw [hlhs, hrhs]
-  exact (congrArg (fun ν => ν S) hperm).symm
+  lia
 
 -- The path law of a reindexed sequence equals reindexing the path law.
 private lemma pathLaw_map_reindex_comm {μ : Measure Ω} {X : ℕ → Ω → α}
diff --git a/Exchangeability/DeFinetti/BridgeProperty.lean b/Exchangeability/DeFinetti/BridgeProperty.lean
index 10da34df..c43d0740 100644
--- a/Exchangeability/DeFinetti/BridgeProperty.lean
+++ b/Exchangeability/DeFinetti/BridgeProperty.lean
@@ -209,9 +209,7 @@ lemma indicator_product_bridge
       = ∫⁻ ω, ∏ j : Fin m, ν ω (B (σ j)) ∂μ := by
     congr 1; funext ω
     symm
-    have hsup : {a : Fin m | σ a ≠ a} ⊆ (Finset.univ : Finset (Fin m)) := by
-      simp only [Finset.coe_univ, Set.subset_univ]
-    exact Equiv.Perm.prod_comp σ Finset.univ (fun j => ν ω (B j)) hsup
+    exact Fintype.prod_equiv σ (fun x => (ν ω) (B (σ x))) (fun x => (ν ω) (B x)) (congrFun rfl)
 
   -- Now use the strictly monotone case with reindexed B
   rw [hL, hR]
diff --git a/Exchangeability/DeFinetti/CommonEnding.lean b/Exchangeability/DeFinetti/CommonEnding.lean
index 9da6f76f..25100ab7 100644
--- a/Exchangeability/DeFinetti/CommonEnding.lean
+++ b/Exchangeability/DeFinetti/CommonEnding.lean
@@ -193,12 +193,8 @@ lemma prod_eq_one_iff_of_zero_one {ι : Type*} [Fintype ι] {f : ι → ENNReal}
 /-- The product of finitely many terms, each bounded by 1, is bounded by 1.
 This is useful for products of indicator functions. -/
 lemma prod_le_one_of_le_one {ι : Type*} [Fintype ι] {f : ι → ENNReal}
-    (hf : ∀ i, f i ≤ 1) : ∏ i, f i ≤ 1 := by
-  apply Finset.prod_le_one
-  · intro i _
-    exact zero_le _
-  · intro i _
-    exact hf i
+    (hf : ∀ i, f i ≤ 1) : ∏ i, f i ≤ 1 :=
+  Finset.prod_le_one' fun i a => hf i
 
 -- Note: measurable_prod_ennreal has been moved to Exchangeability.Probability.MeasureKernels
 
@@ -240,9 +236,7 @@ lemma product_bounded {ι : Type*} [Fintype ι] {α : Type*}
         _ ≤ M' a * s.prod M' :=
             mul_le_mul_of_nonneg_left ih (hM'_nonneg a)
         _ = Finset.prod (insert a s) M' := by rw [Finset.prod_insert ha]
-  refine ⟨Finset.univ.prod M', ?_⟩
-  intro x
-  simpa using key Finset.univ x
+  exact Exists.intro (Finset.univ.prod M') (key Finset.univ)
 
 
 /- ### Key Bridge Lemma
@@ -327,9 +321,7 @@ private lemma measure_via_indicator_integral (μ : Measure Ω) (X : ℕ → Ω 
   have hconst := lintegral_const (μ := μ.restrict E) (c := 1)
   have hconst' : ∫⁻ ω, 1 ∂μ.restrict E = μ E := by
     simp [Measure.restrict_apply, hconst]
-  have hμE : μ E = ∫⁻ ω, E.indicator (fun _ => 1) ω ∂μ := by
-    simpa [hconst'] using hlin.symm
-  rw [hμE, ← hProdEqIndicator]
+  lia
 
 -- Product of measures on rectangles equals Measure.pi evaluation
 private lemma product_measure_on_rectangle {Ω α : Type*} [MeasurableSpace α]
@@ -365,11 +357,7 @@ lemma fidi_eq_avg_product {μ : Measure Ω} [IsProbabilityMeasure μ]
     exact product_measure_on_rectangle ν hν_prob m B ω
 
   -- Chain the equalities: μ E = integral of indicators = integral of products = integral of pi
-  calc μ {ω | ∀ i, X (k i) ω ∈ B i}
-      = ∫⁻ ω, ∏ i : Fin m,
-          ENNReal.ofReal ((B i).indicator (fun _ => (1 : ℝ)) (X (k i) ω)) ∂μ := lhs_eq
-    _ = ∫⁻ ω, ∏ i : Fin m, ν ω (B i) ∂μ := h_bridge
-    _ = ∫⁻ ω, (Measure.pi fun i : Fin m => ν ω) {x | ∀ i, x i ∈ B i} ∂μ := rhs_eq
+  lia
 
 -- Note: rectangles_isPiSystem has been moved to Exchangeability.Probability.MeasureKernels
 
@@ -424,10 +412,7 @@ lemma measure_eq_of_agree_on_pi_system {Ω : Type*} [MeasurableSpace Ω]
     μ = ν := by
   -- For probability measures, μ univ = ν univ = 1
   have h_univ : μ Set.univ = ν Set.univ := by
-    by_cases h : Set.univ ∈ C
-    · exact h_agree Set.univ h
-    · -- Both are probability measures, so both measure univ as 1
-      simp [measure_univ]
+    norm_num
   exact ext_of_generate_finite C hC_gen hC_pi h_agree h_univ
 
 /-!
@@ -504,13 +489,8 @@ private lemma map_coords_isProbabilityMeasure {μ : Measure Ω} [IsProbabilityMe
 -- Product of probability measures is a probability measure
 private lemma pi_of_prob_is_prob {μ : Measure Ω} [IsProbabilityMeasure μ]
     (ν : Ω → Measure α) (hν_prob : ∀ ω, IsProbabilityMeasure (ν ω)) (m : ℕ) :
-    ∀ ω, IsProbabilityMeasure (Measure.pi fun _ : Fin m => ν ω) := by
-  intro ω
-  constructor
-  have h : (Set.univ : Set (Fin m → α)) = Set.univ.pi (fun (_ : Fin m) => Set.univ) := by
-    ext x; simp
-  rw [h, Measure.pi_pi]
-  simp [measure_univ]
+    ∀ ω, IsProbabilityMeasure (Measure.pi fun _ : Fin m => ν ω) :=
+  fun ω => Measure.pi.instIsProbabilityMeasure fun x => ν ω
 
 -- Bind of probability measure with probability kernels is probability
 private lemma bind_pi_isProbabilityMeasure {μ : Measure Ω} [IsProbabilityMeasure μ]
diff --git a/Exchangeability/DeFinetti/ContractableVsExchangeable_Extras.lean b/Exchangeability/DeFinetti/ContractableVsExchangeable_Extras.lean
index 8d12dfb1..ab25ab13 100644
--- a/Exchangeability/DeFinetti/ContractableVsExchangeable_Extras.lean
+++ b/Exchangeability/DeFinetti/ContractableVsExchangeable_Extras.lean
@@ -118,8 +118,8 @@ example :
 
   -- Push forward both sides by the measurable map extracting the first two coordinates.
   let p : (Fin 2 → ℝ) → ℝ × ℝ := fun y => (y 0, y 1)
-  have hp : Measurable p := by
-    exact (measurable_pi_apply (0 : Fin 2)).prod_mk (measurable_pi_apply (1 : Fin 2))
+  have hp : Measurable p :=
+    (measurable_pi_apply (0 : Fin 2)).prod_mk (measurable_pi_apply (1 : Fin 2))
   have h_meas_left : Measurable (fun ω i : Fin 2 => X (σ i : ℕ) ω) :=
     by
       fun_prop
diff --git a/Exchangeability/DeFinetti/L2Helpers.lean b/Exchangeability/DeFinetti/L2Helpers.lean
index 64f703e4..8114f113 100644
--- a/Exchangeability/DeFinetti/L2Helpers.lean
+++ b/Exchangeability/DeFinetti/L2Helpers.lean
@@ -99,15 +99,7 @@ lemma contractable_map_single (hX_contract : Contractable μ X) (hX_meas : ∀ i
   have h_eval := congrArg (Measure.map eval) h_map
   have h_comp := h_left.trans (h_eval.trans h_right)
   -- Evaluate the compositions explicitly.
-  have h_comp_simp :
-      (fun ω => eval (fun j : Fin 1 => X (k j) ω)) = fun ω => X i ω := by
-    funext ω
-    simp [eval, k, fin1Zero]
-  have h_comp_simp' :
-      (fun ω => eval (fun j : Fin 1 => X j.val ω)) = fun ω => X 0 ω := by
-    funext ω
-    simp [eval, fin1Zero]
-  simpa [Function.comp, h_comp_simp, h_comp_simp'] using h_comp
+  assumption
 
 /-- **Strict monotonicity for two-point subsequence selection.**
 
@@ -163,15 +155,7 @@ lemma contractable_map_pair (hX_contract : Contractable μ X) (hX_meas : ∀ i,
   have h_right := Measure.map_map h_eval_meas h_meas_std (μ := μ)
   have h_eval := congrArg (Measure.map eval) h_map
   have h_comp := h_left.trans (h_eval.trans h_right)
-  have h_comp_simp :
-      (fun ω => eval (fun t : Fin 2 => X (k t) ω)) = fun ω => (X i ω, X j ω) := by
-    funext ω
-    simp [eval, k, fin2Zero, fin2One]
-  have h_comp_simp' :
-      (fun ω => eval (fun t : Fin 2 => X t.val ω)) = fun ω => (X 0 ω, X 1 ω) := by
-    funext ω
-    simp [eval, fin2Zero, fin2One]
-  simpa [Function.comp, h_comp_simp, h_comp_simp'] using h_comp
+  assumption
 
 set_option linter.unusedSectionVars false in
 /-- **Contractability is preserved under measurable postcomposition.**
@@ -222,9 +206,7 @@ private lemma abs_mul_le_half_sq_add_sq (a b : ℝ) :
   have h'' : |a| * |b| ≤ (|a| ^ 2 + |b| ^ 2) / 2 := by
     have : |a| * |b| * 2 ≤ |a| ^ 2 + |b| ^ 2 := h'
     linarith [show (0 : ℝ) < 2 by norm_num]
-  have h''' : |a * b| ≤ (|a| ^ 2 + |b| ^ 2) / 2 := by
-    simpa [abs_mul] using h''
-  simpa [sq_abs, pow_two, add_comm, add_left_comm, add_assoc] using h'''
+  simp_all
 
 end CovarianceHelpers
 /-!
@@ -258,10 +240,7 @@ lemma toReal_lt_of_lt_ofReal {x : ENNReal} {ε : ℝ}
     (_hx : x ≠ ⊤) (hε : 0 ≤ ε) :
     x < ENNReal.ofReal ε → ENNReal.toReal x < ε := by
   intro h
-  have : ENNReal.toReal x < ENNReal.toReal (ENNReal.ofReal ε) :=
-    ENNReal.toReal_strict_mono (ENNReal.ofReal_ne_top) h
-  simp [ENNReal.toReal_ofReal hε] at this
-  exact this
+  exact (ENNReal.lt_ofReal_iff_toReal_lt _hx).mp h
 
 /-- **Arithmetic bound for convergence rates: √(Cf/m) < ε/2 when m is large.**
 
@@ -369,9 +348,7 @@ lemma eLpNorm_two_from_integral_sq_le
   -- Goal is (∫ ‖g‖²)^(1/2) ≤ C^(1/2)
   -- Note: the ‖g‖^2 in the integral is with ^(2:ℕ), need to be careful with types
   have h_int_le' : (∫ ω, ‖g ω‖ ^ (2:ℝ) ∂μ) ≤ C := by
-    convert h_int_le using 2
-    ext ω
-    simp [sq]
+    simpa
   gcongr
 
 end LpUtilities
@@ -380,12 +357,7 @@ end LpUtilities
 
 Since Fin 1 has only one element, the premise `i < j` is impossible. -/
 private lemma fin1_strictMono_vacuous (k : Fin 1 → ℕ) : StrictMono k := by
-  intro i j hij
-  exfalso
-  have hi : i = 0 := Fin.eq_zero i
-  have hj : j = 0 := Fin.eq_zero j
-  rw [hi, hj] at hij
-  exact LT.lt.false hij
+  exact Subsingleton.strictMono k
 
 /-- **Single marginals have identical distribution in contractable sequences.**
 
@@ -417,11 +389,7 @@ lemma contractable_single_marginal_eq
   have h_eval := congrArg (Measure.map eval) h_map
   have h_comp := h_left.trans (h_eval.trans h_right)
   -- Simplify the compositions
-  have h_comp_left : (fun ω => eval (fun j : Fin 1 => X (κ j) ω)) = fun ω => X k ω := by
-    funext ω; simp [eval, κ]
-  have h_comp_right : (fun ω => eval (fun j : Fin 1 => X j.val ω)) = fun ω => X 0 ω := by
-    funext ω; simp [eval]
-  simpa [Function.comp, h_comp_left, h_comp_right] using h_comp
+  assumption
 
 -- Helper lemmas for Fin index gymnastics in two-window bounds.
 -- These lemmas isolate the technical reindexing and cardinality proofs needed for
@@ -477,9 +445,7 @@ lemma card_filter_fin_val_lt_two_mul (k : ℕ) :
       have : b.val < 2 * k := b.isLt
       omega
     · ext
-      simp
-      have : k ≤ b.val := hb
-      omega
+      exact Nat.sub_add_cancel hb
 
 /-- Cardinality of `{i : Fin(2k) | i.val ≥ k}` is k. -/
 lemma card_filter_fin_val_ge_two_mul (k : ℕ) :
@@ -519,9 +485,7 @@ lemma sum_filter_fin_val_ge_eq_sum_fin {β : Type*} [AddCommMonoid β] (n k : 
     constructor
     · intro hi
       use ⟨i.val - k, by omega⟩
-      ext
-      simp
-      omega
+      simp_all
     · rintro ⟨j, _, rfl⟩
       simp
   rw [h_eq, Finset.sum_image]
@@ -541,9 +505,7 @@ lemma sum_last_block_eq_sum_fin {β : Type*} [AddCommMonoid β] (n k : ℕ) (g :
     constructor
     · intro hi
       use ⟨i.val - n, by omega⟩
-      ext
-      simp
-      omega
+      simp_all
     · rintro ⟨j, _, rfl⟩
       simp
   rw [h_eq, Finset.sum_image]
diff --git a/Exchangeability/DeFinetti/MartingaleHelpers.lean b/Exchangeability/DeFinetti/MartingaleHelpers.lean
index 7f30f000..ae72a3cb 100644
--- a/Exchangeability/DeFinetti/MartingaleHelpers.lean
+++ b/Exchangeability/DeFinetti/MartingaleHelpers.lean
@@ -97,8 +97,8 @@ lemma forall_mem_erase {γ : Type*} [DecidableEq γ]
   · rintro ⟨haP, hrest⟩ x hx
     by_cases hxa : x = a
     · simpa [hxa] using haP
-    · have hx' : x ∈ s.erase a := by
-        exact Finset.mem_erase.mpr ⟨hxa, hx⟩
+    · have hx' : x ∈ s.erase a :=
+        Finset.mem_erase.mpr ⟨hxa, hx⟩
       exact hrest _ hx'
 
 end SequenceShift
@@ -156,10 +156,7 @@ lemma strictMono_fin_cases
   | succ i =>
     cases j using Fin.cases with
     | zero =>
-      have : (Fin.succ i : Fin (n + 1)).1 < 0 := by
-        set_option linter.unnecessarySimpa false in
-        simpa [Fin.lt_def] using hij
-      exact absurd this (Nat.not_lt.mpr (Nat.zero_le _))
+      trivial
     | succ j =>
       have hij' : i < j := (Fin.succ_lt_succ_iff).1 hij
       simpa using hf hij'
@@ -185,8 +182,6 @@ lemma indicator_comp_preimage
     {Ω α : Type*} [MeasurableSpace Ω] [MeasurableSpace α]
     (f : Ω → α) (B : Set α) (c : ℝ) :
     (B.indicator (fun _ => c)) ∘ f = (f ⁻¹' B).indicator (fun _ => c) := by
-  ext ω
-  simp only [Function.comp_apply, Set.indicator, Set.mem_preimage]
   rfl
 
 /-- Binary indicator takes values in {0, 1}. -/
@@ -195,9 +190,7 @@ lemma indicator_binary
     {Ω : Type*} [MeasurableSpace Ω]
     (A : Set Ω) (ω : Ω) :
     A.indicator (fun _ => (1 : ℝ)) ω = 0 ∨ A.indicator (fun _ => (1 : ℝ)) ω = 1 := by
-  by_cases h : ω ∈ A
-  · simp [Set.indicator, h]
-  · simp [Set.indicator, h]
+  exact Set.indicator_eq_zero_or_self A (fun x => 1) ω
 
 /-- Indicator is bounded by its constant. -/
 @[nolint unusedArguments]
@@ -215,9 +208,7 @@ lemma indicator_nonneg
     {Ω : Type*} [MeasurableSpace Ω]
     (A : Set Ω) (c : ℝ) (hc : 0 ≤ c) (ω : Ω) :
     0 ≤ A.indicator (fun _ => c) ω := by
-  by_cases h : ω ∈ A
-  · simp [Set.indicator, h, hc]
-  · simp [Set.indicator, h]
+  exact Set.indicator_nonneg (fun a a_1 => hc) ω
 
 end IndicatorAlgebra
 
diff --git a/Exchangeability/DeFinetti/TheoremViaKoopman.lean b/Exchangeability/DeFinetti/TheoremViaKoopman.lean
index fec02117..7fb1624f 100644
--- a/Exchangeability/DeFinetti/TheoremViaKoopman.lean
+++ b/Exchangeability/DeFinetti/TheoremViaKoopman.lean
@@ -88,11 +88,7 @@ lemma exchangeable_path_of_exchangeable
   -- FullyExchangeable → path law is permutation-invariant
   have hPathInv := (fullyExchangeable_iff_pathLaw_invariant hX_meas).mp hFull
   -- μ_path μ X = pathLaw μ X (same definition)
-  intro π
-  -- pathLaw μ X = Measure.map (fun ω i => X i ω) μ
-  -- μ_path μ X = Measure.map (pathify X) μ where pathify X ω n = X n ω
-  -- These are definitionally equal
-  convert hPathInv π using 2
+  assumption
 
 /-- Transfer ConditionallyIID from path space to original space.
 
@@ -192,7 +188,7 @@ theorem conditionallyIID_of_contractable_viaKoopman
     (X : ℕ → Ω → ℝ) (hX_meas : ∀ i, Measurable (X i))
     (hContract : Contractable μ X)
     (hX_L2 : ∀ i, MemLp (X i) 2 μ) :
-    ConditionallyIID μ X := by
-  exact ((deFinetti_RyllNardzewski_equivalence_viaKoopman μ X hX_meas hX_L2).mp hContract).2
+    ConditionallyIID μ X :=
+  ((deFinetti_RyllNardzewski_equivalence_viaKoopman μ X hX_meas hX_L2).mp hContract).2
 
 end Exchangeability.DeFinetti
diff --git a/Exchangeability/DeFinetti/TheoremViaL2.lean b/Exchangeability/DeFinetti/TheoremViaL2.lean
index 999185be..3b6c0188 100644
--- a/Exchangeability/DeFinetti/TheoremViaL2.lean
+++ b/Exchangeability/DeFinetti/TheoremViaL2.lean
@@ -91,8 +91,8 @@ theorem deFinetti_RyllNardzewski_equivalence_viaL2
       ViaL2.directing_measure_satisfies_requirements X hX_meas hContract hX_L2
 
     -- Apply CommonEnding to complete the proof
-    have hCIID : ConditionallyIID μ X := by
-      exact CommonEnding.complete_from_directing_measure X hX_meas hContract ν hν_prob hν_meas h_bridge
+    have hCIID : ConditionallyIID μ X :=
+      CommonEnding.complete_from_directing_measure X hX_meas hContract ν hν_prob hν_meas h_bridge
 
     constructor
     · -- (i) → (ii): Contractable → Exchangeable (via ConditionallyIID)
@@ -138,7 +138,7 @@ theorem conditionallyIID_of_contractable_viaL2
     (X : ℕ → Ω → ℝ) (hX_meas : ∀ i, Measurable (X i))
     (hContract : Contractable μ X)
     (hX_L2 : ∀ i, MemLp (X i) 2 μ) :
-    ConditionallyIID μ X := by
-  exact (deFinetti_RyllNardzewski_equivalence_viaL2 μ X hX_meas hX_L2).mp hContract |>.2
+    ConditionallyIID μ X :=
+  (deFinetti_RyllNardzewski_equivalence_viaL2 μ X hX_meas hX_L2).mp hContract |>.2
 
 end Exchangeability.DeFinetti
diff --git a/Exchangeability/DeFinetti/ViaKoopman.lean b/Exchangeability/DeFinetti/ViaKoopman.lean
index 7166e176..7957b8e9 100644
--- a/Exchangeability/DeFinetti/ViaKoopman.lean
+++ b/Exchangeability/DeFinetti/ViaKoopman.lean
@@ -271,17 +271,11 @@ private theorem conditionallyIID_of_contractable_path
     have h_integrands_eq : ∀ i, (fun ω' : Ω[α] => Set.indicator ((fun ω'' => ω'' 0) ⁻¹' sets i)
         (1 : Ω[α] → ℝ) ω') = (fun ω' => fs i (ω' 0)) := by
       intro i
-      ext ω'
-      -- Both are indicator functions that evaluate to 1 iff ω' 0 ∈ sets i
-      simp only [fs]
       rfl
     have h_rhs_eq : (fun ω => ∏ i : Fin m,
         μ[(fun ω' => Set.indicator ((fun ω'' => ω'' 0) ⁻¹' sets i) (1 : Ω[α] → ℝ) ω') | mSI] ω)
         = (fun ω => ∏ i : Fin m, μ[(fun ω' => fs i (ω' 0)) | mSI] ω) := by
-      ext ω
-      apply Finset.prod_congr rfl
-      intro i _
-      simp only [h_integrands_eq i]
+      rfl
     -- Combine using h_fact
     rw [h_prod_eq, h_rhs_eq]
     exact h_fact
@@ -458,10 +452,8 @@ lemma conditionallyIID_transfer
     have h_rhs : μ.bind (fun ω => Measure.pi fun _ : Fin m => ν ω) =
         (μ.map φ).bind (fun ω => Measure.pi fun _ : Fin m => ν_path ω) := by
       simp only [Measure.bind, ν]
-      have h_pi_meas : Measurable (fun ω' : Ω[α] => Measure.pi fun _ : Fin m => ν_path ω') := by
-        apply measurable_measure_pi
-        · intro ω; exact hν_prob ω
-        · intro s hs; exact hν_meas s hs
+      have h_pi_meas : Measurable (fun ω' : Ω[α] => Measure.pi fun _ : Fin m => ν_path ω') :=
+        measurable_measure_pi ν_path hν_prob hν_meas
       rw [Measure.map_map h_pi_meas hφ_meas]
       rfl
     rw [h_lhs, h_rhs]
@@ -563,22 +555,8 @@ lemma indicator_product_bridge_contractable
   have h_ind_integral : ∀ j ω, ∫ x, fs_σ j x ∂(ν (μ := μ) ω) = ((ν (μ := μ) ω) (B (σ j))).toReal :=
     fun j ω => integral_indicator_one (hB_meas (σ j))
   -- Step 5: Integral at ρ-indices equals integral at consecutive indices
-  have h_ρ_to_consec : ∫ ω, ∏ j, fs_σ j (ω (ρ j)) ∂μ = ∫ ω, ∏ j, fs_σ j (ω j.val) ∂μ := by
-    have hρ_meas : Measurable (fun (ω : Ω[α]) (j : Fin m) => ω (ρ j)) :=
-      by
-        fun_prop
-    have hconsec_meas : Measurable (fun (ω : Ω[α]) (j : Fin m) => ω j.val) :=
-      by
-        fun_prop
-    have hg_meas : Measurable (fun ω' : Fin m → α => ∏ j, fs_σ j (ω' j)) :=
-      Finset.measurable_prod Finset.univ (fun j _ => (hfs_meas j).comp (measurable_pi_apply j))
-    calc ∫ ω, ∏ j, fs_σ j (ω (ρ j)) ∂μ
-        = ∫ ω', (fun ω'' => ∏ j, fs_σ j (ω'' j)) ω' ∂(Measure.map (fun ω j => ω (ρ j)) μ) := by
-            rw [integral_map hρ_meas.aemeasurable hg_meas.aestronglyMeasurable]
-      _ = ∫ ω', (fun ω'' => ∏ j, fs_σ j (ω'' j)) ω' ∂(Measure.map (fun ω j => ω j.val) μ) := by
-            rw [h_contr_ρ]
-      _ = ∫ ω, ∏ j, fs_σ j (ω j.val) ∂μ := by
-            rw [integral_map hconsec_meas.aemeasurable hg_meas.aestronglyMeasurable]
+  have h_ρ_to_consec : ∫ ω, ∏ j, fs_σ j (ω (ρ j)) ∂μ = ∫ ω, ∏ j, fs_σ j (ω j.val) ∂μ :=
+    Eq.symm (integral_prod_reindex_of_contractable hContract fs_σ hfs_meas hfs_bd hρ_mono)
   -- Define auxiliary functions for lintegral conversion
   let F_ρ : Ω[α] → ℝ := fun ω => ∏ j, fs_σ j (ω (ρ j))
   let G : Ω[α] → ℝ := fun ω => ∏ j, ((ν (μ := μ) ω) (B (σ j))).toReal
diff --git a/Exchangeability/DeFinetti/ViaKoopman/BlockAverage.lean b/Exchangeability/DeFinetti/ViaKoopman/BlockAverage.lean
index 4f6709d3..7f13307d 100644
--- a/Exchangeability/DeFinetti/ViaKoopman/BlockAverage.lean
+++ b/Exchangeability/DeFinetti/ViaKoopman/BlockAverage.lean
@@ -82,9 +82,7 @@ lemma blockAvg_eq_cesaro_shifted {m n : ℕ} (hn : 0 < n) (k : Fin m) (f : α 
   apply Finset.sum_congr rfl
   intro j _
   rw [shift_iterate_apply]
-  congr 1
-  -- j + k.val * n = k.val * n + j
-  ring
+  lia
 
 /-! ### Measurability of Block Averages -/
 
@@ -239,11 +237,7 @@ lemma blockAvg_tendsto_condExp
       have h_smeas : StronglyMeasurable (fun ω : Ω[α] => |A n ω - Y ω|) := by
         -- A n is measurable (Cesàro average = const * finite sum of measurable functions)
         have hA_meas : Measurable (A n) := by
-          simp only [A]
-          apply Measurable.const_mul
-          apply Finset.measurable_sum
-          intro j _
-          exact hf.comp (measurable_pi_apply j)
+          fun_prop
         -- Y is the conditional expectation, measurable via shiftInvariantSigma_le
         have hY_meas : Measurable Y :=
           stronglyMeasurable_condExp.measurable.mono (shiftInvariantSigma_le (α := α)) le_rfl
diff --git a/Exchangeability/DeFinetti/ViaKoopman/CesaroHelpers.lean b/Exchangeability/DeFinetti/ViaKoopman/CesaroHelpers.lean
index 5967e130..a0129ef5 100644
--- a/Exchangeability/DeFinetti/ViaKoopman/CesaroHelpers.lean
+++ b/Exchangeability/DeFinetti/ViaKoopman/CesaroHelpers.lean
@@ -105,14 +105,7 @@ lemma condexp_precomp_iterate_eq
         ∫ ω, s.indicator f (shiftk ω) ∂μ
           = ∫ ω, s.indicator (fun ω => f (shiftk ω)) ω ∂μ := by
       refine integral_congr_ae (ae_of_all _ ?_)
-      intro ω
-      by_cases hω : ω ∈ s
-      · have h_shiftk_mem : shiftk ω ∈ s := (h_mem_equiv ω).mpr hω
-        simp [Set.indicator, hω, h_shiftk_mem]
-      · have h_shiftk_mem : shiftk ω ∉ s := by
-          intro hcontr
-          exact hω ((h_mem_equiv ω).mp hcontr)
-        simp [Set.indicator, hω, h_shiftk_mem]
+      exact fun a => Set.indicator_eq_indicator (h_mem_equiv a) rfl
     have h_indicator_eq :
         ∫ ω, s.indicator f ω ∂μ
           = ∫ ω, s.indicator (fun ω => f (shiftk ω)) ω ∂μ :=
@@ -163,9 +156,7 @@ lemma cesaro_ce_eq_condexp
               (Finset.range (n + 1)).sum (fun j => g (ω j))) | mSI] ω) := by
     have h_smul := condExp_smul (μ := μ) (m := mSI) (1 / (n + 1 : ℝ))
       (fun ω => (Finset.range (n + 1)).sum (fun j => g (ω j)))
-    filter_upwards [h_smul] with ω hω
-    simp only [A, Pi.smul_apply, smul_eq_mul] at hω ⊢
-    exact hω
+    assumption
 
   -- Push CE through the finite sum
   have h_sum :
diff --git a/Exchangeability/DeFinetti/ViaKoopman/CesaroL1Bounded.lean b/Exchangeability/DeFinetti/ViaKoopman/CesaroL1Bounded.lean
index 86a1cb2c..df97a489 100644
--- a/Exchangeability/DeFinetti/ViaKoopman/CesaroL1Bounded.lean
+++ b/Exchangeability/DeFinetti/ViaKoopman/CesaroL1Bounded.lean
@@ -125,11 +125,7 @@ lemma L1_cesaro_convergence
     have hM' : |g x| < (M : ℝ) := by
       have : (Nat.ceil |g x| : ℝ) < M := by exact_mod_cast hM
       exact lt_of_le_of_lt (Nat.le_ceil _) this
-    simp [g_M]
-    have h_abs : -(M : ℝ) < g x ∧ g x < (M : ℝ) := abs_lt.mp hM'
-    have h1 : -(M : ℝ) < g x := h_abs.1
-    have h2 : g x < (M : ℝ) := h_abs.2
-    simp [min_eq_left (le_of_lt h2), max_eq_left (le_of_lt h1)]
+    grind only [= abs.eq_1, = max_def, = min_def]
 
   -- For each ω, ∫|g(ω j) - g_M M (ω j)| → 0
   have h_trunc_L1 : Tendsto (fun M => ∫ ω, |g (ω 0) - g_M M (ω 0)| ∂μ) atTop (𝓝 0) := by
@@ -174,9 +170,7 @@ lemma L1_cesaro_convergence
       ((hg_meas.comp (measurable_pi_apply 0)).sub
         ((hg_M_meas M).comp (measurable_pi_apply 0))).norm.aestronglyMeasurable
     have h_dom' : ∀ M, (fun ω => ‖g (ω 0) - g_M M (ω 0)‖) ≤ᵐ[μ] (fun ω => 2 * ‖g (ω 0)‖) := by
-      intro M
-      filter_upwards [h_dom M] with ω h
-      simpa [Real.norm_eq_abs] using h
+      assumption
     have h_point' : ∀ᵐ ω ∂μ, Tendsto (fun M => ‖g (ω 0) - g_M M (ω 0)‖) atTop (𝓝 0) := by
       filter_upwards [h_point] with ω h
       simpa [Real.norm_eq_abs] using h
diff --git a/Exchangeability/DeFinetti/ViaKoopman/CesaroL2ToL1.lean b/Exchangeability/DeFinetti/ViaKoopman/CesaroL2ToL1.lean
index 4c2b8f0a..be61811b 100644
--- a/Exchangeability/DeFinetti/ViaKoopman/CesaroL2ToL1.lean
+++ b/Exchangeability/DeFinetti/ViaKoopman/CesaroL2ToL1.lean
@@ -99,9 +99,7 @@ lemma eventuallyEq_comp_measurePreserving {f g : Ω[α] → ℝ}
 @[nolint unusedArguments]
 lemma MeasurePreserving.iterate' (hT : MeasurePreserving shift μ μ) (k : ℕ) :
     MeasurePreserving (shift^[k]) μ μ := by
-  induction k with
-  | zero => exact MeasurePreserving.id μ
-  | succ k ih => simp only [Function.iterate_succ']; exact hT.comp ih
+  exact MeasurePreserving.iterate hT k
 
 /-- General evaluation formula for shift iteration. -/
 @[nolint unusedArguments]
@@ -220,9 +218,7 @@ lemma optionB_Step3b_L2_to_L1
         have h_memLp1 : MemLp f 1 μ := by
           refine ⟨h_memLp2.aestronglyMeasurable, ?_⟩
           calc eLpNorm f 1 μ ≤ eLpNorm f 2 μ := by
-                apply eLpNorm_le_eLpNorm_of_exponent_le
-                · norm_num
-                · exact h_memLp2.aestronglyMeasurable
+                assumption
              _ < ⊤ := h_memLp2.eLpNorm_lt_top
         exact memLp_one_iff_integrable.mp h_memLp1
       -- Apply eLpNorm_one_le_eLpNorm_two_toReal
@@ -474,9 +470,7 @@ lemma optionB_Step4c_triangle
           rw [hB_def]
           simp [hn]
           -- (1/n) * ∑_{j < n} g(ω j) is measurable
-          refine Measurable.const_mul ?_ _
-          refine Finset.measurable_sum (Finset.range n) (fun j _ => ?_)
-          exact Measurable.comp hg_meas (measurable_pi_apply j)
+          fun_prop
         have hB_bd_ae : ∀ᵐ ω ∂μ, ‖B n ω‖ ≤ Cg := ae_of_all μ (fun ω => le_trans (Real.norm_eq_abs _).le (hB_bd ω))
         exact ⟨hB_meas.aestronglyMeasurable, HasFiniteIntegral.of_bounded hB_bd_ae⟩
     -- |B n - Y| is integrable as difference of integrable functions
@@ -540,18 +534,13 @@ lemma optionB_Step4c_triangle
             _ = 2 * Cg := by ring
       have hA_meas : Measurable (A n) := by
         rw [hA_def]
-        simp
-        refine Measurable.const_mul ?_ _
-        refine Finset.measurable_sum (Finset.range (n + 1)) (fun j _ => ?_)
-        exact Measurable.comp hg_meas (measurable_pi_apply j)
+        fun_prop
       have hB_meas : Measurable (B n) := by
         rw [hB_def]
         by_cases hn : n = 0
         · simp [hn]
         · simp [hn]
-          refine Measurable.const_mul ?_ _
-          refine Finset.measurable_sum (Finset.range n) (fun j _ => ?_)
-          exact Measurable.comp hg_meas (measurable_pi_apply j)
+          fun_prop
       have hAB_bd_ae : ∀ᵐ ω ∂μ, ‖|A n ω - B n ω|‖ ≤ 2 * Cg :=
         ae_of_all μ (fun ω => by simp [Real.norm_eq_abs]; exact hAB_bd ω)
       exact ⟨(hA_meas.sub hB_meas).norm.aestronglyMeasurable, HasFiniteIntegral.of_bounded hAB_bd_ae⟩
@@ -751,8 +740,8 @@ theorem optionB_L1_convergence_bounded
     -- Use helper lemma: condexpL2 = condExp a.e.
     have h1 := condexpL2_ae_eq_condExp fL2
     -- condExp preserves a.e. equality
-    have h2 : μ[fL2 | mSI] =ᵐ[μ] μ[G | mSI] := by
-      exact MeasureTheory.condExp_congr_ae hfL2_eq
+    have h2 : μ[fL2 | mSI] =ᵐ[μ] μ[G | mSI] :=
+      MeasureTheory.condExp_congr_ae hfL2_eq
     simp only [Y]
     exact h1.trans h2
 
@@ -773,10 +762,7 @@ theorem optionB_L1_convergence_bounded
     have hG_meas : Measurable G := by
       simp only [G]
       exact hg_meas.comp (measurable_pi_apply 0)
-    have hG_bd_ae : ∀ᵐ ω ∂μ, ‖G ω‖ ≤ Cg := ae_of_all μ (fun ω => by
-      simp [G, Real.norm_eq_abs]
-      exact hCg_bd (ω 0))
-    exact ⟨hG_meas.aestronglyMeasurable, HasFiniteIntegral.of_bounded hG_bd_ae⟩
+    exact integrable_of_bounded_measurable hG_meas Cg fun ω => hCg_bd (ω 0)
 
   have hY_int : Integrable Y μ := by
     -- Y = μ[G | mSI], and condExp preserves integrability
diff --git a/Exchangeability/DeFinetti/ViaKoopman/CylinderFunctions.lean b/Exchangeability/DeFinetti/ViaKoopman/CylinderFunctions.lean
index 9b648ecf..93626905 100644
--- a/Exchangeability/DeFinetti/ViaKoopman/CylinderFunctions.lean
+++ b/Exchangeability/DeFinetti/ViaKoopman/CylinderFunctions.lean
@@ -84,13 +84,8 @@ lemma productCylinder_bounded {m : ℕ} {fs : Fin m → α → ℝ}
     have := hbound k (ω k.val)
     exact this.trans (le_max_left _ _)
   have h_nonneg : ∀ k : Fin m, 0 ≤ |fs k (ω k.val)| := fun _ => abs_nonneg _
-  have hprod : ∏ k : Fin m, |fs k (ω k.val)| ≤ ∏ k : Fin m, C k := by
-    simpa using
-      (Finset.prod_le_prod (s := Finset.univ)
-        (f := fun k : Fin m => |fs k (ω k.val)|)
-        (g := fun k : Fin m => C k)
-        (fun k _ => h_nonneg k)
-        (fun k _ => h_abs_le k))
+  have hprod : ∏ k : Fin m, |fs k (ω k.val)| ≤ ∏ k : Fin m, C k :=
+    Finset.prod_le_prod (fun i a => h_nonneg i) fun i a => h_abs_le i
   have habs_eq : |productCylinder fs ω| = ∏ k : Fin m, |fs k (ω k.val)| := by
     simp [productCylinder, Finset.abs_prod]
   exact (by simpa [habs_eq] using hprod)
diff --git a/Exchangeability/DeFinetti/ViaKoopman/InfraCore.lean b/Exchangeability/DeFinetti/ViaKoopman/InfraCore.lean
index 29156fab..d83ee60a 100644
--- a/Exchangeability/DeFinetti/ViaKoopman/InfraCore.lean
+++ b/Exchangeability/DeFinetti/ViaKoopman/InfraCore.lean
@@ -404,9 +404,7 @@ lemma ae_pullback_iff
         rw [hmp.measure_preimage hSmeas.nullMeasurableSet]
         exact this
       -- identify the preimage set with the set for the composed functions
-      have : μ' {x' | (Fm ∘ g) x' ≠ (Gm ∘ g) x'} = 0 := by
-        simpa using this
-      exact (ae_iff).2 this
+      assumption
     · intro h
       have : μ' {x' | (Fm ∘ g) x' ≠ (Gm ∘ g) x'} = 0 := (ae_iff).1 h
       -- convert back using the same preimage identity and measure-preserving fact
diff --git a/Exchangeability/DeFinetti/ViaKoopman/InfraGeneralized.lean b/Exchangeability/DeFinetti/ViaKoopman/InfraGeneralized.lean
index 405074c1..f2c4c397 100644
--- a/Exchangeability/DeFinetti/ViaKoopman/InfraGeneralized.lean
+++ b/Exchangeability/DeFinetti/ViaKoopman/InfraGeneralized.lean
@@ -279,10 +279,7 @@ lemma Integrable.of_abs_bounded {Ω : Type*} [MeasurableSpace Ω] {μ : Measure
       _ ≤ C * |g ω| := mul_le_mul_of_nonneg_right (h_bound ω) (abs_nonneg _)
   -- Use Integrable.mono' with dominating function C * |g|
   refine Integrable.mono' (hg.norm.const_mul C) hfg_meas ?_
-  filter_upwards with ω
-  simp only [Real.norm_eq_abs, Pi.mul_apply, abs_of_nonneg hC]
-  calc |f ω * g ω| = |f ω| * |g ω| := abs_mul _ _
-    _ ≤ C * |g ω| := mul_le_mul_of_nonneg_right (h_bound ω) (abs_nonneg _)
+  assumption
 
 /-- **Generalized lag-constancy for products** (extends `condexp_lag_constant_from_exchangeability`).
 
diff --git a/Exchangeability/DeFinetti/ViaKoopman/InfraLagConstancy.lean b/Exchangeability/DeFinetti/ViaKoopman/InfraLagConstancy.lean
index 5f6850cf..5be86c20 100644
--- a/Exchangeability/DeFinetti/ViaKoopman/InfraLagConstancy.lean
+++ b/Exchangeability/DeFinetti/ViaKoopman/InfraLagConstancy.lean
@@ -355,11 +355,7 @@ lemma disjointOffsetSwap_id_beyond (S : Finset ℕ) (offset : ℕ) (hS : ∀ i 
     (n : ℕ) (hn : S.sup id + offset < n) : disjointOffsetSwap S offset hS n = n := by
   simp only [disjointOffsetSwap, Equiv.coe_fn_mk]
   have h1 : n ∉ S := by
-    intro habs
-    have hsup : (id n : ℕ) ≤ S.sup id := Finset.le_sup (f := id) habs
-    simp only [id_eq] at hsup
-    have : n ≤ S.sup id := hsup
-    linarith
+    grind only
   simp only [h1, ↓reduceIte]
   split_ifs with h
   · exfalso
diff --git a/Exchangeability/DeFinetti/ViaKoopman/KernelBridge.lean b/Exchangeability/DeFinetti/ViaKoopman/KernelBridge.lean
index 4e39becf..d406f558 100644
--- a/Exchangeability/DeFinetti/ViaKoopman/KernelBridge.lean
+++ b/Exchangeability/DeFinetti/ViaKoopman/KernelBridge.lean
@@ -201,22 +201,7 @@ lemma Kernel.IndepFun.comp
   -- For sets s, t in the target σ-algebras, we need to show:
   -- ∀ s ∈ σ(f∘X), ∀ t ∈ σ(g∘Y), ∀ᵐ a, κ a (s ∩ t) = κ a s * κ a t
 
-  intro s t hs ht
-  -- s is measurable w.r.t. comap (f ∘ X), so s = (f ∘ X)⁻¹(S) for some measurable S ⊆ ℝ
-  -- This means s = X⁻¹(f⁻¹(S)), so s is in comap X
-  -- Similarly t is in comap Y
-
-  -- We need to show s ∈ comap X and t ∈ comap Y
-  -- Key fact: if s is measurable w.r.t. comap (f ∘ X), then s is measurable w.r.t. comap X
-  -- because comap (f ∘ X) ≤ comap X
-
-  have hs' : MeasurableSet[MeasurableSpace.comap X inferInstance] s :=
-    comap_comp_le X f hf s hs
-
-  have ht' : MeasurableSet[MeasurableSpace.comap Y inferInstance] t :=
-    comap_comp_le Y g hg t ht
-
-  exact hXY s t hs' ht'
+  exact ProbabilityTheory.Kernel.IndepFun.comp hXY hf hg
 
 /-- **Bridge lemma**: The Mean Ergodic Theorem projection equals conditional expectation
 onto the shift-invariant σ-algebra.
diff --git a/Exchangeability/DeFinetti/ViaKoopman/KoopmanCommutation.lean b/Exchangeability/DeFinetti/ViaKoopman/KoopmanCommutation.lean
index 71ff8601..ca97ccc5 100644
--- a/Exchangeability/DeFinetti/ViaKoopman/KoopmanCommutation.lean
+++ b/Exchangeability/DeFinetti/ViaKoopman/KoopmanCommutation.lean
@@ -77,26 +77,7 @@ theorem birkhoffAverage_tendsto_condexp (f : Lp ℝ 2 μ) :
   have hP_eq : P = condexpL2 (μ := μ) := by
     -- Both P and condexpL2 are orthogonal projections onto the fixed subspace
     -- Use uniqueness of symmetric idempotent projections with the same range
-    have h_range_P : Set.range P = (fixedSubspace hσ : Set (Lp ℝ 2 μ)) :=
-      metProjectionShift_range_fixedSubspace (μ := μ) hσ
-    have h_range_condexp : Set.range (condexpL2 (μ := μ)) =
-        (fixedSubspace hσ : Set (Lp ℝ 2 μ)) := range_condexp_eq_fixedSubspace hσ
-    have hQ_fixes : ∀ g ∈ fixedSubspace hσ, condexpL2 (μ := μ) g = g :=
-      fun g hg => condexpL2_fixes_fixedSubspace (hσ := hσ) hg
-    have hP_idem : P.comp P = P := metProjectionShift_idem (μ := μ) hσ
-    have hQ_idem : (condexpL2 (μ := μ)).comp (condexpL2 (μ := μ)) = condexpL2 (μ := μ) :=
-      condexpL2_idem (μ := μ)
-    have hP_sym : P.IsSymmetric := metProjectionShift_isSymmetric (μ := μ) hσ
-    have hQ_sym : (condexpL2 (μ := μ)).IsSymmetric := by
-      intro f g
-      unfold condexpL2
-      exact MeasureTheory.inner_condExpL2_left_eq_right shiftInvariantSigma_le
-    haveI : (fixedSubspace hσ).HasOrthogonalProjection := by
-      have hclosed := fixedSubspace_closed hσ
-      have : CompleteSpace (fixedSubspace hσ) := hclosed.completeSpace_coe
-      exact Submodule.HasOrthogonalProjection.ofCompleteSpace (fixedSubspace hσ)
-    exact orthogonalProjections_same_range_eq P (condexpL2 (μ := μ)) (fixedSubspace hσ)
-      h_range_P h_range_condexp hP_fixed hQ_fixes hP_idem hQ_idem hP_sym hQ_sym
+    exact proj_eq_condexp hσ
 
   -- Step 3: Conclude using equality
   rw [← hP_eq]
@@ -455,35 +436,7 @@ theorem birkhoffCylinder_tendsto_condexp
   · exact productCylinderLp_ae_eq (μ := μ) (fs := fs) hmeas hbd
   -- Second conjunct: convergence to condexpL2
   · -- Apply Mean Ergodic Theorem from KoopmanMeanErgodic.lean
-    have h_met := Exchangeability.Ergodic.birkhoffAverage_tendsto_metProjection
-      shift hσ (productCylinderLp (μ := μ) (fs := fs) hmeas hbd)
-    -- Now we need to show metProjection shift hσ (productCylinderLp ...) = condexpL2 (productCylinderLp ...)
-    -- Both metProjection and metProjectionShift are orthogonal projections onto fixedSpace (koopman shift hσ)
-    -- Since fixedSubspace hσ = fixedSpace (koopman shift hσ) by definition
-    -- The proj_eq_condexp theorem shows metProjectionShift hσ = condexpL2
-
-    -- Key insight: metProjection shift hσ and metProjectionShift hσ are both orthogonal projections
-    -- onto the same closed subspace fixedSpace (koopman shift hσ), so they must be equal
-    -- by uniqueness of orthogonal projections.
-
-    -- Both metProjection and metProjectionShift are orthogonal projections onto fixedSpace (koopman shift hσ)
-    -- Since fixedSubspace hσ = fixedSpace (koopman shift hσ) by definition,
-    -- they are projections onto the same subspace and must be equal by uniqueness.
-    have h_proj_eq : Exchangeability.Ergodic.metProjection shift hσ =
-        Exchangeability.DeFinetti.metProjectionShift hσ := by
-      -- Both are defined as S.subtypeL.comp S.orthogonalProjection for the same subspace S
-      -- The orthogonal projection is unique, so they must be equal
-      ext f
-      simp only [Exchangeability.Ergodic.metProjection, Exchangeability.DeFinetti.metProjectionShift]
-      -- Both reduce to orthogonal projection onto fixedSpace (koopman shift hσ) = fixedSubspace hσ
-      rfl
-
-    -- Apply proj_eq_condexp
-    have h_cond := Exchangeability.DeFinetti.proj_eq_condexp (μ := μ) hσ
-
-    -- Rewrite the goal using these equalities
-    rw [← h_cond, ← h_proj_eq]
-    exact h_met
+    exact birkhoffAverage_tendsto_condexp hσ (productCylinderLp fs hmeas hbd)
 
 end MainConvergence
 
diff --git a/Exchangeability/DeFinetti/ViaKoopman/Quantization.lean b/Exchangeability/DeFinetti/ViaKoopman/Quantization.lean
index 29cbbc6a..fe6f7fe7 100644
--- a/Exchangeability/DeFinetti/ViaKoopman/Quantization.lean
+++ b/Exchangeability/DeFinetti/ViaKoopman/Quantization.lean
@@ -47,11 +47,7 @@ lemma quantize_err_le {C ε x : ℝ} (hε : 0 < ε) :
   have h2 : v < ((⌊v / ε⌋ : ℝ) + 1) * ε := by
     calc v = (v / ε) * ε := by field_simp
        _ < ((⌊v / ε⌋ : ℝ) + 1) * ε := by nlinarith [hε, h_ceil]
-  have h3 : v - (⌊v / ε⌋ : ℝ) * ε < ε := by linarith
-  rw [abs_sub_le_iff]
-  constructor
-  · linarith
-  · linarith
+  grind only [= abs.eq_1, = max_def]
 
 /-- Quantized values are bounded by C + 1 when ε ≤ 1. -/
 lemma quantize_abs_le {C ε x : ℝ} (hC : 0 ≤ C) (hε : 0 < ε) (hε1 : ε ≤ 1) :
diff --git a/Exchangeability/DeFinetti/ViaL2/AlphaConvergence.lean b/Exchangeability/DeFinetti/ViaL2/AlphaConvergence.lean
index 35a4ae02..60694252 100644
--- a/Exchangeability/DeFinetti/ViaL2/AlphaConvergence.lean
+++ b/Exchangeability/DeFinetti/ViaL2/AlphaConvergence.lean
@@ -154,11 +154,7 @@ lemma alphaIic_ae_eq_alphaIicCE
     -- Prove integrability of A n m
     have hA_int : Integrable (A n m) μ := by
       have hA_meas_nm : Measurable (A n m) := by
-        simp only [A]
-        apply Measurable.const_mul
-        apply Finset.measurable_sum
-        intro k _
-        exact (indIic_measurable t).comp (hX_meas _)
+        fun_prop
       refine Integrable.of_bound hA_meas_nm.aestronglyMeasurable 1 ?_
       filter_upwards with ω
       unfold A
@@ -562,9 +558,7 @@ lemma alphaIic_ae_eq_alphaIicCE
     -- A n m is a Cesàro average of indIic ∘ X, which are measurable
     -- Each indIic ∘ X_i is measurable, sum is measurable, scalar mult is measurable
     refine Measurable.aestronglyMeasurable ?_
-    show Measurable fun ω => (1 / (m : ℝ)) * ∑ k : Fin m, indIic t (X (n + k.val + 1) ω)
-    refine Measurable.const_mul ?_ _
-    exact Finset.measurable_sum _ (fun k _ => (indIic_measurable t).comp (hX_meas _))
+    fun_prop
 
   -- Step 3: Use uniqueness of L¹ limits to conclude a.e. equality
   -- If both f and g are L¹ limits of the same sequence, then f =ᵐ g
@@ -776,8 +770,6 @@ lemma alphaIicCE_L1_tendsto_zero_atBot
       -- Rewrite composition as indicator on preimage
       have h_comp : (indIic (-(n : ℝ))) ∘ (X 0)
           = (X 0 ⁻¹' Set.Iic (-(n : ℝ))).indicator (fun _ => (1 : ℝ)) := by
-        ext ω
-        simp only [indIic, Function.comp_apply, Set.indicator_apply]
         rfl
       rw [h_comp, integral_indicator (measurableSet_preimage (hX_meas 0) measurableSet_Iic),
           setIntegral_one_eq_measureReal]
@@ -878,8 +870,6 @@ lemma alphaIicCE_L1_tendsto_one_atTop
       -- Rewrite composition as indicator on preimage
       have h_comp : (Set.Ioi (n : ℝ)).indicator (fun _ => (1 : ℝ)) ∘ (X 0)
           = (X 0 ⁻¹' Set.Ioi (n : ℝ)).indicator (fun _ => (1 : ℝ)) := by
-        ext ω
-        simp only [Function.comp_apply, Set.indicator_apply]
         rfl
       rw [h_comp, integral_indicator (measurableSet_preimage (hX_meas 0) measurableSet_Ioi),
           setIntegral_one_eq_measureReal]
@@ -1263,61 +1253,22 @@ lemma alphaIicCE_ae_tendsto_one_atTop
       use 0
       intro n _
       -- Show: 1 - ∫ (1 - f) = ∫ f
-      have h_f_int : Integrable (fun ω => alphaIicCE X hX_contract hX_meas hX_L2 (n : ℝ) ω) μ := by
-        refine Integrable.of_bound (stronglyMeasurable_condExp.aestronglyMeasurable.mono hm_le) 1 ?_
-        filter_upwards [alphaIicCE_nonneg_le_one X hX_contract hX_meas hX_L2 (n : ℝ)] with ω hω
-        rw [Real.norm_eq_abs, abs_of_nonneg hω.1]
-        exact hω.2
+      have h_f_int : Integrable (fun ω => alphaIicCE X hX_contract hX_meas hX_L2 (n : ℝ) ω) μ :=
+        Integrable.mono' h_int (h_meas n) (h_bound_ae n)
       calc 1 - ∫ ω, (1 - alphaIicCE X hX_contract hX_meas hX_L2 (n : ℝ) ω) ∂μ
           = 1 - (∫ ω, 1 ∂μ - ∫ ω, alphaIicCE X hX_contract hX_meas hX_L2 (n : ℝ) ω ∂μ) := by
               rw [integral_sub (integrable_const 1) h_f_int]
           _ = 1 - (μ.real Set.univ - ∫ ω, alphaIicCE X hX_contract hX_meas hX_L2 (n : ℝ) ω ∂μ) := by
               rw [integral_const, smul_eq_mul, mul_one]
           _ = 1 - (1 - ∫ ω, alphaIicCE X hX_contract hX_meas hX_L2 (n : ℝ) ω ∂μ) := by
-              simp only [Measure.real]
-              rw [measure_univ]
-              simp
+              norm_num
           _ = ∫ ω, alphaIicCE X hX_contract hX_meas hX_L2 (n : ℝ) ω ∂μ := by ring
     rw [← tendsto_nhds_unique h_lim h_int_conv]
 
   -- Conclude U_fun = 1 a.e.
   have hU_ae_one : U_fun =ᵐ[μ] 1 := by
     have hU_int : Integrable U_fun μ := by
-      have hU_nonneg : 0 ≤ᵐ[μ] U_fun := by
-        filter_upwards [h_bound] with ω h_bound_ω
-        -- U_fun ω = sup of values all ≥ 0, so U_fun ω ≥ value at 0 ≥ 0
-        refine le_trans ?_ (le_ciSup ⟨1, fun y hy => by obtain ⟨k, hk⟩ := hy; rw [← hk]; exact (h_bound_ω k).2⟩ (0 : ℕ))
-        exact (h_bound_ω 0).1
-      have hU_bound : ∀ᵐ ω ∂μ, ‖U_fun ω‖ ≤ 1 := by
-        filter_upwards [hU_nonneg, h_bound] with ω hω_nn h_bound_ω
-        rw [Real.norm_eq_abs, abs_of_nonneg hω_nn]
-        -- U_fun ω = ⨆ n, f(n) where each f(n) ≤ 1, so U_fun ω ≤ 1
-        -- Use that 1 is an upper bound for all values
-        calc U_fun ω
-            = ⨆ (n : ℕ), alphaIicCE X hX_contract hX_meas hX_L2 (n : ℝ) ω := rfl
-          _ ≤ 1 := by
-              apply ciSup_le
-              intro n
-              exact (h_bound_ω n).2
-      have hU_meas : AEStronglyMeasurable U_fun μ := by
-        -- Each alphaIicCE (n:ℝ) is AEStronglyMeasurable (conditional expectation)
-        have h_meas_n : ∀ (n : ℕ), AEStronglyMeasurable (fun ω => alphaIicCE X hX_contract hX_meas hX_L2 (n : ℝ) ω) μ := by
-          intro n
-          unfold alphaIicCE
-          exact stronglyMeasurable_condExp.aestronglyMeasurable.mono hm_le
-        -- They converge a.e. to U_fun (by monotone convergence)
-        have h_conv_ae_n : ∀ᵐ ω ∂μ, Tendsto (fun (n : ℕ) => alphaIicCE X hX_contract hX_meas hX_L2 (n : ℝ) ω)
-            atTop (𝓝 (U_fun ω)) := by
-          filter_upwards [h_ae_conv, h_bound, h_mono] with ω ⟨L, hL⟩ h_bound_ω h_mono_ω
-          have hU_is_sup : L = U_fun ω := by
-            apply tendsto_nhds_unique hL
-            apply tendsto_atTop_ciSup h_mono_ω
-            exact ⟨1, fun y hy => by obtain ⟨k, hk⟩ := hy; rw [← hk]; exact (h_bound_ω k).2⟩
-          rw [← hU_is_sup]
-          exact hL
-        -- Apply aestronglyMeasurable_of_tendsto_ae
-        exact aestronglyMeasurable_of_tendsto_ae atTop h_meas_n h_conv_ae_n
-      exact Integrable.of_bound hU_meas 1 hU_bound
+      exact integrable_of_integral_eq_one hU_integral_one
     -- Show U_fun = 1 a.e. by showing 1 - U_fun = 0 a.e.
     have h_diff_nonneg : 0 ≤ᵐ[μ] fun ω => 1 - U_fun ω := by
       filter_upwards [hU_le_one] with ω hω
diff --git a/Exchangeability/DeFinetti/ViaL2/AlphaIic.lean b/Exchangeability/DeFinetti/ViaL2/AlphaIic.lean
index 323558df..50b748d8 100644
--- a/Exchangeability/DeFinetti/ViaL2/AlphaIic.lean
+++ b/Exchangeability/DeFinetti/ViaL2/AlphaIic.lean
@@ -92,8 +92,8 @@ lemma alphaIic_measurable
   -- alphaIic is max 0 (min 1 limit) where limit is measurable
   unfold alphaIic
   have h_limit_meas : Measurable (weighted_sums_converge_L1 X hX_contract hX_meas hX_L2
-            (indIic t) (indIic_measurable t) ⟨1, indIic_bdd t⟩).choose := by
-    exact (weighted_sums_converge_L1 X hX_contract hX_meas hX_L2
+            (indIic t) (indIic_measurable t) ⟨1, indIic_bdd t⟩).choose :=
+    (weighted_sums_converge_L1 X hX_contract hX_meas hX_L2
             (indIic t) (indIic_measurable t) ⟨1, indIic_bdd t⟩).choose_spec.1
   -- max and min preserve measurability: max 0 (min 1 limit)
   -- Build: min limit 1, then max 0 result
diff --git a/Exchangeability/DeFinetti/ViaL2/AlphaIicCE.lean b/Exchangeability/DeFinetti/ViaL2/AlphaIicCE.lean
index 0d35ba35..3c25d540 100644
--- a/Exchangeability/DeFinetti/ViaL2/AlphaIicCE.lean
+++ b/Exchangeability/DeFinetti/ViaL2/AlphaIicCE.lean
@@ -336,17 +336,8 @@ lemma alphaIicCE_right_continuous_at
       push_neg at hxt
       simp only [Set.indicator_apply, Set.mem_Iic, not_le.mpr hxt, ↓reduceIte]
       -- u_n → t and X 0 ω > t, so eventually u_n < X 0 ω
-      have h_ev : ∀ᶠ n in Filter.atTop, (u n : ℝ) < X 0 ω := by
-        have : Filter.Tendsto (fun n => (u n : ℝ)) Filter.atTop (nhds t) := u_tendsto
-        rw [Metric.tendsto_atTop] at this
-        specialize this ((X 0 ω) - t) (by linarith)
-        obtain ⟨N, hN⟩ := this
-        apply Filter.eventually_atTop.mpr
-        use N
-        intro n hn
-        specialize hN n hn
-        rw [Real.dist_eq, abs_lt] at hN
-        linarith
+      have h_ev : ∀ᶠ n in Filter.atTop, (u n : ℝ) < X 0 ω :=
+        Tendsto.eventually_lt_const hxt u_tendsto
       apply Filter.Tendsto.congr' _ tendsto_const_nhds
       filter_upwards [h_ev] with n hn
       simp only [Set.mem_Iic, not_le.mpr hn, ↓reduceIte]
@@ -410,12 +401,7 @@ lemma alphaIicCE_right_continuous_at
     -- h_eq: condExpL1(fs n) ω = alphaIicCE (u n) ω for all n
     -- h_eq_lim: condExpL1(f) ω = alphaIicCE t ω
     rw [← h_eq_lim]
-    have h_eq_fun : (fun n => (↑(condExpL1 hm_le μ (fs (ns n))) : Ω → ℝ) ω) =
-        (fun n => alphaIicCE X hX_contract hX_meas hX_L2 (u (ns n) : ℝ) ω) := by
-      ext n
-      exact h_eq (ns n)
-    rw [← h_eq_fun]
-    exact h_conv
+    exact Tendsto.congr (fun x => h_eq (ns x)) h_conv
 
   -- 3j: The sequence alphaIicCE (u_n) is antitone (since u_n is decreasing and alphaIicCE is monotone)
   have h_antitone_ae : ∀ᵐ ω ∂μ, ∀ m n : ℕ, m ≤ n →
@@ -481,9 +467,7 @@ lemma alphaIicCE_right_continuous_at
       -- The limit is unique
       exact tendsto_nhds_unique h_conv_to_inf h_conv
 
-    calc ⨅ n : ℕ, alphaIicCE X hX_contract hX_meas hX_L2 (u n : ℝ) ω
-        ≤ ⨅ k : ℕ, alphaIicCE X hX_contract hX_meas hX_L2 (u (ns k) : ℝ) ω := h1
-      _ = alphaIicCE X hX_contract hX_meas hX_L2 t ω := h2
+    exact le_of_le_of_eq h1 h2
 
   -- Step 4: Combine everything
   filter_upwards [h_infs_le_ae, h_inf_le_lim] with ω h_infs_le h_inf
@@ -668,10 +652,7 @@ lemma alphaIicCE_iInf_rat_gt_eq
           have hr' : q < r := by exact_mod_cast hr
           have h_bdd_below : BddBelow (Set.range fun s : Set.Ioi q =>
               alphaIicCE X hX_contract hX_meas hX_L2 (s : ℝ) ω) := by
-            use 0
-            intro x hx
-            obtain ⟨s, rfl⟩ := hx
-            exact (h_bdd s.val).1
+            assumption
           exact ciInf_le h_bdd_below ⟨r, hr'⟩
       _ ≤ alphaIicCE X hX_contract hX_meas hX_L2 (q : ℝ) ω := h_right_cont
 
diff --git a/Exchangeability/DeFinetti/ViaL2/BlockAverages.lean b/Exchangeability/DeFinetti/ViaL2/BlockAverages.lean
index 21a95ce4..715a0d57 100644
--- a/Exchangeability/DeFinetti/ViaL2/BlockAverages.lean
+++ b/Exchangeability/DeFinetti/ViaL2/BlockAverages.lean
@@ -130,14 +130,10 @@ lemma contractable_covariance_structure
     -- Use contractable_single_marginal_eq to show X_k has same distribution as X_0
     have h_eq_dist := contractable_single_marginal_eq (X := X) hX_contract hX_meas k
     -- Transfer integral via equal distributions
-    have h_int_k : ∫ ω, X k ω ∂μ = ∫ x, x ∂(Measure.map (X k) μ) := by
-      have h_ae : AEStronglyMeasurable (id : ℝ → ℝ) (Measure.map (X k) μ) :=
-        aestronglyMeasurable_id
-      exact (integral_map (hX_meas k).aemeasurable h_ae).symm
-    have h_int_0 : ∫ ω, X 0 ω ∂μ = ∫ x, x ∂(Measure.map (X 0) μ) := by
-      have h_ae : AEStronglyMeasurable (id : ℝ → ℝ) (Measure.map (X 0) μ) :=
-        aestronglyMeasurable_id
-      exact (integral_map (hX_meas 0).aemeasurable h_ae).symm
+    have h_int_k : ∫ ω, X k ω ∂μ = ∫ x, x ∂(Measure.map (X k) μ) :=
+      Eq.symm (Probability.IntegrationHelpers.integral_pushforward_id (hX_meas k))
+    have h_int_0 : ∫ ω, X 0 ω ∂μ = ∫ x, x ∂(Measure.map (X 0) μ) :=
+      Eq.symm (Probability.IntegrationHelpers.integral_pushforward_id (hX_meas 0))
     rw [h_int_k, h_eq_dist, ← h_int_0]
 
   -- Define σSq as the variance of X_0
@@ -152,14 +148,10 @@ lemma contractable_covariance_structure
     -- The variance with k's mean equals variance with m (since they're equal)
     show ∫ ω, (X k ω - m)^2 ∂μ = σSq
     -- Transform X_k integral to X_0 integral via measure map
-    have h_int_k : ∫ ω, (X k ω - m)^2 ∂μ = ∫ x, (x - m)^2 ∂(Measure.map (X k) μ) := by
-      have h_ae : AEStronglyMeasurable (fun x : ℝ => (x - m)^2) (Measure.map (X k) μ) := by
-        exact (continuous_id.sub continuous_const).pow 2 |>.aestronglyMeasurable
-      exact (integral_map (hX_meas k).aemeasurable h_ae).symm
-    have h_int_0 : ∫ ω, (X 0 ω - m)^2 ∂μ = ∫ x, (x - m)^2 ∂(Measure.map (X 0) μ) := by
-      have h_ae : AEStronglyMeasurable (fun x : ℝ => (x - m)^2) (Measure.map (X 0) μ) := by
-        exact (continuous_id.sub continuous_const).pow 2 |>.aestronglyMeasurable
-      exact (integral_map (hX_meas 0).aemeasurable h_ae).symm
+    have h_int_k : ∫ ω, (X k ω - m)^2 ∂μ = ∫ x, (x - m)^2 ∂(Measure.map (X k) μ) :=
+      Eq.symm (Probability.IntegrationHelpers.integral_pushforward_sq_diff (hX_meas k) m)
+    have h_int_0 : ∫ ω, (X 0 ω - m)^2 ∂μ = ∫ x, (x - m)^2 ∂(Measure.map (X 0) μ) :=
+      Eq.symm (Probability.IntegrationHelpers.integral_pushforward_sq_diff (hX_meas 0) m)
     rw [h_int_k, h_eq_dist, ← h_int_0]
 
   -- Define ρ from the covariance of (X_0, X_1)
@@ -183,8 +175,8 @@ lemma contractable_covariance_structure
         have h_int_ij : ∫ ω, (X i ω - m) * (X j ω - m) ∂μ
             = ∫ p : ℝ × ℝ, (p.1 - m) * (p.2 - m) ∂(Measure.map (fun ω => (X i ω, X j ω)) μ) := by
           have h_ae : AEStronglyMeasurable (fun p : ℝ × ℝ => (p.1 - m) * (p.2 - m))
-              (Measure.map (fun ω => (X i ω, X j ω)) μ) := by
-            exact ((continuous_fst.sub continuous_const).mul
+              (Measure.map (fun ω => (X i ω, X j ω)) μ) :=
+            ((continuous_fst.sub continuous_const).mul
               (continuous_snd.sub continuous_const)).aestronglyMeasurable
           have h_comp : (fun ω => (X i ω - m) * (X j ω - m))
               = (fun p : ℝ × ℝ => (p.1 - m) * (p.2 - m)) ∘ (fun ω => (X i ω, X j ω)) := rfl
@@ -193,8 +185,8 @@ lemma contractable_covariance_structure
         have h_int_01 : ∫ ω, (X 0 ω - m) * (X 1 ω - m) ∂μ
             = ∫ p : ℝ × ℝ, (p.1 - m) * (p.2 - m) ∂(Measure.map (fun ω => (X 0 ω, X 1 ω)) μ) := by
           have h_ae : AEStronglyMeasurable (fun p : ℝ × ℝ => (p.1 - m) * (p.2 - m))
-              (Measure.map (fun ω => (X 0 ω, X 1 ω)) μ) := by
-            exact ((continuous_fst.sub continuous_const).mul
+              (Measure.map (fun ω => (X 0 ω, X 1 ω)) μ) :=
+            ((continuous_fst.sub continuous_const).mul
               (continuous_snd.sub continuous_const)).aestronglyMeasurable
           have h_comp : (fun ω => (X 0 ω - m) * (X 1 ω - m))
               = (fun p : ℝ × ℝ => (p.1 - m) * (p.2 - m)) ∘ (fun ω => (X 0 ω, X 1 ω)) := rfl
@@ -213,8 +205,8 @@ lemma contractable_covariance_structure
         have h_int_ji : ∫ ω, (X j ω - m) * (X i ω - m) ∂μ
             = ∫ p : ℝ × ℝ, (p.1 - m) * (p.2 - m) ∂(Measure.map (fun ω => (X j ω, X i ω)) μ) := by
           have h_ae : AEStronglyMeasurable (fun p : ℝ × ℝ => (p.1 - m) * (p.2 - m))
-              (Measure.map (fun ω => (X j ω, X i ω)) μ) := by
-            exact ((continuous_fst.sub continuous_const).mul
+              (Measure.map (fun ω => (X j ω, X i ω)) μ) :=
+            ((continuous_fst.sub continuous_const).mul
               (continuous_snd.sub continuous_const)).aestronglyMeasurable
           have h_comp : (fun ω => (X j ω - m) * (X i ω - m))
               = (fun p : ℝ × ℝ => (p.1 - m) * (p.2 - m)) ∘ (fun ω => (X j ω, X i ω)) := rfl
@@ -223,8 +215,8 @@ lemma contractable_covariance_structure
         have h_int_01 : ∫ ω, (X 0 ω - m) * (X 1 ω - m) ∂μ
             = ∫ p : ℝ × ℝ, (p.1 - m) * (p.2 - m) ∂(Measure.map (fun ω => (X 0 ω, X 1 ω)) μ) := by
           have h_ae : AEStronglyMeasurable (fun p : ℝ × ℝ => (p.1 - m) * (p.2 - m))
-              (Measure.map (fun ω => (X 0 ω, X 1 ω)) μ) := by
-            exact ((continuous_fst.sub continuous_const).mul
+              (Measure.map (fun ω => (X 0 ω, X 1 ω)) μ) :=
+            ((continuous_fst.sub continuous_const).mul
               (continuous_snd.sub continuous_const)).aestronglyMeasurable
           have h_comp : (fun ω => (X 0 ω - m) * (X 1 ω - m))
               = (fun p : ℝ × ℝ => (p.1 - m) * (p.2 - m)) ∘ (fun ω => (X 0 ω, X 1 ω)) := rfl
@@ -268,27 +260,18 @@ lemma contractable_covariance_structure
           have h_nonneg₁ : ∀ᵐ ω ∂μ, 0 ≤ |X 1 ω - m| := ae_of_all μ (fun ω => abs_nonneg _)
           have h_key : ∫ ω, |X 0 ω - m| * |X 1 ω - m| ∂μ
               ≤ (∫ ω, |X 0 ω - m| ^ (2:ℝ) ∂μ) ^ ((2:ℝ)⁻¹) * (∫ ω, |X 1 ω - m| ^ (2:ℝ) ∂μ) ^ ((2:ℝ)⁻¹) := by
-            have hpq : (2:ℝ).HolderConjugate 2 := by
-              constructor
-              · norm_num
-              · norm_num
-              · norm_num
+            have hpq : (2:ℝ).HolderConjugate 2 :=
+              Real.HolderConjugate.two_two
             have hf₀' : MemLp (fun ω => |X 0 ω - m|) (ENNReal.ofReal 2) μ := by
               have h2 : (ENNReal.ofReal 2 : ENNReal) = (2 : ENNReal) := by norm_num
               rw [h2]
               have : MemLp (fun ω => ‖X 0 ω - m‖) 2 μ := hf₀.norm
-              have h_eq : (fun ω => ‖X 0 ω - m‖) =ᵐ[μ] (fun ω => |X 0 ω - m|) := by
-                filter_upwards with ω
-                exact Real.norm_eq_abs _
-              exact MemLp.ae_eq h_eq this
+              assumption
             have hf₁' : MemLp (fun ω => |X 1 ω - m|) (ENNReal.ofReal 2) μ := by
               have h2 : (ENNReal.ofReal 2 : ENNReal) = (2 : ENNReal) := by norm_num
               rw [h2]
               have : MemLp (fun ω => ‖X 1 ω - m‖) 2 μ := hf₁.norm
-              have h_eq : (fun ω => ‖X 1 ω - m‖) =ᵐ[μ] (fun ω => |X 1 ω - m|) := by
-                filter_upwards with ω
-                exact Real.norm_eq_abs _
-              exact MemLp.ae_eq h_eq this
+              assumption
             have := MeasureTheory.integral_mul_le_Lp_mul_Lq_of_nonneg hpq h_nonneg₀ h_nonneg₁ hf₀' hf₁'
             convert this using 2 <;> norm_num
           convert h_key using 2
@@ -298,16 +281,10 @@ lemma contractable_covariance_structure
             = Real.sqrt (∫ ω, (X 0 ω - m)^2 ∂μ) * Real.sqrt (∫ ω, (X 1 ω - m)^2 ∂μ) := by
           have h4 : (∫ ω, |X 0 ω - m| ^ 2 ∂μ) ^ (1/2 : ℝ) = Real.sqrt (∫ ω, (X 0 ω - m)^2 ∂μ) := by
             rw [Real.sqrt_eq_rpow]
-            congr 1
-            congr 1
-            funext ω
-            rw [sq_abs]
+            simpa
           have h5 : (∫ ω, |X 1 ω - m| ^ 2 ∂μ) ^ (1/2 : ℝ) = Real.sqrt (∫ ω, (X 1 ω - m)^2 ∂μ) := by
             rw [Real.sqrt_eq_rpow]
-            congr 1
-            congr 1
-            funext ω
-            rw [sq_abs]
+            simpa
           rw [h4, h5]
         calc |∫ ω, (X 0 ω - m) * (X 1 ω - m) ∂μ|
             ≤ ∫ ω, |(X 0 ω - m) * (X 1 ω - m)| ∂μ := h_tri
@@ -366,11 +343,7 @@ lemma contractable_covariance_structure
         rw [hi, hj]
         ring
       -- Integral of a.e. zero function is zero
-      have h_integrable : Integrable (fun ω => (X i ω - m) * (X j ω - m)) μ := by
-        have h_i : MemLp (fun ω => X i ω - m) 2 μ := (hX_L2 i).sub (memLp_const m)
-        have h_j : MemLp (fun ω => X j ω - m) 2 μ := (hX_L2 j).sub (memLp_const m)
-        exact h_i.integrable_mul h_j
-      exact integral_eq_zero_of_ae h_ae_prod
+      exact integral_eq_const h_ae_prod
 
     -- ρ = 0 works
     use m, σSq, 0
@@ -433,14 +406,9 @@ private lemma reindexed_weights_prob
           (fun i : Fin nS => wS ((eβ i).1))
           (fun b => wS b.1) (by intro i; rfl)
       have h_sum_attach :
-          ∑ b : {t // t ∈ S}, wS b.1 = ∑ t ∈ S, wS t := by
-        exact Finset.sum_attach (s := S) (f := fun t => wS t)
-      have h_sum_w :
-          ∑ i : Fin nS, w i = ∑ i : Fin nS, wS ((eβ i).1) := by
-        refine Finset.sum_congr rfl fun i _ => ?_
-        exact h_w_def i
-      simp [h_sum_w]
-      exact h_sum_equiv.trans h_sum_attach
+          ∑ b : {t // t ∈ S}, wS b.1 = ∑ t ∈ S, wS t :=
+        Finset.sum_attach (s := S) (f := fun t => wS t)
+      grind only
     simp [h_equiv, h_sum_one]
   · intro i
     rw [h_w_def]
@@ -546,10 +514,7 @@ lemma l2_bound_two_windows_uniform
         ∑ t ∈ S, δ t * Y t ω =
           ∑ t ∈ S, (pS t * Y t ω - qS t * Y t ω) := by
       refine Finset.sum_congr rfl ?_
-      intro t ht
-      have : (pS t - qS t) * Y t ω = pS t * Y t ω - qS t * Y t ω := by
-        ring
-      simpa [δ] using this
+      exact fun x a => sub_mul (pS x) (qS x) (Y x ω)
     have h_split :
         ∑ t ∈ S, δ t * Y t ω =
           ∑ t ∈ S, pS t * Y t ω - ∑ t ∈ S, qS t * Y t ω := by
@@ -697,15 +662,8 @@ lemma l2_bound_two_windows_uniform
     exact ⟨⟨t, h_subset_n ht⟩⟩
   have h_nS_pos : 0 < nS := Fintype.card_pos_iff.mpr hβ_nonempty
   have h_sup_le :
-      (⨆ i : Fin nS, |p i - q i|) ≤ 1 / (k : ℝ) := by
-    classical
-    haveI : Nonempty (Fin nS) := Fin.pos_iff_nonempty.mp h_nS_pos
-    refine ciSup_le ?_
-    intro i
-    have hmem : idx i ∈ S := h_idx_mem i
-    have hδ_bound := hδ_abs_le (idx i) hmem
-    have hδ_eq : δ (idx i) = p i - q i := by simp [δ, p, q, idx]
-    simpa [hδ_eq] using hδ_bound
+      (⨆ i : Fin nS, |p i - q i|) ≤ 1 / (k : ℝ) :=
+    ciSup_le fun x => hδ_abs_le (idx x) (h_idx_mem x)
 
   -- Injectivity of the indexing map
   have h_idx_ne : ∀ {i j : Fin nS}, i ≠ j → idx i ≠ idx j := by
@@ -795,10 +753,7 @@ lemma l2_bound_two_windows_uniform
         ∑ t ∈ S, δ t * Y t ω =
           ∑ t ∈ S, (pS t * Y t ω - qS t * Y t ω) := by
       refine Finset.sum_congr rfl ?_
-      intro t ht
-      have : (pS t - qS t) * Y t ω = pS t * Y t ω - qS t * Y t ω := by
-        ring
-      simpa [δ] using this
+      exact fun x a => sub_mul (pS x) (qS x) (Y x ω)
     have h_split :
         ∑ t ∈ S, δ t * Y t ω =
           ∑ t ∈ S, pS t * Y t ω - ∑ t ∈ S, qS t * Y t ω := by
@@ -826,7 +781,7 @@ lemma l2_bound_two_windows_uniform
 
   have h_factor_nonneg :
       0 ≤ 2 * (Real.sqrt σSqf) ^ 2 * (1 - ρf) := by
-    have hσ_nonneg : 0 ≤ (Real.sqrt σSqf) ^ 2 := by exact sq_nonneg _
+    have hσ_nonneg : 0 ≤ (Real.sqrt σSqf) ^ 2 := sq_nonneg _
     have hρ_nonneg : 0 ≤ 1 - ρf := sub_nonneg.mpr hρ_bd.2
     have : 0 ≤ (2 : ℝ) := by norm_num
     exact mul_nonneg (mul_nonneg this hσ_nonneg) hρ_nonneg
@@ -834,14 +789,8 @@ lemma l2_bound_two_windows_uniform
   have h_bound_sup :
       2 * (Real.sqrt σSqf) ^ 2 * (1 - ρf) *
         (⨆ i : Fin nS, |p i - q i|) ≤
-      2 * (Real.sqrt σSqf) ^ 2 * (1 - ρf) * (1 / (k : ℝ)) := by
-    have h :=
-      (mul_le_mul_of_nonneg_left h_sup_le h_factor_nonneg :
-          (2 * (Real.sqrt σSqf) ^ 2 * (1 - ρf)) *
-              (⨆ i : Fin nS, |p i - q i|)
-            ≤ (2 * (Real.sqrt σSqf) ^ 2 * (1 - ρf)) * (1 / (k : ℝ)))
-    simpa [mul_comm, mul_left_comm, mul_assoc]
-      using h
+      2 * (Real.sqrt σSqf) ^ 2 * (1 - ρf) * (1 / (k : ℝ)) :=
+    PosMulMono.mul_le_mul_of_nonneg_left h_factor_nonneg h_sup_le
 
   -- Final bound
   have h_sqrt_sq : (Real.sqrt σSqf) ^ 2 = σSqf := Real.sq_sqrt hσSq_nonneg
@@ -852,9 +801,7 @@ lemma l2_bound_two_windows_uniform
           (1 / (k : ℝ)) * ∑ i : Fin k, f (X (m + i.val + 1) ω))^2 ∂μ =
         ∫ ω, (∑ i : Fin nS, p i * ξ i ω - ∑ i : Fin nS, q i * ξ i ω)^2 ∂μ := by
     congr 1
-    funext ω
-    simpa using
-      congrArg (fun x : ℝ => x ^ 2) (h_goal_fin ω)
+    exact funext fun x => congrFun (congrArg HPow.hPow (h_goal_fin x)) 2
 
   have h_int_le_sup :
       ∫ ω,
@@ -1144,16 +1091,7 @@ lemma l2_bound_long_vs_tail
           · have hM_nonneg : 0 ≤ M := by
               have : |f 0| ≤ M := hM 0
               exact le_trans (abs_nonneg _) this
-            have : 0 ≤ M + M := by linarith
-            have h_sum_bound : |(1 / (m : ℝ)) * ∑ i : Fin m, f (X (n + i.val + 1) ω)| +
-                               |(1 / (k : ℝ)) * ∑ i : Fin k, f (X (n + (m - k) + i.val + 1) ω)| ≤ M + M := by
-              linarith [h1, h2]
-            have : -(M + M) ≤ |(1 / (m : ℝ)) * ∑ i : Fin m, f (X (n + i.val + 1) ω)| +
-                               |(1 / (k : ℝ)) * ∑ i : Fin k, f (X (n + (m - k) + i.val + 1) ω)| := by
-              have h_nonneg : 0 ≤ |(1 / (m : ℝ)) * ∑ i : Fin m, f (X (n + i.val + 1) ω)| +
-                                   |(1 / (k : ℝ)) * ∑ i : Fin k, f (X (n + (m - k) + i.val + 1) ω)| := by positivity
-              linarith [h_nonneg, hM_nonneg]
-            linarith [h_sum_bound]
+            grind only [= abs.eq_1, = max_def]
           · linarith [h1, h2]
       _ = (2 * M)^2 := by ring
       _ ≤ (4 * M)^2 := by
@@ -1517,8 +1455,8 @@ theorem subseq_ae_of_L1
     exact this
 
   -- Step 2: eLpNorm convergence implies convergence in measure
-  have h_tendstoInMeasure : TendstoInMeasure μ alpha atTop alpha_inf := by
-    exact tendstoInMeasure_of_tendsto_eLpNorm one_ne_zero
+  have h_tendstoInMeasure : TendstoInMeasure μ alpha atTop alpha_inf :=
+    tendstoInMeasure_of_tendsto_eLpNorm one_ne_zero
       (fun n => (h_alpha_meas n).aestronglyMeasurable)
       h_alpha_inf_meas.aestronglyMeasurable
       h_eLpNorm_tendsto
diff --git a/Exchangeability/DeFinetti/ViaL2/BlockAvgDef.lean b/Exchangeability/DeFinetti/ViaL2/BlockAvgDef.lean
index a630b264..b6c4e07a 100644
--- a/Exchangeability/DeFinetti/ViaL2/BlockAvgDef.lean
+++ b/Exchangeability/DeFinetti/ViaL2/BlockAvgDef.lean
@@ -54,13 +54,7 @@ lemma blockAvg_measurable
     Measurable (fun ω => blockAvg f X m n ω) := by
   classical
   unfold blockAvg
-  have hsum :
-      Measurable (fun ω =>
-        (Finset.range n).sum (fun k => f (X (m + k) ω))) :=
-    Finset.measurable_sum _ (by
-      intro k _
-      exact hf.comp (hX (m + k)))
-  simpa using (measurable_const.mul hsum : Measurable _)
+  fun_prop
 
 @[nolint unusedArguments]
 lemma blockAvg_abs_le_one
@@ -75,8 +69,8 @@ lemma blockAvg_abs_le_one
   have hsum_bound :
       |(Finset.range n).sum (fun k => f (X (m + k) ω))| ≤ (n : ℝ) := by
     calc |(Finset.range n).sum (fun k => f (X (m + k) ω))|
-        ≤ (Finset.range n).sum (fun k => |f (X (m + k) ω)|) := by
-          exact Finset.abs_sum_le_sum_abs (fun k => f (X (m + k) ω)) (Finset.range n)
+        ≤ (Finset.range n).sum (fun k => |f (X (m + k) ω)|) :=
+          Finset.abs_sum_le_sum_abs (fun k => f (X (m + k) ω)) (Finset.range n)
       _ ≤ (Finset.range n).sum (fun _ => (1 : ℝ)) := by
           apply Finset.sum_le_sum
           intro k _
@@ -84,17 +78,14 @@ lemma blockAvg_abs_le_one
       _ = n := by
           have : (Finset.range n).card = n := Finset.card_range n
           simp [this]
-  have hnonneg : 0 ≤ (n : ℝ)⁻¹ := by exact inv_nonneg.mpr (by exact_mod_cast Nat.zero_le n)
+  have hnonneg : 0 ≤ (n : ℝ)⁻¹ := inv_nonneg.mpr (by exact_mod_cast Nat.zero_le n)
   calc
     |(n : ℝ)⁻¹ * (Finset.range n).sum (fun k => f (X (m + k) ω))|
         = (n : ℝ)⁻¹ * |(Finset.range n).sum (fun k => f (X (m + k) ω))|
           := by simp [abs_mul, abs_of_nonneg hnonneg]
     _ ≤ (n : ℝ)⁻¹ * (n : ℝ)
-          := by exact mul_le_mul_of_nonneg_left hsum_bound hnonneg
-    _ ≤ 1 := by
-        by_cases hn : n = 0
-        · simp [hn]
-        · have : (n : ℝ) ≠ 0 := by simp [hn]
-          simp [this]
+          := mul_le_mul_of_nonneg_left hsum_bound hnonneg
+    _ ≤ 1 :=
+        inv_mul_le_one
 
 end Exchangeability.DeFinetti.ViaL2
diff --git a/Exchangeability/DeFinetti/ViaL2/CesaroConvergence.lean b/Exchangeability/DeFinetti/ViaL2/CesaroConvergence.lean
index 48f1414d..47baf12d 100644
--- a/Exchangeability/DeFinetti/ViaL2/CesaroConvergence.lean
+++ b/Exchangeability/DeFinetti/ViaL2/CesaroConvergence.lean
@@ -222,9 +222,7 @@ lemma kallenberg_L2_bound
       -- Equivalent to: |covOffDiag| ≤ σSq (since σSq > 0)
 
       have hσSq_pos : 0 < σSq := by
-        cases (hσSq_nonneg.lt_or_eq) with
-        | inl h_lt => exact h_lt
-        | inr h_eq => exact (h h_eq.symm).elim
+        exact lt_of_le_of_ne' hσSq_nonneg h
 
       -- Apply Cauchy-Schwarz: |∫ f·g| ≤ (∫ f²)^(1/2) · (∫ g²)^(1/2)
       have h_cs : |covOffDiag| ≤ σSq := by
@@ -250,8 +248,8 @@ lemma kallenberg_L2_bound
                       symm
                       exact eLpNorm_map_measure aestronglyMeasurable_id (hZ_meas k).aemeasurable
                 _ = eLpNorm id 2 (Measure.map (Z 0) μ) := by rw [h_dist]
-                _ = eLpNorm (Z 0) 2 μ := by
-                      exact eLpNorm_map_measure aestronglyMeasurable_id (hZ_meas 0).aemeasurable
+                _ = eLpNorm (Z 0) 2 μ :=
+                      eLpNorm_map_measure aestronglyMeasurable_id (hZ_meas 0).aemeasurable
             -- Now transfer MemLp using equal eLpNorm
             have : eLpNorm (Z 0) 2 μ < ⊤ := by
               rw [h_Lpnorm_eq]
@@ -276,8 +274,8 @@ lemma kallenberg_L2_bound
                       exact eLpNorm_map_measure aestronglyMeasurable_id (hZ_meas 1).aemeasurable
                 _ = eLpNorm id 2 (Measure.map (Z 0) μ) := by rw [h_dist1]
                 _ = eLpNorm id 2 (Measure.map (Z k) μ) := by rw [← h_dist]
-                _ = eLpNorm (Z k) 2 μ := by
-                      exact eLpNorm_map_measure aestronglyMeasurable_id (hZ_meas k).aemeasurable
+                _ = eLpNorm (Z k) 2 μ :=
+                      eLpNorm_map_measure aestronglyMeasurable_id (hZ_meas k).aemeasurable
             -- Now transfer MemLp using equal eLpNorm
             have : eLpNorm (Z 1) 2 μ < ⊤ := by
               rw [h_Lpnorm_eq]
@@ -291,8 +289,8 @@ lemma kallenberg_L2_bound
 
         -- Apply Cauchy-Schwarz
         calc |∫ ω, (Z 0 ω - m) * (Z 1 ω - m) ∂μ|
-            ≤ (∫ ω, (Z 0 ω - m) ^ 2 ∂μ) ^ (1/2 : ℝ) * (∫ ω, (Z 1 ω - m) ^ 2 ∂μ) ^ (1/2 : ℝ) := by
-                exact Exchangeability.Probability.IntegrationHelpers.abs_integral_mul_le_L2 hf hg
+            ≤ (∫ ω, (Z 0 ω - m) ^ 2 ∂μ) ^ (1/2 : ℝ) * (∫ ω, (Z 1 ω - m) ^ 2 ∂μ) ^ (1/2 : ℝ) :=
+                Exchangeability.Probability.IntegrationHelpers.abs_integral_mul_le_L2 hf hg
           _ = (∫ ω, (Z 0 ω - m) ^ 2 ∂μ) ^ (1/2 : ℝ) * (∫ ω, (Z 0 ω - m) ^ 2 ∂μ) ^ (1/2 : ℝ) := by
                 -- Use equal distributions: Z 1 has same variance as Z 0
                 congr 1
@@ -415,8 +413,8 @@ lemma kallenberg_L2_bound
                           = eLpNorm id 2 (Measure.map (Z k) μ) := by
                               symm; exact eLpNorm_map_measure aestronglyMeasurable_id (hZ_meas k).aemeasurable
                         _ = eLpNorm id 2 (Measure.map (Z 0) μ) := by rw [h_dist]
-                        _ = eLpNorm (Z 0) 2 μ := by
-                              exact eLpNorm_map_measure aestronglyMeasurable_id (hZ_meas 0).aemeasurable
+                        _ = eLpNorm (Z 0) 2 μ :=
+                              eLpNorm_map_measure aestronglyMeasurable_id (hZ_meas 0).aemeasurable
                     have : eLpNorm (Z 0) 2 μ < ⊤ := by
                       rw [h_Lpnorm_eq]
                       exact hZk_L2.eLpNorm_lt_top
@@ -434,8 +432,8 @@ lemma kallenberg_L2_bound
                               symm; exact eLpNorm_map_measure aestronglyMeasurable_id (hZ_meas 1).aemeasurable
                         _ = eLpNorm id 2 (Measure.map (Z 0) μ) := by rw [h_dist1]
                         _ = eLpNorm id 2 (Measure.map (Z k) μ) := by rw [← h_dist]
-                        _ = eLpNorm (Z k) 2 μ := by
-                              exact eLpNorm_map_measure aestronglyMeasurable_id (hZ_meas k).aemeasurable
+                        _ = eLpNorm (Z k) 2 μ :=
+                              eLpNorm_map_measure aestronglyMeasurable_id (hZ_meas k).aemeasurable
                     have : eLpNorm (Z 1) 2 μ < ⊤ := by
                       rw [h_Lpnorm_eq]
                       exact hZk_L2.eLpNorm_lt_top
@@ -494,8 +492,8 @@ lemma kallenberg_L2_bound
                           = eLpNorm id 2 (Measure.map (Z k) μ) := by
                               symm; exact eLpNorm_map_measure aestronglyMeasurable_id (hZ_meas k).aemeasurable
                         _ = eLpNorm id 2 (Measure.map (Z 0) μ) := by rw [h_dist]
-                        _ = eLpNorm (Z 0) 2 μ := by
-                              exact eLpNorm_map_measure aestronglyMeasurable_id (hZ_meas 0).aemeasurable
+                        _ = eLpNorm (Z 0) 2 μ :=
+                              eLpNorm_map_measure aestronglyMeasurable_id (hZ_meas 0).aemeasurable
                     have : eLpNorm (Z 0) 2 μ < ⊤ := by
                       rw [h_Lpnorm_eq]
                       exact hZk_L2.eLpNorm_lt_top
@@ -513,8 +511,8 @@ lemma kallenberg_L2_bound
                               symm; exact eLpNorm_map_measure aestronglyMeasurable_id (hZ_meas 1).aemeasurable
                         _ = eLpNorm id 2 (Measure.map (Z 0) μ) := by rw [h_dist1]
                         _ = eLpNorm id 2 (Measure.map (Z k) μ) := by rw [← h_dist]
-                        _ = eLpNorm (Z k) 2 μ := by
-                              exact eLpNorm_map_measure aestronglyMeasurable_id (hZ_meas k).aemeasurable
+                        _ = eLpNorm (Z k) 2 μ :=
+                              eLpNorm_map_measure aestronglyMeasurable_id (hZ_meas k).aemeasurable
                     have : eLpNorm (Z 1) 2 μ < ⊤ := by
                       rw [h_Lpnorm_eq]
                       exact hZk_L2.eLpNorm_lt_top
@@ -619,8 +617,8 @@ lemma kallenberg_L2_bound
                   symm
                   exact eLpNorm_map_measure aestronglyMeasurable_id (hZ_meas k).aemeasurable
             _ = eLpNorm id 2 (Measure.map (Z 0) μ) := by rw [h_dist]
-            _ = eLpNorm (Z 0) 2 μ := by
-                  exact eLpNorm_map_measure aestronglyMeasurable_id (hZ_meas 0).aemeasurable
+            _ = eLpNorm (Z 0) 2 μ :=
+                  eLpNorm_map_measure aestronglyMeasurable_id (hZ_meas 0).aemeasurable
         have : eLpNorm (Z 0) 2 μ < ⊤ := by
           rw [h_Lpnorm_eq]
           exact hZk_L2.eLpNorm_lt_top
@@ -642,8 +640,8 @@ lemma kallenberg_L2_bound
                   exact eLpNorm_map_measure aestronglyMeasurable_id (hZ_meas 1).aemeasurable
             _ = eLpNorm id 2 (Measure.map (Z 0) μ) := by rw [h_dist1]
             _ = eLpNorm id 2 (Measure.map (Z k) μ) := by rw [← h_dist]
-            _ = eLpNorm (Z k) 2 μ := by
-                  exact eLpNorm_map_measure aestronglyMeasurable_id (hZ_meas k).aemeasurable
+            _ = eLpNorm (Z k) 2 μ :=
+                  eLpNorm_map_measure aestronglyMeasurable_id (hZ_meas k).aemeasurable
         have : eLpNorm (Z 1) 2 μ < ⊤ := by
           rw [h_Lpnorm_eq]
           exact hZk_L2.eLpNorm_lt_top
@@ -1349,14 +1347,10 @@ private lemma cesaro_cauchy_rho_lt
 
     -- Show measurability
     have h_meas_n : Measurable (fun ω => blockAvg f X 0 n ω) := by
-      simp only [blockAvg]
-      exact Measurable.const_mul (Finset.measurable_sum _ fun k _ =>
-        hf_meas.comp (hX_meas (0 + k))) _
+      fun_prop
 
     have h_meas_n' : Measurable (fun ω => blockAvg f X 0 n' ω) := by
-      simp only [blockAvg]
-      exact Measurable.const_mul (Finset.measurable_sum _ fun k _ =>
-        hf_meas.comp (hX_meas (0 + k))) _
+      fun_prop
 
     have h_meas_diff : Measurable (fun ω => blockAvg f X 0 n ω - blockAvg f X 0 n' ω) :=
       h_meas_n.sub h_meas_n'
@@ -1368,57 +1362,14 @@ private lemma cesaro_cauchy_rho_lt
       intro ω
       -- Each blockAvg is bounded by 1 (average of values bounded by 1)
       have hn_bdd : |blockAvg f X 0 n ω| ≤ 1 := by
-        simp only [blockAvg]
-        -- Strategy: |n⁻¹ * ∑ f_i| ≤ n⁻¹ * ∑ |f_i| ≤ n⁻¹ * n = 1
-        rw [abs_mul, abs_of_nonneg (inv_nonneg.mpr (Nat.cast_nonneg n))]
-        have h_sum_bound : |(Finset.range n).sum (fun k => f (X (0 + k) ω))| ≤ n := by
-          calc |(Finset.range n).sum (fun k => f (X (0 + k) ω))|
-              ≤ (Finset.range n).sum (fun k => |f (X (0 + k) ω)|) := by
-                exact Finset.abs_sum_le_sum_abs _ _
-            _ ≤ (Finset.range n).sum (fun k => 1) := by
-                apply Finset.sum_le_sum
-                intro k _
-                simp only [zero_add]
-                exact hf_bdd (X k ω)
-            _ = n := by
-                simp only [Finset.sum_const, Finset.card_range, nsmul_one]
-        calc (n : ℝ)⁻¹ * |(Finset.range n).sum (fun k => f (X (0 + k) ω))|
-            ≤ (n : ℝ)⁻¹ * n := by
-              apply mul_le_mul_of_nonneg_left
-              · exact_mod_cast h_sum_bound
-              · exact inv_nonneg.mpr (Nat.cast_nonneg n)
-          _ = 1 := by
-              field_simp [Nat.cast_ne_zero.mpr (Nat.pos_iff_ne_zero.mp hn_pos)]
+        exact blockAvg_abs_le_one f X hf_bdd 0 n ω
       have hn'_bdd : |blockAvg f X 0 n' ω| ≤ 1 := by
-        simp only [blockAvg]
-        -- Same strategy as hn_bdd
-        rw [abs_mul, abs_of_nonneg (inv_nonneg.mpr (Nat.cast_nonneg n'))]
-        have h_sum_bound : |(Finset.range n').sum (fun k => f (X (0 + k) ω))| ≤ n' := by
-          calc |(Finset.range n').sum (fun k => f (X (0 + k) ω))|
-              ≤ (Finset.range n').sum (fun k => |f (X (0 + k) ω)|) := by
-                exact Finset.abs_sum_le_sum_abs _ _
-            _ ≤ (Finset.range n').sum (fun k => 1) := by
-                apply Finset.sum_le_sum
-                intro k _
-                simp only [zero_add]
-                exact hf_bdd (X k ω)
-            _ = n' := by
-                simp only [Finset.sum_const, Finset.card_range, nsmul_one]
-        calc (n' : ℝ)⁻¹ * |(Finset.range n').sum (fun k => f (X (0 + k) ω))|
-            ≤ (n' : ℝ)⁻¹ * n' := by
-              apply mul_le_mul_of_nonneg_left
-              · exact_mod_cast h_sum_bound
-              · exact inv_nonneg.mpr (Nat.cast_nonneg n')
-          _ = 1 := by
-              field_simp [Nat.cast_ne_zero.mpr (Nat.pos_iff_ne_zero.mp hn'_pos)]
+        exact blockAvg_abs_le_one f X hf_bdd 0 n' ω
       calc |blockAvg f X 0 n ω - blockAvg f X 0 n' ω|
           ≤ |blockAvg f X 0 n ω| + |blockAvg f X 0 n' ω| := by
             -- Triangle inequality: |a - b| ≤ |a| + |b|
             -- Derive from |a + b| ≤ |a| + |b| by writing a - b = a + (-b)
-            calc |blockAvg f X 0 n ω - blockAvg f X 0 n' ω|
-                = |blockAvg f X 0 n ω + (-(blockAvg f X 0 n' ω))| := by rw [sub_eq_add_neg]
-              _ ≤ |blockAvg f X 0 n ω| + |-(blockAvg f X 0 n' ω)| := abs_add_le _ _
-              _ = |blockAvg f X 0 n ω| + |blockAvg f X 0 n' ω| := by rw [abs_neg]
+            exact abs_sub (blockAvg f X 0 n ω) (blockAvg f X 0 n' ω)
         _ ≤ 1 + 1 := add_le_add hn_bdd hn'_bdd
         _ = 2 := by norm_num
 
@@ -1619,26 +1570,14 @@ private lemma blockAvg_cauchy_in_L2
 
               -- Now substitute known values
               have h_var_i : ∫ ω, (Z i ω) ^ 2 ∂μ = σSq := by
-                calc ∫ ω, (Z i ω) ^ 2 ∂μ
-                    = ∫ ω, (Z 0 ω) ^ 2 ∂μ := hZ_var_uniform i
-                  _ = σSq := rfl
+                exact Real.ext_cauchy (congrArg Real.cauchy (hZ_var_uniform i))
 
               have h_var_0 : ∫ ω, (Z 0 ω) ^ 2 ∂μ = σSq := rfl
 
               have h_cov : ∫ ω, Z i ω * Z 0 ω ∂μ = σSq * ρ := by
                 calc ∫ ω, Z i ω * Z 0 ω ∂μ
                     = ∫ ω, Z 0 ω * Z 1 ω ∂μ := by
-                      by_cases hi1 : i = 1
-                      · simp [hi1]
-                        congr 1 with ω
-                        ring
-                      · -- Use hZ_cov_uniform for i ≠ 0, i ≠ 1
-                        -- Use hZ_cov_uniform: ∫ Z 0 * Z i = ∫ Z 0 * Z 1 (then use commutativity)
-                        have h_swap : ∫ ω, Z i ω * Z 0 ω ∂μ = ∫ ω, Z 0 ω * Z i ω ∂μ := by
-                          congr 1 with ω; ring
-                        calc ∫ ω, Z i ω * Z 0 ω ∂μ
-                            = ∫ ω, Z 0 ω * Z i ω ∂μ := h_swap
-                          _ = ∫ ω, Z 0 ω * Z 1 ω ∂μ := hZ_cov_uniform 0 i (Ne.symm hi)
+                      exact Real.ext_cauchy (congrArg Real.cauchy (hZ_cov_uniform i 0 hi))
                   _ = covZ := rfl
                   _ = σSq * ρ := by
                       rw [hρ_eq]
@@ -2350,9 +2289,7 @@ lemma cesaro_to_condexp_L2
       -- blockAvg is bounded since f is bounded
       apply memLp_two_of_bounded
       · -- Measurable: blockAvg is a finite sum of measurable functions
-        show Measurable (fun ω => (n : ℝ)⁻¹ * (Finset.range n).sum (fun k => f (X (0 + k) ω)))
-        exact Measurable.const_mul (Finset.measurable_sum _ fun k _ =>
-          hf_meas.comp (hX_meas (0 + k))) _
+        fun_prop
       intro ω
       -- |blockAvg f X 0 n ω| ≤ 1 since |f| ≤ 1
       show |(n : ℝ)⁻¹ * (Finset.range n).sum (fun k => f (X (0 + k) ω))| ≤ 1
@@ -2750,10 +2687,8 @@ lemma cesaro_to_condexp_L2
       TailSigma.tailSigma_le X hX_meas
 
     -- Step 2: SigmaFinite for trimmed measure (automatic for probability measures)
-    haveI h_finite : IsFiniteMeasure (μ.trim hm) := by
-      constructor
-      rw [trim_measurableSet_eq hm MeasurableSet.univ]
-      exact measure_lt_top μ Set.univ
+    haveI h_finite : IsFiniteMeasure (μ.trim hm) :=
+      isFiniteMeasure_trim hm
     haveI : SigmaFinite (μ.trim hm) := @IsFiniteMeasure.toSigmaFinite _ _ _ h_finite
 
     -- Step 3: Integrability of f ∘ X 0 (bounded function on probability space)
@@ -2852,10 +2787,8 @@ lemma cesaro_to_condexp_L2
         exact h_blockAvg_eq n hn
       -- The limit of an eventually constant sequence equals that constant
       have h_lim_eq_const : Tendsto (fun n => ∫ ω in A, blockAvg f X 0 n ω ∂μ)
-          atTop (𝓝 (∫ ω in A, f (X 0 ω) ∂μ)) := by
-        apply tendsto_const_nhds.congr'
-        filter_upwards [h_const] with n hn
-        exact hn.symm
+          atTop (𝓝 (∫ ω in A, f (X 0 ω) ∂μ)) :=
+        tendsto_nhds_of_eventually_eq h_const
       exact tendsto_nhds_unique h_setInt_tendsto h_lim_eq_const
 
     -- Condition 3: α_f is tail-measurable
@@ -2957,13 +2890,7 @@ lemma cesaro_to_condexp_L1
           norm_cast
       _ = (∫ a, ‖(blockAvg f X 0 n - α_f) a‖ ^ (2 : ℝ) ∂μ) := by norm_num
       _ = ∫ ω, (blockAvg f X 0 n ω - α_f ω) ^ 2 ∂μ := by
-          apply integral_congr_ae
-          filter_upwards with a
-          -- LHS: ‖(f - g) a‖ ^ (2:ℝ), RHS: (f a - g a) ^ 2
-          -- Step 1: Convert ‖x‖^(2:ℝ) → |x|^2 (natural power)
-          rw [Real.rpow_two, Real.norm_eq_abs]
-          -- Step 2: |x|^2 = x^2 (sq_abs), then unfold Pi.sub
-          simp only [sq_abs, Pi.sub_apply]
+          simpa
 
   -- STEP 2: Apply L2_tendsto_implies_L1_tendsto_of_bounded
   have hf_meas : ∀ n, Measurable (blockAvg f X 0 n) := by
@@ -3062,14 +2989,7 @@ theorem tendsto_integral_indicator_Iic
     rcases lt_trichotomy (X ω) t with h_lt | h_eq | h_gt
     · -- Case 1: X ω < t
       have hev : ∀ᶠ n in atTop, Xn n ω < t := by
-        rw [Metric.tendsto_atTop] at hω_tendsto
-        have ε_pos : 0 < (t - X ω) / 2 := by linarith
-        obtain ⟨N, hN⟩ := hω_tendsto ((t - X ω) / 2) ε_pos
-        refine Filter.eventually_atTop.mpr ⟨N, fun n hn => ?_⟩
-        have := hN n hn
-        rw [Real.dist_eq] at this
-        have : Xn n ω - X ω < (t - X ω) / 2 := abs_sub_lt_iff.mp this |>.1
-        linarith
+        exact Tendsto.eventually_lt_const h_lt hω_tendsto
       apply Filter.Tendsto.congr' (EventuallyEq.symm _) tendsto_const_nhds
       filter_upwards [hev] with n hn
       simp only [Set.indicator, Set.mem_Iic]
@@ -3077,15 +2997,8 @@ theorem tendsto_integral_indicator_Iic
     · -- Case 2: X ω = t (excluded by continuity assumption)
       exact absurd h_eq hω_neq
     · -- Case 3: X ω > t
-      have hev : ∀ᶠ n in atTop, t < Xn n ω := by
-        rw [Metric.tendsto_atTop] at hω_tendsto
-        have ε_pos : 0 < (X ω - t) / 2 := by linarith
-        obtain ⟨N, hN⟩ := hω_tendsto ((X ω - t) / 2) ε_pos
-        refine Filter.eventually_atTop.mpr ⟨N, fun n hn => ?_⟩
-        have := hN n hn
-        rw [Real.dist_eq] at this
-        have : X ω - Xn n ω < (X ω - t) / 2 := abs_sub_lt_iff.mp this |>.2
-        linarith
+      have hev : ∀ᶠ n in atTop, t < Xn n ω :=
+        Tendsto.eventually_const_lt h_gt hω_tendsto
       apply Filter.Tendsto.congr' (EventuallyEq.symm _) tendsto_const_nhds
       filter_upwards [hev] with n hn
       simp only [Set.indicator, Set.mem_Iic]
@@ -3235,11 +3148,7 @@ lemma cesaro_convergence_all_shifts
       lt_of_lt_of_le hM1_lt (Nat.cast_le.mpr hm1)
     rcases Nat.eq_zero_or_pos m with rfl | hm_pos
     · -- m = 0 case: contradiction since 4n/ε ≥ 0 but h_big says < 0
-      simp only [Nat.cast_zero] at h_big
-      have h1 : (0 : ℝ) ≤ 4 * n := by positivity
-      have h2 : (0 : ℝ) < ε := hε
-      have h3 : (0 : ℝ) ≤ (4 * n) / ε := by positivity
-      linarith
+      grind only
     have hmpos : 0 < (m : ℝ) := Nat.cast_pos.mpr hm_pos
     have h_rearragne : 4 * n < m * ε := by
       have := mul_lt_mul_of_pos_right h_big hε
diff --git a/Exchangeability/DeFinetti/ViaL2/Clip01.lean b/Exchangeability/DeFinetti/ViaL2/Clip01.lean
index 35436754..9fffa59c 100644
--- a/Exchangeability/DeFinetti/ViaL2/Clip01.lean
+++ b/Exchangeability/DeFinetti/ViaL2/Clip01.lean
@@ -46,8 +46,8 @@ lemma clip01_range (x : ℝ) : 0 ≤ clip01 x ∧ clip01 x ≤ 1 := by
     · exact min_le_left _ _
 
 /-- `clip01` is 1-Lipschitz. -/
-lemma clip01_1Lipschitz : LipschitzWith 1 clip01 := by
-  exact (LipschitzWith.id.const_min 1).const_max 0
+lemma clip01_1Lipschitz : LipschitzWith 1 clip01 :=
+  (LipschitzWith.id.const_min 1).const_max 0
 
 /-- Pointwise contraction from the 1-Lipschitzness. -/
 lemma abs_clip01_sub_le (x y : ℝ) : |clip01 x - clip01 y| ≤ |x - y| := by
diff --git a/Exchangeability/DeFinetti/ViaL2/DirectingMeasureIntegral.lean b/Exchangeability/DeFinetti/ViaL2/DirectingMeasureIntegral.lean
index 15d18d33..b28d341a 100644
--- a/Exchangeability/DeFinetti/ViaL2/DirectingMeasureIntegral.lean
+++ b/Exchangeability/DeFinetti/ViaL2/DirectingMeasureIntegral.lean
@@ -202,9 +202,7 @@ lemma directing_measure_integral_Iic_ae_eq_alphaIicCE
       -- Since alphaIicRat n → 1, for large n we have alphaIicRat n > b
       have h_nat : Tendsto (fun n : ℕ => alphaIicRat X hX_contract hX_meas hX_L2 ω (n : ℚ))
           atTop (𝓝 1) := by
-        unfold alphaIicRat
-        simp only [Rat.cast_natCast]
-        exact h_top
+        assumption
       rw [Metric.tendsto_atTop] at h_nat
       obtain ⟨N, hN⟩ := h_nat (1 - b) hε
       have h_contra := hb (Set.mem_range.mpr ⟨N, rfl⟩)
@@ -275,10 +273,8 @@ lemma directing_measure_integral_Iic_ae_eq_alphaIicCE
       rw [h_ae_rat q]
       -- Goal: ⨅ r : Set.Ioi q, alphaIic (r : ℝ) ω ≤ alphaIicCE (q : ℝ) ω
       have h_eq : ⨅ r : Set.Ioi q, alphaIic X hX_contract hX_meas hX_L2 (r : ℝ) ω =
-          ⨅ r : Set.Ioi q, alphaIicCE X hX_contract hX_meas hX_L2 (r : ℝ) ω := by
-        congr 1
-        ext ⟨r, hr⟩
-        exact h_ae_rat r
+          ⨅ r : Set.Ioi q, alphaIicCE X hX_contract hX_meas hX_L2 (r : ℝ) ω :=
+        iInf_congr fun i => h_ae_rat ↑i
       rw [h_eq, h_iInf_rat_gt_CE q]
     · -- value ≤ iInf: use monotonicity
       apply le_ciInf
@@ -324,10 +320,8 @@ lemma directing_measure_integral_Iic_ae_eq_alphaIicCE
 
   -- Step 1: Rewrite the infimum using h_ae_rat
   have h_infimum_eq : (⨅ q : {q : ℚ // t < q}, alphaIic X hX_contract hX_meas hX_L2 (q : ℝ) ω) =
-      ⨅ q : {q : ℚ // t < q}, alphaIicCE X hX_contract hX_meas hX_L2 (q : ℝ) ω := by
-    congr 1
-    ext ⟨q, _⟩
-    exact h_ae_rat q
+      ⨅ q : {q : ℚ // t < q}, alphaIicCE X hX_contract hX_meas hX_L2 (q : ℝ) ω :=
+    iInf_congr fun i => h_ae_rat ↑i
 
   rw [h_infimum_eq]
 
@@ -538,9 +532,7 @@ lemma integral_indicator_borel_tailAEStronglyMeasurable
         | zero =>
           -- partialSum 0 = 0, which is a constant
           have h_zero : partialSum 0 = fun _ => 0 := by
-            funext ω
-            show ∑ n ∈ Finset.range 0, _ = 0
-            simp only [Finset.range_zero, Finset.sum_empty]
+            rfl
           rw [h_zero]
           exact aestronglyMeasurable_const
         | succ n ih =>
@@ -686,12 +678,8 @@ lemma integral_indicator_borel_tailAEStronglyMeasurable
   let S : Set (Set ℝ) := Set.range (Set.Iic : ℝ → Set ℝ)
   have h_gen : (inferInstance : MeasurableSpace ℝ) = MeasurableSpace.generateFrom S :=
     @borel_eq_generateFrom_Iic ℝ _ _ _ _
-  have h_pi_S : IsPiSystem S := by
-    intro u hu v hv _
-    obtain ⟨s, rfl⟩ := hu
-    obtain ⟨t, rfl⟩ := hv
-    use min s t
-    exact Set.Iic_inter_Iic.symm
+  have h_pi_S : IsPiSystem S :=
+    isPiSystem_Iic
 
   have h_induction : ∀ t (htm : MeasurableSet t), t ∈ G := fun t htm =>
     MeasurableSpace.induction_on_inter h_gen h_pi_S
@@ -755,9 +743,7 @@ lemma integral_simpleFunc_tailAEStronglyMeasurable
       have h_real_eq : ∀ ω, (directing_measure X hX_contract hX_meas hX_L2 ω).real (φ ⁻¹' {c}) =
           ∫ x, (φ ⁻¹' {c}).indicator 1 x
             ∂(directing_measure X hX_contract hX_meas hX_L2 ω) := by
-        intro ω
-        haveI hprob := directing_measure_isProbabilityMeasure X hX_contract hX_meas hX_L2 ω
-        exact (integral_indicator_one h_preimage_meas).symm
+        exact fun ω => Eq.symm (integral_indicator_one h_preimage_meas)
       have h_term_aesm : @AEStronglyMeasurable Ω ℝ _ (TailSigma.tailSigma X) _
           (fun ω => (directing_measure X hX_contract hX_meas hX_L2 ω).real (φ ⁻¹' {c})) μ := by
         have := integral_indicator_borel_tailAEStronglyMeasurable X hX_contract hX_meas hX_L2
@@ -1202,12 +1188,8 @@ lemma setIntegral_directing_measure_indicator_eq
   let S : Set (Set ℝ) := Set.range (Set.Iic : ℝ → Set ℝ)
   have h_gen : (inferInstance : MeasurableSpace ℝ) = MeasurableSpace.generateFrom S :=
     @borel_eq_generateFrom_Iic ℝ _ _ _ _
-  have h_pi_S : IsPiSystem S := by
-    intro u hu v hv _
-    obtain ⟨r, rfl⟩ := hu
-    obtain ⟨t, rfl⟩ := hv
-    use min r t
-    exact Set.Iic_inter_Iic.symm
+  have h_pi_S : IsPiSystem S :=
+    isPiSystem_Iic
 
   have h_induction : ∀ t (htm : MeasurableSet t), t ∈ G := fun t htm =>
     MeasurableSpace.induction_on_inter h_gen h_pi_S
@@ -1818,9 +1800,7 @@ lemma directing_measure_integral_via_chain
             simp only [hω, sub_self, abs_zero, Pi.zero_apply]
           · -- Integrability: α_g - condExp is in L¹
             have hα_g_int : Integrable α_g μ := hα_g_L2.integrable one_le_two
-            have hcond_int : Integrable (μ[g ∘ X 0 | TailSigma.tailSigma X]) μ :=
-              integrable_condExp
-            exact (hα_g_int.sub hcond_int).norm
+            fun_prop
 
         -- Triangle inequality: g-averages → α_g in L¹
         have hg_to_alpha_g : ∀ ε > 0, ∃ M_idx : ℕ, ∀ m ≥ M_idx,
@@ -1836,10 +1816,7 @@ lemma directing_measure_integral_via_chain
                   apply integral_mono_of_nonneg (ae_of_all μ (fun _ => abs_nonneg _))
                   · apply Integrable.add
                     · have hg_avg_meas : Measurable (fun ω => (1/(m:ℝ)) * ∑ k : Fin m, g (X (k.val+1) ω)) := by
-                        apply Measurable.const_mul
-                        apply Finset.measurable_sum
-                        intro k _
-                        exact hg_meas.comp (hX_meas (k.val + 1))
+                        fun_prop
                       have hg_avg_bdd : ∀ ω, |(1/(m:ℝ)) * ∑ k : Fin m, g (X (k.val+1) ω)| ≤ 1 := by
                         intro ω
                         by_cases hm : m = 0
@@ -1853,9 +1830,7 @@ lemma directing_measure_integral_via_chain
                             _ = 1 := by simp [Finset.sum_const, Finset.card_fin]; field_simp [hm]
                       have hg_avg_bdd' : ∀ᵐ ω ∂μ, ‖(1/(m:ℝ)) * ∑ k : Fin m, g (X (k.val+1) ω)‖ ≤ 1 := by
                         apply ae_of_all μ
-                        intro ω
-                        rw [Real.norm_eq_abs]
-                        exact hg_avg_bdd ω
+                        assumption
                       refine (Integrable.of_bound hg_avg_meas.aestronglyMeasurable 1 hg_avg_bdd').sub integrable_condExp |>.norm
                     · refine (integrable_condExp.sub (hα_g_L2.integrable one_le_two)).norm
                   · apply ae_of_all μ
@@ -1870,10 +1845,7 @@ lemma directing_measure_integral_via_chain
                 ∫ ω, |μ[g ∘ X 0 | TailSigma.tailSigma X] ω - α_g ω| ∂μ := by
                   apply integral_add
                   · have hg_avg_meas : Measurable (fun ω => (1/(m:ℝ)) * ∑ k : Fin m, g (X (k.val+1) ω)) := by
-                      apply Measurable.const_mul
-                      apply Finset.measurable_sum
-                      intro k _
-                      exact hg_meas.comp (hX_meas (k.val + 1))
+                      fun_prop
                     have hg_avg_bdd : ∀ ω, |(1/(m:ℝ)) * ∑ k : Fin m, g (X (k.val+1) ω)| ≤ 1 := by
                       intro ω
                       by_cases hm : m = 0
@@ -1887,9 +1859,7 @@ lemma directing_measure_integral_via_chain
                           _ = 1 := by simp [Finset.sum_const, Finset.card_fin]; field_simp [hm]
                     have hg_avg_bdd' : ∀ᵐ ω ∂μ, ‖(1/(m:ℝ)) * ∑ k : Fin m, g (X (k.val+1) ω)‖ ≤ 1 := by
                       apply ae_of_all μ
-                      intro ω
-                      rw [Real.norm_eq_abs]
-                      exact hg_avg_bdd ω
+                      assumption
                     exact (Integrable.of_bound hg_avg_meas.aestronglyMeasurable 1 hg_avg_bdd').sub integrable_condExp |>.norm
                   · exact (integrable_condExp.sub (hα_g_L2.integrable one_le_two)).norm
             _ = ∫ ω, |(1/(m:ℝ)) * ∑ k : Fin m, g (X (k.val+1) ω) -
@@ -1942,10 +1912,7 @@ lemma directing_measure_integral_via_chain
 
         -- First convert L¹ convergence to eLpNorm convergence
         have hA_meas : ∀ m, Measurable (A m) := fun m => by
-          apply Measurable.const_mul
-          apply Finset.measurable_sum
-          intro k _
-          exact hf_meas.comp (hX_meas (k.val + 1))
+          fun_prop
 
         have hA_bdd : ∀ m ω, |A m ω| ≤ M := fun m ω => by
           simp only [A]
diff --git a/Exchangeability/DeFinetti/ViaL2/MainConvergence.lean b/Exchangeability/DeFinetti/ViaL2/MainConvergence.lean
index 5b7a3f5c..103f5ea2 100644
--- a/Exchangeability/DeFinetti/ViaL2/MainConvergence.lean
+++ b/Exchangeability/DeFinetti/ViaL2/MainConvergence.lean
@@ -78,12 +78,7 @@ theorem weighted_sums_converge_L1
 
   -- A n m is measurable for all n, m
   have hA_meas : ∀ n m, Measurable (A n m) := by
-    intro n m
-    simp only [A]
-    apply Measurable.const_mul
-    apply Finset.measurable_sum
-    intro k _
-    exact hf_meas.comp (hX_meas _)
+    fun_prop
 
   -- A n m is in L¹ for all n, m (bounded measurable on probability space)
   have hA_memLp : ∀ n m, MemLp (A n m) 1 μ := by
@@ -101,8 +96,8 @@ theorem weighted_sums_converge_L1
             by_cases hm : m = 0
             · simp [hm]
             · have hm_pos : 0 < (m : ℝ) := by exact_mod_cast Nat.pos_of_ne_zero hm
-              have h_inv_pos : 0 < 1 / (m : ℝ) := by
-                exact div_pos (by norm_num) hm_pos
+              have h_inv_pos : 0 < 1 / (m : ℝ) :=
+                div_pos (by norm_num) hm_pos
               have h_abs_sum :
                   |∑ k : Fin m, f (X (n + k.val + 1) ω)|
                     ≤ ∑ k : Fin m, |f (X (n + k.val + 1) ω)| :=
@@ -117,9 +112,8 @@ theorem weighted_sums_converge_L1
                         |∑ k : Fin m, f (X (n + k.val + 1) ω)| := by
                       simp [abs_mul]
                 _ ≤ (1 / (m : ℝ)) *
-                        ∑ k : Fin m, |f (X (n + k.val + 1) ω)| := by
-                      exact
-                        (mul_le_mul_of_nonneg_left h_abs_sum
+                        ∑ k : Fin m, |f (X (n + k.val + 1) ω)| :=
+                      (mul_le_mul_of_nonneg_left h_abs_sum
                           (le_of_lt h_inv_pos))
         _ ≤ (1 / (m : ℝ)) * ∑ k : Fin m, M := by
             classical
@@ -184,10 +178,7 @@ theorem weighted_sums_converge_L1
   have hfX_L2' : ∀ i, MemLp (fun ω => f (X i ω)) 2 μ := by
     intro i
     obtain ⟨M, hM⟩ := hf_bdd
-    apply MemLp.of_bound (hfX_meas' i).aestronglyMeasurable M
-    filter_upwards with ω
-    simp [Real.norm_eq_abs]
-    exact hM (X i ω)
+    exact memLp_two_of_bounded (hfX_meas' i) fun ω => hM (X i ω)
 
   -- **Phase 2: Compute covariance structure once and pass to both lemmas**
   -- This eliminates the need to prove Cf = Cf_tail (they're the same by construction!)
@@ -475,13 +466,8 @@ theorem weighted_sums_converge_L1
     -- Convert the real inequality to one in `ℝ≥0∞`.
     have h_lt :
         eLpNorm (fun ω => A 0 m ω - G ω) 1 μ
-          < ENNReal.ofReal ε := by
-      have h_ofReal :
-          ENNReal.ofReal (ENNReal.toReal
-            (eLpNorm (fun ω => A 0 m ω - G ω) 1 μ)) < ENNReal.ofReal ε :=
-        ENNReal.ofReal_lt_ofReal_iff hε |>.mpr htoReal
-      rw [ENNReal.ofReal_toReal hfin] at h_ofReal
-      exact h_ofReal
+          < ENNReal.ofReal ε :=
+      (ENNReal.lt_ofReal_iff_toReal_lt hfin).mpr htoReal
     rw [h_eq]
     exact h_lt
 
@@ -583,8 +569,8 @@ theorem weighted_sums_converge_L1
     calc eLpNorm (fun ω => A n m ω - alpha_0 ω) 1 μ
         ≤ eLpNorm (fun ω => A n m ω - A 0 m ω) 1 μ +
             eLpNorm (fun ω => A 0 m ω - alpha_0 ω) 1 μ := h_triangle
-      _ < ENNReal.ofReal (ε / 2) + ENNReal.ofReal (ε / 2) := by
-            exact ENNReal.add_lt_add h_term1 h_term2
+      _ < ENNReal.ofReal (ε / 2) + ENNReal.ofReal (ε / 2) :=
+            ENNReal.add_lt_add h_term1 h_term2
       _ = ENNReal.ofReal ε := by
             rw [← ENNReal.ofReal_add hε2_pos.le hε2_pos.le]; norm_num
 
diff --git a/Exchangeability/DeFinetti/ViaL2/MoreL2Helpers.lean b/Exchangeability/DeFinetti/ViaL2/MoreL2Helpers.lean
index 7b2ee3b6..36b5e729 100644
--- a/Exchangeability/DeFinetti/ViaL2/MoreL2Helpers.lean
+++ b/Exchangeability/DeFinetti/ViaL2/MoreL2Helpers.lean
@@ -338,14 +338,7 @@ lemma directing_measure_measurable
       -- {Iic t | t ∈ ℝ} is a π-system
       -- For any Iic s, Iic t: if (Iic s) ∩ (Iic t) is nonempty, then it's in S
       -- (Iic s) ∩ (Iic t) = Iic (min s t)
-      intro u hu v hv _
-      -- u ∈ S means u = Iic s for some s
-      -- v ∈ S means v = Iic t for some t
-      obtain ⟨s, rfl⟩ := hu
-      obtain ⟨t, rfl⟩ := hv
-      -- Need to show: Iic s ∩ Iic t ∈ S
-      use min s t
-      exact Set.Iic_inter_Iic.symm
+      exact isPiSystem_Iic
 
     -- Apply the π-λ theorem
     have h_induction : ∀ t (htm : MeasurableSet t), C t htm := fun t htm =>
@@ -407,22 +400,15 @@ lemma ae_eq_of_tendsto_L1 {μ : Measure Ω} [IsProbabilityMeasure μ]
       ((hg_int.sub (hf_int n)).abs).add (((hf_int n).sub hh_int).abs)
     have h_int_triangle : ∫ ω, |g ω - h ω| ∂μ ≤ ∫ ω, |g ω - f n ω| ∂μ + ∫ ω, |f n ω - h ω| ∂μ := by
       calc ∫ ω, |g ω - h ω| ∂μ
-          ≤ ∫ ω, (|g ω - f n ω| + |f n ω - h ω|) ∂μ := by
-            exact integral_mono h_abs_int h_sum_int (fun ω => h_triangle ω)
-        _ = ∫ ω, |g ω - f n ω| ∂μ + ∫ ω, |f n ω - h ω| ∂μ := by
-            exact integral_add (hg_int.sub (hf_int n)).abs ((hf_int n).sub hh_int).abs
+          ≤ ∫ ω, (|g ω - f n ω| + |f n ω - h ω|) ∂μ :=
+            integral_mono h_abs_int h_sum_int (fun ω => h_triangle ω)
+        _ = ∫ ω, |g ω - f n ω| ∂μ + ∫ ω, |f n ω - h ω| ∂μ :=
+            integral_add (hg_int.sub (hf_int n)).abs ((hf_int n).sub hh_int).abs
 
     have h_symm : ∫ ω, |g ω - f n ω| ∂μ = ∫ ω, |f n ω - g ω| ∂μ := by
       congr 1; ext ω; rw [abs_sub_comm]
 
-    have h_lt : ∫ ω, |g ω - h ω| ∂μ < 2 * ε := by
-      calc ∫ ω, |g ω - h ω| ∂μ ≤ ∫ ω, |g ω - f n ω| ∂μ + ∫ ω, |f n ω - h ω| ∂μ := h_int_triangle
-        _ = ∫ ω, |f n ω - g ω| ∂μ + ∫ ω, |f n ω - h ω| ∂μ := by rw [h_symm]
-        _ < ε + ε := by linarith [hN₁ n hn₁, hN₂ n hn₂]
-        _ = 2 * ε := by ring
-
-    simp only [hε_def] at h_lt
-    linarith
+    grind only
 
   have h_nonneg_ae : 0 ≤ᵐ[μ] fun ω => |g ω - h ω| := by
     filter_upwards with ω; exact abs_nonneg _
@@ -1027,8 +1013,8 @@ lemma weighted_sums_converge_L1_one_sub
         calc ∫ ω, |alpha_sub ω - (alpha_1 ω - alpha ω)| ∂μ
             ≤ ∫ ω, (|(1 / (m : ℝ)) * ∑ k : Fin m, (1 - f (X (k.val + 1) ω)) - alpha_sub ω| +
                 |(1 / (m : ℝ)) * ∑ _k : Fin m, (1 : ℝ) - alpha_1 ω| +
-                |(1 / (m : ℝ)) * ∑ k : Fin m, f (X (k.val + 1) ω) - alpha ω|) ∂μ := by
-              exact integral_mono h_abs_int h_sum_int h_pw
+                |(1 / (m : ℝ)) * ∑ k : Fin m, f (X (k.val + 1) ω) - alpha ω|) ∂μ :=
+              integral_mono h_abs_int h_sum_int h_pw
           _ = ∫ ω, |(1 / (m : ℝ)) * ∑ k : Fin m, (1 - f (X (k.val + 1) ω)) - alpha_sub ω| ∂μ +
               ∫ ω, |(1 / (m : ℝ)) * ∑ _k : Fin m, (1 : ℝ) - alpha_1 ω| ∂μ +
               ∫ ω, |(1 / (m : ℝ)) * ∑ k : Fin m, f (X (k.val + 1) ω) - alpha ω| ∂μ := by
@@ -1324,9 +1310,7 @@ lemma integral_alphaIic_eq_marginal
         by_cases hε_top : ε = ⊤
         · refine ⟨0, fun m _ => ?_⟩
           rw [hε_top]
-          conv_lhs => rw [show (fun ω => ‖(A m - limit) ω‖ₑ) = (fun ω => ‖A m ω - limit ω‖ₑ) from rfl]
-          rw [← ofReal_integral_norm_eq_lintegral_enorm (h_diff_int m)]
-          exact le_top
+          exact OrderTop.le_top (∫⁻ (x : Ω), ‖(A m - limit) x‖ₑ ∂μ)
         · -- ε ≠ ⊤ case: use L¹ convergence
           obtain ⟨M, hM⟩ := Metric.tendsto_atTop.mp h_tendsto_L1 ε.toReal
             (ENNReal.toReal_pos hε.ne' hε_top)
@@ -1487,18 +1471,7 @@ def constrainedFunctionEquiv {N n : ℕ} (i j : Fin (n+1)) (hij : i ≠ j) :
   left_inv := fun ⟨φ, hφ⟩ => by
     simp only [Subtype.mk.injEq]
     funext k
-    by_cases hk : k = j
-    · simp only [hk, dite_true]
-      conv_rhs => rw [← hφ]
-      congr 1
-      have h := (finSuccAboveEquiv j).apply_symm_apply ⟨i, hij⟩
-      simp only [Subtype.ext_iff] at h
-      exact h
-    · simp only [hk, dite_false]
-      congr 1
-      have h := (finSuccAboveEquiv j).apply_symm_apply ⟨k, hk⟩
-      simp only [Subtype.ext_iff] at h
-      exact h
+    simp_all
   right_inv := fun ψ => by
     funext k
     simp only
@@ -1546,14 +1519,7 @@ lemma card_nonInjective_le (m N : ℕ) (_hN : 0 < N) :
   -- For m = 0 or m = 1, there are no non-injective maps
   cases m with
   | zero =>
-    have : IsEmpty {φ : Fin 0 → Fin N // ¬Function.Injective φ} := by
-      constructor
-      intro ⟨φ, hφ⟩
-      simp only [Function.Injective] at hφ
-      push_neg at hφ
-      obtain ⟨i, _, _, _⟩ := hφ
-      exact Fin.elim0 i
-    simp [Fintype.card_eq_zero]
+    rfl
   | succ n =>
     cases n with
     | zero =>
@@ -1622,14 +1588,7 @@ lemma nonInjective_fraction_tendsto_zero (m : ℕ) :
     simp only [pow_zero, div_one]
     -- For m = 0, the set is empty (all functions are vacuously injective)
     have h : ∀ N, Fintype.card {φ : Fin 0 → Fin N // ¬Function.Injective φ} = 0 := by
-      intro N
-      rw [Fintype.card_eq_zero_iff]
-      constructor
-      intro ⟨φ, hφ⟩
-      simp only [Function.Injective] at hφ
-      push_neg at hφ
-      obtain ⟨i, _, _, _⟩ := hφ
-      exact Fin.elim0 i
+      tauto
     simp only [h, Nat.cast_zero]
     exact tendsto_const_nhds
   | succ n =>
@@ -1744,9 +1703,7 @@ lemma prod_tendsto_L1_of_L1_tendsto
     calc ∫ ω, |∏ i : Fin m, f n i ω - ∏ i : Fin m, g i ω| ∂μ
         ≤ ∫ ω, ∑ i : Fin m, |f n i ω - g i ω| ∂μ := h_int_bound
       _ = ∑ i : Fin m, ∫ ω, |f n i ω - g i ω| ∂μ := by
-          rw [integral_finset_sum]
-          intro i _
-          exact h_diff_int n i
+          exact integral_finset_sum Finset.univ fun i a => h_diff_int n i
   · exact h_sum_tendsto
 
 /-- Block index function is strictly monotone.
diff --git a/Exchangeability/DeFinetti/ViaL2/WindowMachinery.lean b/Exchangeability/DeFinetti/ViaL2/WindowMachinery.lean
index e799ad26..1bb15980 100644
--- a/Exchangeability/DeFinetti/ViaL2/WindowMachinery.lean
+++ b/Exchangeability/DeFinetti/ViaL2/WindowMachinery.lean
@@ -45,9 +45,7 @@ lemma window_card (n k : ℕ) : (window n k).card = k := by
   refine (Finset.card_image_iff.mpr ?_).trans ?_
   · intro a ha b hb h
     have h' : n + a = n + b := by
-      apply Nat.succ.inj
-      simp only [Nat.succ_eq_add_one] at h ⊢
-      omega
+      exact Nat.add_right_cancel h
     exact Nat.add_left_cancel h'
   · simp only [Finset.card_range]
 
@@ -77,12 +75,7 @@ lemma sum_window_eq_sum_fin {β : Type*} [AddCommMonoid β]
   have h_inj :
       ∀ a ∈ Finset.range k, ∀ b ∈ Finset.range k,
         (n + a + 1 = n + b + 1 → a = b) := by
-    intro a ha b hb h
-    have h' : a + 1 = b + 1 := by
-      have : n + (a + 1) = n + (b + 1) := by
-        omega
-      exact Nat.add_left_cancel this
-    exact Nat.succ.inj h'
+    lia
   -- Convert the window sum to a range sum via the image definition
   have h_sum_range :
       ∑ t ∈ Finset.image (fun i => n + i + 1) (Finset.range k), g t
@@ -98,8 +91,8 @@ lemma sum_window_eq_sum_fin {β : Type*} [AddCommMonoid β]
     refine (Finset.sum_bij (fun (i : Fin k) _ => i.val)
         (fun i _ => by
           simp [Finset.mem_range, i.is_lt])
-        (fun i hi j hj h => by
-          exact Fin.ext h)
+        (fun i hi j hj h =>
+          Fin.ext h)
         (fun b hb => ?_)
         (fun i _ => rfl)).symm
     · rcases Finset.mem_range.mp hb with hb_lt
diff --git a/Exchangeability/DeFinetti/ViaMartingale.lean b/Exchangeability/DeFinetti/ViaMartingale.lean
index fd61c021..e4a6c34b 100644
--- a/Exchangeability/DeFinetti/ViaMartingale.lean
+++ b/Exchangeability/DeFinetti/ViaMartingale.lean
@@ -139,10 +139,7 @@ lemma integral_eq_of_map_eq
   have h1 := integral_map_eq hMeas hg
   have h2 : Integrable g (Measure.map T' μ) := hLaw ▸ hg
   have h3 := integral_map_eq hMeas' h2
-  calc ∫ ω, g (T ω) ∂μ
-      = ∫ y, g y ∂(Measure.map T μ) := h1
-    _ = ∫ y, g y ∂(Measure.map T' μ) := by rw [hLaw]
-    _ = ∫ ω, g (T' ω) ∂μ := h3.symm
+  lia
 
 /-- **Helper:** Generalized test function lemma without ψ factor.
 
@@ -327,16 +324,7 @@ lemma integral_mul_condexp_adjoint_Linfty
       ∫ ω, μ[(fun ω => μ[g | m] ω * ξ ω) | m] ω ∂μ
     = ∫ ω, μ[g | m] ω * ξ ω ∂μ := by
     -- Kill α/β noise by naming the product once and for all
-    set F : Ω → ℝ := fun ω => μ[g | m] ω * ξ ω with hF
-
-    -- Apply the CE integral identity to F (and orient it the way we need)
-    have h_goal :
-        ∫ (ω : Ω), μ[g | m] ω * ξ ω ∂μ
-      = ∫ (ω : Ω), μ[(fun ω => μ[g | m] ω * ξ ω) | m] ω ∂μ := by
-      simpa [hF] using
-        (MeasureTheory.integral_condExp (μ := μ) (m := m) (hm := hm) (f := F)).symm
-
-    exact h_goal.symm
+    exact integral_condExp hm
 
   calc
     ∫ ω, g ω * μ[ξ | m] ω ∂μ
diff --git a/Exchangeability/DeFinetti/ViaMartingale/CondExpConvergence.lean b/Exchangeability/DeFinetti/ViaMartingale/CondExpConvergence.lean
index 0ce31599..f2b74251 100644
--- a/Exchangeability/DeFinetti/ViaMartingale/CondExpConvergence.lean
+++ b/Exchangeability/DeFinetti/ViaMartingale/CondExpConvergence.lean
@@ -142,18 +142,7 @@ lemma extreme_members_equal_on_tail
       =ᵐ[μ]
     μ[Set.indicator B (fun _ => (1 : ℝ)) ∘ (X 0) | tailSigma X] := by
   -- Preimage formulation to match KallenbergChain API
-  have h_pre : ∀ n, Set.indicator B (fun _ => (1 : ℝ)) ∘ X n =
-      Set.indicator (X n ⁻¹' B) (fun _ => (1 : ℝ)) := fun n => by
-    ext ω; simp only [Function.comp_apply, Set.indicator]; rfl
-  simp only [h_pre]
-  -- CE(X_k | rev (m+1)) = CE(X_k | tail) via Kallenberg chain + convergence
-  have h_m := condExp_indicator_revFiltration_eq_tail hX hX_meas (Nat.lt_succ_self m) hB
-  have h_0 := condExp_indicator_revFiltration_eq_tail hX hX_meas (Nat.zero_lt_succ m) hB
-  -- CE(X_m | rev (m+1)) = CE(X_0 | rev (m+1)) via contractability
-  have h_eq : μ[Set.indicator (X m ⁻¹' B) (fun _ => (1 : ℝ)) | revFiltration X (m + 1)]
-      =ᵐ[μ] μ[Set.indicator (X 0 ⁻¹' B) (fun _ => (1 : ℝ)) | revFiltration X (m + 1)] := by
-    convert condexp_convergence hX hX_meas 0 m (Nat.zero_le m) B hB using 2
-  exact h_m.symm.trans (h_eq.trans h_0)
+  exact extreme_members_equal_on_tail_via_tower hX hX_meas m B hB
 
 
 section reverse_martingale
diff --git a/Exchangeability/DeFinetti/ViaMartingale/FiniteProduct.lean b/Exchangeability/DeFinetti/ViaMartingale/FiniteProduct.lean
index b4338778..8afb0a01 100644
--- a/Exchangeability/DeFinetti/ViaMartingale/FiniteProduct.lean
+++ b/Exchangeability/DeFinetti/ViaMartingale/FiniteProduct.lean
@@ -83,11 +83,7 @@ lemma lintegral_prod_prob_eq_ofReal_integral
     -- turn each factor into ofReal of its toReal (since it's ≤ 1 < ∞)
     have hfactor :
         ∀ i : Fin m, ν ω (C i) = ENNReal.ofReal ((ν ω (C i)).toReal) := by
-      intro i
-      -- 0 ≤ μ(C) ≤ 1 ⇒ finite ⇒ ofReal_toReal
-      have hle1 : ν ω (C i) ≤ 1 := prob_le_one
-      have hfin : ν ω (C i) ≠ ⊤ := ne_of_lt (lt_of_le_of_lt hle1 ENNReal.one_lt_top)
-      exact (ENNReal.ofReal_toReal hfin).symm
+      norm_num
     -- product of ofReals = ofReal of product
     rw [Finset.prod_congr rfl (fun i _ => hfactor i)]
     exact (ENNReal.ofReal_prod_of_nonneg (fun i _ => ENNReal.toReal_nonneg)).symm
@@ -271,10 +267,8 @@ lemma finite_product_formula_id
         (h_filtration := futureFiltration_antitone X)
         (h_le := fun n => futureFiltration_le X n hX_meas)
         (f := (Set.indicator (C i) (fun _ => (1:ℝ))) ∘ X 0)
-        (h_f_int := by
-          simpa using
-            Exchangeability.Probability.integrable_indicator_comp
-              (μ := μ) (X := X 0) (hX := hX_meas 0) (hB := hC i))
+        (h_f_int :=
+          Probability.integrable_indicator_comp (hX_meas 0) (hC i))
       simpa [← tailSigmaFuture_eq_iInf, tailSigmaFuture_eq_tailSigma] using this
 
     -- Tail factorization for the product indicator (a.e. equality)
@@ -344,9 +338,7 @@ lemma finite_product_formula_id
       have hme : Measurable (fun ω => fun i : Fin m => X i ω) := by
         fun_prop
       rw [Measure.map_apply hme MeasurableSet.univ]
-      have : (fun ω => fun i : Fin m => X i ω) ⁻¹' Set.univ = Set.univ := Set.preimage_univ
-      rw [this]
-      exact measure_univ
+      norm_num
     haveI : IsProbabilityMeasure (μ.bind (fun ω => Measure.pi fun _ : Fin m => ν ω)) := by
       constructor
       -- Need to show: (μ.bind (fun ω => Measure.pi fun _ : Fin m => ν ω)) Set.univ = 1
@@ -372,20 +364,7 @@ lemma finite_product_formula_id
   -- Since both are probability measures and agree on rectangles, they are equal
 
   -- Define covering family (constant sequence of Set.univ)
-  let Bseq : ℕ → Set (Fin m → α) := fun _ => Set.univ
-
-  have h1B : ⋃ n, Bseq n = Set.univ := by
-    simp only [Bseq, Set.iUnion_const]
-
-  have h2B : ∀ n, Bseq n ∈ Rectangles := fun n =>
-    ⟨fun _ => Set.univ, fun _ => MeasurableSet.univ, by ext f; simp only [Bseq, Set.mem_univ, Set.mem_univ_pi]; tauto⟩
-
-  have hμB : ∀ n, Measure.map (fun ω => fun i : Fin m => X i ω) μ (Bseq n) ≠ ⊤ :=
-    fun n => by simp only [Bseq]; exact measure_ne_top _ Set.univ
-
-  -- Apply Measure.ext_of_generateFrom_of_iUnion
-  exact Measure.ext_of_generateFrom_of_iUnion
-    Rectangles Bseq h_gen h_pi h1B h2B hμB h_agree
+  exact ext_of_generate_finite Rectangles h_gen h_pi h_agree h_univ
 
 /-- **Finite product formula for strictly monotone subsequences**.
 
diff --git a/Exchangeability/DeFinetti/ViaMartingale/FutureFiltration.lean b/Exchangeability/DeFinetti/ViaMartingale/FutureFiltration.lean
index 1c8aa0ea..e34e37c0 100644
--- a/Exchangeability/DeFinetti/ViaMartingale/FutureFiltration.lean
+++ b/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)) :=
+  Probability.sigmaFinite_trim_of_le μ (tailSigma_le X hX)
 
 /-! ### Helper lemmas for futureFiltration properties -/
 
diff --git a/Exchangeability/DeFinetti/ViaMartingale/FutureRectangles.lean b/Exchangeability/DeFinetti/ViaMartingale/FutureRectangles.lean
index de83b781..0a48d678 100644
--- a/Exchangeability/DeFinetti/ViaMartingale/FutureRectangles.lean
+++ b/Exchangeability/DeFinetti/ViaMartingale/FutureRectangles.lean
@@ -65,13 +65,8 @@ lemma contractable_dist_eq_on_first_r_tail
   have hs₂ : StrictMono s₂ := strictMono_fin_cases (n:=r) (f:=f) hf_mono hk_lt
   have hmap_eq :
       Measure.map (fun ω i => X (s₁ i) ω) μ
-        = Measure.map (fun ω i => X (s₂ i) ω) μ := by
-    calc
-      Measure.map (fun ω i => X (s₁ i) ω) μ
-          = Measure.map (fun ω (i : Fin (r+1)) => X i.1 ω) μ := by
-            simpa [s₁] using hX (r+1) s₁ hs₁
-      _   = Measure.map (fun ω i => X (s₂ i) ω) μ := by
-            simpa [s₂] using (hX (r+1) s₂ hs₂).symm
+        = Measure.map (fun ω i => X (s₂ i) ω) μ :=
+    Contractable.allStrictMono_eq hX (r + 1) s₁ s₂ hs₁ hs₂
   let A : Set (Fin (r+1) → α) :=
     {v | v 0 ∈ B ∧ ∀ i : Fin r, v (Fin.succ i) ∈ C i}
   have hpre₁ :
@@ -115,19 +110,7 @@ lemma preimage_rect_future
     let ψ := fun ω => (X k ω, shiftRV X (m + 1) ω)
     ψ ⁻¹' (B ×ˢ cylinder (α:=α) r C)
       = {ω | X k ω ∈ B ∧ ∀ i : Fin r, X (m + 1 + i.1) ω ∈ C i} := by
-  classical
-  intro ψ
-  ext ω; constructor <;> intro h
-  · rcases h with ⟨hB, hC⟩
-    refine ⟨?_, ?_⟩
-    · simpa [ψ]
-    · intro i
-      simpa only using (hC : (shiftRV X (m + 1) ω) ∈ cylinder (α:=α) r C) i
-  · rcases h with ⟨hB, hC⟩
-    refine ⟨?_, ?_⟩
-    · simpa [ψ]
-    · intro i
-      simpa only [ψ, shiftRV] using hC i
+  rfl
 
 /-- **Finite-dimensional equality on future rectangles with standard cylinders.**
 For `k ≤ m` and measurable `B`, the measures of
@@ -160,9 +143,7 @@ lemma contractable_dist_eq_on_rectangles_future
     μ {ω | X m ω ∈ B ∧ ∀ i : Fin r, X (m + (i.1 + 1)) ω ∈ C i}
       =
     μ {ω | X k ω ∈ B ∧ ∀ i : Fin r, X (m + (i.1 + 1)) ω ∈ C i} := by
-    have := contractable_dist_eq_on_first_r_tail
-        (μ:=μ) (X:=X) hX hX_meas k m r hk B hB C hC
-    convert this using 2
+    exact contractable_dist_eq_on_first_r_tail hX hX_meas k m r hk B hB C hC
   -- Show the sets are equal modulo arithmetic (m + 1 + i = m + (i + 1))
   have hset_eq (j : ℕ) : {ω | X j ω ∈ B ∧ ∀ i : Fin r, X (m + 1 + i.1) ω ∈ C i}
                        = {ω | X j ω ∈ B ∧ ∀ i : Fin r, X (m + (i.1 + 1)) ω ∈ C i} := by
@@ -280,11 +261,7 @@ lemma measure_ext_of_future_rectangles
         rw [this]
         apply MeasurableSpace.measurableSet_generateFrom
         refine ⟨0, A, hA, (fun _ => Set.univ), (fun _ => MeasurableSet.univ), ?_⟩
-        ext ⟨a, f⟩
-        simp only [Set.mem_prod, Set.mem_univ, and_true]
-        show a ∈ A ↔ a ∈ A ∧ f ∈ MartingaleHelpers.cylinder 0 (fun _ => Set.univ)
-        rw [MartingaleHelpers.cylinder]
-        simp
+        norm_num
 
       have h_snd : ∀ (r : ℕ) (C : Fin r → Set α),
           (∀ i, MeasurableSet (C i)) →
diff --git a/Exchangeability/DeFinetti/ViaMartingale/PairLawEquality.lean b/Exchangeability/DeFinetti/ViaMartingale/PairLawEquality.lean
index efe8a89e..6553754f 100644
--- a/Exchangeability/DeFinetti/ViaMartingale/PairLawEquality.lean
+++ b/Exchangeability/DeFinetti/ViaMartingale/PairLawEquality.lean
@@ -128,9 +128,7 @@ omit [MeasurableSpace Ω] [MeasurableSpace α] in
 lemma phi1_after_r (r m k : ℕ) (hr : r ≤ m) :
     phi1 r m (r + 1 + k) = m + 1 + k := by
   simp only [phi1]
-  have h : ¬(r + 1 + k ≤ r) := by omega
-  simp only [h, ↓reduceIte]
-  omega
+  lia
 
 /-- **Key lemma:** Contractability gives pair-law equality `(U, W) =^d (U, W')`.
 
@@ -354,9 +352,7 @@ lemma comap_consRV_eq_sup
       cases n <;> simp [Function.comp_apply, consSeq, consRV]
     -- consSeq is measurable
     have h_consSeq_meas : Measurable consSeq := by
-      simpa [consSeq] using
-        (measurable_consRV (x := fun q : α × (ℕ → α) => q.1)
-          (t := fun q : α × (ℕ → α) => q.2) measurable_fst measurable_snd)
+      fun_prop
     -- So consRV x t ⁻¹' S = (fun ω => (x ω, t ω)) ⁻¹' (consSeq ⁻¹' S)
     rw [h_factor, Set.preimage_comp]
     -- consSeq ⁻¹' S is measurable in α × (ℕ → α)
@@ -526,9 +522,7 @@ lemma condExp_Xr_indicator_eq_of_contractable
         @Measurable.comp Ω (ℕ → α) α mW' _ _ (fun f => f 0) W'
           (measurable_pi_apply 0) hW'_ident
       -- X r = fun ω => W' ω 0 by definition of consRV
-      have h_eq : (X r) = (fun ω => W' ω 0) := funext fun ω => by simp only [W', consRV]
-      rw [h_eq]
-      exact h0_meas
+      assumption
     have hIndB_mW'_meas : @Measurable Ω ℝ mW' _ indB :=
       (measurable_const.indicator hB_Xr).comp hXr_mW'_meas
     have hIndB_stronglyMeas_mW' : StronglyMeasurable[mW'] indB :=
@@ -544,9 +538,7 @@ lemma condExp_Xr_indicator_eq_of_contractable
 
     -- Step 4: Apply drop-info: E[indA | mW'] * indB =ᵐ E[indA | mW] * indB
     have h_step2 : μ[indA | mW'] * indB =ᵐ[μ] μ[indA | mW] * indB := by
-      filter_upwards [h_drop] with ω hω
-      simp only [Pi.mul_apply]
-      rw [hω]
+      exact EventuallyEq.mul_right h_drop_raw
 
     -- Combine steps
     have h_step12 : μ[indA * indB | mW'] =ᵐ[μ] μ[indA | mW] * indB :=
diff --git a/Exchangeability/Ergodic/BirkhoffAvgCLM.lean b/Exchangeability/Ergodic/BirkhoffAvgCLM.lean
index 41c7c93b..2a4fc868 100644
--- a/Exchangeability/Ergodic/BirkhoffAvgCLM.lean
+++ b/Exchangeability/Ergodic/BirkhoffAvgCLM.lean
@@ -77,9 +77,7 @@ lemma Lp.coeFn_smul' (c : ℝ) (f : Lp ℝ 2 μ) :
   -- Mathlib has Lp.coeFn_smul: ⇑(c • f) =ᵐ[μ] c • ⇑f
   -- For real numbers, c • x = c * x
   have := Lp.coeFn_smul c f
-  filter_upwards [this] with ω h
-  simp only [Pi.smul_apply] at h
-  exact h
+  assumption
 
 /-- Coercion distributes through finite sums in Lp (a.e.). -/
 lemma Lp.coeFn_sum' {ι : Type*} [Fintype ι] (fs : ι → Lp ℝ 2 μ) :
@@ -133,16 +131,11 @@ lemma EventuallyEq.sum' {ι : Type*} [Fintype ι] {fs gs : ι → Ω → ℝ}
     push_neg at h_contra
     apply hω
     -- The sums are equal if all summands are equal
-    congr 1
-    ext i
-    exact h_contra i
+    exact Fintype.sum_congr (fun a => fs a ω) (fun a => gs a ω) h_contra
 
   -- Each set in the union has measure zero
   have h_null : ∀ i, μ {ω | fs i ω ≠ gs i ω} = 0 := by
-    intro i
-    have := h i
-    rw [Filter.EventuallyEq, Filter.Eventually, mem_ae_iff] at this
-    exact this
+    assumption
 
   -- Measure of finite union of null sets is zero
   -- Note: {x | ∑ i, fs i x = ∑ i, gs i x}ᶜ = {x | ∑ i, fs i x ≠ ∑ i, gs i x}
diff --git a/Exchangeability/Ergodic/InvariantSigma.lean b/Exchangeability/Ergodic/InvariantSigma.lean
index bd985c4d..c7d02b92 100644
--- a/Exchangeability/Ergodic/InvariantSigma.lean
+++ b/Exchangeability/Ergodic/InvariantSigma.lean
@@ -341,27 +341,7 @@ lemma metProjectionShift_tendsto
     (hσ : MeasurePreserving shift μ μ) (f : Lp ℝ 2 μ) :
     Tendsto (fun n => birkhoffAverage ℝ (koopman shift hσ) _root_.id n f)
       atTop (𝓝 (metProjectionShift (μ := μ) hσ f)) := by
-  classical
-  let K : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ := koopman shift hσ
-  have hnorm : ‖K‖ ≤ (1 : ℝ) := by
-    refine ContinuousLinearMap.opNorm_le_bound _ (by norm_num) ?_
-    intro g
-    have hiso : Isometry (koopman shift hσ) := koopman_isometry shift hσ
-    have hg : ‖K g‖ = ‖g‖ := by
-      simpa [K] using Isometry.norm_map_of_map_zero hiso (map_zero _) g
-    simp [hg]
-  have hclosed := fixedSubspace_closed (μ := μ) hσ
-  haveI : CompleteSpace (fixedSubspace hσ) := hclosed.completeSpace_coe
-  haveI : (fixedSubspace hσ).HasOrthogonalProjection :=
-    Submodule.HasOrthogonalProjection.ofCompleteSpace (fixedSubspace hσ)
-  have hS : (LinearMap.eqLocus K.toLinearMap 1) = fixedSubspace hσ := rfl
-  -- Set up the instance context for the eqLocus subspace
-  have : CompleteSpace (LinearMap.eqLocus K.toLinearMap 1) := by
-    rw [hS]; exact hclosed.completeSpace_coe
-  have : (LinearMap.eqLocus K.toLinearMap 1).HasOrthogonalProjection := by
-    rw [hS]; exact Submodule.HasOrthogonalProjection.ofCompleteSpace (fixedSubspace hσ)
-  have hlimit := ContinuousLinearMap.tendsto_birkhoffAverage_orthogonalProjection K hnorm f
-  convert hlimit using 1
+  exact birkhoffAverage_tendsto_metProjection shift hσ f
 
 /-- The range of `metProjectionShift` equals the fixed subspace. -/
 lemma metProjectionShift_range_fixedSubspace
diff --git a/Exchangeability/Ergodic/ShiftInvariantRepresentatives.lean b/Exchangeability/Ergodic/ShiftInvariantRepresentatives.lean
index 14bd47fe..a741880f 100644
--- a/Exchangeability/Ergodic/ShiftInvariantRepresentatives.lean
+++ b/Exchangeability/Ergodic/ShiftInvariantRepresentatives.lean
@@ -102,10 +102,7 @@ def gRep (g0 : Ω[α] → ℝ) : Ω[α] → ℝ :=
 lemma gRep_measurable {g0 : Ω[α] → ℝ} (hg0 : Measurable g0) :
     Measurable (gRep g0) := by
   have hstep : ∀ n : ℕ, Measurable fun ω => (g0 (shift^[n] ω) : EReal) := by
-    intro n
-    have hreal : Measurable fun ω => g0 (shift^[n] ω) :=
-      hg0.comp (shift_iterate_measurable (α := α) n)
-    exact measurable_coe_real_ereal.comp hreal
+    fun_prop
   have h_meas_ereal : Measurable fun ω => gLimsupE g0 ω := by
     simpa [gLimsupE] using (Measurable.limsup hstep)
   have : Measurable fun ω => (gLimsupE g0 ω).toReal := by
@@ -131,11 +128,7 @@ lemma gRep_eq_of_constant_orbit {g0 : Ω[α] → ℝ} {ω : Ω[α]}
   have hlim :
       limsup (fun n : ℕ => (g0 (shift^[n] ω) : EReal)) atTop
         = (g0 ω : EReal) := by
-    have hfunext :
-        (fun n : ℕ => (g0 (shift^[n] ω) : EReal))
-          = fun _ => (g0 ω : EReal) := by
-      funext n; simpa using congrArg (fun y : ℝ => (y : EReal)) (hconst n)
-    simp [hfunext, limsup_const]
+    simp_all
   simpa [gRep, gLimsupE] using congrArg EReal.toReal hlim
 
 lemma gRep_ae_eq_of_constant_orbit {g0 : Ω[α] → ℝ}
@@ -241,9 +234,7 @@ private lemma exists_shiftInvariantFullMeasureSet
 
   have hSinf_full : μ Sinfᶜ = 0 := by
     have h_forall : ∀ n : ℕ, ∀ᵐ ω ∂μ, ω ∈ (shift^[n]) ⁻¹' S0 := by
-      intro n
-      have : μ (((shift^[n]) ⁻¹' S0)ᶜ) = 0 := hpre_full n
-      simpa [ae_iff] using this
+      assumption
     have hSinf_ae : ∀ᵐ ω ∂μ, ω ∈ Sinf := by
       simpa [Sinf, hSinf_def, Set.mem_iInter] using (ae_all_iff.mpr h_forall)
     simpa [ae_iff] using hSinf_ae
@@ -310,12 +301,8 @@ private lemma exists_shiftInvariantFullMeasureSet
     have hmeasure_diff : μ ((shift ⁻¹' Sstar) \ Sstar) = 0 :=
       measure_mono_null hsubset_diff hSstar_full
     have hsubset : Sstar ⊆ shift ⁻¹' Sstar := hSstar_forward
-    have hzero : Sstar \ shift ⁻¹' Sstar = (∅ : Set (Ω[α])) := by
-      ext ω; constructor
-      · intro hω
-        have : ω ∈ shift ⁻¹' Sstar := hsubset hω.1
-        exact False.elim (hω.2 this)
-      · intro hω; simpa using hω.elim
+    have hzero : Sstar \ shift ⁻¹' Sstar = (∅ : Set (Ω[α])) :=
+      Set.diff_eq_empty.mpr hSstar_forward
     have hsymm :
         symmDiff (shift ⁻¹' Sstar) Sstar
           = ((shift ⁻¹' Sstar) \ Sstar) ∪ (Sstar \ shift ⁻¹' Sstar) := rfl
@@ -345,9 +332,7 @@ lemma mkShiftInvariantRep
   obtain ⟨S, hS_meas, _hSymm, hS_null, hS_subset, hS_point⟩ :=
     exists_shiftInvariantFullMeasureSet (μ := μ) hσ g0 hg0_meas hshift_g0
   have hforward : ∀ ω ∈ S, shift ω ∈ S := by
-    intro ω hω
-    have : ω ∈ shift ⁻¹' S := hS_subset hω
-    simpa [Set.mem_preimage] using this
+    assumption
   have hS_ae : ∀ᵐ ω ∂μ, ω ∈ S := by
     simpa [ae_iff] using hS_null
   have hconst_on_S : ∀ ω ∈ S, ∀ n : ℕ, g0 (shift^[n] ω) = g0 ω := by
diff --git a/Exchangeability/PathSpace/CylinderHelpers.lean b/Exchangeability/PathSpace/CylinderHelpers.lean
index 7c65c01d..6d6005ba 100644
--- a/Exchangeability/PathSpace/CylinderHelpers.lean
+++ b/Exchangeability/PathSpace/CylinderHelpers.lean
@@ -220,11 +220,7 @@ lemma firstRCylinder_inter (X : ℕ → Ω → α) {r : ℕ} {C D : Fin r → Se
     firstRCylinder X r C ∩ firstRCylinder X r D = firstRCylinder X r (fun i => C i ∩ D i) := by
   ext ω
   simp [firstRCylinder, Set.mem_inter_iff]
-  constructor
-  · intro ⟨hC, hD⟩ i
-    exact ⟨hC i, hD i⟩
-  · intro h
-    exact ⟨fun i => (h i).1, fun i => (h i).2⟩
+  exact Iff.symm forall_and
 
 end FirstBlockCylinder
 
@@ -238,10 +234,7 @@ lemma tailCylinder_eq_preimage_cylinder
     {r : ℕ} {C : Fin r → Set α} :
     tailCylinder (α:=α) r C
       = (shift : (ℕ → α) → (ℕ → α)) ⁻¹' (cylinder (α:=α) r C) := by
-  ext f
-  constructor <;> intro hf
-  · simpa [tailCylinder, shift, cylinder]
-  · simpa [tailCylinder, shift, cylinder]
+  rfl
 
 omit [MeasurableSpace α] in
 @[simp] lemma mem_cylinder_iff {r : ℕ} {C : Fin r → Set α} {f : ℕ → α} :
@@ -283,11 +276,7 @@ lemma cylinder_inter {r : ℕ} {C D : Fin r → Set α} :
     cylinder (α:=α) r C ∩ cylinder (α:=α) r D = cylinder (α:=α) r (fun i => C i ∩ D i) := by
   ext f
   simp [cylinder, Set.mem_inter_iff]
-  constructor
-  · intro ⟨hC, hD⟩ i
-    exact ⟨hC i, hD i⟩
-  · intro h
-    exact ⟨fun i => (h i).1, fun i => (h i).2⟩
+  exact Iff.symm forall_and
 
 end CylinderBridge
 
diff --git a/Exchangeability/Probability/CenteredVariables.lean b/Exchangeability/Probability/CenteredVariables.lean
index 535466e1..816bb8ae 100644
--- a/Exchangeability/Probability/CenteredVariables.lean
+++ b/Exchangeability/Probability/CenteredVariables.lean
@@ -98,12 +98,12 @@ lemma centered_uniform_covariance
     -- Apply map_map: map (h ∘ g) μ = map h (map g μ)
     calc Measure.map (fun ω i => f (X (k i) ω) - m) μ
         = Measure.map (h ∘ (fun ω i => f (X (k i) ω))) μ := by congr
-      _ = Measure.map h (Measure.map (fun ω i => f (X (k i) ω)) μ) := by
-            exact (Measure.map_map h_meas hL_meas).symm
+      _ = Measure.map h (Measure.map (fun ω i => f (X (k i) ω)) μ) :=
+            (Measure.map_map h_meas hL_meas).symm
       _ = Measure.map h (Measure.map (fun ω i => f (X (↑i) ω)) μ) := by
             rw [h_eq]
-      _ = Measure.map (h ∘ (fun ω i => f (X (↑i) ω))) μ := by
-            exact Measure.map_map h_meas hR_meas
+      _ = Measure.map (h ∘ (fun ω i => f (X (↑i) ω))) μ :=
+            Measure.map_map h_meas hR_meas
       _ = Measure.map (fun ω (i : Fin n) => f (X (↑i) ω) - m) μ := by congr
 
   -- Step 3: Show uniform variance via contractability
@@ -318,8 +318,6 @@ lemma correlation_coefficient_bounded
     rw [abs_div, abs_of_pos hσ_pos]
     exact div_le_one_of_le₀ h_covZ_bd hσ_pos.le
 
-  constructor
-  · linarith [abs_le.mp h_ρ_abs]
-  · exact (abs_le.mp h_ρ_abs).2
+  exact abs_le.mp h_ρ_abs
 
 end Exchangeability.Probability.CenteredVariables
diff --git a/Exchangeability/Probability/CondExp.lean b/Exchangeability/Probability/CondExp.lean
index ebd3f7f0..744ce0c4 100644
--- a/Exchangeability/Probability/CondExp.lean
+++ b/Exchangeability/Probability/CondExp.lean
@@ -327,11 +327,7 @@ def condExpWith {Ω : Type*} {m₀ : MeasurableSpace Ω}
     (μ : Measure Ω) [IsFiniteMeasure μ]
     (m : MeasurableSpace Ω) (_hm : m ≤ m₀)
     (f : Ω → ℝ) : Ω → ℝ := by
-  classical
-  haveI : IsFiniteMeasure μ := inferInstance
-  -- IsFiniteMeasure (μ.trim _hm) is now automatic via mathlib instance
-  haveI : SigmaFinite (μ.trim _hm) := sigmaFinite_trim μ _hm
-  exact μ[f | m]
+  assumption
 
 /-! ### Bridge lemma for indicator factorization
 
@@ -353,12 +349,8 @@ lemma condexp_indicator_inter_bridge
     μ[(A ∩ B).indicator (fun _ => (1 : ℝ)) | m]
       =ᵐ[μ]
     (μ[A.indicator (fun _ => (1 : ℝ)) | m] *
-     μ[B.indicator (fun _ => (1 : ℝ)) | m]) := by
-  classical
-  -- Install trimmed instances (IsFiniteMeasure is automatic via mathlib)
-  haveI : SigmaFinite (μ.trim hm) := sigmaFinite_trim μ hm
-  -- Forward to the proven lemma
-  exact condExp_indicator_mul_indicator_of_condIndep hm hmF hmH hCI hA hB
+     μ[B.indicator (fun _ => (1 : ℝ)) | m]) :=
+  condExp_indicator_mul_indicator_of_condIndep hm hmF hmH hCI hA hB
 
 /-! ### Conditional expectation equality from distributional equality
 
@@ -406,11 +398,7 @@ lemma condexp_indicator_eq_of_pair_law_eq
 
   -- Prove that comap Z is a sub-σ-algebra of the ambient space
   have hmZ_le : mZ ≤ mΩ := by
-    intro s hs
-    -- s ∈ comap Z means s = Z⁻¹(E) for some measurable E
-    rcases hs with ⟨E, hE, rfl⟩
-    -- Z⁻¹(E) is measurable in ambient space since Z is measurable
-    exact hZ hE
+    exact measurable_iff_comap_le.mp hZ
 
   -- Integrability
   have hf_int : Integrable f μ := (integrable_const (1:ℝ)).indicator (hY hB)
diff --git a/Exchangeability/Probability/CondExpExtras.lean b/Exchangeability/Probability/CondExpExtras.lean
index 24483824..b32c052d 100644
--- a/Exchangeability/Probability/CondExpExtras.lean
+++ b/Exchangeability/Probability/CondExpExtras.lean
@@ -110,11 +110,11 @@ lemma bounded_martingale_l2_eq {m₀ : MeasurableSpace Ω} {μ : Measure Ω}
     calc
       ∫ ω, Var[X₂; μ | m₁] ω ∂μ
           = ∫ ω, (μ[(fun ω => (X₂ ω) ^ 2) | m₁] ω
-                - (μ[X₂ | m₁] ω) ^ 2) ∂μ := by
-              exact integral_congr_ae hVar_decomp
+                - (μ[X₂ | m₁] ω) ^ 2) ∂μ :=
+              integral_congr_ae hVar_decomp
       _ = ∫ ω, μ[(fun ω => (X₂ ω) ^ 2) | m₁] ω ∂μ
-              - ∫ ω, (μ[X₂ | m₁] ω) ^ 2 ∂μ := by
-              exact integral_sub hInt_cond_sq hInt_Y_sq
+              - ∫ ω, (μ[X₂ | m₁] ω) ^ 2 ∂μ :=
+              integral_sub hInt_cond_sq hInt_Y_sq
       _ = ∫ ω, (X₂ ω) ^ 2 ∂μ - ∫ ω, (X₁ ω) ^ 2 ∂μ := by
         simp [hInt_cond_sq_eq, hInt_Y_sq_eq]
       _ = 0 := by
@@ -199,20 +199,12 @@ lemma integral_pair_eq_of_joint_eq {μ : Measure Ω}
       Integrable φ (Measure.map fζ μ) := by
     simpa [fη, fζ, h_dist] using hφ_int
   have h_eta :
-      ∫ ω, φ (ξ ω, η ω) ∂μ = ∫ p, φ p ∂(Measure.map fη μ) := by
-    simpa [fη] using
-      (MeasureTheory.integral_map (μ := μ) (φ := fη) (f := φ)
-        hfη hφ).symm
+      ∫ ω, φ (ξ ω, η ω) ∂μ = ∫ p, φ p ∂(Measure.map fη μ) :=
+    Eq.symm (integral_map hfη hφ)
   have h_zeta :
-      ∫ ω, φ (ξ ω, ζ ω) ∂μ = ∫ p, φ p ∂(Measure.map fζ μ) := by
-    simpa [fζ] using
-      (MeasureTheory.integral_map (μ := μ) (φ := fζ) (f := φ)
-        hfζ hφ_meas_zeta).symm
-  calc
-    ∫ ω, φ (ξ ω, η ω) ∂μ
-        = ∫ p, φ p ∂(Measure.map fη μ) := h_eta
-    _ = ∫ p, φ p ∂(Measure.map fζ μ) := by simp [fη, fζ, h_dist]
-    _ = ∫ ω, φ (ξ ω, ζ ω) ∂μ := h_zeta.symm
+      ∫ ω, φ (ξ ω, ζ ω) ∂μ = ∫ p, φ p ∂(Measure.map fζ μ) :=
+    Eq.symm (integral_map hfζ hφ_meas_zeta)
+  lia
 
 /-- If `(ξ, η)` and `(ξ, ζ)` share the same joint law, then for every measurable `g` and
 measurable set `s`, the mixed moments `E[g(ξ) · 𝟙_{η ∈ s}]` and `E[g(ξ) · 𝟙_{ζ ∈ s}]` agree. -/
@@ -409,10 +401,8 @@ theorem condExp_project_of_condIndepFun
     specialize hCI A B hA hB
     -- Key: (Y ⁻¹' A).indicator 1 * (Z ⁻¹' B).indicator 1 = (Y ⁻¹' A ∩ Z ⁻¹' B).indicator 1
     have h_prod_eq : (Y ⁻¹' A).indicator (1 : Ω → ℝ) * (Z ⁻¹' B).indicator (1 : Ω → ℝ) =
-        (Y ⁻¹' A ∩ Z ⁻¹' B).indicator (1 : Ω → ℝ) := by
-      ext x
-      convert (Set.inter_indicator_mul (s := Y ⁻¹' A) (t := Z ⁻¹' B) (fun _ : Ω => (1 : ℝ)) (fun _ => 1) x).symm
-      simp [mul_one]
+        (Y ⁻¹' A ∩ Z ⁻¹' B).indicator (1 : Ω → ℝ) :=
+      Eq.symm inter_indicator_one
     rw [h_prod_eq]
     -- Now apply the CondIndepFun characterization. The convert automatically handles
     -- the notation matching between `1` and `fun ω => 1`
@@ -1144,10 +1134,8 @@ theorem condExp_project_of_condIndepFun
         simpa using h_norm_int.const_mul 2
 
       -- Measurability of f_n ∘ Y
-      have h_fn_meas : ∀ n, @AEStronglyMeasurable Ω ℝ _ mΩ mΩ (f_n n ∘ Y) μ := by
-        intro n
-        have : Measurable (f_n n) := (f_n n).measurable
-        exact this.aestronglyMeasurable.comp_measurable hY
+      have h_fn_meas : ∀ n, @AEStronglyMeasurable Ω ℝ _ mΩ mΩ (f_n n ∘ Y) μ :=
+        fun n => Integrable.aestronglyMeasurable (h_fn_int n)
 
       -- Step 1: Get L¹ convergence of conditional expectations using DCT
       have h_L1_conv : Filter.Tendsto
@@ -1275,8 +1263,8 @@ theorem condExp_project_of_condIndepFun
       calc
         ‖μ[ f_n n ∘ Y | mW ] ω * μ[ (Z ⁻¹' B).indicator 1 | mW ] ω‖
             = ‖μ[ f_n n ∘ Y | mW ] ω‖ * ‖μ[ (Z ⁻¹' B).indicator 1 | mW ] ω‖ := this
-        _ ≤ ‖μ[ f_n n ∘ Y | mW ] ω‖ := by
-              exact mul_le_of_le_one_right (norm_nonneg _) h_ind
+        _ ≤ ‖μ[ f_n n ∘ Y | mW ] ω‖ :=
+              mul_le_of_le_one_right (norm_nonneg _) h_ind
         _ ≤ μ[ (fun ω => ‖(f_n n ∘ Y) ω‖) | mW ] ω := by
               -- Jensen for conditional expectation
               simpa using (norm_condExp_le
@@ -1681,9 +1669,7 @@ theorem condExp_project_of_condIndepFun
                       ∫ x in S, g x * μ[(Z ⁻¹' B).indicator 1|mW] x ∂μ := by
       apply setIntegral_congr_ae (hmW_le _ hS)
       filter_upwards [h_factor] with ω hω _
-      simp only [Pi.mul_apply] at hω
-      rw [hg_def]
-      exact hω
+      assumption
 
     -- Finally, connect via condExp_mul_of_stronglyMeasurable_left with g
     -- Since g = μ[f∘Y|mW] is mW-strongly measurable, we can pull it through:
@@ -1728,10 +1714,7 @@ theorem condExp_project_of_condIndepFun
     -- Combine h_g_mult and h_tower_lhs
     have h_combine : S.indicator 1 * μ[g * (Z ⁻¹' B).indicator 1|mW] =ᵐ[μ]
                      S.indicator 1 * (g * μ[(Z ⁻¹' B).indicator 1|mW]) := by
-      filter_upwards [h_g_mult] with ω hω
-      by_cases hS : ω ∈ S
-      · simp [Set.indicator_of_mem hS, hω]
-      · simp [Set.indicator_of_notMem hS]
+      exact EventuallyEq.mul_left h_g_mult
 
     -- Integrate h_tower_lhs
     have h_int_lhs : ∫ x, S.indicator 1 x * (g x * (Z ⁻¹' B).indicator 1 x) ∂μ =
@@ -1856,8 +1839,8 @@ theorem condExp_project_of_condIndepFun
 
     -- Apply π-λ induction using induction_on_inter
     -- We need to show: ∀ S, @MeasurableSet Ω mZW S → (μ S < ⊤ → ∫_S g = ∫_S f(Y))
-    suffices ∀ S (hS : @MeasurableSet Ω mZW S), μ S < ⊤ → ∫ x in S, g x ∂μ = ∫ x in S, (f ∘ Y) x ∂μ by
-      exact this T hT hμT
+    suffices ∀ S (hS : @MeasurableSet Ω mZW S), μ S < ⊤ → ∫ x in S, g x ∂μ = ∫ x in S, (f ∘ Y) x ∂μ
+      this T hT hμT
 
     intro S hS
 
@@ -1892,8 +1875,8 @@ theorem condExp_project_of_condIndepFun
       -- Convert measurability from mZW to mΩ
       have hS'_meas_mΩ : @MeasurableSet Ω mΩ S' := hmZW_le _ hS'_meas
 
-      have hg_add : ∫ x in S', g x ∂μ + ∫ x in S'ᶜ, g x ∂μ = ∫ x, g x ∂μ := by
-        exact integral_add_compl hS'_meas_mΩ integrable_condExp
+      have hg_add : ∫ x in S', g x ∂μ + ∫ x in S'ᶜ, g x ∂μ = ∫ x, g x ∂μ :=
+        integral_add_compl hS'_meas_mΩ integrable_condExp
       have hf_add : ∫ x in S', (f ∘ Y) x ∂μ + ∫ x in S'ᶜ, (f ∘ Y) x ∂μ = ∫ x, (f ∘ Y) x ∂μ := by
         exact integral_add_compl hS'_meas_mΩ hf_int
 
@@ -1909,12 +1892,7 @@ theorem condExp_project_of_condIndepFun
       -- Apply h_rect_all to univ to get ∫ g = ∫ f∘Y
       have huniv_eq : ∫ x, g x ∂μ = ∫ x, (f ∘ Y) x ∂μ := by
         -- Key insight: univ = Z⁻¹(univ) ∩ W⁻¹(univ) ∈ 𝓡, so we can use h_rect_all!
-        have huniv_in_R : Set.univ ∈ 𝓡 := by
-          refine ⟨Set.univ, Set.univ, MeasurableSet.univ, MeasurableSet.univ, ?_⟩
-          ext ω
-          simp only [Set.mem_univ, Set.mem_inter_iff, Set.mem_preimage, true_and]
-        have h := h_rect_all Set.univ huniv_in_R (measure_lt_top μ Set.univ)
-        rwa [setIntegral_univ, setIntegral_univ] at h
+        exact integral_condExp hmW_le
 
       -- Now we can complete the calc
       calc ∫ x in S'ᶜ, g x ∂μ
@@ -1928,9 +1906,7 @@ theorem condExp_project_of_condIndepFun
 
       -- Each Sₙ has finite measure (since sum is finite)
       have hSeq_finite : ∀ n, μ (Sseq n) < ⊤ := by
-        intro n
-        calc μ (Sseq n) ≤ μ (⋃ i, Sseq i) := measure_mono (Set.subset_iUnion Sseq n)
-          _ < ⊤ := hμUnion
+        exact fun n => measure_lt_top μ (Sseq n)
 
       -- Apply IH to each Sₙ
       have hSeq_eq : ∀ n, ∫ x in Sseq n, g x ∂μ = ∫ x in Sseq n, (f ∘ Y) x ∂μ := by
@@ -1948,9 +1924,7 @@ theorem condExp_project_of_condIndepFun
             apply integral_iUnion hSeq_meas_mΩ hSeq_disj
             exact integrable_condExp.integrableOn
         _ = ∑' n, ∫ x in Sseq n, (f ∘ Y) x ∂μ := by
-            congr 1
-            ext n
-            exact hSeq_eq n
+            exact tsum_congr hSeq_eq
         _ = ∫ x in ⋃ n, Sseq n, (f ∘ Y) x ∂μ := by
             symm
             apply integral_iUnion hSeq_meas_mΩ hSeq_disj
diff --git a/Exchangeability/Probability/CondExpHelpers/Convergence.lean b/Exchangeability/Probability/CondExpHelpers/Convergence.lean
index 9c84d29c..bdaa82cc 100644
--- a/Exchangeability/Probability/CondExpHelpers/Convergence.lean
+++ b/Exchangeability/Probability/CondExpHelpers/Convergence.lean
@@ -35,14 +35,8 @@ lemma tendsto_condExpL1_domconv
     (h_int : Integrable bound μ)
     (hbound : ∀ n, ∀ᵐ x ∂μ, ‖fs n x‖ ≤ bound x)
     (hpt : ∀ᵐ x ∂μ, Filter.Tendsto (fun n => fs n x) Filter.atTop (nhds (f x))) :
-    Filter.Tendsto (fun n => condExpL1 hm μ (fs n)) Filter.atTop (nhds (condExpL1 hm μ f)) := by
-  classical
-  -- This is exactly mathlib's lemma; we just instantiate the parameters.
-  simpa using
-    (MeasureTheory.tendsto_condExpL1_of_dominated_convergence
-      (μ := μ) (hm := hm) (fs := fs) (f := f)
-      (bound_fs := bound) (hfs_meas := hfs_meas) (h_int_bound_fs := h_int)
-      (hfs_bound := hbound) (hfs := hpt))
+    Filter.Tendsto (fun n => condExpL1 hm μ (fs n)) Filter.atTop (nhds (condExpL1 hm μ f)) :=
+  tendsto_condExpL1_of_dominated_convergence hm bound hfs_meas h_int hbound hpt
 
 /-- From L¹ convergence of `condExpL1` to a.e. convergence of a subsequence of its representatives. -/
 lemma exists_subseq_ae_tendsto_of_condExpL1_tendsto
diff --git a/Exchangeability/Probability/CondExpHelpers/Integrability.lean b/Exchangeability/Probability/CondExpHelpers/Integrability.lean
index bb345a47..dea84a77 100644
--- a/Exchangeability/Probability/CondExpHelpers/Integrability.lean
+++ b/Exchangeability/Probability/CondExpHelpers/Integrability.lean
@@ -192,9 +192,7 @@ lemma tendsto_set_integral_mul_of_L1 {α : Type*} [MeasurableSpace α] {μ : Mea
             congr 1; ext ω
             -- Need: ↑‖fn n ω - f ω‖₊ * ↑(Real.toNNReal C) = ENNReal.ofReal C * ↑‖fn n ω - f ω‖₊
             rw [mul_comm]
-            simp only [ENNReal.ofReal_eq_coe_nnreal hC]
-            congr 1
-            exact congr_arg ENNReal.ofNNReal (Real.toNNReal_of_nonneg hC)
+            rfl
     -- Apply squeeze theorem with C * hL1 → C * 0 = 0
     have h_limit : Filter.Tendsto (fun n => ENNReal.ofReal C * ∫⁻ ω, ‖(fn n) ω - f ω‖₊ ∂μ)
         Filter.atTop (nhds 0) := by
diff --git a/Exchangeability/Probability/CondIndep/Bounded/Approximation.lean b/Exchangeability/Probability/CondIndep/Bounded/Approximation.lean
index 319d0e7c..7910b5a7 100644
--- a/Exchangeability/Probability/CondIndep/Bounded/Approximation.lean
+++ b/Exchangeability/Probability/CondIndep/Bounded/Approximation.lean
@@ -518,9 +518,7 @@ lemma tendsto_condExp_L1_of_dominated
     filter_upwards [hfn_bdd n, hf_bdd] with ω hn hf
     calc |fn n ω - f ω|
         ≤ |fn n ω| + |f ω| := by
-          have := abs_add_le (fn n ω) (-(f ω))
-          simp only [abs_neg, ← sub_eq_add_neg] at this
-          exact this
+          exact abs_sub (fn n ω) (f ω)
       _ ≤ M + M := add_le_add hn hf
       _ = 2 * M := by ring
   have h_L1 := tendsto_L1_of_pointwise_dominated μ M hM_nn hfn_int hf_int h_bound h_tendsto
diff --git a/Exchangeability/Probability/CondIndep/Bounded/Extension.lean b/Exchangeability/Probability/CondIndep/Bounded/Extension.lean
index a8661e11..156ff021 100644
--- a/Exchangeability/Probability/CondIndep/Bounded/Extension.lean
+++ b/Exchangeability/Probability/CondIndep/Bounded/Extension.lean
@@ -65,8 +65,8 @@ lemma condIndep_simpleFunc_left
     · exact Finset.sum_nonneg (fun _ _ => abs_nonneg _)
     · intro a
       have h_mem := φ.mem_range_self a
-      calc |φ a| ≤ |φ a| + (φ.range.erase (φ a)).sum (fun x => |x|) := by
-            exact le_add_of_nonneg_right (Finset.sum_nonneg (fun _ _ => abs_nonneg _))
+      calc |φ a| ≤ |φ a| + (φ.range.erase (φ a)).sum (fun x => |x|) :=
+            le_add_of_nonneg_right (Finset.sum_nonneg (fun _ _ => abs_nonneg _))
         _ = φ.range.sum (fun x => |x|) := by
             rw [← Finset.add_sum_erase _ _ h_mem]
   obtain ⟨Mφ, hMφ_nn, hφ_bdd⟩ := hMφ
@@ -105,10 +105,10 @@ lemma condIndep_simpleFunc_left
           _ ≤ |ψ (Z ω)| := h_sψ_bdd n (Z ω)
           _ ≤ Mψ := hω
       calc ∫ ω in C, ((φ ∘ Y) * ((sψ n) ∘ Z)) ω ∂μ
-          = ∫ ω in C, μ[((φ ∘ Y) * ((sψ n) ∘ Z)) | mW] ω ∂μ := by
-              exact (setIntegral_condExp hmW_le hprod_int hC).symm
-        _ = ∫ ω in C, (μ[(φ ∘ Y) | mW] * μ[((sψ n) ∘ Z) | mW]) ω ∂μ := by
-              exact setIntegral_congr_ae (hmW_le _ hC) (by filter_upwards [h_rect_n n] with x hx _; exact hx)
+          = ∫ ω in C, μ[((φ ∘ Y) * ((sψ n) ∘ Z)) | mW] ω ∂μ :=
+              (setIntegral_condExp hmW_le hprod_int hC).symm
+        _ = ∫ ω in C, (μ[(φ ∘ Y) | mW] * μ[((sψ n) ∘ Z) | mW]) ω ∂μ :=
+              setIntegral_congr_ae (hmW_le _ hC) (by filter_upwards [h_rect_n n] with x hx _; exact hx)
 
     -- Step 4: LHS convergence via DCT
     have hLHS :
@@ -204,15 +204,8 @@ lemma condIndep_simpleFunc_left
       -- Step 5b: Push through conditional expectation
       have h_ce_conv : Filter.Tendsto
           (fun n => ∫ ω, |μ[((sψ n) ∘ Z) | mW] ω - μ[(ψ ∘ Z) | mW] ω| ∂μ)
-          Filter.atTop (nhds 0) := by
-        have hsψ_int : ∀ n, Integrable ((sψ n) ∘ Z) μ := fun n =>
-          ((sψ n).integrable_of_isFiniteMeasure).comp_measurable hZ
-        have hψ_int : Integrable (ψ ∘ Z) μ := by
-          refine Integrable.of_mem_Icc (-Mψ) Mψ (hψ_meas.comp hZ).aemeasurable ?_
-          filter_upwards [hψ_bdd] with ω hω
-          simp only [Function.comp_apply, Set.mem_Icc]
-          exact abs_le.mp hω
-        exact tendsto_condexp_L1 μ mW hmW_le hsψ_int hψ_int h_conv
+          Filter.atTop (nhds 0) :=
+        tendsto_condexp_L1 μ mW hmW_le hsψZ_int hψZ_int' h_conv
 
       -- Step 5c: Product L¹ convergence: φY bounded * (sψZ - ψZ) → 0
       have h_prod_L1 : Filter.Tendsto
@@ -238,9 +231,7 @@ lemma condIndep_simpleFunc_left
               |(μ[(φ ∘ Y) | mW] ω) * (μ[((sψ n) ∘ Z) | mW] ω - μ[(ψ ∘ Z) | mW] ω)|) μ := by
             have h_bdd_asm := (integrable_condExp (μ := μ) (m := mW) (f := φ ∘ Y)).aestronglyMeasurable
             have h_bdd_bound : ∀ᵐ ω ∂μ, ‖μ[(φ ∘ Y) | mW] ω‖ ≤ Mφ := by
-              filter_upwards [hφY_bdd] with ω hω
-              rw [Real.norm_eq_abs]
-              exact hω
+              assumption
             have h_diff_int' : Integrable (μ[((sψ n) ∘ Z) | mW] - μ[(ψ ∘ Z) | mW]) μ :=
               integrable_condExp.sub integrable_condExp
             have h_prod : Integrable (fun ω => μ[(φ ∘ Y) | mW] ω * (μ[((sψ n) ∘ Z) | mW] ω - μ[(ψ ∘ Z) | mW] ω)) μ :=
@@ -271,17 +262,13 @@ lemma condIndep_simpleFunc_left
         refine Integrable.bdd_mul (c := Mφ)
           (integrable_condExp (m := mW) (f := (sψ n) ∘ Z))
           (integrable_condExp (m := mW) (f := φ ∘ Y)).aestronglyMeasurable ?_
-        filter_upwards [hφY_bdd] with ω hω
-        rw [Real.norm_eq_abs]
-        exact hω
+        assumption
 
       have h_int_prod_lim : Integrable (μ[(φ ∘ Y) | mW] * μ[(ψ ∘ Z) | mW]) μ := by
         refine Integrable.bdd_mul (c := Mφ)
           (integrable_condExp (m := mW) (f := ψ ∘ Z))
           (integrable_condExp (m := mW) (f := φ ∘ Y)).aestronglyMeasurable ?_
-        filter_upwards [hφY_bdd] with ω hω
-        rw [Real.norm_eq_abs]
-        exact hω
+        assumption
 
       have h_diff_L1_bochner : Filter.Tendsto
           (fun n => ∫ ω, |(μ[(φ ∘ Y) | mW] * μ[((sψ n) ∘ Z) | mW]) ω -
@@ -361,9 +348,7 @@ lemma condIndep_simpleFunc_left
     -- Actually: ψ is bounded, φ is integrable, so use φ as hg, ψ as hf
     have h_prod : Integrable ((ψ ∘ Z) * (φ ∘ Y)) μ := by
       refine Integrable.bdd_mul (c := Mψ) hφ_int (hψ_meas.comp hZ).aestronglyMeasurable ?_
-      filter_upwards [hψ_bdd] with ω hω
-      rw [Real.norm_eq_abs]
-      exact hω
+      assumption
     convert h_prod using 1
     ext ω; exact mul_comm ((φ ∘ Y) ω) ((ψ ∘ Z) ω)
 
@@ -389,9 +374,7 @@ lemma condIndep_simpleFunc_left
       -- So hf = μ[φY|mW], hg = μ[ψZ|mW], but ψZ is bounded so use it as hf
       have h_prod : Integrable (μ[(ψ ∘ Z) | mW] * μ[(φ ∘ Y) | mW]) μ := by
         refine h1.bdd_mul (c := Mψ) h2.aestronglyMeasurable ?_
-        filter_upwards [hψZ_ce_bdd] with ω hω
-        rw [Real.norm_eq_abs]
-        exact hω
+        assumption
       convert h_prod using 1
       ext ω; exact mul_comm (μ[(φ ∘ Y) | mW] ω) (μ[(ψ ∘ Z) | mW] ω)
     exact hprod.integrableOn
@@ -474,10 +457,10 @@ lemma condIndep_bddMeas_extend_left
           _ ≤ Mφ := hω
       -- Use setIntegral_condExp followed by setIntegral_congr_ae
       calc ∫ ω in C, ((sφ n ∘ Y) * (ψ ∘ Z)) ω ∂μ
-          = ∫ ω in C, μ[((sφ n ∘ Y) * (ψ ∘ Z)) | mW] ω ∂μ := by
-              exact (setIntegral_condExp hmW_le hprod_int hC).symm
-        _ = ∫ ω in C, (μ[(sφ n ∘ Y) | mW] * μ[(ψ ∘ Z) | mW]) ω ∂μ := by
-              exact setIntegral_congr_ae (hmW_le _ hC) (by filter_upwards [h_rect_n n] with x hx _; exact hx)
+          = ∫ ω in C, μ[((sφ n ∘ Y) * (ψ ∘ Z)) | mW] ω ∂μ :=
+              (setIntegral_condExp hmW_le hprod_int hC).symm
+        _ = ∫ ω in C, (μ[(sφ n ∘ Y) | mW] * μ[(ψ ∘ Z) | mW]) ω ∂μ :=
+              setIntegral_congr_ae (hmW_le _ hC) (by filter_upwards [h_rect_n n] with x hx _; exact hx)
 
     -- Limit passage n→∞ on both sides.
     -- LHS: DCT
@@ -622,8 +605,8 @@ lemma condIndep_bddMeas_extend_left
             filter_upwards [hψZ_bdd] with ω hω
             rw [abs_mul]
             calc |μ[((sφ n) ∘ Y) | mW] ω - μ[(φ ∘ Y) | mW] ω| * |μ[(ψ ∘ Z) | mW] ω|
-                ≤ |μ[((sφ n) ∘ Y) | mW] ω - μ[(φ ∘ Y) | mW] ω| * Mψ := by
-                  exact mul_le_mul_of_nonneg_left hω (abs_nonneg _)
+                ≤ |μ[((sφ n) ∘ Y) | mW] ω - μ[(φ ∘ Y) | mW] ω| * Mψ :=
+                  mul_le_mul_of_nonneg_left hω (abs_nonneg _)
               _ = Mψ * |μ[((sφ n) ∘ Y) | mW] ω - μ[(φ ∘ Y) | mW] ω| := by ring
           -- Integrate the a.e. inequality
           have h_lhs_int : Integrable (fun ω =>
@@ -634,9 +617,7 @@ lemma condIndep_bddMeas_extend_left
               integrable_condExp.sub integrable_condExp
             have h_bdd_asm := (integrable_condExp (μ := μ) (m := mW) (f := ψ ∘ Z)).aestronglyMeasurable
             have h_bdd_bound : ∀ᵐ ω ∂μ, ‖μ[(ψ ∘ Z) | mW] ω‖ ≤ Mψ := by
-              filter_upwards [hψZ_bdd] with ω hω
-              rw [Real.norm_eq_abs]
-              exact hω
+              assumption
             have h_prod : Integrable (fun ω => μ[(ψ ∘ Z) | mW] ω * (μ[((sφ n) ∘ Y) | mW] ω - μ[(φ ∘ Y) | mW] ω)) μ :=
               h_diff_int'.bdd_mul h_bdd_asm h_bdd_bound
             -- Swap order using mul_comm, then take abs
@@ -644,11 +625,11 @@ lemma condIndep_bddMeas_extend_left
             ext ω
             rw [abs_mul, abs_mul, mul_comm]
           have h_rhs_int : Integrable (fun ω =>
-              Mψ * |μ[((sφ n) ∘ Y) | mW] ω - μ[(φ ∘ Y) | mW] ω|) μ := by
-            exact (integrable_condExp.sub integrable_condExp).abs.const_mul Mψ
+              Mψ * |μ[((sφ n) ∘ Y) | mW] ω - μ[(φ ∘ Y) | mW] ω|) μ :=
+            (integrable_condExp.sub integrable_condExp).abs.const_mul Mψ
           calc ∫ ω, |(μ[((sφ n) ∘ Y) | mW] ω - μ[(φ ∘ Y) | mW] ω) * μ[(ψ ∘ Z) | mW] ω| ∂μ
-              ≤ ∫ ω, Mψ * |μ[((sφ n) ∘ Y) | mW] ω - μ[(φ ∘ Y) | mW] ω| ∂μ := by
-                exact integral_mono_ae h_lhs_int h_rhs_int h_bd
+              ≤ ∫ ω, Mψ * |μ[((sφ n) ∘ Y) | mW] ω - μ[(φ ∘ Y) | mW] ω| ∂μ :=
+                integral_mono_ae h_lhs_int h_rhs_int h_bd
             _ = Mψ * ∫ ω, |μ[((sφ n) ∘ Y) | mW] ω - μ[(φ ∘ Y) | mW] ω| ∂μ := by
                 rw [integral_const_mul]
 
@@ -681,9 +662,7 @@ lemma condIndep_bddMeas_extend_left
           refine Integrable.bdd_mul (c := Mψ)
             (integrable_condExp (m := mW) (f := (sφ n) ∘ Y))
             (integrable_condExp (m := mW) (f := ψ ∘ Z)).aestronglyMeasurable ?_
-          filter_upwards [hψZ_bdd] with ω hω
-          rw [Real.norm_eq_abs]
-          exact hω
+          assumption
         -- Swap the order
         simpa only [mul_comm] using h_prod
       have h_int_limit : Integrable (μ[(φ ∘ Y) | mW] * μ[(ψ ∘ Z) | mW]) μ := by
@@ -691,9 +670,7 @@ lemma condIndep_bddMeas_extend_left
           refine Integrable.bdd_mul (c := Mψ)
             (integrable_condExp (m := mW) (f := φ ∘ Y))
             (integrable_condExp (m := mW) (f := ψ ∘ Z)).aestronglyMeasurable ?_
-          filter_upwards [hψZ_bdd] with ω hω
-          rw [Real.norm_eq_abs]
-          exact hω
+          assumption
         simpa only [mul_comm] using h_prod
 
       -- Use that |∫_C (fn - f)| ≤ ∫|fn - f| → 0
@@ -761,10 +738,7 @@ lemma condIndep_bddMeas_extend_left
     -- Use Integrable.bdd_mul: requires hg integrable, hf ae strongly measurable, hf bounded a.e.
     refine Integrable.bdd_mul (c := Mφ) hψZ_int (hφ_meas.comp hY).aestronglyMeasurable ?_
     -- Need: ∀ᵐ ω ∂μ, ‖(φ ∘ Y) ω‖ ≤ Mφ
-    filter_upwards [hφ_bdd] with ω hω
-    simp only [Function.comp_apply]
-    rw [Real.norm_eq_abs]
-    exact hω
+    assumption
 
   -- Apply the uniqueness characterization lemma (gives g =ᵐ μ[f|m], need symm)
   refine (ae_eq_condExp_of_forall_setIntegral_eq hmW_le hf_int ?_ ?_ ?_).symm
@@ -791,9 +765,7 @@ lemma condIndep_bddMeas_extend_left
       -- Apply Integrable.bdd_mul: g integrable, f ae strongly measurable and bounded
       -- Use h1.aestronglyMeasurable since h1 : Integrable (μ[(φ ∘ Y) | mW]) μ
       refine h2.bdd_mul (c := Mφ) h1.aestronglyMeasurable ?_
-      filter_upwards [hφY_ce_bdd] with ω hω
-      rw [Real.norm_eq_abs]
-      exact hω
+      assumption
     -- Product integrable on whole space implies integrable on subset
     exact hprod.integrableOn
 
diff --git a/Exchangeability/Probability/CondIndep/Bounded/Projection.lean b/Exchangeability/Probability/CondIndep/Bounded/Projection.lean
index a22a75bf..1d11f4cc 100644
--- a/Exchangeability/Probability/CondIndep/Bounded/Projection.lean
+++ b/Exchangeability/Probability/CondIndep/Bounded/Projection.lean
@@ -136,9 +136,7 @@ lemma condExp_project_of_condIndep (μ : Measure Ω) [IsProbabilityMeasure μ]
       -- (Z⁻¹B₁ ∩ W⁻¹C₁) ∩ (Z⁻¹B₂ ∩ W⁻¹C₂) = Z⁻¹(B₁ ∩ B₂) ∩ W⁻¹(C₁ ∩ C₂)
       use B₁ ∩ B₂, C₁ ∩ C₂
       refine ⟨hB₁.inter hB₂, hC₁.inter hC₂, ?_⟩
-      ext ω
-      simp only [Set.mem_inter_iff, Set.mem_preimage]
-      tauto
+      grind only [= mem_inter_iff, = mem_preimage]
 
     -- Apply π-λ induction
     intro s hs hμs
@@ -209,19 +207,15 @@ lemma condExp_project_of_condIndep (μ : Measure Ω) [IsProbabilityMeasure μ]
       -- Rectangle is in mZW
       have hrect : MeasurableSet[mZW] (Z ⁻¹' B ∩ W ⁻¹' C) := by
         -- Z⁻¹B ∩ W⁻¹C = (Z,W)⁻¹(B ×ˢ C)
-        have : Z ⁻¹' B ∩ W ⁻¹' C = (fun ω => (Z ω, W ω)) ⁻¹' (B ×ˢ C) := by
-          ext ω
-          simp only [Set.mem_inter_iff, Set.mem_preimage, Set.mem_prod]
-        rw [this]
-        exact measurableSet_preimage (Measurable.of_comap_le le_rfl) (hB.prod hC)
+        exact MeasurableSet.inter hBpre hCpre_mZW
 
       -- By setIntegral_condExp on mZW
-      have h1 : ∫ x in Z ⁻¹' B ∩ W ⁻¹' C, (μ[f | mZW]) x ∂μ = ∫ x in Z ⁻¹' B ∩ W ⁻¹' C, f x ∂μ := by
-        exact setIntegral_condExp hmZW_le hf_int hrect
+      have h1 : ∫ x in Z ⁻¹' B ∩ W ⁻¹' C, (μ[f | mZW]) x ∂μ = ∫ x in Z ⁻¹' B ∩ W ⁻¹' C, f x ∂μ :=
+        setIntegral_condExp hmZW_le hf_int hrect
 
       -- By tower property: E[E[f|mZW]|mW] = E[f|mW] (since mW ≤ mZW)
-      have h2 : μ[μ[f | mZW] | mW] =ᵐ[μ] μ[f | mW] := by
-        exact condExp_condExp_of_le hle hmZW_le
+      have h2 : μ[μ[f | mZW] | mW] =ᵐ[μ] μ[f | mW] :=
+        condExp_condExp_of_le hle hmZW_le
 
       -- So ∫_{rectangle} E[f|mW] = ∫_{rectangle} E[E[f|mZW]|mW]
       have h3 : ∫ x in Z ⁻¹' B ∩ W ⁻¹' C, (μ[f | mW]) x ∂μ =
@@ -239,10 +233,8 @@ lemma condExp_project_of_condIndep (μ : Measure Ω) [IsProbabilityMeasure μ]
 
           -- Rewrite LHS using h2
           have : ∫ x in Z ⁻¹' B ∩ W ⁻¹' C, (μ[μ[f | mZW] | mW]) x ∂μ =
-                 ∫ x in Z ⁻¹' B ∩ W ⁻¹' C, (μ[f | mW]) x ∂μ := by
-            apply setIntegral_congr_ae (hmZW_le _ hrect)
-            filter_upwards [h2] with x hx _
-            exact hx
+                 ∫ x in Z ⁻¹' B ∩ W ⁻¹' C, (μ[f | mW]) x ∂μ :=
+            Real.ext_cauchy (congrArg Real.cauchy (id (Eq.symm h3)))
           rw [this]
 
           -- Now show: ∫_{Z⁻¹B ∩ W⁻¹C} μ[f|mW] = ∫_{Z⁻¹B ∩ W⁻¹C} f
@@ -348,8 +340,8 @@ lemma condExp_project_of_condIndep (μ : Measure Ω) [IsProbabilityMeasure μ]
     · -- Complement
       intro t htm ht_ind
       -- For complement: ∫_{t} g + ∫_{tᶜ} g = ∫_Ω g, so ∫_{tᶜ} g = ∫_Ω g - ∫_t g
-      have h_add : ∫ x in t, (μ[f | mW]) x ∂μ + ∫ x in tᶜ, (μ[f | mW]) x ∂μ = ∫ x, (μ[f | mW]) x ∂μ := by
-        exact integral_add_compl₀ (hmZW_le _ htm).nullMeasurableSet integrable_condExp
+      have h_add : ∫ x in t, (μ[f | mW]) x ∂μ + ∫ x in tᶜ, (μ[f | mW]) x ∂μ = ∫ x, (μ[f | mW]) x ∂μ :=
+        integral_add_compl₀ (hmZW_le _ htm).nullMeasurableSet integrable_condExp
       have h_add' : ∫ x in t, f x ∂μ + ∫ x in tᶜ, f x ∂μ = ∫ x, f x ∂μ := by
         exact integral_add_compl₀ (hmZW_le _ htm).nullMeasurableSet hf_int
       -- ht_ind is the equality for t, use it to substitute in h_add
diff --git a/Exchangeability/Probability/CondIndep/Indicator.lean b/Exchangeability/Probability/CondIndep/Indicator.lean
index a583e7c6..0ccba298 100644
--- a/Exchangeability/Probability/CondIndep/Indicator.lean
+++ b/Exchangeability/Probability/CondIndep/Indicator.lean
@@ -128,8 +128,6 @@ theorem condIndep_of_indep_pair (μ : Measure Ω) [IsProbabilityMeasure μ]
   -- f = (Set.indicator A (fun _ => 1)) ∘ Y
   have hf_indep : IndepFun f W μ := by
     have : f = (Set.indicator A (fun _ => (1 : ℝ))) ∘ Y := by
-      ext ω
-      simp only [Function.comp_apply, Set.indicator_apply]
       rfl
     rw [this]
     exact hY_W_indep.comp (measurable_const.indicator hA) measurable_id
@@ -137,8 +135,6 @@ theorem condIndep_of_indep_pair (μ : Measure Ω) [IsProbabilityMeasure μ]
   -- Step 2: g is a function of Z, so g ⊥ W
   have hg_indep : IndepFun g W μ := by
     have : g = (Set.indicator B (fun _ => (1 : ℝ))) ∘ Z := by
-      ext ω
-      simp only [Function.comp_apply, Set.indicator_apply]
       rfl
     rw [this]
     exact hZ_W_indep.comp (measurable_const.indicator hB) measurable_id
@@ -168,12 +164,8 @@ theorem condIndep_of_indep_pair (μ : Measure Ω) [IsProbabilityMeasure μ]
   -- Since f is a function of Y and g is a function of Z, f ⊥ g follows from Y ⊥ Z
   have hfg_indep' : IndepFun f g μ := by
     have hf_comp : f = (Set.indicator A (fun _ => (1 : ℝ))) ∘ Y := by
-      ext ω
-      show f ω = Set.indicator A (fun _ => 1) (Y ω)
       rfl
     have hg_comp : g = (Set.indicator B (fun _ => (1 : ℝ))) ∘ Z := by
-      ext ω
-      show g ω = Set.indicator B (fun _ => 1) (Z ω)
       rfl
     rw [hf_comp, hg_comp]
     exact hYZ_indep.comp (measurable_const.indicator hA) (measurable_const.indicator hB)
@@ -238,8 +230,8 @@ lemma condIndep_indicator (μ : Measure Ω) [IsProbabilityMeasure μ]
         ext ω
         simp [Pi.smul_apply, Pi.mul_apply]
         ring
-    _ =ᵐ[μ] μ[ c • (Y ⁻¹' A).indicator (fun _ => 1) | mW ] * μ[ d • (Z ⁻¹' B).indicator (fun _ => 1) | mW ] := by
-        exact Filter.EventuallyEq.mul (condExp_smul c _ mW).symm (condExp_smul d _ mW).symm
+    _ =ᵐ[μ] μ[ c • (Y ⁻¹' A).indicator (fun _ => 1) | mW ] * μ[ d • (Z ⁻¹' B).indicator (fun _ => 1) | mW ] :=
+        Filter.EventuallyEq.mul (condExp_smul c _ mW).symm (condExp_smul d _ mW).symm
     _ =ᵐ[μ] μ[ (A.indicator (fun _ => c)) ∘ Y | mW ] * μ[ (B.indicator (fun _ => d)) ∘ Z | mW ] := by
         -- Prove c • (Y ⁻¹' A).indicator (fun _ => 1) = (A.indicator (fun _ => c)) ∘ Y
         have hY_ind : c • (Y ⁻¹' A).indicator (fun _ => 1) = (A.indicator (fun _ => c)) ∘ Y := by
diff --git a/Exchangeability/Probability/CondIndep/KallenbergIndicator.lean b/Exchangeability/Probability/CondIndep/KallenbergIndicator.lean
index fda0cf0d..32d8ab9b 100644
--- a/Exchangeability/Probability/CondIndep/KallenbergIndicator.lean
+++ b/Exchangeability/Probability/CondIndep/KallenbergIndicator.lean
@@ -137,10 +137,8 @@ lemma condIndep_indicator_of_dropInfoY
     condExp_mul_of_stronglyMeasurable_right hIndB_stronglyMeas_mZW hProd_int hIndA_int
 
   -- Step 2: From h_drop, substitute condExp mW (indA) for condExp mZW (indA)
-  have h_step2 : μ[indA | mZW] * indB =ᵐ[μ] μ[indA | mW] * indB := by
-    filter_upwards [h_drop] with ω hω
-    simp only [Pi.mul_apply]
-    rw [hω]
+  have h_step2 : μ[indA | mZW] * indB =ᵐ[μ] μ[indA | mW] * indB :=
+    Filter.EventuallyEq.mul_right (dropY A hA)
 
   -- Combine step 1 and step 2
   have h_step12 : μ[indA * indB | mZW] =ᵐ[μ] μ[indA | mW] * indB :=
diff --git a/Exchangeability/Probability/CondProb.lean b/Exchangeability/Probability/CondProb.lean
index ec7298ec..6c11ce38 100644
--- a/Exchangeability/Probability/CondProb.lean
+++ b/Exchangeability/Probability/CondProb.lean
@@ -120,10 +120,8 @@ lemma condProb_integral_eq {m₀ : MeasurableSpace Ω} {μ : Measure Ω}
   -- Rewrite as an integral over `B ∩ A` of the constant 1.
   have h_indicator :
       ∫ ω in B, A.indicator (fun _ : Ω => (1 : ℝ)) ω ∂μ
-        = ∫ ω in B ∩ A, (1 : ℝ) ∂μ := by
-    simpa [Set.inter_comm, Set.inter_left_comm, Set.inter_assoc]
-      using setIntegral_indicator (μ := μ) (s := B) (t := A)
-        (f := fun _ : Ω => (1 : ℝ)) hA
+        = ∫ ω in B ∩ A, (1 : ℝ) ∂μ :=
+    setIntegral_indicator hA
   -- Evaluate the integral of 1 over the set.
   have h_const : ∫ ω in B ∩ A, (1 : ℝ) ∂μ = (μ (B ∩ A)).toReal := by
     simp [Measure.real_def, Set.inter_comm]
diff --git a/Exchangeability/Probability/InfiniteProduct.lean b/Exchangeability/Probability/InfiniteProduct.lean
index 1d3874e0..5a257a1d 100644
--- a/Exchangeability/Probability/InfiniteProduct.lean
+++ b/Exchangeability/Probability/InfiniteProduct.lean
@@ -227,9 +227,7 @@ lemma cylinder_fintype {n : ℕ} :
         simp only [Set.mem_setOf_eq, Set.mem_pi]
         constructor
         · intro hf i (hi : i ∈ Finset.range n)
-          have hi' : i < n := Finset.mem_range.mp hi
-          simp only [hi', dite_true]
-          exact hf ⟨i, hi'⟩
+          exact (mem_dite_univ_right (i < n) (fun h => s ⟨i, h⟩) (f i)).mpr fun h => hf ⟨i, h⟩
         · intro hf ⟨i, hi⟩
           have hi' : i ∈ Finset.range n := Finset.mem_range.mpr hi
           specialize hf i hi'
@@ -309,10 +307,7 @@ lemma perm_eq {σ : Equiv.Perm ℕ} :
     refine Finset.prod_congr rfl fun i _ => ?_
     rw [Equiv.toEmbedding_apply, σ.symm_apply_apply]
   · intro j hj
-    simp only [Finset.mem_map, Equiv.toEmbedding_apply] at hj
-    obtain ⟨i, hi, rfl⟩ := hj
-    rw [show t (σ.symm (σ i)) = t i by rw [σ.symm_apply_apply]]
-    exact ht i
+    grind only
 
 end iidProduct
 
diff --git a/Exchangeability/Probability/IntegrationHelpers.lean b/Exchangeability/Probability/IntegrationHelpers.lean
index 9bd338df..df90f281 100644
--- a/Exchangeability/Probability/IntegrationHelpers.lean
+++ b/Exchangeability/Probability/IntegrationHelpers.lean
@@ -153,19 +153,9 @@ lemma L2_tendsto_implies_L1_tendsto_of_bounded
       _ ≤ (∫ ω, (|f n ω - g ω|) ^ 2 ∂μ) ^ (1/2 : ℝ) * (∫ ω, (1 : ℝ) ^ 2 ∂μ) ^ (1/2 : ℝ) := cs_abs
       _ = (∫ ω, (f n ω - g ω) ^ 2 ∂μ) ^ (1/2 : ℝ) * (∫ ω, (1 : ℝ) ^ 2 ∂μ) ^ (1/2 : ℝ) := by
           congr 1
-          apply congr_arg (· ^ (1/2 : ℝ))
-          apply integral_congr_ae
-          filter_upwards with ω
-          exact sq_abs _
+          simpa
       _ = (∫ ω, (f n ω - g ω) ^ 2 ∂μ) ^ (1/2 : ℝ) * 1 := by
-          congr 2
-          -- Show (∫ 1² ∂μ)^(1/2) = 1 for probability measure
-          have : ∫ ω, (1 : ℝ) ^ 2 ∂μ = 1 := by
-            simp only [one_pow, integral_const, smul_eq_mul, mul_one]
-            rw [Measure.real]
-            simp [measure_univ]
-          rw [this]
-          norm_num
+          simpa
       _ = (∫ ω, (f n ω - g ω) ^ 2 ∂μ) ^ (1/2 : ℝ) := by ring
 
   -- Step 3: Apply squeeze theorem
diff --git a/Exchangeability/Probability/LpNormHelpers.lean b/Exchangeability/Probability/LpNormHelpers.lean
index 44b0a62b..ed0bedc3 100644
--- a/Exchangeability/Probability/LpNormHelpers.lean
+++ b/Exchangeability/Probability/LpNormHelpers.lean
@@ -161,9 +161,7 @@ lemma memLp_of_abs_le_const
     MemLp f p μ := by
   -- Use MemLp.of_bound from mathlib
   apply MemLp.of_bound hf_meas.aestronglyMeasurable M
-  apply Filter.Eventually.mono hf_bdd
-  intro ω hω
-  exact (Real.norm_eq_abs _).le.trans hω
+  assumption
 
 /-- **Block average of bounded function is in L².**
 
diff --git a/Exchangeability/Tail/CondExpShiftInvariance.lean b/Exchangeability/Tail/CondExpShiftInvariance.lean
index b6d6faa7..240adf18 100644
--- a/Exchangeability/Tail/CondExpShiftInvariance.lean
+++ b/Exchangeability/Tail/CondExpShiftInvariance.lean
@@ -106,9 +106,7 @@ lemma condExp_shift_eq_condExp
       have h_int_map : Integrable f (Measure.map (X 0) μ) :=
         (integrable_map_measure hf_aesm_0 (hX_meas 0).aemeasurable).mpr hf_int
       rw [← h_map_eq] at h_int_map
-      have hf_aesm_n1 : AEStronglyMeasurable f (Measure.map (X (n + 1)) μ) :=
-        hf_meas.aestronglyMeasurable
-      exact (integrable_map_measure hf_aesm_n1 (hX_meas (n + 1)).aemeasurable).mp h_int_map
+      exact Integrable.comp_measurable h_int_map (hX_meas (n + 1))
 
     -- Apply uniqueness of conditional expectation
     -- The sub-σ-algebra condition
@@ -116,15 +114,11 @@ lemma condExp_shift_eq_condExp
       simp only [tailFamily]
       apply iSup_le
       intro k
-      have h_eq : (fun ω => X (0 + k) ω) = X k := by simp only [Nat.zero_add]
-      rw [h_eq]
-      exact (hX_meas k).comap_le)
+      exact measurable_iff_comap_le.mp (hX_meas (0 + k)))
 
     -- σ-finiteness of trimmed measure (automatic for probability measures)
-    haveI h_finite : IsFiniteMeasure (μ.trim h_le) := by
-      constructor
-      rw [trim_measurableSet_eq h_le MeasurableSet.univ]
-      exact measure_lt_top μ Set.univ
+    haveI h_finite : IsFiniteMeasure (μ.trim h_le) :=
+      isFiniteMeasure_trim h_le
     haveI : SigmaFinite (μ.trim h_le) := @IsFiniteMeasure.toSigmaFinite _ _ _ h_finite
 
     -- Use ae_eq_condExp_of_forall_setIntegral_eq
diff --git a/Exchangeability/Tail/ShiftInvariantMeasure.lean b/Exchangeability/Tail/ShiftInvariantMeasure.lean
index b75720d4..cdd3a856 100644
--- a/Exchangeability/Tail/ShiftInvariantMeasure.lean
+++ b/Exchangeability/Tail/ShiftInvariantMeasure.lean
@@ -215,17 +215,10 @@ private lemma setIntegral_cylinder_eq
 
   have hS_σ : ∀ ω, ((fun i : Fin (M + 2) => X (σ ⟨i.val + 1, by omega⟩) ω) ∈ S) ↔ ω ∈ C' := by
     intro ω
-    simp only [Set.mem_setOf_eq, C']
-    constructor
-    · intro h; convert h using 1
-    · intro h; convert h using 1
+    rfl
 
   have hS_τ : ∀ ω, ((fun i : Fin (M + 2) => X (τ ⟨i.val + 1, by omega⟩) ω) ∈ S) ↔ ω ∈ C' := by
-    intro ω
-    simp only [Set.mem_setOf_eq, C']
-    constructor
-    · intro h; convert h using 1
-    · intro h; convert h using 1
+    assumption
 
   have hg_σ : ∀ ω, g (fun i => X (σ i) ω) = f (X (k + 1) ω) * (C'.indicator 1 ω) := by
     intro ω
@@ -275,9 +268,7 @@ private lemma setIntegral_cylinder_eq
           filter_upwards with ω
           exact h_ind_eq_k ω
     _ = ∫ ω, g (fun i => X (σ i) ω) ∂μ := by
-          apply integral_congr_ae
-          filter_upwards with ω
-          rw [hg_σ]
+          rfl
     _ = ∫ z, g z ∂(Measure.map (fun ω i => X (σ i) ω) μ) := by
           rw [integral_map hσ_meas.aemeasurable]
           apply Measurable.aestronglyMeasurable
@@ -294,9 +285,7 @@ private lemma setIntegral_cylinder_eq
           · apply Measurable.indicator measurable_const
             exact MeasurableSet.preimage _hS (by fun_prop)
     _ = ∫ ω, f (X 0 ω) * (C'.indicator 1 ω) ∂μ := by
-          apply integral_congr_ae
-          filter_upwards with ω
-          rw [hg_τ]
+          rfl
     _ = ∫ ω, C'.indicator (fun ω => f (X 0 ω)) ω ∂μ := by
           apply integral_congr_ae
           filter_upwards with ω
@@ -573,9 +562,7 @@ lemma setIntegral_comp_shift_eq
           have hω_ft := (Set.mem_iInter.mp (Set.mem_iInter.mp hω
             (indices.get ⟨i.val, by rw [h_len]; exact i.isLt⟩))) h_idx_mem
           rw [(hTj _ h_idx_mem).2] at hω_ft
-          simp only [Set.mem_preimage] at hω_ft
-          rw [hσ_succ i]
-          exact hω_ft
+          assumption
         · intro hS_mem
           simp only [C, Set.mem_iInter]
           intro j hj
diff --git a/Exchangeability/Tail/TailSigma.lean b/Exchangeability/Tail/TailSigma.lean
index c6280cf5..514b63a5 100644
--- a/Exchangeability/Tail/TailSigma.lean
+++ b/Exchangeability/Tail/TailSigma.lean
@@ -99,13 +99,7 @@ namespace MeasurableSpace
 lemma preimage_injective_of_surjective {α β} {f : α → β}
     (hf : Function.Surjective f) :
   Function.Injective (fun (s : Set β) => f ⁻¹' s) := by
-  intro s t hpre
-  have : f ⁻¹' s = f ⁻¹' t := hpre
-  ext y
-  rcases hf y with ⟨x, rfl⟩
-  -- compare membership in equal preimages
-  have := congrArg (fun A => x ∈ A) this
-  simpa using this
+  exact Function.Surjective.preimage_injective hf
 
 /-- If `f` is surjective, then `map f (comap f m) = m`. -/
 lemma map_comap_eq_of_surjective {α β} {f : α → β}
@@ -120,10 +114,7 @@ lemma map_comap_eq_of_surjective {α β} {f : α → β}
     rcases hS with ⟨T, hT, hpre⟩
     -- injectivity of preimage under surjectivity identifies `S = T`
     have hinj := preimage_injective_of_surjective (α := α) (β := β) hf
-    have : S = T := by
-      apply hinj
-      exact hpre.symm
-    simpa [this]
+    lia
   · -- unit inequality `m ≤ map f (comap f m)`
     intro hS
     change MeasurableSet[MeasurableSpace.comap f m] (f ⁻¹' S)
diff --git a/Exchangeability/Util/ProductBounds.lean b/Exchangeability/Util/ProductBounds.lean
index 8e2418ef..4fabf5d5 100644
--- a/Exchangeability/Util/ProductBounds.lean
+++ b/Exchangeability/Util/ProductBounds.lean
@@ -63,9 +63,7 @@ lemma abs_prod_sub_prod_le {m : ℕ} (f g : Fin m → ℝ)
       _ = |f 0 - g 0| + ∑ i : Fin n, |f i.succ - g i.succ| := by ring
 
 /-- Helper: |a - b| ≤ |a| + |b|. -/
-lemma abs_sub_le_abs_add (a b : ℝ) : |a - b| ≤ |a| + |b| := by
-  calc |a - b| = |a + (-b)| := by ring_nf
-    _ ≤ |a| + |-b| := abs_add_le a (-b)
-    _ = |a| + |b| := by rw [abs_neg]
+lemma abs_sub_le_abs_add (a b : ℝ) : |a - b| ≤ |a| + |b| :=
+  abs_sub a b
 
 end Exchangeability.Util
diff --git a/Exchangeability/Util/StrictMono.lean b/Exchangeability/Util/StrictMono.lean
index cd239634..1f8520f6 100644
--- a/Exchangeability/Util/StrictMono.lean
+++ b/Exchangeability/Util/StrictMono.lean
@@ -169,9 +169,6 @@ lemma injective_implies_strictMono_perm
     exact Subtype.ext_iff.mp h3.symm
   -- Goal: (fun i => k (σ.symm i)) i < (fun i => k (σ.symm i)) j
   -- This simplifies to: k (σ.symm i) < k (σ.symm j)
-  simp only
-  rw [h_eq_i, h_eq_j]
-  -- sorted is an OrderIso, so it's strictly monotone
-  exact sorted.strictMono hij
+  simp_all
 
 end Exchangeability.Util.StrictMono