Import autocompletion sometimes forgets about some files

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

In certain cases, import autocompletion fails to find some imports that is has found immediately before.

Steps to Reproduce

https://github.com/user-attachments/assets/36cd4fdd-93d0-439f-9392-b1ef3d597bc3

1. In an empty Lean file, type import Std.Iter and notice that the autocompletion suggests Std.Data.Iterators as desired
2. Using autocomplete or otherwise, complete the import to import Std.Data.Iterators.
3. Now press backspace enough times so that only import Std. remains
4. Now, without pressing Ctrl+Space, type Iter again and notice that Std.Data.Iterators is now missing from the results.

If Step 4 is modified to press Ctrl+Space instead, then Std.Data.Iterators is found.

Expected behavior: Std.Data.Iterators should be found when autocompleting import Std.Iter.

Actual behavior: Sometimes it is missing.

Versions

This is reproducible both on 4.21.0-rc3 and nightly-2025-06-11.

**Operating system**: Linux (release: 6.14.9-300.fc42.x86_64)
**CPU architecture**: x64
**CPU model**: 16 x AMD Ryzen 9 PRO 7940HS w/ Radeon 780M Graphics
**Available RAM**: 65.97 GB

**VS Code version**: Reasonably up-to-date (version: 1.100.3)
**Lean 4 extension version**: 0.0.208
**Curl installed**: true
**Git installed**: true
**Elan**: Reasonably up-to-date (version: 4.1.2)
**Lean**: Reasonably up-to-date (version: 4.21.0-rc3)
**Project**: Valid Lean project (path: /home/markus/code/human-eval-lean)
**Active Lean version**: leanprover/lean4:v4.21.0-rc3 (set by `file:///home/markus/code/human-eval-lean/lean-toolchain`)

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Reproduce the issue using the numbered steps in an empty Lean file, comparing completion after typing import Std.Iter with the behavior after deleting back to import Std.. Start by tracing the import-completion path involved in that interaction. Done means Std.Data.Iterators is consistently suggested without requiring Ctrl+Space.