From 5219ccd66f461b63ec1df196cc138e7423078bc4 Mon Sep 17 00:00:00 2001
From: Hillosanation <88579655+Hillosanation@users.noreply.github.com>
Date: Wed, 26 Aug 2026 14:04:29 +0800
Subject: [PATCH] doc: clarify wording in Annotation.lean

---
 Manual/Grind/Annotation.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Manual/Grind/Annotation.lean b/Manual/Grind/Annotation.lean
index f0727f2d7..77578ac07 100644
--- a/Manual/Grind/Annotation.lean
+++ b/Manual/Grind/Annotation.lean
@@ -148,6 +148,6 @@ grind_pattern sin_sq_add_cos_sq => sin x, cos x
 ```
 which will instantiate the theorem as soon as *both* {lean}`sin x` and {lean}`cos x` (with the same {lean}`x`) are encountered.
 This theorem will then automatically enter the Gröbner basis module, and be used to reason about polynomial expressions involving both {lean}`sin x` and {lean}`cos x`.
-One both alternatively, more aggressively, write two separate grind patterns so that this theorem instantiated when either {lean}`sin x` or {lean}`cos x` is encountered.
+Alternatively, one could more aggressively write two separate grind patterns so that this theorem will be instantiated when either {lean}`sin x` or {lean}`cos x` is encountered.
 :::
 ::::