diff --git a/src/Lean/Meta/Tactic/Grind/AC/Internalize.lean b/src/Lean/Meta/Tactic/Grind/AC/Internalize.lean
index a890237b83..d3f0bf85f3 100644
--- a/src/Lean/Meta/Tactic/Grind/AC/Internalize.lean
+++ b/src/Lean/Meta/Tactic/Grind/AC/Internalize.lean
@@ -15,7 +15,8 @@ private def isParentSameOpApp (parent? : Option Expr) (op : Expr) : GoalM Bool :
   unless e.isApp && e.appFn!.isApp do return false
   return isSameExpr e.appFn!.appFn! op
 
-def internalize (e : Expr) (parent? : Option Expr) : GoalM Unit := do
+@[export lean_grind_ac_internalize]
+def internalizeImpl (e : Expr) (parent? : Option Expr) : GoalM Unit := do
   unless (← getConfig).ac do return ()
   unless e.isApp && e.appFn!.isApp do return ()
   let op := e.appFn!.appFn!
diff --git a/src/Lean/Meta/Tactic/Grind/Arith.lean b/src/Lean/Meta/Tactic/Grind/Arith.lean
index ee1c2b36e2..cd53e9321b 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith.lean
@@ -16,5 +16,6 @@ public import Lean.Meta.Tactic.Grind.Arith.CommRing
 public import Lean.Meta.Tactic.Grind.Arith.Linear
 public import Lean.Meta.Tactic.Grind.Arith.Simproc
 public import Lean.Meta.Tactic.Grind.Arith.VarRename
+public import Lean.Meta.Tactic.Grind.Arith.Internalize
 
 public section
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Internalize.lean b/src/Lean/Meta/Tactic/Grind/Arith/Internalize.lean
index 233af5862d..5f1e865ca5 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Internalize.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Internalize.lean
@@ -15,7 +15,8 @@ public section
 
 namespace Lean.Meta.Grind.Arith
 
-def internalize (e : Expr) (parent? : Option Expr) : GoalM Unit := do
+@[export lean_grind_arith_internalize]
+def internalizeImpl (e : Expr) (parent? : Option Expr) : GoalM Unit := do
   Offset.internalize e parent?
   Cutsat.internalize e parent?
   CommRing.internalize e parent?
diff --git a/src/Lean/Meta/Tactic/Grind/EMatch.lean b/src/Lean/Meta/Tactic/Grind/EMatch.lean
index 5ec9f063d9..a545409d65 100644
--- a/src/Lean/Meta/Tactic/Grind/EMatch.lean
+++ b/src/Lean/Meta/Tactic/Grind/EMatch.lean
@@ -6,9 +6,6 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Types
-import Lean.Meta.Tactic.Grind.Intro
-import Lean.Meta.Tactic.Grind.MatchDiscrOnly
-import Lean.Meta.Tactic.Grind.MatchCond
 import Lean.Meta.Tactic.Grind.Core
 public section
 namespace Lean.Meta.Grind
diff --git a/src/Lean/Meta/Tactic/Grind/Internalize.lean b/src/Lean/Meta/Tactic/Grind/Internalize.lean
index db3d394a4d..1ed9ad12a6 100644
--- a/src/Lean/Meta/Tactic/Grind/Internalize.lean
+++ b/src/Lean/Meta/Tactic/Grind/Internalize.lean
@@ -17,12 +17,16 @@ public import Lean.Meta.Tactic.Grind.Types
 public import Lean.Meta.Tactic.Grind.Util
 public import Lean.Meta.Tactic.Grind.Beta
 public import Lean.Meta.Tactic.Grind.MatchCond
-public import Lean.Meta.Tactic.Grind.Arith.Internalize
-public import Lean.Meta.Tactic.Grind.AC.Internalize
 
 public section
 
 namespace Lean.Meta.Grind
+
+@[extern "lean_grind_ac_internalize"] -- forward definition
+opaque AC.internalize (e : Expr) (parent? : Option Expr) : GoalM Unit
+@[extern "lean_grind_arith_internalize"] -- forward definition
+opaque Arith.internalize (e : Expr) (parent? : Option Expr) : GoalM Unit
+
 /-- Adds `e` to congruence table. -/
 def addCongrTable (e : Expr) : GoalM Unit := do
   if let some { e := e' } := (← get).congrTable.find? { e } then
diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean
index bf47b03e84..7c99f2ef94 100644
--- a/src/Lean/Meta/Tactic/Grind/Types.lean
+++ b/src/Lean/Meta/Tactic/Grind/Types.lean
@@ -10,17 +10,11 @@ public import Init.Grind.Tactics
 public import Init.Data.Queue
 public import Std.Data.TreeSet.Basic
 public import Lean.HeadIndex
-public import Lean.Meta.Basic
-public import Lean.Meta.CongrTheorems
-public import Lean.Meta.AbstractNestedProofs
 public import Lean.Meta.Tactic.Simp.Types
-public import Lean.Meta.Tactic.Util
-public import Lean.Meta.Tactic.Ext
 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.Cases
 public import Lean.Meta.Tactic.Grind.Arith.Types
 public import Lean.Meta.Tactic.Grind.AC.Types
 public import Lean.Meta.Tactic.Grind.EMatchTheorem