max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: grind_pattern for Exists.choose_spec (#11316)

Browse source 
This PR adds `grind_pattern Exists.choose_spec => P.choose`.
This commit is contained in:
Kim Morrison 2025-11-22 13:19:00 +11:00 • committed by GitHub
parent 80224c72c9
commit fd4ff1f7e2
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Classical.lean
View file

@ -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