diff --git a/tests/lean/grind/min.lean b/tests/lean/grind/min.lean
new file mode 100644
index 0000000000..de5794fb2c
--- /dev/null
+++ b/tests/lean/grind/min.lean
@@ -0,0 +1,4 @@
+example (as : Array α) (lo hi i j : Nat) (h₁ : lo ≤ i) (_ : i < j) (_ : j ≤ hi) (_ : j < as.size)
+    (_ : ¬as.size = 0) : min lo (as.size - 1) ≤ i := by
+  -- grind -- fails
+  omega