diff --git a/src/Lean/Server/AsyncList.lean b/src/Lean/Server/AsyncList.lean
index 3fade41b13..bdb4f7de7d 100644
--- a/src/Lean/Server/AsyncList.lean
+++ b/src/Lean/Server/AsyncList.lean
@@ -78,7 +78,7 @@ partial def getFinishedPrefix : AsyncList ε α → BaseIO (List α × Option ε
   | nil => pure ⟨[], none, true⟩
   | delayed tl => do
     if ← tl.hasFinished then
-      match tl.get with
+      match ← tl.wait with
       | Except.ok tl => tl.getFinishedPrefix
       | Except.error e => pure ⟨[], some e, true⟩
     else pure ⟨[], none, false⟩
@@ -102,14 +102,18 @@ where
       return ⟨hd :: tl, e?, isComplete⟩
     | nil => return ⟨[], none, true⟩
     | delayed tl =>
-      let tl : ServerTask (Except ε (AsyncList ε α)) := tl
-      let tl := tl.mapCheap .inr
-      let cancelTks := cancelTks.map (·.mapCheap .inl)
-      let r ← ServerTask.waitAny (tl :: cancelTks ++ [timeoutTask])
-      match r with
-      | .inl _ => return ⟨[], none, false⟩ -- Timeout or cancellation - stop waiting
-      | .inr (.ok tl) => go timeoutTask tl
-      | .inr (.error e) => return ⟨[], some e, true⟩
+      if ← tl.hasFinished then
+        match ← tl.wait with
+        | .ok tl => go timeoutTask tl
+        | .error e => return ⟨[], some e, true⟩
+      else
+        let tl := tl.mapCheap .inr
+        let cancelTks := cancelTks.map (·.mapCheap .inl)
+        let r ← ServerTask.waitAny (tl :: cancelTks ++ [timeoutTask])
+        match r with
+        | .inl _ => return ⟨[], none, false⟩ -- Timeout or cancellation - stop waiting
+        | .inr (.ok tl) => go timeoutTask tl
+        | .inr (.error e) => return ⟨[], some e, true⟩
 
 partial def getFinishedPrefixWithConsistentLatency (xs : AsyncList ε α) (latencyMs : UInt32)
     (cancelTks : List (ServerTask Unit) := []) : BaseIO (List α × Option ε × Bool) := do
diff --git a/src/Lean/Server/ServerTask.lean b/src/Lean/Server/ServerTask.lean
index 11c5f1538f..d755c14b39 100644
--- a/src/Lean/Server/ServerTask.lean
+++ b/src/Lean/Server/ServerTask.lean
@@ -54,6 +54,8 @@ def pure (x : α) : ServerTask α := Task.pure x
 
 def get (t : ServerTask α) : α := t.task.get
 
+def wait (t : ServerTask α) : BaseIO α := IO.wait t.task
+
 def mapCheap (f : α → β) (t : ServerTask α) : ServerTask β :=
   t.task.map f (sync := true)