feat: grind_pattern for Exists.choose_spec

2026-04-04 11:14:09 +00:00 · 2025-11-22 11:17:25 +11:00
1 changed files with 2 additions and 0 deletions
--- 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