grind_pattern ドキュメントに _ ワイルドカード必須の利用例を追加

LeanByExample/Declarative/GrindPattern.lean

@@ -17,6 +17,33 @@ example (x y z : Nat) (h₁ : R x y) (h₂ : R y z) : R x z := by
   -- grind で証明できる
   grind
 
+section
+
+  /-- `f 0` で始まる辺を右に 1 つ進められる -/
+  private opaque f : Nat → Nat
+  private axiom RfSucc {y : Nat} : R (f 0) y → R (f 0) (y + 1)
+
+  example (b : Nat) (h : R (f 0) b) : R (f 0) (b + 1) := by
+    fail_if_success grind
+    exact RfSucc h
+
+  /- `f` の引数位置に対応する変数は `RfSucc` の引数に存在しないため、
+  新しい変数名を置くことはできない。 -/
+  /-⋆-//--
+  error: Unknown identifier `z`
+  -/
+  #guard_msgs in --#
+  local grind_pattern RfSucc => R (f z) y
+
+  -- ここは定理の引数に現れない位置なので `_` が必要
+  -- （存在量化された位置を埋めたいときも同様）
+  local grind_pattern RfSucc => R (f _) y
+
+  example (b : Nat) (h : R (f 0) b) : R (f 0) (b + 1) := by
+    grind
+
+end
+
 /-
 ## `[grind]` 属性では登録できない例