diff --git a/tests/bench/parser.lean b/tests/bench/parser.lean
index 4438f31822..e3457f9726 100644
--- a/tests/bench/parser.lean
+++ b/tests/bench/parser.lean
@@ -1,4 +1,4 @@
-import Init.Lean.Parser
+import Lean.Parser
 
 def main : List String → IO Unit
 | [fname, n] => do
diff --git a/tests/compiler/expr.lean b/tests/compiler/expr.lean
index 30c712d644..ccccbb9408 100644
--- a/tests/compiler/expr.lean
+++ b/tests/compiler/expr.lean
@@ -1,4 +1,4 @@
-import Init.Lean.Expr
+import Lean.Expr
 open Lean
 
 def main : IO UInt32 :=
diff --git a/tests/compiler/phashmap.lean b/tests/compiler/phashmap.lean
index a429f11012..cce12ef257 100644
--- a/tests/compiler/phashmap.lean
+++ b/tests/compiler/phashmap.lean
@@ -1,5 +1,5 @@
 import Init.Data.PersistentHashMap
-import Init.Lean.Data.Format
+import Lean.Data.Format
 open Lean PersistentHashMap
 
 abbrev Map := PersistentHashMap Nat Nat
diff --git a/tests/compiler/phashmap2.lean b/tests/compiler/phashmap2.lean
index c924b1389b..31ddea6b5a 100644
--- a/tests/compiler/phashmap2.lean
+++ b/tests/compiler/phashmap2.lean
@@ -1,5 +1,5 @@
 import Init.Data.PersistentHashMap
-import Init.Lean.Data.Format
+import Lean.Data.Format
 open Lean PersistentHashMap
 
 abbrev Map := PersistentHashMap Nat Nat
diff --git a/tests/compiler/phashmap3.lean b/tests/compiler/phashmap3.lean
index efbeb6a76b..f525954b8a 100644
--- a/tests/compiler/phashmap3.lean
+++ b/tests/compiler/phashmap3.lean
@@ -1,5 +1,5 @@
 import Init.Data.PersistentHashMap
-import Init.Lean.Data.Format
+import Lean.Data.Format
 open Lean PersistentHashMap
 
 abbrev Map := PersistentHashMap Nat Nat
diff --git a/tests/compiler/termparsertest1.lean b/tests/compiler/termparsertest1.lean
index 222ce942ac..3603f6251d 100644
--- a/tests/compiler/termparsertest1.lean
+++ b/tests/compiler/termparsertest1.lean
@@ -1,4 +1,4 @@
-import Init.Lean.Parser.Term
+import Lean.Parser.Term
 open Lean
 open Lean.Parser
 
diff --git a/tests/lean/abst.lean b/tests/lean/abst.lean
index d0bb3646f0..5a4de4ad11 100644
--- a/tests/lean/abst.lean
+++ b/tests/lean/abst.lean
@@ -1,4 +1,4 @@
-import Init.Lean.Expr
+import Lean.Expr
 open Lean
 
 def tst : IO Unit :=
diff --git a/tests/lean/ctor_layout.lean b/tests/lean/ctor_layout.lean
index ae61cf7f62..b76f654aae 100644
--- a/tests/lean/ctor_layout.lean
+++ b/tests/lean/ctor_layout.lean
@@ -1,4 +1,4 @@
-import Init.Lean.Compiler.IR
+import Lean.Compiler.IR
 open Lean
 open Lean.IR
 
diff --git a/tests/lean/inst.lean b/tests/lean/inst.lean
index 6f20b2a980..7073510e5a 100644
--- a/tests/lean/inst.lean
+++ b/tests/lean/inst.lean
@@ -1,4 +1,4 @@
-import Init.Lean.Expr
+import Lean.Expr
 open Lean
 
 def tst : IO Unit :=
diff --git a/tests/lean/json.lean b/tests/lean/json.lean
index 319cae4e5e..808237893b 100644
--- a/tests/lean/json.lean
+++ b/tests/lean/json.lean
@@ -1,5 +1,5 @@
-import Init.Lean.Data.Json.Parser
-import Init.Lean.Data.Json.Printer
+import Lean.Data.Json.Parser
+import Lean.Data.Json.Printer
 
 def test (s : String) : String :=
 match Lean.Json.parse s with
diff --git a/tests/lean/lvl1.lean b/tests/lean/lvl1.lean
index 68449f95fb..0228d2673f 100644
--- a/tests/lean/lvl1.lean
+++ b/tests/lean/lvl1.lean
@@ -1,4 +1,4 @@
-import Init.Lean.Level
+import Lean.Level
 
 namespace Lean
 namespace Level
