fix: preprocessLight at ensureInternalized (#8466)

This PR fixes another instance of the `grind` issue "unexpected kernel
projection term during internalization".

Author: leodemoura

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

@@ -17,14 +17,6 @@ import Lean.Meta.Tactic.Grind.MatchCond
 import Lean.Meta.Tactic.Grind.Arith.Internalize
 
 namespace Lean.Meta.Grind
-
-/--
-A lighter version of `preprocess` which produces a definitionally equal term,
-but ensures assumptions made by `grind` are satisfied.
--/
-private def preprocessLight (e : Expr) : GoalM Expr := do
-  shareCommon (← canon (← normalizeLevels (← foldProjs (← eraseIrrelevantMData (← markNestedProofs (← unfoldReducible e))))))
-
 /-- Adds `e` to congruence table. -/
 def addCongrTable (e : Expr) : GoalM Unit := do
   if let some { e := e' } := (← get).congrTable.find? { e } then

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

@@ -8,6 +8,12 @@ import Lean.Meta.Tactic.Grind.Types
 import Lean.Meta.Tactic.Grind.Simp
 
 namespace Lean.Meta.Grind
+/--
+A lighter version of `preprocess` which produces a definitionally equal term,
+but ensures assumptions made by `grind` are satisfied.
+-/
+def preprocessLight (e : Expr) : GoalM Expr := do
+  shareCommon (← canon (← normalizeLevels (← foldProjs (← eraseIrrelevantMData (← markNestedProofs (← unfoldReducible e))))))
 
 /--
 If `e` has not been internalized yet, instantiate metavariables, unfold reducible, canonicalize,
@@ -24,7 +30,7 @@ private def ensureInternalized (e : Expr) : GoalM Expr := do
     `¬ a = []` and `b ≠ []` by congruence closure even when `a` and `b` are in the same
     equivalence class.
     -/
-    let e ← shareCommon (← canon (← unfoldReducible (← instantiateMVars e)))
+    let e ← preprocessLight (← instantiateMVars e)
     internalize e 0
     return e