chore: fix test

This PR fixes a panic when an invalid pattern is provided to `grind`.

closes #9899

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

@@ -706,7 +706,7 @@ private partial def go (pattern : Expr) (inSupport : Bool) (root : Bool) : M Exp
     else
       return mkOffsetPattern e k
   let some f ← getPatternFn? pattern inSupport root .relevant
-    | throwError "invalid pattern, (non-forbidden) application expected{indentExpr pattern}"
+    | throwError "invalid pattern, (non-forbidden) application expected{indentD (ppPattern pattern)}"
   assert! f.isConst || f.isFVar
   unless f.isConstOf ``Grind.eqBwdPattern do
     saveSymbol f.toHeadIndex

tests/lean/run/grind_9899.lean

@@ -0,0 +1,6 @@
+namespace List
+-- Should not panic
+#guard_msgs (drop error) in
+theorem countP_filterMap' {p : β → Bool} {f : α → Option β} {l : List α} :
+    countP p (filterMap f l) = countP (fun a => ((f a).map p).getD false) l := by
+  induction l with grind [=_ Option.getD_map]

tests/lean/run/grind_pattern1.lean

@@ -115,7 +115,7 @@ grind_pattern hThm1 => plus a c, plus a b
 
 /--
 error: invalid pattern, (non-forbidden) application expected
-  #4 ∧ #3
+  And #4 #3
 -/
 #guard_msgs (error) in
 grind_pattern And.imp_left => a ∧ b