From 03139ed81d1c514f2a411b14a6f7cb41700065c6 Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Mon, 31 Jul 2023 10:00:49 +0200
Subject: [PATCH] chore: update lean

---
 Mathport/Syntax/Translate/Tactic/Mathlib/Padics.lean | 3 ++-
 lake-manifest.json                                   | 2 +-
 lean-toolchain                                       | 2 +-
 3 files changed, 4 insertions(+), 3 deletions(-)

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