chore: imports

src/Lean/Meta/Tactic/Grind/AlphaShareCommon.lean

@@ -4,12 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Meta.Tactic.Grind.ExprPtr
-
 public section
-
 namespace Lean.Meta.Grind
 
 private def hashChild (e : Expr) : UInt64 :=

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/DvdCnstr.lean

@@ -6,6 +6,8 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
+import Init.Data.Int.OfNat
+import Init.Grind.Propagator
 import Lean.Meta.Tactic.Simp.Arith.Int
 import Lean.Meta.Tactic.Grind.Simp
 import Lean.Meta.Tactic.Grind.PropagatorAttr

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/LeCnstr.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
+import Init.Data.Int.OfNat
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
 import Lean.Meta.Tactic.Simp.Arith.Int
 import Lean.Meta.Tactic.Grind.PropagatorAttr

src/Lean/Meta/Tactic/Grind/Arith/Main.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Types
+import Init.Grind.Propagator
 import Lean.Meta.Tactic.Grind.PropagatorAttr
 import Lean.Meta.Tactic.Grind.Arith.Offset.Types
 import Lean.Meta.Tactic.Grind.Arith.Offset.Main

src/Lean/Meta/Tactic/Grind/Beta.lean

@@ -4,12 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Meta.Tactic.Grind.Types
-
 public section
-
 namespace Lean.Meta.Grind
 
 /-- Returns all lambda expressions in the equivalence class with root `root`. -/

src/Lean/Meta/Tactic/Grind/Cases.lean

@@ -4,12 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Meta.Tactic.Cases
-
 public section
-
 namespace Lean.Meta.Grind
 
 /-- Types that `grind` will case-split on. -/

src/Lean/Meta/Tactic/Grind/CasesMatch.lean

@@ -7,6 +7,7 @@ module
 prelude
 public import Lean.Meta.Tactic.Util
 import Lean.Meta.Tactic.Grind.Types
+import Lean.Meta.Tactic.Grind.Util
 import Lean.Meta.Tactic.Cases
 import Lean.Meta.Match.MatcherApp
 import Lean.Meta.Tactic.Grind.MatchCond

src/Lean/Meta/Tactic/Grind/Core.lean

@@ -4,21 +4,18 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
-public import Init.Grind.Util
-public import Lean.Meta.LitValues
 public import Lean.Meta.Tactic.Grind.Types
-public import Lean.Meta.Tactic.Grind.Inv
-public import Lean.Meta.Tactic.Grind.PP
-public import Lean.Meta.Tactic.Grind.Ctor
-public import Lean.Meta.Tactic.Grind.Util
-public import Lean.Meta.Tactic.Grind.Beta
-public import Lean.Meta.Tactic.Grind.Internalize
-public import Lean.Meta.Tactic.Grind.Simp
-
+import Init.Grind.Util
+import Lean.Meta.LitValues
+import Lean.Meta.Tactic.Grind.Inv
+import Lean.Meta.Tactic.Grind.PP
+import Lean.Meta.Tactic.Grind.Ctor
+import Lean.Meta.Tactic.Grind.Util
+import Lean.Meta.Tactic.Grind.Beta
+import Lean.Meta.Tactic.Grind.Simp
+import Lean.Meta.Tactic.Grind.Internalize
 public section
-
 namespace Lean.Meta.Grind
 
 /--

src/Lean/Meta/Tactic/Grind/Ctor.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Meta.Tactic.Grind.Types
 import Lean.Meta.Tactic.Grind.Simp

src/Lean/Meta/Tactic/Grind/Diseq.lean

@@ -4,13 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
-public import Init.Grind.Lemmas
 public import Lean.Meta.Tactic.Grind.Types
-
+import Init.Grind.Lemmas
 public section
-
 namespace Lean.Meta.Grind
 
 private def dummyEq : Expr := mkApp (mkConst ``Eq [1]) default

src/Lean/Meta/Tactic/Grind/EMatch.lean

