diff --git a/src/Lean/Meta/ReduceEval.lean b/src/Lean/Meta/ReduceEval.lean
index 6c867be776..ab28b50c0f 100644
--- a/src/Lean/Meta/ReduceEval.lean
+++ b/src/Lean/Meta/ReduceEval.lean
@@ -3,11 +3,10 @@ Copyright (c) 2020 Sebastian Ullrich. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Ullrich
 -/
+import Lean.Meta.Offset
 
 /-! Evaluation by reduction -/
 
-import Lean.Meta.Offset
-
 namespace Lean.Meta
 
 class ReduceEval (α : Type) where
diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean
index 32f2c4f6b4..a9740fa7d4 100644
--- a/src/Lean/Parser/Basic.lean
+++ b/src/Lean/Parser/Basic.lean
@@ -3,6 +3,15 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Sebastian Ullrich
 -/
+import Lean.Data.Trie
+import Lean.Data.Position
+import Lean.Syntax
+import Lean.ToExpr
+import Lean.Environment
+import Lean.Attributes
+import Lean.Message
+import Lean.Compiler.InitAttr
+import Lean.ResolveName
 
 /-!
 # Basic Lean parser infrastructure
@@ -54,15 +63,6 @@ running multiple parsers should check if an error message is set in the parser s
 Error recovery is left to the designer of the specific language; for example, Lean's top-level `parseCommand` loop skips
 tokens until the next command keyword on error.
 -/
-import Lean.Data.Trie
-import Lean.Data.Position
-import Lean.Syntax
-import Lean.ToExpr
-import Lean.Environment
-import Lean.Attributes
-import Lean.Message
-import Lean.Compiler.InitAttr
-import Lean.ResolveName
 
 namespace Lean
 
diff --git a/src/Lean/ParserCompiler.lean b/src/Lean/ParserCompiler.lean
index 5b42588338..53b09cf806 100644
--- a/src/Lean/ParserCompiler.lean
+++ b/src/Lean/ParserCompiler.lean
@@ -3,17 +3,16 @@ Copyright (c) 2020 Sebastian Ullrich. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Ullrich
 -/
-
-/-!
-Gadgets for compiling parser declarations into other programs, such as pretty printers.
--/
-
 import Lean.Util.ReplaceExpr
 import Lean.Meta.Basic
 import Lean.Meta.WHNF
 import Lean.ParserCompiler.Attribute
 import Lean.Parser.Extension
 
+/-!
+Gadgets for compiling parser declarations into other programs, such as pretty printers.
+-/
+
 namespace Lean
 namespace ParserCompiler
 
diff --git a/src/Lean/PrettyPrinter/Delaborator/Basic.lean b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
index d23957605f..fdb32397fc 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Basic.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
@@ -3,6 +3,14 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Ullrich
 -/
+import Lean.KeyedDeclsAttribute
+import Lean.ProjFns
+import Lean.Syntax
+import Lean.Meta.Match
+import Lean.Elab.Term
+import Lean.PrettyPrinter.Delaborator.Options
+import Lean.PrettyPrinter.Delaborator.SubExpr
+import Lean.PrettyPrinter.Delaborator.TopDownAnalyze
 
 /-!
 The delaborator is the first stage of the pretty printer, and the inverse of the
@@ -25,15 +33,6 @@ back to the subterm.
 The delaborator is extensible via the `[delab]` attribute.
 -/
 
-import Lean.KeyedDeclsAttribute
-import Lean.ProjFns
-import Lean.Syntax
-import Lean.Meta.Match
-import Lean.Elab.Term
-import Lean.PrettyPrinter.Delaborator.Options
-import Lean.PrettyPrinter.Delaborator.SubExpr
-import Lean.PrettyPrinter.Delaborator.TopDownAnalyze
-
 namespace Lean.PrettyPrinter.Delaborator
 
 open Lean.Meta SubExpr
