chore: cleanup

Author: leodemoura

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

@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Meta.Tactic.Grind.Types
-import Lean.Meta.Tactic.Grind.Internalize
+import Lean.Meta.Tactic.Grind.Intro
 
 namespace Lean.Meta.Grind
 namespace EMatch
@@ -278,4 +278,15 @@ def ematch : GoalM Unit := do
       gmt          := s.gmt + 1
     }
 
+/-- Performs one round of E-matching, and assert new instances. -/
+def ematchAndAssert? (goal : Goal) : GrindM (Option (List Goal)) := do
+  let numInstances := goal.numInstances
+  let goal ← GoalM.run' goal ematch
+  if goal.numInstances == numInstances then
+    return none
+  assertAll goal
+
+def ematchStar (goal : Goal) : GrindM (List Goal) := do
+  iterate goal ematchAndAssert?
+
 end Lean.Meta.Grind

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

@@ -11,10 +11,9 @@ import Lean.Meta.Tactic.Grind.PropagatorAttr
 import Lean.Meta.Tactic.Grind.Proj
 import Lean.Meta.Tactic.Grind.ForallProp
 import Lean.Meta.Tactic.Grind.Util
-import Lean.Meta.Tactic.Grind.Simp
-import Lean.Meta.Tactic.Grind.PP
 import Lean.Meta.Tactic.Grind.Inv
 import Lean.Meta.Tactic.Grind.Intro
+import Lean.Meta.Tactic.Grind.EMatch
 
 namespace Lean.Meta.Grind
 
@@ -65,17 +64,6 @@ private def initCore (mvarId : MVarId) : GrindM (List Goal) := do
   goals.forM (·.checkInvariants (expensive := true))
   return goals.filter fun goal => !goal.inconsistent
 
-/-- Performs one round of E-matching, and assert new instances. -/
-def ematchAndAssert? (goal : Goal) : GrindM (Option (List Goal)) := do
-  let numInstances := goal.numInstances
-  let goal ← GoalM.run' goal ematch
-  if goal.numInstances == numInstances then
-    return none
-  assertAll goal
-
-def ematchStar (goal : Goal) : GrindM (List Goal) := do
-  iterate goal ematchAndAssert?
-
 def all (goals : List Goal) (f : Goal → GrindM (List Goal)) : GrindM (List Goal) := do
   goals.foldlM (init := []) fun acc goal => return acc ++ (← f goal)
 

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

@@ -10,10 +10,6 @@ import Lean.Meta.Tactic.Simp.Main
 import Lean.Meta.Tactic.Grind.Util
 import Lean.Meta.Tactic.Grind.Types
 import Lean.Meta.Tactic.Grind.MarkNestedProofs
-import Lean.Meta.Tactic.Grind.Cases
-import Lean.Meta.Tactic.Grind.Injection
-import Lean.Meta.Tactic.Grind.Core
-import Lean.Meta.Tactic.Grind.EMatch
 
 namespace Lean.Meta.Grind
 /-- Simplifies the given expression using the `grind` simprocs and normalization theorems. -/