Commit 2024-06-06 00:45 d75ac8f6

View on Github →

chore(Data/List/Lex): golf and generalize (#13546)

Estimated changes

Modified Mathlib/Data/List/Lex.lean

modified theorem List.head!_le_of_lt

modified theorem List.head_le_of_lt