From 2dce18655dcc23c1d146d5edd8dd888e24fca25b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Wed, 23 Jul 2025 10:34:44 -0700
Subject: [PATCH] fix: incorrect proof term in `grind linarith` (#9487)

This PR fixes an incorrect proof term constructed by `grind linarith`,
as reported in #9485.

closes #9485
---
 .../Grind/Arith/Linear/PropagateEq.lean       |  2 +-
 tests/lean/run/grind_9485.lean                | 32 +++++++++++++++++++
 2 files changed, 33 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/grind_9485.lean

diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Linear/PropagateEq.lean b/src/Lean/Meta/Tactic/Grind/Arith/Linear/PropagateEq.lean
index 12e951b215..6a8c7ea553 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/PropagateEq.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/PropagateEq.lean
@@ -19,7 +19,7 @@ namespace Lean.Meta.Grind.Arith.Linear
 private def _root_.Lean.Grind.Linarith.Poly.substVar (p : Poly) : LinearM (Option (Var × EqCnstr × Poly)) := do
   let some (a, x, c) ← p.findVarToSubst | return none
   let b := c.p.coeff x
-  let p' := p.mul (-b) |>.combine (c.p.mul a)
+  let p' := p.mul b |>.combine (c.p.mul (-a))
   trace[grind.debug.linarith.subst] "{← p.denoteExpr}, {a}, {← getVar x}, {← c.denoteExpr}, {b}, {← p'.denoteExpr}"
   return some (x, c, p')
 
diff --git a/tests/lean/run/grind_9485.lean b/tests/lean/run/grind_9485.lean
new file mode 100644
index 0000000000..bc392e1a9f
--- /dev/null
+++ b/tests/lean/run/grind_9485.lean
@@ -0,0 +1,32 @@
+variable (G : Type)
+
+structure G' where p : G
+
+@[ext, grind ext]
+theorem ext_ {f g : G' G} (h : f.p = g.p) : f = g := by
+  cases f
+  subst h
+  rfl
+
+variable [Lean.Grind.IntModule G]
+
+instance : Add (G' G) where add f g := ⟨f.p + g.p⟩
+@[grind] theorem add_p (f g : G' G) : (f + g).p = f.p + g.p := rfl
+
+instance : Zero (G' G) where zero := ⟨0⟩
+@[grind] theorem zero_p : (0 : G' G).p = 0 := rfl
+
+instance : Neg (G' G) where neg x := ⟨-x.p⟩
+@[grind] theorem neg_p (f : G' G) : (-f).p = -(f.p) := rfl
+
+example (f g h : G' G) :
+    f + g + h = f + (g + h) := by
+  grind -- should work without extra options
+
+example (f g h : G' G) :
+    f + g + h = f + (g + h) := by
+  grind [Lean.Grind.AddCommMonoid.add_assoc] -- should work too
+
+example (f g h : G' G) :
+    f + g + h = f + (g + h) := by
+  grind -linarith [Lean.Grind.AddCommMonoid.add_assoc] -- should work too