diff --git a/tests/lean/mvar1.lean b/tests/lean/mvar1.lean
index 56aa57c5e4..dd4adc971b 100644
--- a/tests/lean/mvar1.lean
+++ b/tests/lean/mvar1.lean
@@ -1,4 +1,4 @@
-import Init.Lean.MetavarContext
+import Lean.MetavarContext
 open Lean
 
 def check (b : Bool) : IO Unit :=
diff --git a/tests/lean/mvar2.lean b/tests/lean/mvar2.lean
index 3bae591d80..482cb8a766 100644
--- a/tests/lean/mvar2.lean
+++ b/tests/lean/mvar2.lean
@@ -1,4 +1,4 @@
-import Init.Lean.MetavarContext
+import Lean.MetavarContext
 open Lean
 
 def check (b : Bool) : IO Unit :=
diff --git a/tests/lean/mvar3.lean b/tests/lean/mvar3.lean
index a5494cf603..438f52901a 100644
--- a/tests/lean/mvar3.lean
+++ b/tests/lean/mvar3.lean
@@ -1,4 +1,4 @@
-import Init.Lean.MetavarContext
+import Lean.MetavarContext
 open Lean
 
 def mkLambdaTest (mctx : MetavarContext) (ngen : NameGenerator) (lctx : LocalContext) (xs : Array Expr) (e : Expr)
diff --git a/tests/lean/run/DefEqAssignBug.lean b/tests/lean/run/DefEqAssignBug.lean
index 46cf4deb5c..5b5ea25316 100644
--- a/tests/lean/run/DefEqAssignBug.lean
+++ b/tests/lean/run/DefEqAssignBug.lean
@@ -1,4 +1,4 @@
-import Init.Lean.Meta
+import Lean.Meta
 open Lean
 open Lean.Meta
 
diff --git a/tests/lean/run/Reparen.lean b/tests/lean/run/Reparen.lean
index b09b492ff2..49ec279dad 100644
--- a/tests/lean/run/Reparen.lean
+++ b/tests/lean/run/Reparen.lean
@@ -1,5 +1,5 @@
 /-! Reprint file after removing all parentheses and then passing it through the parenthesizer -/
-import Init.Lean.PrettyPrinter.Parenthesizer
+import Lean.PrettyPrinter.Parenthesizer
 
 open Lean
 open Lean.Elab
diff --git a/tests/lean/run/expr1.lean b/tests/lean/run/expr1.lean
index dc22007508..8bfaac0e95 100644
--- a/tests/lean/run/expr1.lean
+++ b/tests/lean/run/expr1.lean
@@ -1,4 +1,4 @@
-import Init.Lean.Expr
+import Lean.Expr
 open Lean
 
 def tst1 : IO Unit :=
diff --git a/tests/lean/run/expr_maps.lean b/tests/lean/run/expr_maps.lean
index 3487308fe2..e8b78370f3 100644
--- a/tests/lean/run/expr_maps.lean
+++ b/tests/lean/run/expr_maps.lean
@@ -1,4 +1,4 @@
-import Init.Lean.Expr
+import Lean.Expr
 open Lean
 
 def exprType : Expr := mkSort levelOne
diff --git a/tests/lean/run/frontend1.lean b/tests/lean/run/frontend1.lean
index b6ae9f9811..0d5d4586f4 100644
--- a/tests/lean/run/frontend1.lean
+++ b/tests/lean/run/frontend1.lean
@@ -1,4 +1,4 @@
-import Init.Lean.Elab
+import Lean.Elab
 open Lean
 open Lean.Elab
 
diff --git a/tests/lean/run/level.lean b/tests/lean/run/level.lean
index 30a7f8d9a9..d246389ce9 100644
--- a/tests/lean/run/level.lean
+++ b/tests/lean/run/level.lean
@@ -1,4 +1,4 @@
-import Init.Lean.Level
+import Lean.Level
 open Lean
 
 #eval levelZero == levelZero
diff --git a/tests/lean/run/meta1.lean b/tests/lean/run/meta1.lean
index dc805be8f1..851c49e223 100644
--- a/tests/lean/run/meta1.lean
+++ b/tests/lean/run/meta1.lean
@@ -1,4 +1,4 @@
-import Init.Lean.Meta
+import Lean.Meta
 open Lean
 open Lean.Meta
 
diff --git a/tests/lean/run/meta2.lean b/tests/lean/run/meta2.lean
index 092de79bee..b0aca01abd 100644
--- a/tests/lean/run/meta2.lean
+++ b/tests/lean/run/meta2.lean
@@ -1,4 +1,4 @@
-import Init.Lean.Meta
+import Lean.Meta
 open Lean
 open Lean.Meta
 
diff --git a/tests/lean/run/meta3.lean b/tests/lean/run/meta3.lean
index 6b9d20118b..ca7a89b904 100644
--- a/tests/lean/run/meta3.lean
+++ b/tests/lean/run/meta3.lean
@@ -1,4 +1,4 @@
-import Init.Lean.Meta
+import Lean.Meta
 open Lean
 open Lean.Meta
 
