From 5ca2ef1fe7cb53aaaae3f1ade392a6f2df390566 Mon Sep 17 00:00:00 2001
From: damiano <adomani@gmail.com>
Date: Tue, 1 Jul 2025 09:25:11 +0200
Subject: [PATCH] doc: swap sides of equality in grind

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

diff --git a/Manual/Grind.lean b/Manual/Grind.lean
index 309e714b9..91270bc3f 100644
--- a/Manual/Grind.lean
+++ b/Manual/Grind.lean
@@ -467,7 +467,7 @@ axiom q : Nat → Nat
 
 /-- info: h₁: [q #1] -/
 #guard_msgs (info) in
-@[grind? →] theorem h₁ (w : 7 = p (q x)) : p (x + 1) = q x := sorry
+@[grind? →] theorem h₁ (w : p (q x) = 7) : p (x + 1) = q x := sorry
 ```
 
 First, to understand the output we need to recall that the `#n` appearing in patterns are arguments of the theorem, numbered as de-Bruijn variables, i.e. in reverse order (so `#0` would be `w : p (q x) = 7`, while `#1` is the implicit argument `x`).