diff --git a/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean b/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean
index 2c969c8f12..cdf37f52ca 100644
--- a/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean
@@ -3,6 +3,8 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Daniel Selsam
 -/
+import Lean.Meta.Basic
+import Std.Data.RBMap
 
 /-!
 This file defines utilities for `MetaM` computations to traverse subexpressions
@@ -13,8 +15,6 @@ map a path of `childIdxs` to a natural number by computing the value of the 4-ar
 representation `1 :: childIdxs`, since n-ary representations without leading zeros
 are unique. Note that `pos` is initialized to `1` (case `childIdxs == []`).
 -/
-import Lean.Meta.Basic
-import Std.Data.RBMap
 
 namespace Lean.PrettyPrinter.Delaborator
 
diff --git a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
index 1498a66eb9..d555eb1854 100644
--- a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
@@ -3,6 +3,14 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Daniel Selsam
 -/
+import Lean.Meta
+import Lean.Util.FindMVar
+import Lean.Util.FindLevelMVar
+import Lean.Util.CollectLevelParams
+import Lean.Util.ReplaceLevel
+import Lean.PrettyPrinter.Delaborator.Options
+import Lean.PrettyPrinter.Delaborator.SubExpr
+import Std.Data.RBMap
 
 /-!
 The top-down analyzer is an optional preprocessor to the delaborator that aims
@@ -13,15 +21,6 @@ can still not be re-elaborated correctly, and it may also add many annotations
 that are not strictly necessary.
 -/
 
-import Lean.Meta
-import Lean.Util.FindMVar
-import Lean.Util.FindLevelMVar
-import Lean.Util.CollectLevelParams
-import Lean.Util.ReplaceLevel
-import Lean.PrettyPrinter.Delaborator.Options
-import Lean.PrettyPrinter.Delaborator.SubExpr
-import Std.Data.RBMap
-
 namespace Lean
 
 open Lean.Meta
diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index ad0ae82ce6..bc424cc20b 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -3,6 +3,11 @@ Copyright (c) 2020 Sebastian Ullrich. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Ullrich
 -/
+import Lean.CoreM
+import Lean.Parser.Extension
+import Lean.KeyedDeclsAttribute
+import Lean.ParserCompiler.Attribute
+import Lean.PrettyPrinter.Basic
 
 /-!
 The formatter turns a `Syntax` tree into a `Format` object, inserting both mandatory whitespace (to separate adjacent
@@ -13,12 +18,6 @@ parser-specific handlers registered via attributes. The traversal is right-to-le
 already know the text following it and can decide whether or not whitespace between the two is necessary.
 -/
 
-import Lean.CoreM
-import Lean.Parser.Extension
-import Lean.KeyedDeclsAttribute
-import Lean.ParserCompiler.Attribute
-import Lean.PrettyPrinter.Basic
-
 namespace Lean
 namespace PrettyPrinter
 namespace Formatter
diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean
index 84228d1ab0..77a2346945 100644
--- a/src/Lean/PrettyPrinter/Parenthesizer.lean
+++ b/src/Lean/PrettyPrinter/Parenthesizer.lean
@@ -3,6 +3,12 @@ Copyright (c) 2020 Sebastian Ullrich. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Ullrich
 -/
+import Lean.CoreM
+import Lean.KeyedDeclsAttribute
+import Lean.Parser.Extension
+import Lean.ParserCompiler.Attribute
+import Lean.PrettyPrinter.Basic
+
 
 /-!
 The parenthesizer inserts parentheses into a `Syntax` object where syntactically necessary, usually as an intermediary
@@ -71,12 +77,6 @@ node).
 
 -/
 
-import Lean.CoreM
-import Lean.KeyedDeclsAttribute
-import Lean.Parser.Extension
-import Lean.ParserCompiler.Attribute
-import Lean.PrettyPrinter.Basic
-
 namespace Lean
 namespace PrettyPrinter
 namespace Parenthesizer