diff --git a/lake-manifest.json b/lake-manifest.json
index 195d8b30..82a8f2d2 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e9c65db4823976353cd0bb03199a172719efbeb7",
+   "rev": "57286efe32042270335d2235798f85deab54d22d",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "stable",
diff --git a/lean-toolchain b/lean-toolchain
index b9f9eea1..14a44240 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.21.0
\ No newline at end of file
+leanprover/lean4:v4.23.0
\ No newline at end of file
diff --git a/src/Iris/ProofMode/Tactics/Assumption.lean b/src/Iris/ProofMode/Tactics/Assumption.lean
index fcb017e5..6a1cbdf3 100644
--- a/src/Iris/ProofMode/Tactics/Assumption.lean
+++ b/src/Iris/ProofMode/Tactics/Assumption.lean
@@ -53,7 +53,7 @@ def assumptionFast {e} (hyps : Hyps bi e) : MetaM Q($e ⊢ $Q) := do
     hyps.removeG true fun _ _ b ty => try? do
       synthInstance q(FromAssumption $b $ty $Q)
     | failure
-  let (_ : Q(FromAssumption $b $ty $Q)) := inst
+  let _ : Q(FromAssumption $b $ty $Q) := inst
   have : $out =Q iprop(□?$b $ty) := ⟨⟩
   match fastPath with
   | .absorbing _ => return q(assumption (Q := $Q) $pf)
diff --git a/src/Iris/Std/DelabRule.lean b/src/Iris/Std/DelabRule.lean
index f677b798..aef1a205 100644
--- a/src/Iris/Std/DelabRule.lean
+++ b/src/Iris/Std/DelabRule.lean
@@ -22,8 +22,7 @@ macro_rules
       | [(name, [])] => pure name
       | _           => throwUnsupported
 
-    let (p : TSyntaxArray `term) := p
-    if p.any (· matches `(`($$_))) then
+    if p.any fun t : TSyntax _ ↦ t matches `(`($$_)) then
       `(@[app_unexpander $(mkIdent f)]
         def unexpand : Lean.PrettyPrinter.Unexpander
           $[| $p => $s]*)
diff --git a/src/Iris/Tests/Notation.lean b/src/Iris/Tests/Notation.lean
index d4239fd1..a6046719 100644
--- a/src/Iris/Tests/Notation.lean
+++ b/src/Iris/Tests/Notation.lean
@@ -18,10 +18,10 @@ variable [BIBase PROP] (P Q R : PROP) (Ψ : Nat → PROP) (Φ : Nat → Nat →
 /-- info: P ⊢ Q : Prop -/
 #guard_msgs in #check P ⊢ Q
 
-/-- info: iprop(emp) : ?m.103 -/
+/-- info: iprop(emp) : ?m.2 -/
 #guard_msgs in #check iprop(emp)
 
-/-- info: iprop(⌜φ⌝) : ?m.144 -/
+/-- info: iprop(⌜φ⌝) : ?m.2 -/
 #guard_msgs in #check iprop(⌜φ⌝)
 
 /-- info: iprop(P ∧ Q) : PROP -/
@@ -86,9 +86,9 @@ variable [BIBase PROP] (P Q R : PROP) (Ψ : Nat → PROP) (Φ : Nat → Nat →
 /-- info: iprop(P ∗ <pers> Q) : PROP -/
 #guard_msgs in #check iprop(P ∗ (<pers> Q))
 
-/-- info: iprop(True) : ?m.1425 -/
+/-- info: iprop(True) : ?m.2 -/
 #guard_msgs in #check iprop(True)
-/-- info: iprop(False) : ?m.1466 -/
+/-- info: iprop(False) : ?m.2 -/
 #guard_msgs in #check iprop(False)
 
 /-- info: iprop(¬P) : PROP -/