From e9844738862fdc474bccd9bf69a79e695a1663aa Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Mon, 19 May 2025 21:46:23 -0400
Subject: [PATCH] fix: `markNestedProofs` preprocessor in `grind` (#8412)

This PR fixes the `markNestedProofs` preprocessor used in `grind`. There
was a missing case (e.g., `Expr.mdata`)
---
 src/Lean/Meta/Tactic/Grind/MarkNestedProofs.lean | 4 +++-
 tests/lean/run/grind_mark_nested_proofs_bug.lean | 6 ++++++
 2 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Meta/Tactic/Grind/MarkNestedProofs.lean b/src/Lean/Meta/Tactic/Grind/MarkNestedProofs.lean
index e074ab15b9..b9a9fe42a1 100644
--- a/src/Lean/Meta/Tactic/Grind/MarkNestedProofs.lean
+++ b/src/Lean/Meta/Tactic/Grind/MarkNestedProofs.lean
@@ -47,7 +47,7 @@ where
       return e'
     -- Remark: we have to process `Expr.proj` since we only
     -- fold projections later during term internalization
-    unless e.isApp || e.isForall || e.isProj do
+    unless e.isApp || e.isForall || e.isProj || e.isMData do
       return e
     -- Check whether it is cached
     if let some r := (← get).find? e then
@@ -68,6 +68,8 @@ where
           pure e
       | .proj _ _ b =>
         pure <| e.updateProj! (← visit b)
+      | .mdata _ b =>
+        pure <| e.updateMData! (← visit b)
       | .forallE _ d b _ =>
         -- Recall that we have `ForallProp.lean`.
         let d' ← visit d
diff --git a/tests/lean/run/grind_mark_nested_proofs_bug.lean b/tests/lean/run/grind_mark_nested_proofs_bug.lean
index adc145d25e..cbaef54291 100644
--- a/tests/lean/run/grind_mark_nested_proofs_bug.lean
+++ b/tests/lean/run/grind_mark_nested_proofs_bug.lean
@@ -26,3 +26,9 @@ example (as bs cs : Array α) (v : α)
         (h₆ : j < as.size)
         : cs[j] = as[j] := by
   grind only [= Array.getElem_set_ne_abstracted, = Array.size_set] -- should work
+
+opaque p : (i : Nat) → i ≠ 10 → Prop
+
+example (h : ∀ i, (¬i > 0) ∨ ∀ h : i ≠ 10, p i h) : p 5 (by decide) := by
+  have := h 5; clear h
+  grind