From 429e09cd8251a15bf5cc8e287f5393fa482d37bd Mon Sep 17 00:00:00 2001
From: Evan Chen <evan@evanchen.cc>
Date: Sun, 14 Dec 2025 12:12:47 -0800
Subject: [PATCH] doc: trivial typo in Grind/Attr.lean (#11676)

This PR fixes typo "the the custom pattern" -> "the custom pattern".
---
 src/Init/Grind/Attr.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Grind/Attr.lean b/src/Init/Grind/Attr.lean
index 6fed70b90a..0f2c0053c4 100644
--- a/src/Init/Grind/Attr.lean
+++ b/src/Init/Grind/Attr.lean
@@ -143,7 +143,7 @@ the `grind_pattern` command, which lets you specify how `grind` should
 match and use particular theorems.
 
 Example:
-- `grind [usr myThm]` means `grind` is using `myThm`, but with the
+- `grind [usr myThm]` means `grind` is using `myThm`, but with
   the custom pattern you defined with `grind_pattern`.
 -/
 syntax grindUsr    := &"usr"