Commits at f13dc69cc9e52b62c0a5056f434ddf7eb196685f

1. f13dc69c Don't need to abbrev when already @[simp]ed Anthony Wang authored at 2026-01-12 21:27:44 -0600 Anthony Wang comitted at 2026-01-12 21:27:44 -0600
2. 42eb7d85 Completely vibecoded solution, better golf, enlightened sort, make grind default tactic for SortedRange Anthony Wang authored at 2026-01-12 21:21:27 -0600 Anthony Wang comitted at 2026-01-12 21:21:27 -0600
3. f089fdc9 Don't need the names of invariant cases Anthony Wang authored at 2026-01-12 17:39:52 -0600 Anthony Wang comitted at 2026-01-12 17:39:52 -0600
4. 9ebe5846 Oh how could I forget about native_decide Anthony Wang authored at 2026-01-12 16:50:41 -0600 Anthony Wang comitted at 2026-01-12 16:50:41 -0600
5. a4b7906e Nuke README Anthony Wang authored at 2026-01-12 16:41:03 -0600 Anthony Wang comitted at 2026-01-12 16:41:03 -0600
6. 40e05cc5 Note that AristotleLemmas section is AI-generated Anthony Wang authored at 2026-01-12 16:36:11 -0600 Anthony Wang comitted at 2026-01-12 16:36:11 -0600
7. 7baa176d More consistency Anthony Wang authored at 2026-01-12 16:28:21 -0600 Anthony Wang comitted at 2026-01-12 16:28:21 -0600
8. ae0439d7 It's not that long... Anthony Wang authored at 2026-01-12 16:27:50 -0600 Anthony Wang comitted at 2026-01-12 16:27:50 -0600
9. b79c2fa7 Finished! Anthony Wang authored at 2026-01-12 16:17:30 -0600 Anthony Wang comitted at 2026-01-12 16:17:30 -0600
10. 9eaa66e2 Initial commit Anthony Wang authored at 2026-01-11 17:04:34 -0600 Anthony Wang comitted at 2026-01-11 17:04:34 -0600