fix: assigned universe metavars in grind (#11247)

This PR fixes an issue in the `grind` preprocessor. `simp` may introduce
assigned (universe) metavariables (e.g., when performing
zeta-reduction).

Author: leodemoura

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

@@ -335,8 +335,7 @@ private def processNewFactsImpl : GoalM Unit := do
       resetNewFacts
       return ()
     checkSystem "grind"
-    let some next := (← popNextFact?)
-      | return ()
+    let some next ← popNextFact? | return ()
     match next with
     | .eq lhs rhs proof isHEq => addEqStep lhs rhs proof isHEq
     | .fact prop proof gen => addFactStep prop proof gen

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

@@ -48,7 +48,12 @@ and then applies several other preprocessing steps.
 def preprocess (e : Expr) : GoalM Simp.Result := do
   let e ← instantiateMVars e
   let r ← simpCore e
-  let e' := r.expr
+  /-
+  **Note**: Some transformation performed by `simp` may introduce metavariables.
+  Example: zeta-reduction. Recall that `simp` does not necessarily visit every subterm.
+  In particular, it does not visit universe terms and does not instantiate them.
+  -/
+  let e' ← instantiateMVars r.expr
   -- Remark: `simpCore` unfolds reducible constants, but it does not consistently visit all possible subterms.
   -- So, we must use the following `unfoldReducible` step. It is non-op in most cases
   let e' ← unfoldReducible e'