From 8a8c67518e1d0c1be0634b5e43291e347ab05458 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Thu, 21 May 2026 01:19:26 +0000
Subject: [PATCH 1/5] Initial plan


From 6568e3da19f201085ecf7d35d5ceaeddfd3955ee Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Thu, 21 May 2026 01:32:59 +0000
Subject: [PATCH 2/5] docs: add grind_pattern wildcard example

Agent-Logs-Url: https://github.com/lean-ja/lean-by-example/sessions/3749ba0d-3ac0-4eaa-a246-c80b3b06a19e

Co-authored-by: Seasawher <47292598+Seasawher@users.noreply.github.com>
---
 LeanByExample/Declarative/GrindPattern.lean | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/LeanByExample/Declarative/GrindPattern.lean b/LeanByExample/Declarative/GrindPattern.lean
index 1daff63f..3a87e326 100644
--- a/LeanByExample/Declarative/GrindPattern.lean
+++ b/LeanByExample/Declarative/GrindPattern.lean
@@ -17,6 +17,22 @@ example (x y z : Nat) (h₁ : R x y) (h₂ : R y z) : R x z := by
   -- grind で証明できる
   grind
 
+section
+
+  /-- `R` でつながっている値を右に 1 つ進められる -/
+  local axiom Rsucc {x y : Nat} : R x y → R x (y + 1)
+
+  example (a b : Nat) (h : R a b) : R a (b + 1) := by
+    fail_if_success grind
+
+  -- `grind_pattern` のパターンでは `_` ワイルドカードを使える
+  local grind_pattern Rsucc => R _ y
+
+  example (a b : Nat) (h : R a b) : R a (b + 1) := by
+    grind
+
+end
+
 /-
 ## `[grind]` 属性では登録できない例
 

From df6b8bc298f081aa69a7e410742dc492c0cebb3e Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Thu, 21 May 2026 02:19:09 +0000
Subject: [PATCH 3/5] docs: add wildcard-required grind_pattern scenario

Agent-Logs-Url: https://github.com/lean-ja/lean-by-example/sessions/161765a1-01be-4465-be63-40d56967a3f6

Co-authored-by: Seasawher <47292598+Seasawher@users.noreply.github.com>
---
 LeanByExample/Declarative/GrindPattern.lean | 21 +++++++++++++++------
 1 file changed, 15 insertions(+), 6 deletions(-)

diff --git a/LeanByExample/Declarative/GrindPattern.lean b/LeanByExample/Declarative/GrindPattern.lean
index 3a87e326..fe13bfae 100644
--- a/LeanByExample/Declarative/GrindPattern.lean
+++ b/LeanByExample/Declarative/GrindPattern.lean
@@ -19,16 +19,25 @@ example (x y z : Nat) (h₁ : R x y) (h₂ : R y z) : R x z := by
 
 section
 
-  /-- `R` でつながっている値を右に 1 つ進められる -/
-  local axiom Rsucc {x y : Nat} : R x y → R x (y + 1)
+  /-- `f 0` で始まる辺を右に 1 つ進められる -/
+  local opaque f : Nat → Nat
+  local axiom RfSucc {y : Nat} : R (f 0) y → R (f 0) (y + 1)
 
-  example (a b : Nat) (h : R a b) : R a (b + 1) := by
+  example (b : Nat) (h : R (f 0) b) : R (f 0) (b + 1) := by
     fail_if_success grind
 
-  -- `grind_pattern` のパターンでは `_` ワイルドカードを使える
-  local grind_pattern Rsucc => R _ y
+  /- `f` の引数位置に対応する変数は `RfSucc` の引数に存在しないため、
+  新しい変数名を置くことはできない。 -/
+  /-⋆-//--
+  error: unknown identifier 'z'
+  -/
+  #guard_msgs in --#
+  local grind_pattern RfSucc => R (f z) y
 
-  example (a b : Nat) (h : R a b) : R a (b + 1) := by
+  -- この位置は `_` ワイルドカードでしか書けない
+  local grind_pattern RfSucc => R (f _) y
+
+  example (b : Nat) (h : R (f 0) b) : R (f 0) (b + 1) := by
     grind
 
 end

From f30f805a4ed5b1d2c464cba164e81af8c65f48cb Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Thu, 21 May 2026 02:35:00 +0000
Subject: [PATCH 4/5] docs: clarify wildcard usefulness in grind_pattern
 example

Agent-Logs-Url: https://github.com/lean-ja/lean-by-example/sessions/85c495d7-c534-4048-881e-329f2e911da5

Co-authored-by: Seasawher <47292598+Seasawher@users.noreply.github.com>
---
 LeanByExample/Declarative/GrindPattern.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/LeanByExample/Declarative/GrindPattern.lean b/LeanByExample/Declarative/GrindPattern.lean
index fe13bfae..fe3d878c 100644
--- a/LeanByExample/Declarative/GrindPattern.lean
+++ b/LeanByExample/Declarative/GrindPattern.lean
@@ -34,7 +34,8 @@ section
   #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

From 391372010c152dc6a72c74ad249301e1112a84c5 Mon Sep 17 00:00:00 2001
From: Seasawher <47292598+Seasawher@users.noreply.github.com>
Date: Mon, 25 May 2026 02:48:22 +0900
Subject: [PATCH 5/5] fix: make grind_pattern wildcard example compile

---
 LeanByExample/Declarative/GrindPattern.lean | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/LeanByExample/Declarative/GrindPattern.lean b/LeanByExample/Declarative/GrindPattern.lean
index fe3d878c..c8b0b40c 100644
--- a/LeanByExample/Declarative/GrindPattern.lean
+++ b/LeanByExample/Declarative/GrindPattern.lean
@@ -20,16 +20,17 @@ example (x y z : Nat) (h₁ : R x y) (h₂ : R y z) : R x z := by
 section
 
   /-- `f 0` で始まる辺を右に 1 つ進められる -/
-  local opaque f : Nat → Nat
-  local axiom RfSucc {y : Nat} : R (f 0) y → R (f 0) (y + 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'
+  error: Unknown identifier `z`
   -/
   #guard_msgs in --#
   local grind_pattern RfSucc => R (f z) y