@@ -8,9 +8,11 @@ prelude
 public import Lean.Meta.Tactic.Grind.Types
 import Lean.Util.CollectLevelMVars
 import Lean.Meta.Tactic.Grind.Core
+import Lean.Meta.Tactic.Grind.Util
 import Lean.Meta.Tactic.Grind.MatchDiscrOnly
 import Lean.Meta.Tactic.Grind.ProveEq
 import Lean.Meta.Tactic.Grind.SynthInstance
+import Lean.Meta.Tactic.Grind.Simp
 public section
 namespace Lean.Meta.Grind
 namespace EMatch

src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean

@@ -5,16 +5,16 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Init.Grind.Util
-public import Init.Grind.Tactics
-public import Lean.HeadIndex
-public import Lean.Util.FoldConsts
-public import Lean.Util.CollectFVars
 public import Lean.Meta.Basic
-public import Lean.Meta.InferType
-public import Lean.Meta.Eqns
-public import Lean.Meta.Tactic.Grind.Util
 public import Lean.Meta.Tactic.Grind.Theorems
+import Init.Grind.Util
+import Init.Grind.Tactics
+import Lean.Util.FoldConsts
+import Lean.Util.CollectFVars
+import Lean.Meta.Basic
+import Lean.Meta.InferType
+import Lean.Meta.Eqns
+import Lean.Meta.Tactic.Grind.Util
 import Lean.Message
 import Lean.Meta.Tactic.FVarSubst
 import Lean.Meta.Match.Basic

src/Lean/Meta/Tactic/Grind/EqResolution.lean

@@ -4,14 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
-public import Lean.Meta.AppBuilder
-public import Lean.Meta.MatchUtil
-public import Lean.Util.ForEachExpr
-
+public import Lean.Meta.Basic
+import Lean.Meta.AppBuilder
+import Lean.Meta.MatchUtil
+import Lean.Util.ForEachExpr
 public section
-
 namespace Lean.Meta.Grind
 /-! A basic "equality resolution" procedure. -/
 

src/Lean/Meta/Tactic/Grind/ExprPtr.lean

@@ -4,12 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Expr
-
 public section
-
 namespace Lean.Meta.Grind
 
 @[inline] def isSameExpr (a b : Expr) : Bool :=

src/Lean/Meta/Tactic/Grind/Ext.lean

@@ -4,13 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Meta.Tactic.Grind.Types
-public import Lean.Meta.Tactic.Grind.SynthInstance
-
+import Lean.Meta.Tactic.Grind.SynthInstance
 public section
-
 namespace Lean.Meta.Grind
 /-! Extensionality theorems support. -/
 

src/Lean/Meta/Tactic/Grind/ExtAttr.lean

@@ -4,12 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Meta.Tactic.Ext
-
 public section
-
 namespace Lean.Meta.Grind
 /-! Grind extensionality attribute to mark which `[ext]` theorems should be used. -/
 

src/Lean/Meta/Tactic/Grind/ForallProp.lean

@@ -7,8 +7,10 @@ module
 prelude
 public import Lean.Meta.Tactic.Grind.Types
 public import Init.Grind.Propagator
+import Init.Simproc
 import Init.Grind.Lemmas
 import Init.Grind.Norm
+import Lean.Meta.Tactic.Grind.PropagatorAttr
 import Lean.Meta.Tactic.Grind.Propagate
 import Lean.Meta.Tactic.Grind.Internalize
 import Lean.Meta.Tactic.Grind.Simp

src/Lean/Meta/Tactic/Grind/Injection.lean

@@ -4,11 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
-public import Lean.Meta.CtorRecognizer
-public import Lean.Meta.Tactic.Util
-public import Lean.Meta.Tactic.Clear
+public import Lean.Meta.Basic
+import Lean.Meta.CtorRecognizer
+import Lean.Meta.Tactic.Util
+import Lean.Meta.Tactic.Clear
 import Lean.Meta.AppBuilder
 
 public section

src/Lean/Meta/Tactic/Grind/Internalize.lean

