From 9080df3110bd680956237c82dbbe96e1c818992f Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Sat, 4 Jan 2025 15:13:13 +1100
Subject: [PATCH] chore: import cleanup in Init (#6522)

This PR avoids unnecessarily importing "kitchen sink" files.
---
 src/Lean/Data/Lsp/Utf16.lean                                  | 1 -
 src/Lean/Linter/MissingDocs.lean                              | 1 +
 src/Lean/PrettyPrinter/Delaborator/Builtins.lean              | 1 -
 src/Lean/Server/Completion.lean                               | 1 +
 src/Lean/Util/ShareCommon.lean                                | 4 ++--
 src/Std/Sat/AIG/Basic.lean                                    | 1 -
 .../Tactic/BVDecide/LRAT/Internal/Formula/Implementation.lean | 1 -
 src/Std/Time/DateTime/Timestamp.lean                          | 1 -
 src/Std/Time/Internal/Bounded.lean                            | 2 +-
 9 files changed, 5 insertions(+), 8 deletions(-)

diff --git a/src/Lean/Data/Lsp/Utf16.lean b/src/Lean/Data/Lsp/Utf16.lean
index b9d5bea8ba80..30d36e8a478a 100644
--- a/src/Lean/Data/Lsp/Utf16.lean
+++ b/src/Lean/Data/Lsp/Utf16.lean
@@ -6,7 +6,6 @@ Authors: Marc Huisinga, Wojciech Nawrocki
 -/
 prelude
 import Init.Data.String
-import Init.Data.Array
 import Lean.Data.Lsp.Basic
 import Lean.Data.Position
 import Lean.DeclarationRange
diff --git a/src/Lean/Linter/MissingDocs.lean b/src/Lean/Linter/MissingDocs.lean
index 6df6d7473f90..742ad05f8b96 100644
--- a/src/Lean/Linter/MissingDocs.lean
+++ b/src/Lean/Linter/MissingDocs.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 prelude
+import Lean.Parser.Syntax
 import Lean.Meta.Tactic.Simp.RegisterCommand
 import Lean.Elab.Command
 import Lean.Elab.SetOption
diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index 5dc3aa3ee97f..61d9e209f42e 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Ullrich, Leonardo de Moura, Gabriel Ebner, Mario Carneiro
 -/
 prelude
-import Lean.Parser
 import Lean.PrettyPrinter.Delaborator.Attributes
 import Lean.PrettyPrinter.Delaborator.Basic
 import Lean.PrettyPrinter.Delaborator.SubExpr
diff --git a/src/Lean/Server/Completion.lean b/src/Lean/Server/Completion.lean
index aec3001948f7..9ffb290958a4 100644
--- a/src/Lean/Server/Completion.lean
+++ b/src/Lean/Server/Completion.lean
@@ -5,6 +5,7 @@ Authors: Leonardo de Moura, Marc Huisinga
 -/
 prelude
 import Lean.Server.Completion.CompletionCollectors
+import Std.Data.HashMap
 
 namespace Lean.Server.Completion
 open Lsp
diff --git a/src/Lean/Util/ShareCommon.lean b/src/Lean/Util/ShareCommon.lean
index 4bc3bc7b694d..3a508533fd5b 100644
--- a/src/Lean/Util/ShareCommon.lean
+++ b/src/Lean/Util/ShareCommon.lean
@@ -5,8 +5,8 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.ShareCommon
-import Std.Data.HashSet
-import Std.Data.HashMap
+import Std.Data.HashSet.Basic
+import Std.Data.HashMap.Basic
 import Lean.Data.PersistentHashMap
 import Lean.Data.PersistentHashSet
 
diff --git a/src/Std/Sat/AIG/Basic.lean b/src/Std/Sat/AIG/Basic.lean
index 4a12ef54dce9..f68ce1a3c9e4 100644
--- a/src/Std/Sat/AIG/Basic.lean
+++ b/src/Std/Sat/AIG/Basic.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
 prelude
-import Std.Data.HashMap
 import Std.Data.HashSet
 
 namespace Std
diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Implementation.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Implementation.lean
index 7027a2c52b06..108fc7114ed0 100644
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Implementation.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Implementation.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Josh Clune
 -/
 prelude
-import Init.Data.Array
 import Std.Tactic.BVDecide.LRAT.Internal.Formula.Class
 import Std.Tactic.BVDecide.LRAT.Internal.Assignment
 import Std.Sat.CNF.Basic
diff --git a/src/Std/Time/DateTime/Timestamp.lean b/src/Std/Time/DateTime/Timestamp.lean
index 8ba43cc11892..3d4527a00a4f 100644
--- a/src/Std/Time/DateTime/Timestamp.lean
+++ b/src/Std/Time/DateTime/Timestamp.lean
@@ -5,7 +5,6 @@ Authors: Sofia Rodrigues
 -/
 prelude
 import Std.Time.Internal
-import Init.Data.Int
 import Init.System.IO
 import Std.Time.Time
 import Std.Time.Date
diff --git a/src/Std/Time/Internal/Bounded.lean b/src/Std/Time/Internal/Bounded.lean
index 897636c9a077..951dc73b43ce 100644
--- a/src/Std/Time/Internal/Bounded.lean
+++ b/src/Std/Time/Internal/Bounded.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sofia Rodrigues
 -/
 prelude
-import Init.Data.Int
+import Init.Omega
 
 namespace Std
 namespace Time