chore(MathlibTest/slow_instance): add test for Grind.OrderedAdd (leanprover-community#35667)

This PR adds a test to show that some instance search fails quickly.

Author: JovanGerb

MathlibTest/slow_instances.lean

@@ -26,3 +26,14 @@ Hint: Additional diagnostic information may be available using the `set_option d
 -/
 #guard_msgs in
 #synth NoZeroSMulDivisors ℕ K
+
+variable {d : Type*} in
+set_option maxHeartbeats 3000 in -- uses about 2400 as of 2026-02-20
+/--
+error: failed to synthesize
+  Lean.Grind.OrderedAdd (Submodule ℂ (WithLp 2 (d → ℂ)))
+
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+-/
+#guard_msgs in
+#synth Lean.Grind.OrderedAdd (Submodule ℂ (WithLp 2 (d → ℂ)))