From e46bf0db638788090d7470646d2af29e788a6350 Mon Sep 17 00:00:00 2001 From: "mathlib-nightly-testing[bot]" Date: Fri, 15 May 2026 20:33:35 +0000 Subject: [PATCH] chore: bump mathlib to 54f98fd: doc(Data/NNReal): document the defeq footgun (#39409) (2026-05-15) --- lake-manifest.json | 10 +++++----- lakefile.toml | 2 +- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index ca8591cf3..cf0696cf9 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "6cf3ab1c11e19e328c2e535bdd32d66dc7842fb5", + "rev": "54f98fd67e63d316ddc3452ae31e18b2283be6e1", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "6cf3ab1c11e19e328c2e535bdd32d66dc7842fb5", + "inputRev": "54f98fd67e63d316ddc3452ae31e18b2283be6e1", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "cdab3938ccabbdb044be6896e251b5814bec932e", + "rev": "fd70b40073aeca8fa60fe0fb492f189d3b12c0ef", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -75,10 +75,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "5c57f3857ba81924a88b2cdf4f062e34ec04ff11", + "rev": "48ff08a0e30a15078186548f11981d8988dee0c5", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0-rc2", + "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", diff --git a/lakefile.toml b/lakefile.toml index 4169d4b8e..26b1e6daf 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -18,7 +18,7 @@ weak.linter.unicodeLinter = false [[require]] name = "mathlib" scope = "leanprover-community" -rev = "6cf3ab1c11e19e328c2e535bdd32d66dc7842fb5" +rev = "54f98fd67e63d316ddc3452ae31e18b2283be6e1" [[lean_lib]] name = "Cslib"