From b0acdef43354de641ccbb275b185fdc4ae1d197b Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Mon, 7 Apr 2025 17:28:28 +1000
Subject: [PATCH] chore: a failing `grind` test about `Bool` equality (#7850)

---
 tests/lean/grind/bool.lean | 8 ++++++++
 1 file changed, 8 insertions(+)
 create mode 100644 tests/lean/grind/bool.lean

diff --git a/tests/lean/grind/bool.lean b/tests/lean/grind/bool.lean
new file mode 100644
index 0000000000..c7c9cac459
--- /dev/null
+++ b/tests/lean/grind/bool.lean
@@ -0,0 +1,8 @@
+reset_grind_attrs%
+
+example [BEq α] (a b : α) : (a == b && a == b) = (a == b) := by
+  rw [Bool.eq_iff_iff]
+  grind -- succeeds
+
+example [BEq α] (a b : α) : (a == b && a == b) = (a == b) := by
+  grind -- fails