From 3b0107068fb7d8276b6ab6c44e2f19137e2c9061 Mon Sep 17 00:00:00 2001
From: "github-actions[bot]"
 <41898282+github-actions[bot]@users.noreply.github.com>
Date: Mon, 13 Jul 2026 19:28:30 +0000
Subject: [PATCH] chore: bump mathlib to 4a7edd3: chore: update Mathlib
 dependencies 2026-07-13 (#41687) (2026-07-13)

---
 lake-manifest.json | 14 +++++++-------
 lakefile.toml      |  2 +-
 2 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/lake-manifest.json b/lake-manifest.json
index ec7d8b8..6091b1e 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "3ee3f85eb48438ad4f8ce98b79a198f6573d5f70",
+   "rev": "4a7edd35ec64de7117995da659e9d4d80e6cca19",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master-2026-06-22",
+   "inputRev": "4a7edd35ec64de7117995da659e9d4d80e6cca19",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/verso",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f3f26cc72646205ca167117487c008ee1dafe816",
+   "rev": "e12c1910fe855cbfc38803cd4e55543906d5fa62",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e6518a674e62de322b8f79eebeda7bcae2a36bc3",
+   "rev": "6e311e2a844da9b2cc3971187df2fe0066947b93",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b5b9e2bb45ce91e4bc44eaa738c3a8910404ab82",
+   "rev": "24fa6b3599743c23e6debd53d5fd09ebfa587d29",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7a62bd13860cd39ac98da16ffc8c24d601353f69",
+   "rev": "38d591e778f100aec9762bb582f9c7f55f50e9dc",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7d1b02eb63b526dff04cb990cf05b06b38ccbd3f",
+   "rev": "dfb6d7e9949d1bb0706f651e330176bc66fc6f3d",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/lakefile.toml b/lakefile.toml
index 27b8003..1cb587b 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -19,7 +19,7 @@ rev = "v4.32.0-rc1"
 [[require]]
 name = "mathlib"
 scope = "leanprover-community"
-rev = "master-2026-06-22"
+rev = "4a7edd35ec64de7117995da659e9d4d80e6cca19"
 
 [[lean_lib]]
 name = "DynamicalSystems"