fix(lint-style): filter out duplicate Init from Mathlib.lean imports

`Lean.parseImports'` now emits `Init` more than once for module-system
files such as `Mathlib.lean`, but `findImportsFromSource` (in importGraph)
only `.erase`s the first occurrence. The remaining `Init` was treated as a
module to lint, producing `uncaught exception: no such file or directory ...
file: Init.lean` and breaking the `lint-style` CI job on `nightly-testing`.

Defensively filter out any remaining `Init` after `findImportsFromSource`.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: kim-em

scripts/lint-style.lean

@@ -105,7 +105,11 @@ def missingInitImports (opts : LinterOptions) : IO Nat := do
 
   -- Find any file in the Mathlib directory which does not contain any Mathlib import.
   -- We simply parse `Mathlib.lean`, as CI ensures this file is up to date.
-  let allModuleNames := eraseExplicitImports (← findImportsFromSource "Mathlib.lean")
+  -- Note: `findImportsFromSource` only erases the *first* occurrence of `Init`.
+  -- On module-system files (such as `Mathlib.lean`), `Lean.parseImports'` may emit
+  -- `Init` multiple times, so we filter out any remaining occurrences here.
+  let allModuleNames := (eraseExplicitImports (← findImportsFromSource "Mathlib.lean")).filter
+    (· != `Init)
   let mut modulesWithoutMathlibImports := #[]
   let mut importsHeaderLinter := #[]
   for module in allModuleNames do