Commit 2025-07-22 01:30 5eb29c48
View on Github →chore(List/TakeWhile): golf and move dropWhile_eq_self_iff (#27326)
Adds a lemma about dropWhile length, allowing dropWhile_eq_self_iff to be reproved and moved to a more appropriate file.
This lemma was found while doing work for Project Numina.