From edade0cea81c875effd71614c10d21ad0edb00a4 Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Tue, 29 Jul 2025 12:53:43 +1000
Subject: [PATCH] chore: add failing grind test about exponents (#9611)

---
 tests/lean/grind/algebra/exponents.lean | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/tests/lean/grind/algebra/exponents.lean b/tests/lean/grind/algebra/exponents.lean
index d6be041c02..26d25e15d4 100644
--- a/tests/lean/grind/algebra/exponents.lean
+++ b/tests/lean/grind/algebra/exponents.lean
@@ -13,6 +13,11 @@ example (n m : Nat) : (n+m)^2 = n^2 + 2*n*m + m^2 := by grind
 example (a : R) (n m : Nat) : a^((n+m)^2) = a^(n^2 + 2*n*m + m^2) := by grind
 example (a : R) (n m : Nat) : a^((n+m)^2) = a^(n^2) * a^(2*n*m) * a^(m^2) := by grind
 
+-- from Mathlib.NumberTheory.Multiplicity
+theorem pow_two_pow_sub_pow_two_pow.extracted_1_1 {x y : R} (d : Nat) :
+    x ^ 2 ^ (d + 1) - y ^ 2 ^ (d + 1) = (x ^ 2 ^ d + y ^ 2 ^ d) * (x ^ 2 ^ d - y ^ 2 ^ d) := by
+  grind
+
 end CommRing