From 7b244eafac9dd0d47735d0a9a3a906bfb4910246 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Mon, 12 Aug 2024 12:35:52 +1000
Subject: [PATCH] chore: shake Batteries (#903)

---
 Batteries/CodeAction/Attr.lean            | 2 +-
 Batteries/CodeAction/Deprecated.lean      | 1 -
 Batteries/Data/ByteArray.lean             | 1 -
 Batteries/Data/HashMap/Lemmas.lean        | 1 -
 Batteries/Data/HashMap/WF.lean            | 3 ++-
 Batteries/Data/List/Pairwise.lean         | 1 -
 Batteries/Data/Rat/Basic.lean             | 1 -
 Batteries/Data/String/Lemmas.lean         | 1 -
 Batteries/Data/UnionFind/Basic.lean       | 2 +-
 Batteries/Lean/Meta/AssertHypotheses.lean | 2 +-
 Batteries/Lean/Meta/Basic.lean            | 4 +---
 Batteries/Lean/Meta/Clear.lean            | 1 +
 Batteries/Lean/Meta/Inaccessible.lean     | 2 +-
 Batteries/Lean/Position.lean              | 1 -
 Batteries/Lean/System/IO.lean             | 1 -
 Batteries/Logic.lean                      | 2 --
 Batteries/StdDeprecations.lean            | 8 ++++----
 Batteries/Tactic/Case.lean                | 2 +-
 Batteries/Tactic/Classical.lean           | 2 +-
 Batteries/Tactic/Init.lean                | 6 ++----
 Batteries/Tactic/NoMatch.lean             | 2 +-
 Batteries/Tactic/PrintDependents.lean     | 1 -
 Batteries/Tactic/PrintPrefix.lean         | 1 -
 Batteries/Tactic/SeqFocus.lean            | 2 +-
 Batteries/Tactic/ShowUnused.lean          | 1 -
 Batteries/Tactic/Unreachable.lean         | 2 +-
 Batteries/Util/Cache.lean                 | 2 +-
 Batteries/Util/ExtendedBinder.lean        | 2 --
 Batteries/Util/LibraryNote.lean           | 2 +-
 test/MLList.lean                          | 1 +
 30 files changed, 22 insertions(+), 38 deletions(-)

diff --git a/Batteries/CodeAction/Attr.lean b/Batteries/CodeAction/Attr.lean
index ad5e0f62d3..79802d6932 100644
--- a/Batteries/CodeAction/Attr.lean
+++ b/Batteries/CodeAction/Attr.lean
@@ -3,7 +3,7 @@ Copyright (c) 2023 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import Lean.Server.CodeActions
+import Lean.Server.CodeActions.Basic
 
 /-!
 # Initial setup for code action attributes
diff --git a/Batteries/CodeAction/Deprecated.lean b/Batteries/CodeAction/Deprecated.lean
index ec6a2f11c2..ce98bcc5c6 100644
--- a/Batteries/CodeAction/Deprecated.lean
+++ b/Batteries/CodeAction/Deprecated.lean
@@ -5,7 +5,6 @@ Authors: Mario Carneiro
 -/
 import Lean.Server.CodeActions
 import Batteries.CodeAction.Basic
-import Batteries.Lean.Position
 
 /-!
 # Code action for @[deprecated] replacements
diff --git a/Batteries/Data/ByteArray.lean b/Batteries/Data/ByteArray.lean
index f147eaf47b..585563ec5a 100644
--- a/Batteries/Data/ByteArray.lean
+++ b/Batteries/Data/ByteArray.lean
@@ -3,7 +3,6 @@ Copyright (c) 2023 François G. Dorais. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: François G. Dorais
 -/
-import Batteries.Data.Array.Lemmas
 
 namespace ByteArray
 
diff --git a/Batteries/Data/HashMap/Lemmas.lean b/Batteries/Data/HashMap/Lemmas.lean
index 290f4c0cff..79107fc0bf 100644
--- a/Batteries/Data/HashMap/Lemmas.lean
+++ b/Batteries/Data/HashMap/Lemmas.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import Batteries.Data.HashMap.Basic
-import Batteries.Data.Array.Lemmas
 
 /-!
 # Lemmas for `Batteries.HashMap`
diff --git a/Batteries/Data/HashMap/WF.lean b/Batteries/Data/HashMap/WF.lean
index e83e32e567..ae51625133 100644
--- a/Batteries/Data/HashMap/WF.lean
+++ b/Batteries/Data/HashMap/WF.lean
@@ -3,9 +3,10 @@ Copyright (c) 2022 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
+import Batteries.Tactic.SeqFocus
 import Batteries.Data.HashMap.Basic
-import Batteries.Data.Array.Lemmas
 import Batteries.Data.Nat.Lemmas
+import Batteries.Data.List.Lemmas
 
 namespace Batteries.HashMap
 namespace Imp
diff --git a/Batteries/Data/List/Pairwise.lean b/Batteries/Data/List/Pairwise.lean
index dd94875ca9..9df947bf4c 100644
--- a/Batteries/Data/List/Pairwise.lean
+++ b/Batteries/Data/List/Pairwise.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, James Gallicchio
 -/
 import Batteries.Data.List.Count
-import Batteries.Data.Fin.Lemmas
 
 /-!
 # Pairwise relations on a list
diff --git a/Batteries/Data/Rat/Basic.lean b/Batteries/Data/Rat/Basic.lean
index 600e67981f..f96651d34c 100644
--- a/Batteries/Data/Rat/Basic.lean
+++ b/Batteries/Data/Rat/Basic.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import Batteries.Data.Nat.Gcd
-import Batteries.Data.Int.DivMod
 import Batteries.Lean.Float
 
 /-! # Basics for the Rational Numbers -/
diff --git a/Batteries/Data/String/Lemmas.lean b/Batteries/Data/String/Lemmas.lean
index 9984d0fb52..df338e03ff 100644
--- a/Batteries/Data/String/Lemmas.lean
+++ b/Batteries/Data/String/Lemmas.lean
@@ -8,7 +8,6 @@ import Batteries.Data.List.Lemmas
 import Batteries.Data.String.Basic
 import Batteries.Tactic.Lint.Misc
 import Batteries.Tactic.SeqFocus
-import Batteries.Tactic.SqueezeScope
 
 namespace String
 
diff --git a/Batteries/Data/UnionFind/Basic.lean b/Batteries/Data/UnionFind/Basic.lean
index 292f4285eb..e0b4174112 100644
--- a/Batteries/Data/UnionFind/Basic.lean
+++ b/Batteries/Data/UnionFind/Basic.lean
@@ -3,8 +3,8 @@ Copyright (c) 2021 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import Batteries.Data.Array.Lemmas
 import Batteries.Tactic.Lint.Misc
+import Batteries.Tactic.SeqFocus
 
 namespace Batteries
 
diff --git a/Batteries/Lean/Meta/AssertHypotheses.lean b/Batteries/Lean/Meta/AssertHypotheses.lean
index a0905c6718..6275032063 100644
--- a/Batteries/Lean/Meta/AssertHypotheses.lean
+++ b/Batteries/Lean/Meta/AssertHypotheses.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg
 -/
 
-import Batteries.Lean.Meta.Basic
+import Lean.Meta.Tactic.Assert
 
 open Lean Lean.Meta
 
diff --git a/Batteries/Lean/Meta/Basic.lean b/Batteries/Lean/Meta/Basic.lean
index 3e72809893..d2c55af7ea 100644
--- a/Batteries/Lean/Meta/Basic.lean
+++ b/Batteries/Lean/Meta/Basic.lean
@@ -3,9 +3,7 @@ Copyright (c) 2022 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Jannis Limperg
 -/
-import Lean.Elab.Term
-import Lean.Meta.Tactic.Apply
-import Lean.Meta.Tactic.Replace
+import Lean.Meta.Tactic.Intro
 
 open Lean Lean.Meta
 
diff --git a/Batteries/Lean/Meta/Clear.lean b/Batteries/Lean/Meta/Clear.lean
index 47caaaa4d3..66f38b7798 100644
--- a/Batteries/Lean/Meta/Clear.lean
+++ b/Batteries/Lean/Meta/Clear.lean
@@ -5,6 +5,7 @@ Authors: Jannis Limperg
 -/
 
 import Batteries.Lean.Meta.Basic
+import Lean.Meta.Tactic.Clear
 
 open Lean Lean.Meta
 
diff --git a/Batteries/Lean/Meta/Inaccessible.lean b/Batteries/Lean/Meta/Inaccessible.lean
index e308364616..e63c4ec4f7 100644
--- a/Batteries/Lean/Meta/Inaccessible.lean
+++ b/Batteries/Lean/Meta/Inaccessible.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Jannis Limperg. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg
 -/
-import Lean.Meta.InferType
+import Lean.Meta.Basic
 
 open Lean Lean.Meta
 
diff --git a/Batteries/Lean/Position.lean b/Batteries/Lean/Position.lean
index f2bc155886..49fdad203e 100644
--- a/Batteries/Lean/Position.lean
+++ b/Batteries/Lean/Position.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import Lean.Syntax
-import Lean.Meta.Tactic.TryThis
 import Lean.Data.Lsp.Utf16
 
 /-- Gets the LSP range of syntax `stx`. -/
diff --git a/Batteries/Lean/System/IO.lean b/Batteries/Lean/System/IO.lean
index c4d6b6ce84..40dcda5365 100644
--- a/Batteries/Lean/System/IO.lean
+++ b/Batteries/Lean/System/IO.lean
@@ -3,7 +3,6 @@ Copyright (c) 2023 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import Batteries.Data.List.Lemmas
 
 /-!
 # Functions for manipulating a list of tasks
diff --git a/Batteries/Logic.lean b/Batteries/Logic.lean
index 5c6efe108a..03c82eb5ac 100644
--- a/Batteries/Logic.lean
+++ b/Batteries/Logic.lean
@@ -3,9 +3,7 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn, Mario Carneiro
 -/
-import Batteries.Tactic.Init
 import Batteries.Tactic.Alias
-import Batteries.Tactic.Lint.Misc
 
 instance {f : α → β} [DecidablePred p] : DecidablePred (p ∘ f) :=
   inferInstanceAs <| DecidablePred fun x => p (f x)
diff --git a/Batteries/StdDeprecations.lean b/Batteries/StdDeprecations.lean
index f82b1739a7..cb49a3bdbf 100644
--- a/Batteries/StdDeprecations.lean
+++ b/Batteries/StdDeprecations.lean
@@ -4,12 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
 import Batteries.Tactic.Alias
-import Batteries.Data.HashMap
 import Batteries.Data.DList
 import Batteries.Data.PairingHeap
-import Batteries.Data.RBMap
-import Batteries.Data.BinomialHeap
-import Batteries.Data.UnionFind
+import Batteries.Data.BinomialHeap.Basic
+import Batteries.Data.HashMap.Basic
+import Batteries.Data.RBMap.Basic
+import Batteries.Data.UnionFind.Basic
 
 /-!
 # We set up deprecations for identifiers formerly in the `Std` namespace.
diff --git a/Batteries/Tactic/Case.lean b/Batteries/Tactic/Case.lean
index 60bd585244..375d351b05 100644
--- a/Batteries/Tactic/Case.lean
+++ b/Batteries/Tactic/Case.lean
@@ -3,7 +3,7 @@ Copyright (c) 2023 Kyle Miller. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kyle Miller
 -/
-import Lean.Elab.Tactic.Conv.Pattern
+import Lean.Elab.Tactic.BuiltinTactic
 
 /-!
 # Extensions to the `case` tactic
diff --git a/Batteries/Tactic/Classical.lean b/Batteries/Tactic/Classical.lean
index 7d3e6eb3c0..a3bc78b0a4 100644
--- a/Batteries/Tactic/Classical.lean
+++ b/Batteries/Tactic/Classical.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import Lean.Elab.ElabRules
+import Lean.Elab.Tactic.Basic
 
 /-! # `classical` tactic -/
 
diff --git a/Batteries/Tactic/Init.lean b/Batteries/Tactic/Init.lean
index fed3c1ad99..db7894f633 100644
--- a/Batteries/Tactic/Init.lean
+++ b/Batteries/Tactic/Init.lean
@@ -3,16 +3,14 @@ Copyright (c) 2021 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import Batteries.Lean.Meta.Basic
-import Lean.Elab.Command
-import Lean.Elab.Tactic.BuiltinTactic
+import Lean.Elab.Tactic.ElabTerm
 
 /-!
 # Simple tactics that are used throughout Batteries.
 -/
 
 namespace Batteries.Tactic
-open Lean Parser.Tactic Elab Command Elab.Tactic Meta
+open Lean Parser.Tactic Elab Elab.Tactic Meta
 
 /--
 `_` in tactic position acts like the `done` tactic: it fails and gives the list
diff --git a/Batteries/Tactic/NoMatch.lean b/Batteries/Tactic/NoMatch.lean
index 7efe68e7d2..ee6acefaf0 100644
--- a/Batteries/Tactic/NoMatch.lean
+++ b/Batteries/Tactic/NoMatch.lean
@@ -3,8 +3,8 @@ Copyright (c) 2021 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import Lean.Elab.ElabRules
 import Lean.DocString
+import Lean.Elab.Tactic.Basic
 
 /-!
 Deprecation warnings for `match ⋯ with.`, `fun.`, `λ.`, and `intro.`.
diff --git a/Batteries/Tactic/PrintDependents.lean b/Batteries/Tactic/PrintDependents.lean
index 9c55a04ecd..e927713886 100644
--- a/Batteries/Tactic/PrintDependents.lean
+++ b/Batteries/Tactic/PrintDependents.lean
@@ -5,7 +5,6 @@ Authors: Mario Carneiro
 -/
 import Lean.Elab.Command
 import Lean.Util.FoldConsts
-import Batteries.Lean.Delaborator
 
 /-!
 # `#print dependents` command
diff --git a/Batteries/Tactic/PrintPrefix.lean b/Batteries/Tactic/PrintPrefix.lean
index 63d2c3bbf5..b83e7b0ad8 100644
--- a/Batteries/Tactic/PrintPrefix.lean
+++ b/Batteries/Tactic/PrintPrefix.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Shing Tak Lam, Daniel Selsam, Mario Carneiro
 -/
 import Batteries.Lean.Util.EnvSearch
-import Batteries.Lean.Delaborator
 import Lean.Elab.Tactic.Config
 
 namespace Batteries.Tactic
diff --git a/Batteries/Tactic/SeqFocus.lean b/Batteries/Tactic/SeqFocus.lean
index 8972f77891..cbbe70a44a 100644
--- a/Batteries/Tactic/SeqFocus.lean
+++ b/Batteries/Tactic/SeqFocus.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad
 -/
-import Lean.Elab.ElabRules
+import Lean.Elab.Tactic.Basic
 
 open Lean Elab Meta Tactic
 
diff --git a/Batteries/Tactic/ShowUnused.lean b/Batteries/Tactic/ShowUnused.lean
index 25989a3da9..3797801cd8 100644
--- a/Batteries/Tactic/ShowUnused.lean
+++ b/Batteries/Tactic/ShowUnused.lean
@@ -5,7 +5,6 @@ Authors: Mario Carneiro
 -/
 import Lean.Util.FoldConsts
 import Lean.Linter.UnusedVariables
-import Batteries.Lean.Delaborator
 
 /-!
 # The `#show_unused` command
diff --git a/Batteries/Tactic/Unreachable.lean b/Batteries/Tactic/Unreachable.lean
index 76571dc850..4d6e6cf0a1 100644
--- a/Batteries/Tactic/Unreachable.lean
+++ b/Batteries/Tactic/Unreachable.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import Lean.Elab.ElabRules
+import Lean.Elab.Tactic.Basic
 
 namespace Batteries.Tactic
 
diff --git a/Batteries/Util/Cache.lean b/Batteries/Util/Cache.lean
index edfac4fe97..866325df5a 100644
--- a/Batteries/Util/Cache.lean
+++ b/Batteries/Util/Cache.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Gabriel Ebner. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner
 -/
-import Batteries.Lean.Meta.DiscrTree
+import Lean.Meta.DiscrTree
 
 /-!
 # Once-per-file cache for tactics
diff --git a/Batteries/Util/ExtendedBinder.lean b/Batteries/Util/ExtendedBinder.lean
index d577e1d785..c489c0a432 100644
--- a/Batteries/Util/ExtendedBinder.lean
+++ b/Batteries/Util/ExtendedBinder.lean
@@ -3,8 +3,6 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner
 -/
-import Lean.Elab.MacroArgUtil
-import Lean.Linter.MissingDocs
 
 /-!
 Defines an extended binder syntax supporting `∀ ε > 0, ...` etc.
diff --git a/Batteries/Util/LibraryNote.lean b/Batteries/Util/LibraryNote.lean
index eb08bf0b27..8c1d45f786 100644
--- a/Batteries/Util/LibraryNote.lean
+++ b/Batteries/Util/LibraryNote.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Gabriel Ebner. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner
 -/
-import Lean.Elab.ElabRules
+import Lean.Elab.Command
 
 /-!
 # Define the `library_note` command.
diff --git a/test/MLList.lean b/test/MLList.lean
index 278d6dc83d..78f0299717 100644
--- a/test/MLList.lean
+++ b/test/MLList.lean
@@ -1,4 +1,5 @@
 import Batteries.Data.MLList.IO
+import Batteries.Data.List.Basic
 
 set_option linter.missingDocs false