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