fix: grind theorem activation

This PR fixes E-matching theorem activation in `grind`.

Fixes #9856

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

@@ -240,10 +240,10 @@ private def addMatchEqns (f : Expr) (generation : Nat) : GoalM Unit := do
 private def activateTheoremPatterns (fName : Name) (generation : Nat) : GoalM Unit := do
   if let some (thms, thmMap) := (← get).ematch.thmMap.retrieve? fName then
     modify fun s => { s with ematch.thmMap := thmMap }
-    let appMap := (← get).appMap
     for thm in thms do
       trace_goal[grind.debug.ematch.activate] "`{fName}` => `{thm.origin.key}`"
       unless (← get).ematch.thmMap.isErased thm.origin do
+        let appMap := (← get).appMap
         let symbols := thm.symbols.filter fun sym => !appMap.contains sym
         let thm := { thm with symbols }
         match symbols with

tests/lean/run/grind_9856.lean

@@ -0,0 +1,43 @@
+inductive T (a:Type) where
+  | constuctor1: T a
+  | constuctor2: T a
+
+instance : LE (T a) where
+  le := sorry
+
+axiom L: Type
+axiom L.pred (l1: L) (t: T α): Prop
+
+axiom L.pred_le (l1: L) (t1 t2: T α):
+  t1 ≤ t2 → l1.pred t1 → l1.pred t2
+grind_pattern L.pred_le => t1 ≤ t2, l1.pred t1
+
+abbrev T' := T Unit
+
+axiom l (t: T'): L
+
+-- l keeps the same value when t gets bigger
+axiom l_le (t1 t2: T'):
+  t1 ≤ t2 → l t1 = l t2
+grind_pattern l_le => t1 ≤ t2, l t1
+
+-- construction using l and L.pred
+abbrev pred (t: T'): Prop :=
+  (l t).pred t
+
+example: pred t1 → t1 ≤ t2 → pred t2 := by
+  grind
+
+example: t1 ≤ t2 → pred t1 → pred t2 := by
+  grind
+
+def is_mono (p: T' → Prop): Prop :=
+  ∀ t1 t2,
+    p t1 → t1 ≤ t2 → p t2
+
+example: is_mono pred := by
+  grind [is_mono]
+
+example: is_mono pred := by
+  unfold is_mono
+  grind