diff --git a/lake-manifest.json b/lake-manifest.json index 7b29f88..8dcdfd1 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,10 +15,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "1f414401f69059aa7eead47b53ee40bd38455eeb", + "rev": "051bc081081f2bb77b81d47ee69146c4cef28bbe", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "1f414401f69059aa7eead47b53ee40bd38455eeb", + "inputRev": "051bc081081f2bb77b81d47ee69146c4cef28bbe", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", diff --git a/lakefile.toml b/lakefile.toml index 4e9caaf..b8562dc 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -13,7 +13,7 @@ weak.linter.mathlibStandardSet = true [[require]] name = "mathlib" git = "https://github.com/leanprover-community/mathlib4" -rev = "1f414401f69059aa7eead47b53ee40bd38455eeb" +rev = "051bc081081f2bb77b81d47ee69146c4cef28bbe" [[require]] name = "subverso"