From 91f564343244bf6c57dfdad8203d457e10c43178 Mon Sep 17 00:00:00 2001
From: Johan Commelin <johan@commelin.net>
Date: Mon, 3 Feb 2025 15:58:19 +0100
Subject: [PATCH 1/3] chore: bump toolchain to v4.16.0

---
 lean-toolchain | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lean-toolchain b/lean-toolchain
index a3edb8f..2586f88 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.16.0-rc2
+leanprover/lean4:v4.16.0

From c2681ef5d34aad291908c6dc5d66c5173e000c91 Mon Sep 17 00:00:00 2001
From: Johan Commelin <johan@commelin.net>
Date: Tue, 4 Feb 2025 05:52:03 +0100
Subject: [PATCH 2/3] wip

---
 test/Mathlib/lake-manifest.json | 8 ++++----
 test/Mathlib/lakefile.toml      | 2 +-
 test/Mathlib/lean-toolchain     | 2 +-
 3 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/test/Mathlib/lake-manifest.json b/test/Mathlib/lake-manifest.json
index 14f86bc..317a4cf 100644
--- a/test/Mathlib/lake-manifest.json
+++ b/test/Mathlib/lake-manifest.json
@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "15f16b1ec50f425147926be1aede7b4baa725380",
+   "rev": "a6276f4c6097675b1cf5ebd49b1146b735f38c02",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.16.0-rc2",
+   "inputRev": "v4.16.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f72319c9686788305a8ab059f3c4d8c724785c83",
+   "rev": "1a6613663c3eb08c401ce0fd1a408412f2c2321e",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c104265c34eb8181af14e8dbc14c2f034292cb02",
+   "rev": "01006c9e86bf9e397c026fef4190478dd1fd897e",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/test/Mathlib/lakefile.toml b/test/Mathlib/lakefile.toml
index d103c76..6e993ae 100644
--- a/test/Mathlib/lakefile.toml
+++ b/test/Mathlib/lakefile.toml
@@ -4,7 +4,7 @@ defaultTargets = ["ReplMathlibTests"]
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4"
-rev = "v4.16.0-rc2"
+rev = "v4.16.0"
 
 [[lean_lib]]
 name = "ReplMathlibTests"
diff --git a/test/Mathlib/lean-toolchain b/test/Mathlib/lean-toolchain
index 2ffc30c..8b4f470 100644
--- a/test/Mathlib/lean-toolchain
+++ b/test/Mathlib/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.16.0-rc2
\ No newline at end of file
+leanprover/lean4:v4.16.0
\ No newline at end of file

From 51879e15266ba5cc3cf9c8835d377d6ac39305ca Mon Sep 17 00:00:00 2001
From: Johan Commelin <johan@commelin.net>
Date: Tue, 4 Feb 2025 06:05:22 +0100
Subject: [PATCH 3/3] fix test

---
 test/Mathlib/test/H20231020.in   | 4 ++--
 test/Mathlib/test/H20231020.lean | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/test/Mathlib/test/H20231020.in b/test/Mathlib/test/H20231020.in
index f508554..15d58d5 100644
--- a/test/Mathlib/test/H20231020.in
+++ b/test/Mathlib/test/H20231020.in
@@ -2,7 +2,7 @@
 
 {"cmd": "theorem mathd_numbertheory_188 : Nat.gcd 180 168 = 12 := by norm_num", "env": 0}
 
-{"cmd": "theorem mathd_numbertheory_403 : ∑ k in (Nat.properDivisors 198), k = 270 := by simp (config := {decide := true})", "env": 0}
+{"cmd": "theorem mathd_numbertheory_403 : ∑ k ∈ (Nat.properDivisors 198), k = 270 := by simp (config := {decide := true})", "env": 0}
 
-{"cmd": "theorem mathd_numbertheory_109 (v : ℕ → ℕ) (h₀ : ∀ n, v n = 2 * n - 1) : (∑ k in Finset.Icc 1 100, v k) % 7 = 4 := by simp_rw (config := {decide := true}) [h₀]", "env": 0}
+{"cmd": "theorem mathd_numbertheory_109 (v : ℕ → ℕ) (h₀ : ∀ n, v n = 2 * n - 1) : (∑ k ∈ Finset.Icc 1 100, v k) % 7 = 4 := by simp_rw (config := {decide := true}) [h₀]", "env": 0}
 
diff --git a/test/Mathlib/test/H20231020.lean b/test/Mathlib/test/H20231020.lean
index f23a305..93ae613 100644
--- a/test/Mathlib/test/H20231020.lean
+++ b/test/Mathlib/test/H20231020.lean
@@ -17,6 +17,6 @@ open Topology
 
 theorem mathd_numbertheory_188 : Nat.gcd 180 168 = 12 := by norm_num
 
-theorem mathd_numbertheory_403 : ∑ k in (Nat.properDivisors 198), k = 270 := by simp (config := {decide := true})
+theorem mathd_numbertheory_403 : ∑ k ∈ (Nat.properDivisors 198), k = 270 := by simp (config := {decide := true})
 
-theorem mathd_numbertheory_109 (v : ℕ → ℕ) (h₀ : ∀ n, v n = 2 * n - 1) : (∑ k in Finset.Icc 1 100, v k) % 7 = 4 := by simp_rw (config := {decide := true}) [h₀]
+theorem mathd_numbertheory_109 (v : ℕ → ℕ) (h₀ : ∀ n, v n = 2 * n - 1) : (∑ k ∈ Finset.Icc 1 100, v k) % 7 = 4 := by simp_rw (config := {decide := true}) [h₀]