chore: autoGolf proof bodies across 61 files (−841 lines)

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.

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 : ℕ → Ω → α}

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]

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 μ]

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

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]

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
 

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