fix: missing foldProjs

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

@@ -115,7 +115,7 @@ private def pushCastHEqs (e : Expr) : GoalM Unit := do
   | _ => return ()
 
 private def preprocessGroundPattern (e : Expr) : GoalM Expr := do
-  shareCommon (← canon (← normalizeLevels (← eraseIrrelevantMData (← unfoldReducible e))))
+  shareCommon (← canon (← normalizeLevels (← foldProjs (← eraseIrrelevantMData (← unfoldReducible e)))))
 
 private def mkENode' (e : Expr) (generation : Nat) : GoalM Unit :=
   mkENodeCore e (ctor := false) (interpreted := false) (generation := generation)

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

@@ -32,6 +32,8 @@ where
       let prop ← unfoldReducible prop
       /- We must also apply beta-reduction to improve the effectiveness of the congruence closure procedure. -/
       let prop ← Core.betaReduce prop
+      /- We must fold kernel projections like it is done in the preprocessor. -/
+      let prop ← foldProjs prop
       /- We must mask proofs occurring in `prop` too. -/
       let prop ← visit prop
       let e' := mkApp2 (mkConst ``Lean.Grind.nestedProof) prop e