@@ -5,9 +5,10 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Init.Grind.Util
-public import Init.Grind.Lemmas
-public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
+public import Lean.Meta.Tactic.Grind.Types
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
+import Init.Grind.Util
+import Init.Grind.Lemmas
 import Lean.Meta.LitValues
 import Lean.Meta.Match.MatcherInfo
 import Lean.Meta.Match.MatchEqsExt

src/Lean/Meta/Tactic/Grind/Intro.lean

@@ -11,6 +11,7 @@ public import Lean.Meta.Tactic.Grind.SearchM
 import Lean.Meta.Tactic.Assert
 import Lean.Meta.Tactic.Apply
 import Lean.Meta.Tactic.Grind.Simp
+import Lean.Meta.Tactic.Grind.Util
 import Lean.Meta.Tactic.Grind.Cases
 import Lean.Meta.Tactic.Grind.CasesMatch
 import Lean.Meta.Tactic.Grind.Injection

src/Lean/Meta/Tactic/Grind/Inv.lean

@@ -6,8 +6,10 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Types
+import Init.Grind.Util
 import Lean.Meta.Tactic.Grind.Proof
 import Lean.Meta.Tactic.Grind.MatchCond
+import Lean.Meta.Tactic.Grind.Util
 namespace Lean.Meta.Grind
 /-!
 Debugging support code for checking basic invariants.

src/Lean/Meta/Tactic/Grind/LawfulEqCmp.lean

@@ -4,23 +4,20 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Meta.Tactic.Grind.Types
-public import Lean.Meta.Tactic.Grind.SynthInstance
-
+import Lean.Meta.Tactic.Grind.Util
+import Lean.Meta.Tactic.Grind.SynthInstance
 public section
-
+namespace Lean.Meta.Grind
 /-!
 Support for type class `LawfulEqCmp`.
 -/
 /-
-Note: we will have similar support for `Associative` and `Commutative`. In the future, we should have
+**Note**: we will have similar support for `Associative` and `Commutative`. In the future, we should have
 a mechanism for letting users to install their own handlers.
 -/
 
-namespace Lean.Meta.Grind
-
 /--
 If `op` implements `LawfulEqCmp`, then returns the proof term for
 `∀ a b, op a b = .eq → a = b`

src/Lean/Meta/Tactic/Grind/MBTC.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Types
-public import Lean.Meta.Tactic.Grind.Canon
+import Lean.Meta.Tactic.Grind.Canon
 import Lean.Meta.Tactic.Grind.CastLike
 public section
 namespace Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/Main.lean

@@ -8,8 +8,10 @@ prelude
 public import Lean.Meta.Tactic.Util
 public import Lean.Meta.Tactic.Grind.Types
 import Init.Grind.Lemmas
+import Lean.PrettyPrinter
 import Lean.Meta.Tactic.ExposeNames
 import Lean.Meta.Tactic.Simp.Diagnostics
+import Lean.Meta.Tactic.Simp.Rewrite
 import Lean.Meta.Tactic.Grind.Split
 import Lean.Meta.Tactic.Grind.RevertAll
 import Lean.Meta.Tactic.Grind.PropagatorAttr
@@ -20,6 +22,7 @@ import Lean.Meta.Tactic.Grind.Inv
 import Lean.Meta.Tactic.Grind.Intro
 import Lean.Meta.Tactic.Grind.EMatch
 import Lean.Meta.Tactic.Grind.Solve
+import Lean.Meta.Tactic.Grind.Internalize
 import Lean.Meta.Tactic.Grind.SimpUtil
 import Lean.Meta.Tactic.Grind.Cases
 import Lean.Meta.Tactic.Grind.LawfulEqCmp

src/Lean/Meta/Tactic/Grind/MarkNestedSubsingletons.lean

@@ -4,19 +4,16 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
-public import Init.Grind.Util
-public import Lean.Util.PtrSet
-public import Lean.Meta.Transform
-public import Lean.Meta.Basic
-public import Lean.Meta.InferType
-public import Lean.Meta.Tactic.Grind.ExprPtr
-public import Lean.Meta.Tactic.Grind.Util
 public import Lean.Meta.Tactic.Grind.Types
