diff --git a/src/Init/Data/Int/Basic.lean b/src/Init/Data/Int/Basic.lean
index 1ade341c59..dbf661c4be 100644
--- a/src/Init/Data/Int/Basic.lean
+++ b/src/Init/Data/Int/Basic.lean
@@ -8,7 +8,7 @@ The integers, with addition, multiplication, and subtraction.
 prelude
 import Init.Data.Cast
 import Init.Data.Nat.Div
-import Init.Data.List.Basic
+
 set_option linter.missingDocs true -- keep it documented
 open Nat
 
diff --git a/src/Init/Data/List/Impl.lean b/src/Init/Data/List/Impl.lean
index 79528b6007..f5967b5bac 100644
--- a/src/Init/Data/List/Impl.lean
+++ b/src/Init/Data/List/Impl.lean
@@ -38,8 +38,8 @@ The following operations were already given `@[csimp]` replacements in `Init/Dat
 `length`, `map`, `filter`, `replicate`, `leftPad`, `unzip`, `range'`, `iota`, `intersperse`.
 
 The following operations are given `@[csimp]` replacements below:
-``set`, `filterMap`, `foldr`, `append`, `bind`, `join`,
-`take`, `takeWhile`, `dropLast`, `replace`, `erase`, `eraseIdx`, `zipWith`, ,
+`set`, `filterMap`, `foldr`, `append`, `bind`, `join`,
+`take`, `takeWhile`, `dropLast`, `replace`, `erase`, `eraseIdx`, `zipWith`,
 `enumFrom`, and `intercalate`.
 
 -/
diff --git a/src/Lean/Data/AssocList.lean b/src/Lean/Data/AssocList.lean
index 751c755373..91953d5b05 100644
--- a/src/Lean/Data/AssocList.lean
+++ b/src/Lean/Data/AssocList.lean
@@ -5,7 +5,8 @@ Author: Leonardo de Moura
 -/
 prelude
 import Init.Control.Id
-import Init.Data.List.Basic
+import Init.Data.List.Impl
+
 universe u v w w'
 namespace Lean
 
diff --git a/src/Lean/Data/HashSet.lean b/src/Lean/Data/HashSet.lean
index cf6d67ebd0..44895f5576 100644
--- a/src/Lean/Data/HashSet.lean
+++ b/src/Lean/Data/HashSet.lean
@@ -5,7 +5,6 @@ Author: Leonardo de Moura
 -/
 prelude
 import Init.Data.Nat.Power2
-import Init.Data.List.Control
 import Std.Data.HashSet.Basic
 import Std.Data.HashSet.Raw
 namespace Lean
diff --git a/src/Lean/Data/Json/Basic.lean b/src/Lean/Data/Json/Basic.lean
index 00344dfb27..8efce0000d 100644
--- a/src/Lean/Data/Json/Basic.lean
+++ b/src/Lean/Data/Json/Basic.lean
@@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Marc Huisinga
 -/
 prelude
-import Init.Data.List.Control
 import Init.Data.Range
 import Init.Data.OfScientific
 import Init.Data.Hashable
diff --git a/src/Lean/Data/KVMap.lean b/src/Lean/Data/KVMap.lean
index 63d534acd9..60db90bbb7 100644
--- a/src/Lean/Data/KVMap.lean
+++ b/src/Lean/Data/KVMap.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Init.Data.List.Control
+import Init.Data.List.Impl
 import Init.Data.Format.Syntax
 
 namespace Lean
diff --git a/src/Lean/Util/Path.lean b/src/Lean/Util/Path.lean
index 6d1ba4c407..d9b3a0b07a 100644
--- a/src/Lean/Util/Path.lean
+++ b/src/Lean/Util/Path.lean
@@ -10,7 +10,6 @@ with a directory `A/`. `import A` resolves to `path/A.olean`.
 -/
 prelude
 import Init.System.IO
-import Init.Data.List.Control
 
 namespace Lean
 open System
diff --git a/src/Lean/Util/SCC.lean b/src/Lean/Util/SCC.lean
index 2bff601321..fbd213c0fd 100644
--- a/src/Lean/Util/SCC.lean
+++ b/src/Lean/Util/SCC.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Init.Data.List.Control
 import Lean.Data.HashMap
 import Std.Data.HashMap.Basic
 namespace Lean.SCC
diff --git a/tests/lean/run/discrTreeSimp.lean b/tests/lean/run/discrTreeSimp.lean
index 3c50f95921..7c62252129 100644
--- a/tests/lean/run/discrTreeSimp.lean
+++ b/tests/lean/run/discrTreeSimp.lean
@@ -1,6 +1,8 @@
 prelude
 import Init.MetaTypes
-import Init.Data.List.Basic
+import Init.Data.List.Lemmas
+
+attribute [-simp] List.map_map -- Turn off the global simp lemma so we can turn on and off the local version.
 
 @[simp] theorem map_comp_map (f : α → β) (g : β → γ) : List.map g ∘ List.map f = List.map (g ∘ f) :=
   sorry