From 9399b2ee36343a7f71d6fc236fee098733f061f9 Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Tue, 29 Jul 2025 11:36:53 +1000
Subject: [PATCH] chore: add failing grind test (#9607)

This PR adds a failing grind test.
---
 tests/lean/grind/algebra/linarith_cc.lean | 4 ++++
 1 file changed, 4 insertions(+)
 create mode 100644 tests/lean/grind/algebra/linarith_cc.lean

diff --git a/tests/lean/grind/algebra/linarith_cc.lean b/tests/lean/grind/algebra/linarith_cc.lean
new file mode 100644
index 0000000000..4a3e88bb0e
--- /dev/null
+++ b/tests/lean/grind/algebra/linarith_cc.lean
@@ -0,0 +1,4 @@
+-- This fails unless we manually substitute `hb`.
+-- `grind` doesn't recognise this as a linear arithmetic problem.
+example (a : Nat) (ha : a < 8) (b : Nat) (hb : b = 2) : a * b < 8 * b := by
+  grind -- fails