-
+import Init.Grind.Util
+import Lean.Util.PtrSet
+import Lean.Meta.Transform
+import Lean.Meta.Basic
+import Lean.Meta.InferType
+import Lean.Meta.Tactic.Grind.ExprPtr
+import Lean.Meta.Tactic.Grind.Util
 public section
-
 namespace Lean.Meta.Grind
 
 private abbrev M := StateRefT (Std.HashMap ExprPtr Expr) GrindM

src/Lean/Meta/Tactic/Grind/MatchCond.lean

@@ -4,16 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
-public import Init.Grind
-public import Init.Simproc
-public import Lean.Meta.Tactic.Contradiction
-public import Lean.Meta.Tactic.Grind.ProveEq
-public import Lean.Meta.Tactic.Grind.PropagatorAttr
-
+public import Lean.Meta.Tactic.Grind.Types
+import Init.Grind
+import Init.Simproc
+import Lean.Meta.Tactic.Contradiction
+import Lean.Meta.Tactic.Grind.ProveEq
+import Lean.Meta.Tactic.Grind.PropagatorAttr
 public section
-
 namespace Lean.Meta.Grind
 /-
 Remark: the `simp` module has some support for `MatchCond`, but it is

src/Lean/Meta/Tactic/Grind/MatchDiscrOnly.lean

@@ -4,15 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
-public import Init.Grind.Util
-public import Init.Simproc
 public import Lean.Meta.Tactic.Simp.Simproc
-public import Lean.Meta.Tactic.Simp.Rewrite
-
+import Init.Grind.Util
+import Init.Simproc
+import Lean.Meta.Tactic.Simp.Rewrite
 public section
-
 namespace Lean.Meta.Grind
 /--
 Returns `Grind.simpMatchDiscrsOnly e`. Recall that `Grind.simpMatchDiscrsOnly` is

src/Lean/Meta/Tactic/Grind/PP.lean

@@ -5,15 +5,15 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Init.Grind.Util
-public import Init.Grind.Injective
-public import Init.Grind.PP
 public import Lean.Meta.Tactic.Grind.Types
-public import Lean.Meta.Tactic.Grind.Arith.Model
-public import Lean.Meta.Tactic.Grind.Arith.Offset.Types
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.PP
-public import Lean.Meta.Tactic.Grind.Arith.Linear.PP
-public import Lean.Meta.Tactic.Grind.AC.PP
+import Init.Grind.Util
+import Init.Grind.Injective
+import Init.Grind.PP
+import Lean.Meta.Tactic.Grind.Arith.Model
+import Lean.Meta.Tactic.Grind.Arith.Offset.Types
+import Lean.Meta.Tactic.Grind.Arith.CommRing.PP
+import Lean.Meta.Tactic.Grind.Arith.Linear.PP
+import Lean.Meta.Tactic.Grind.AC.PP
 import Lean.Meta.Tactic.Grind.CastLike
 import Lean.PrettyPrinter
 import Lean.Meta.CtorRecognizer

src/Lean/Meta/Tactic/Grind/Parser.lean

@@ -4,12 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Parser.Command
-
 public section
-
 namespace Lean.Parser.Command
 /-!
 Builtin parsers for `grind` related commands

src/Lean/Meta/Tactic/Grind/Proj.lean

@@ -4,14 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
-public import Lean.ProjFns
 public import Lean.Meta.Tactic.Grind.Types
-public import Lean.Meta.Tactic.Grind.Internalize
-
+import Lean.ProjFns
+import Lean.Meta.Tactic.Grind.Internalize
 public section
-
 namespace Lean.Meta.Grind
 
 /--

src/Lean/Meta/Tactic/Grind/Proof.lean

@@ -4,13 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
-public import Init.Grind.Lemmas
 public import Lean.Meta.Tactic.Grind.Types
-
+import Init.Grind.Lemmas
 public section
-
 namespace Lean.Meta.Grind
 
 private def isEqProof (h : Expr) : MetaM Bool := do