diff --git a/tests/lean/run/meta4.lean b/tests/lean/run/meta4.lean
index 9219811936..79394cfbb1 100644
--- a/tests/lean/run/meta4.lean
+++ b/tests/lean/run/meta4.lean
@@ -1,4 +1,4 @@
-import Init.Lean.Meta
+import Lean.Meta
 open Lean
 open Lean.Meta
 
diff --git a/tests/lean/run/meta5.lean b/tests/lean/run/meta5.lean
index 394e58137f..2f06ea0366 100644
--- a/tests/lean/run/meta5.lean
+++ b/tests/lean/run/meta5.lean
@@ -1,4 +1,4 @@
-import Init.Lean.Meta
+import Lean.Meta
 open Lean
 open Lean.Meta
 
diff --git a/tests/lean/run/meta6.lean b/tests/lean/run/meta6.lean
index d92a156eb6..03717473e4 100644
--- a/tests/lean/run/meta6.lean
+++ b/tests/lean/run/meta6.lean
@@ -1,4 +1,4 @@
-import Init.Lean.Meta
+import Lean.Meta
 open Lean
 open Lean.Meta
 
diff --git a/tests/lean/run/parseCore.lean b/tests/lean/run/parseCore.lean
index a6953f6b2c..6c04619379 100644
--- a/tests/lean/run/parseCore.lean
+++ b/tests/lean/run/parseCore.lean
@@ -1,4 +1,4 @@
-import Init.Lean.Parser
+import Lean.Parser
 
 def test : IO Unit :=
 if System.Platform.isWindows then
diff --git a/tests/lean/run/recInfo1.lean b/tests/lean/run/recInfo1.lean
index b2e5a52c6f..6451f5786a 100644
--- a/tests/lean/run/recInfo1.lean
+++ b/tests/lean/run/recInfo1.lean
@@ -1,4 +1,4 @@
-import Init.Lean.Meta
+import Lean.Meta
 
 open Lean
 open Lean.Meta
diff --git a/tests/lean/run/synth1.lean b/tests/lean/run/synth1.lean
index 5a3b1bb39f..28faf0b083 100644
--- a/tests/lean/run/synth1.lean
+++ b/tests/lean/run/synth1.lean
@@ -1,4 +1,4 @@
-import Init.Lean.Meta
+import Lean.Meta
 open Lean
 open Lean.Meta
 
diff --git a/tests/lean/run/tactic.lean b/tests/lean/run/tactic.lean
index e6488b060f..8a1db54e60 100644
--- a/tests/lean/run/tactic.lean
+++ b/tests/lean/run/tactic.lean
@@ -1,4 +1,4 @@
-import Init.Lean.Meta
+import Lean.Meta
 open Lean
 open Lean.Meta
 
diff --git a/tests/lean/run/termparsertest1.lean b/tests/lean/run/termparsertest1.lean
index a0cf6da4ad..3ad94c1027 100644
--- a/tests/lean/run/termparsertest1.lean
+++ b/tests/lean/run/termparsertest1.lean
@@ -1,4 +1,4 @@
-import Init.Lean.Parser.Term
+import Lean.Parser.Term
 open Lean
 open Lean.Parser
 
diff --git a/tests/lean/run/trace.lean b/tests/lean/run/trace.lean
index 3ad86865e0..41dd678497 100644
--- a/tests/lean/run/trace.lean
+++ b/tests/lean/run/trace.lean
@@ -1,4 +1,4 @@
-import Init.Lean.Util.Trace
+import Lean.Util.Trace
 open Lean
 
 structure MyState :=
diff --git a/tests/lean/run/update.lean b/tests/lean/run/update.lean
index 289591478d..ae13b2e6c8 100644
--- a/tests/lean/run/update.lean
+++ b/tests/lean/run/update.lean
@@ -1,4 +1,4 @@
-import Init.Lean.Expr
+import Lean.Expr
 open Lean
 
 def main : IO Unit :=
diff --git a/tests/playground/DiscrTree.lean b/tests/playground/DiscrTree.lean
index c8d22fbd4d..7d856f177b 100644
--- a/tests/playground/DiscrTree.lean
+++ b/tests/playground/DiscrTree.lean
@@ -1,4 +1,4 @@
-import Init.Lean.Format
+import Lean.Format
 open Lean
 
 def List.insert {α} [HasBeq α] (as : List α) (a : α) : List α :=
diff --git a/tests/playground/cmdparsertest1.lean b/tests/playground/cmdparsertest1.lean
index 31e661630c..7293984425 100644
--- a/tests/playground/cmdparsertest1.lean
+++ b/tests/playground/cmdparsertest1.lean
@@ -1,4 +1,4 @@
-import Init.Lean.Parser.Command
+import Lean.Parser.Command
 open Lean
 open Lean.Parser