fix

Author: Rob23oba

src/Lean/Elab/Tactic/Grind.lean

@@ -33,8 +33,7 @@ def elabGrindPattern : CommandElab := fun stx => do
   | _ => throwUnsupportedSyntax
 where
   go (thmName : TSyntax `ident) (terms : Syntax.TSepArray `term ",") (kind : AttributeKind) : CommandElabM Unit := liftTermElabM do
-    let declName ← resolveGlobalConstNoOverload thmName
-    discard <| addTermInfo thmName (← mkConstWithLevelParams declName)
+    let declName ← realizeGlobalConstNoOverloadWithInfo thmName
     let info ← getConstVal declName
     forallTelescope info.type fun xs _ => do
       let patterns ← terms.getElems.mapM fun term => do

tests/lean/run/grind_10426.lean

@@ -0,0 +1,10 @@
+/-!
+# Test that `grind_pattern` causes realizations
+-/
+
+def f (n : Nat) : Prop := sorry
+def g (n : Nat) : Prop := sorry
+
+def fg (n : Nat) := f n ∧ g n
+
+grind_pattern fg.eq_def => fg n