Bump mathlib to v4.28.0

PFR/MoreRuzsaDist.lean

@@ -893,8 +893,7 @@ variable {G : Type uG} [hG : MeasurableSpace G] [AddCommGroup G]
 /-- Let `X_[m] = (X₁, ..., Xₘ)` be a non-empty finite tuple of `G`-valued random variables `X_i`.
 Then we define `D[X_[m]] = H[∑ i, X_i'] - 1/m*∑ i, H[X_i']`, where the `X_i'` are independent copies
 of the `X_i`. -/
-noncomputable
-def multiDist {m : ℕ} {Ω : Fin m → Type*} (hΩ : ∀ i, MeasureSpace (Ω i))
+@[expose] noncomputable def multiDist {m : ℕ} {Ω : Fin m → Type*} (hΩ : ∀ i, MeasureSpace (Ω i))
     (X : ∀ i, Ω i → G) : ℝ :=
   H[fun x ↦ ∑ i, x i; .pi (fun i ↦ (hΩ i).volume.map (X i))] - (m:ℝ)⁻¹ * ∑ i, H[X i]
 
@@ -2104,7 +2103,9 @@ lemma iter_multiDist_chainRule' {m : ℕ} (hm : m > 0)
         I[∑ i : Fin m, X i : fun ω i ↦ π d.succ (X i ω)|
           ⟨π d.succ ∘ ∑ i : Fin m, X i, fun ω i ↦ π d.castSucc (X i ω)⟩]) := by
       rw [← Fin.sum_univ_castSucc']
-      congr! <;> rw [Fin.coeSucc_eq_succ]
+      congr!
+      any_goals rw [Fin.coeSucc_eq_succ]
+      simp_all
   _ ≥ _ := by
       rw [Finset.sum_add_distrib]
       gcongr

PFR/MultiTauFunctional.lean

@@ -279,10 +279,7 @@ lemma sub_condMultiDistance_le {G Ω₀ : Type u} [MeasurableFinGroup G] [Measur
     _ = ∏ i, ∑ ωi, Measure.real ℙ (Y i ⁻¹' {ωi}) := by
       convert Finset.sum_prod_piFinset Finset.univ _ with ω _ i _
       rfl
-    _ = ∏ i, 1 := by
-      apply Finset.prod_congr rfl
-      intro i _
-      exact probmes i
+    _ = ∏ i, 1 := by congr with i; exact probmes i
     _ = 1 := by
       simp only [Finset.prod_const_one]
   calc
@@ -310,11 +307,9 @@ lemma sub_condMultiDistance_le {G Ω₀ : Type u} [MeasurableFinGroup G] [Measur
       exact sub_multiDistance_le hΩprob hmeasX h_min hΩ'prob_cond hmeasX'
     _ = p.η * ∑ i, ∑ ω, μ ω * d[X i ; (hΩ i).volume # X' i; ℙ[|Y i ⁻¹' {ω i}] ] := by
       rw [Finset.sum_comm, Finset.mul_sum]
-      apply Finset.sum_congr rfl
-      intro ω _
+      congr with ω
       rw [Finset.mul_sum, Finset.mul_sum, Finset.mul_sum]
-      apply Finset.sum_congr rfl
-      intro i _
+      congr with i
       ring
     _ = _ := by
       congr with i

lake-manifest.json

@@ -15,27 +15,27 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "13fd6dd3a47445b6dd10826f0ffc1116f4e13144",
+   "rev": "eba2c2b0e8309e19de76037c188dc14899729bce",
    "name": "APAP",
    "manifestFile": "lake-manifest.json",
-   "inputRev": null,
+   "inputRev": "v4.28.0",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "507f18fc9044549fc730d8d0270521e3b090360a",
+   "rev": "8f9d9cff6bd728b17a24e163c9402775d9e6a365",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": null,
+   "inputRev": "v4.28.0",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7311586e1a56af887b1081d05e80c11b6c41d212",
+   "rev": "55c8532eb21ec9f6d565d51d96b8ca50bd1fbef3",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28",
+   "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b5908dbac486279f1133cb937648c63c30b455af",
+   "rev": "85b59af46828c029a9168f2f9c35119bd0721e6e",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,17 +65,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6d65c6e0a25b8a52c13c3adeb63ecde3bfbb6294",
+   "rev": "be3b2e63b1bbf496c478cef98b86972a37c1417d",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.86",
+   "inputRev": "v0.0.87",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f08e838d4f9aea519f3cde06260cfb686fd4bab0",
+   "rev": "f642a64c76df8ba9cb53dba3b919425a0c2aeaf1",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "23324752757bf28124a518ec284044c8db79fee5",
+   "rev": "b8f98e9087e02c8553945a2c5abf07cec8e798c3",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -95,7 +95,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "0100f1a3222df01286db33fcb6a1f98564f5439d",
+   "rev": "495c008c3e3f4fb4256ff5582ddb3abf3198026f",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -105,10 +105,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "28e0856d4424863a85b18f38868c5420c55f9bae",
+   "rev": "4f10f47646cb7d5748d6f423f4a07f98f7bbcc9e",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.28.0-rc1",
+   "inputRev": "v4.28.0",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "PFR",

lakefile.toml

@@ -16,6 +16,7 @@ warn.sorry = false
 [[require]]
 name = "APAP"
 git = "https://github.com/YaelDillies/apap.git"
+rev = "v4.28.0"
 
 [[require]]
 name = "checkdecls"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.28.0-rc1
+leanprover/lean4:v4.28.0