diff --git a/lake-manifest.json b/lake-manifest.json
index 521790b8a1..cf209067e3 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,15 +4,15 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "f8f5030037dcb6ca50023dea02a2bb85542dbdff",
+    "rev": "c25957b989829678283578280ae1d8ae2de185d3",
     "name": "lean3port",
-    "inputRev?": "f8f5030037dcb6ca50023dea02a2bb85542dbdff"}},
+    "inputRev?": "c25957b989829678283578280ae1d8ae2de185d3"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "ff33484322fbce1ead24eb4ca948306955c68664",
+    "rev": "816a4c0cf4fdf4cf5dbcff9d21a413ddcfaf117a",
     "name": "mathlib",
-    "inputRev?": "ff33484322fbce1ead24eb4ca948306955c68664"}},
+    "inputRev?": "816a4c0cf4fdf4cf5dbcff9d21a413ddcfaf117a"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,
diff --git a/lakefile.lean b/lakefile.lean
index 48a0b415e9..c345cfc4bf 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -4,7 +4,7 @@ open Lake DSL System
 -- Usually the `tag` will be of the form `nightly-2021-11-22`.
 -- If you would like to use an artifact from a PR build,
 -- it will be of the form `pr-branchname-sha`.
-def tag : String := "nightly-2023-05-03-22"
+def tag : String := "nightly-2023-05-04-01"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg : Package) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"f8f5030037dcb6ca50023dea02a2bb85542dbdff"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"c25957b989829678283578280ae1d8ae2de185d3"
 
 @[default_target]
 lean_lib Mathbin where