src/Lean/Meta/Tactic/Grind/Propagate.lean

@@ -5,12 +5,12 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Init.Grind
-public import Lean.Meta.Tactic.Grind.Proof
-public import Lean.Meta.Tactic.Grind.PropagatorAttr
-public import Lean.Meta.Tactic.Grind.Simp
-public import Lean.Meta.Tactic.Grind.Ext
-public import Lean.Meta.Tactic.Grind.Internalize
+public import Lean.Meta.Tactic.Grind.Types
+import Init.Grind
+import Lean.Meta.Tactic.Grind.Proof
+import Lean.Meta.Tactic.Grind.PropagatorAttr
+import Lean.Meta.Tactic.Grind.Simp
+import Lean.Meta.Tactic.Grind.Ext
 import Lean.Meta.Tactic.Grind.Diseq
 public section
 namespace Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/PropagateInj.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Types
+import Init.Grind.Propagator
 import Init.Grind.Injective
 import Lean.Meta.Tactic.Grind.Proof
 import Lean.Meta.Tactic.Grind.PropagatorAttr

src/Lean/Meta/Tactic/Grind/PropagatorAttr.lean

@@ -4,13 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
-public import Init.Grind
 public import Lean.Meta.Tactic.Grind.Proof
-
+import Lean.Compiler.InitAttr
+import Init.Grind
 public section
-
 namespace Lean.Meta.Grind
 
 /-- Builtin propagators. -/

src/Lean/Meta/Tactic/Grind/ProveEq.lean

@@ -4,13 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Meta.Tactic.Grind.Types
 import Lean.Meta.Tactic.Grind.Simp
-
 public section
-
 namespace Lean.Meta.Grind
 /--
 If `e` has not been internalized yet, instantiate metavariables, unfold reducible, canonicalize,

src/Lean/Meta/Tactic/Grind/ReflCmp.lean

@@ -4,13 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
 module
-
 prelude
 public import Lean.Meta.Tactic.Grind.Types
-public import Lean.Meta.Tactic.Grind.SynthInstance
-
+import Lean.Meta.Tactic.Grind.SynthInstance
+import Lean.Meta.Tactic.Grind.Util
 public section
-
+namespace Lean.Meta.Grind
 /-!
 Support for type class `ReflCmp`.
 -/
@@ -19,8 +18,6 @@ Note: we will have similar support for `Associative` and `Commutative`. In the f
 a mechanism for letting users to install their own handlers.
 -/
 
-namespace Lean.Meta.Grind
-
 /--
 If `op` implements `ReflCmp`, then returns the proof term for
 `∀ a b, a = b → op a b = .eq`

src/Lean/Meta/Tactic/Grind/RevertAll.lean

@@ -4,12 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Meta.Tactic.Revert
-
 public section
-
 namespace Lean.Meta.Grind
 /--
 Reverts all free variables in the goal `mvarId`.

src/Lean/Meta/Tactic/Grind/SearchM.lean

@@ -4,13 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
-public import Lean.Util.ForEachExpr
 public import Lean.Meta.Tactic.Grind.Types
-
+import Lean.Util.ForEachExpr
 public section
-
 namespace Lean.Meta.Grind
 /--
 A `choice` (aka backtracking) point in the search tree.

src/Lean/Meta/Tactic/Grind/SimpUtil.lean

@@ -4,19 +4,18 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Meta.Tactic.Simp.Simproc
-public import Lean.Meta.Tactic.Grind.Simp
-public import Lean.Meta.Tactic.Grind.MatchDiscrOnly
-public import Lean.Meta.Tactic.Grind.MatchCond
-public import Lean.Meta.Tactic.Grind.ForallProp
-public import Lean.Meta.Tactic.Grind.Arith.Simproc
-public import Lean.Meta.Tactic.Simp.BuiltinSimprocs.List
-public import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Core
-
+import Lean.Meta.Tactic.Grind.Simp
+import Lean.Meta.Tactic.Grind.MatchDiscrOnly
+import Lean.Meta.Tactic.Grind.MatchCond
+import Lean.Meta.Tactic.Grind.ForallProp
+import Lean.Meta.Tactic.Grind.Arith.Simproc
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs.List
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Core
+import Lean.Meta.Tactic.Grind.Util
+import Init.Grind.Norm
 public section
