diff --git a/Mathport/Syntax/Translate/Tactic/Mathlib/Padics.lean b/Mathport/Syntax/Translate/Tactic/Mathlib/Padics.lean
index 77314b88a..4fd3fb396 100644
--- a/Mathport/Syntax/Translate/Tactic/Mathlib/Padics.lean
+++ b/Mathport/Syntax/Translate/Tactic/Mathlib/Padics.lean
@@ -29,7 +29,8 @@ open Parser
   `(tactic| init_ring $[using $(← liftM $ (← parse (tk "using" *> pExpr)?).mapM trExpr)]?)
 
 @[tr_tactic ghost_simp] def trGhostSimp : TacM Syntax.Tactic := do
-  `(tactic| ghost_simp $[[$((← trSimpArgs (← parse simpArgList)).asNonempty),*]]?)
+  let args := (← trSimpArgs (← parse simpArgList)).asNonempty
+  `(tactic| ghost_simp $[[$args,*]]?)
 
 @[tr_tactic witt_truncate_fun_tac] def trWittTruncateFunTac : TacM Syntax.Tactic :=
   `(tactic| witt_truncate_fun_tac)
diff --git a/lake-manifest.json b/lake-manifest.json
index d982d6bb5..65b207911 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -16,7 +16,7 @@
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4",
     "subDir?": null,
-    "rev": "f39466cb99f0b941b72e1d918d139ef25a419023",
+    "rev": "dc89373908a65cd4807c248c566cbb75c18328f9",
     "name": "mathlib",
     "inputRev?": "master"}},
   {"git":
diff --git a/lean-toolchain b/lean-toolchain
index 4a54a0e55..e183d2cbe 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2023-07-24
+leanprover/lean4:nightly-2023-07-30