From c0d67e2a65ba1386cfea286bd03ceeae0a3d81f3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Thu, 2 Jan 2025 03:14:45 +0100
Subject: [PATCH] fix: bug in `markNestedProofs` within `grind` (#6500)

This PR fixes a bug in the `markNestedProofs` used in `grind`. See new
test.
---
 src/Lean/Meta/Tactic/Grind/MarkNestedProofs.lean | 6 +++---
 tests/lean/run/grind_nested_proof_issue.lean     | 6 ++++++
 2 files changed, 9 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/run/grind_nested_proof_issue.lean

diff --git a/src/Lean/Meta/Tactic/Grind/MarkNestedProofs.lean b/src/Lean/Meta/Tactic/Grind/MarkNestedProofs.lean
index 600847671d02..485bd0a35c7d 100644
--- a/src/Lean/Meta/Tactic/Grind/MarkNestedProofs.lean
+++ b/src/Lean/Meta/Tactic/Grind/MarkNestedProofs.lean
@@ -28,9 +28,9 @@ where
       | .bvar .. => unreachable!
       -- See comments on `Canon.lean` for why we do not visit these cases.
       | .letE .. | .forallE .. | .lam ..
-      | .const .. | .lit .. | .mvar .. | .sort .. | .fvar ..
-      | .proj ..
-      | .mdata ..  => return e
+      | .const .. | .lit .. | .mvar .. | .sort .. | .fvar .. => return e
+      | .proj _ _ b => return e.updateProj! (← visit b)
+      | .mdata _ b  => return e.updateMData! (← visit b)
       -- We only visit applications
       | .app .. =>
         -- Check whether it is cached
diff --git a/tests/lean/run/grind_nested_proof_issue.lean b/tests/lean/run/grind_nested_proof_issue.lean
new file mode 100644
index 000000000000..de8b141fef3a
--- /dev/null
+++ b/tests/lean/run/grind_nested_proof_issue.lean
@@ -0,0 +1,6 @@
+example (as bs : Array α) (v : α)
+        (i : Nat)
+        (h₁ : i < as.size)
+        (h₂ : bs = as.set i v)
+        : (as.set i v).size = as.size → as.size = bs.size := by
+  grind