Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-22 13:16 bee8d4ac

View on Github →

chore(order/filter/basic): golf a proof (#9874)

Estimated changes