From dcba6dfa7e0a44dbd0294ff0428d73802bd96ac9 Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Wed, 6 Aug 2025 19:31:09 +1000
Subject: [PATCH] chore: failing grind test cases for linarith on ordered
 fields (#9756)

---
 tests/lean/grind/algebra/linarith_field.lean | 14 ++++++++++++++
 1 file changed, 14 insertions(+)
 create mode 100644 tests/lean/grind/algebra/linarith_field.lean

diff --git a/tests/lean/grind/algebra/linarith_field.lean b/tests/lean/grind/algebra/linarith_field.lean
new file mode 100644
index 0000000000..1ca8e581d1
--- /dev/null
+++ b/tests/lean/grind/algebra/linarith_field.lean
@@ -0,0 +1,14 @@
+open Lean.Grind
+
+variable {α : Type} [Field α] [LinearOrder α] [OrderedRing α]
+
+example (a b : α) (h : a < b / 2) : 2 * a < b := by grind
+example (a b : α) (h : a < b / 2) : a + a < b := by grind
+example (a b : α) (h : a < b / 2) : 2 * a ≤ b := by grind
+example (a b : α) (h : a < b / 2) : a + a ≤ b := by grind
+example (a b : α) (h : a ≤ b / 2) : 2 * a ≤ b := by grind
+example (a b : α) (h : a ≤ b / 2) : a + a ≤ b := by grind
+
+example (a b : α) (_ : 0 ≤ a) (h : a ≤ b) : a / 7 ≤ b / 2 := by grind
+
+example (a b : α) (_ : b < 0) (h : a < b) : (3/2) * a < (5/4) * b := by grind