From fd4ff1f7e2d0092233bbb33faa0c5104c762adbd Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Sat, 22 Nov 2025 13:19:00 +1100
Subject: [PATCH] feat: `grind_pattern` for `Exists.choose_spec` (#11316)

This PR adds `grind_pattern Exists.choose_spec => P.choose`.
---
 src/Init/Classical.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/Init/Classical.lean b/src/Init/Classical.lean
index 5a403ba54d..366d29b6ec 100644
--- a/src/Init/Classical.lean
+++ b/src/Init/Classical.lean
@@ -205,3 +205,5 @@ export Classical (imp_iff_right_iff imp_and_neg_imp_iff and_or_imp not_imp)
 
 /-- Show that an element extracted from `P : ∃ a, p a` using `P.choose` satisfies `p`. -/
 theorem Exists.choose_spec {p : α → Prop} (P : ∃ a, p a) : p P.choose := Classical.choose_spec P
+
+grind_pattern Exists.choose_spec => P.choose