fix: bump numInstances for delayed grind theorem instances (#12176)

This PR fixes a bug where delayed E-match theorem instances could cause
uniqueId collisions in the instance tracking map.

The `uniqueId` for theorem instances is generated using `numInstances`,
but this counter was only bumped for immediately activated instances
(`.ready` case), not for delayed instances (`.next` case). This caused
ID collisions:

1. Theorem A matches, becomes delayed, gets `uniqueId = N`
2. Counter isn't bumped (stays at N)
3. Theorem B matches next, gets `uniqueId = N` (same!)
4. B's entry overwrites A's entry in `instanceMap`
5. A's tracking is lost

This manifested as `grind?` and `finish?` producing `instantiate approx`
(meaning "we couldn't determine which theorems to use") instead of
proper `instantiate only [...]` with specific theorem lists.

The fix bumps `numInstances` for delayed instances too, ensuring each
theorem instance gets a truly unique ID.

🤖 Prepared with Claude Code

Co-authored-by: Claude <noreply@anthropic.com>

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

@@ -1679,6 +1679,9 @@ def addTheoremInstance (thm : EMatchTheorem) (proof : Expr) (prop : Expr) (gener
     modify fun s => { s with
       ematch.delayedThmInsts := s.ematch.delayedThmInsts.insert { expr := guard } thms
       ematch.numDelayedInstances := s.ematch.numDelayedInstances + 1
+      -- Bump numInstances for delayed instances too, so that uniqueId generation
+      -- in EMatch.instantiateTheorem' doesn't produce collisions.
+      ematch.numInstances := s.ematch.numInstances + 1
     }
 
 def DelayedTheoremInstance.check (delayed : DelayedTheoremInstance) : GoalM Unit := do

tests/lean/run/grind_indexmap_trace.lean

@@ -251,7 +251,7 @@ info: Try these:
       · instantiate only
         instantiate only [size, = HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push]
     · instantiate only [= mem_indices_of_mem, = getElem_def]
-      instantiate only [usr getElem_indices_lt, usr Array.eq_empty_of_size_eq_zero]
+      instantiate only [usr getElem_indices_lt]
       instantiate only [size]
       cases #ffdf
       · instantiate only [usr getElem_indices_lt, =_ WF]
@@ -260,8 +260,8 @@ info: Try these:
       · instantiate only
         instantiate only [= HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push]
   [apply] finish only [= mem_indices_of_mem, insert, = getElem_def, = getElem?_neg, = getElem?_pos, = Array.getElem_set,
-    size, = HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push, usr getElem_indices_lt,
-    usr Array.eq_empty_of_size_eq_zero, =_ WF, = Array.size_set, WF', #f590, #ffdf]
+    size, = HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push, usr getElem_indices_lt, =_ WF,
+    = Array.size_set, WF', #f590, #ffdf]
 -/
 #guard_msgs in
 example (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) :
@@ -294,11 +294,11 @@ example (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) :
 /--
 info: Try these:
   [apply] grind only [= mem_indices_of_mem, insert, = getElem_def, = getElem?_neg, = getElem?_pos, = Array.getElem_set,
-    size, = HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push, usr getElem_indices_lt,
-    usr Array.eq_empty_of_size_eq_zero, =_ WF, = Array.size_set, WF', #f590, #ffdf]
+    size, = HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push, usr getElem_indices_lt, =_ WF,
+    = Array.size_set, WF', #f590, #ffdf]
   [apply] grind only [= mem_indices_of_mem, insert, = getElem_def, = getElem?_neg, = getElem?_pos, = Array.getElem_set,
-    size, = HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push, usr getElem_indices_lt,
-    usr Array.eq_empty_of_size_eq_zero, =_ WF, = Array.size_set, WF']
+    size, = HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push, usr getElem_indices_lt, =_ WF,
+    = Array.size_set, WF']
   [apply] grind =>
     instantiate only [= mem_indices_of_mem, insert, = getElem_def]
     instantiate only [= getElem?_neg, = getElem?_pos]
@@ -309,7 +309,7 @@ info: Try these:
       · instantiate only
         instantiate only [size, = HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push]
     · instantiate only [= mem_indices_of_mem, = getElem_def]
-      instantiate only [usr getElem_indices_lt, usr Array.eq_empty_of_size_eq_zero]
+      instantiate only [usr getElem_indices_lt]
       instantiate only [size]
       cases #ffdf
       · instantiate only [usr getElem_indices_lt, =_ WF]
@@ -357,7 +357,6 @@ info: Try these:
   [apply] ⏎
     instantiate only [findIdx, insert, = mem_indices_of_mem]
     instantiate only [= getElem?_neg, = getElem?_pos]
-    instantiate approx
     cases #1bba
     · instantiate only [findIdx]
     · instantiate only
@@ -380,7 +379,6 @@ info: Try these:
   [apply] grind =>
     instantiate only [findIdx, insert, = mem_indices_of_mem]
     instantiate only [= getElem?_neg, = getElem?_pos]
-    instantiate approx
     cases #1bba
     · instantiate only [findIdx]
     · instantiate only