-
 namespace Lean.Meta.Grind
 
 builtin_initialize normExt : SimpExtension ← mkSimpExt

src/Lean/Meta/Tactic/Grind/Split.lean

@@ -9,6 +9,7 @@ public import Lean.Meta.Tactic.Grind.Types
 public import Lean.Meta.Tactic.Grind.SearchM
 import Lean.Meta.Tactic.Grind.Intro
 import Lean.Meta.Tactic.Grind.Cases
+import Lean.Meta.Tactic.Grind.Util
 import Lean.Meta.Tactic.Grind.CasesMatch
 import Lean.Meta.Tactic.Grind.Internalize
 public section

src/Lean/Meta/Tactic/Grind/SynthInstance.lean

@@ -5,8 +5,8 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Lean.Meta.SynthInstance
 public import Lean.Meta.Tactic.Grind.Types
+import Lean.Meta.SynthInstance
 public section
 namespace Lean.Meta.Grind
 /--

src/Lean/Meta/Tactic/Grind/Types.lean

@@ -5,19 +5,20 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Init.Grind.Tactics
-public import Init.Data.Queue
-public import Std.Data.TreeSet.Basic
-public import Lean.HeadIndex
+public import Lean.Meta.Tactic.Grind.EMatchTheorem
 public import Lean.Meta.Tactic.Simp.Types
-public import Lean.Meta.Tactic.Grind.ExprPtr
 public import Lean.Meta.Tactic.Grind.AlphaShareCommon
 public import Lean.Meta.Tactic.Grind.Attr
-public import Lean.Meta.Tactic.Grind.ExtAttr
-public import Lean.Meta.Tactic.Grind.EMatchTheorem
-meta import Lean.Parser.Do
+public import Init.Data.Queue
+import Lean.Meta.Tactic.Grind.ExprPtr
+import Init.Grind.Tactics
+import Std.Data.TreeSet.Basic
+import Lean.HeadIndex
+import Lean.Meta.Tactic.Grind.ExtAttr
+import Lean.Meta.AbstractNestedProofs
 import Lean.Meta.Match.MatchEqsExt
 import Lean.PrettyPrinter
+meta import Lean.Parser.Do
 public section
 namespace Lean.Meta.Grind
 

src/Lean/Meta/Tactic/Grind/Util.lean

@@ -4,18 +4,16 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
-public import Init.Simproc
-public import Init.Grind.Tactics
-public import Lean.Meta.AbstractNestedProofs
+public import Lean.Meta.Basic
 public import Lean.Meta.Transform
-public import Lean.Meta.Tactic.Util
-public import Lean.Meta.Tactic.Clear
 public import Lean.Meta.Tactic.Simp.Simproc
-
+import Init.Simproc
+import Init.Grind.Tactics
+import Lean.Meta.AbstractNestedProofs
+import Lean.Meta.Tactic.Util
+import Lean.Meta.Tactic.Clear
 public section
-
 namespace Lean.Meta.Grind
 /--
 Throws an exception if target of the given goal contains metavariables.

src/Lean/Meta/Tactic/Grind/VarRename.lean

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Init.Prelude
 public import Init.Data.Array.QSort
 public import Std.Data.HashSet
 public section

src/Lean/Meta/Tactic/Try/Collect.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Init.Try
 public import Lean.Meta.Tactic.LibrarySearch
@@ -13,9 +12,8 @@ public import Lean.Meta.Tactic.Grind.Cases
 public import Lean.Meta.Tactic.Grind.EMatchTheorem
 public import Lean.Meta.Tactic.FunIndInfo
 public import Lean.Meta.Tactic.FunIndCollect
-
+import Lean.Meta.Eqns
 public section
-
 namespace Lean.Meta.Try.Collector
 
 structure InductionCandidate where