chore(order/filter/small_sets): redefine, golf (#13672)
chore(order/filter/small_sets): redefine, golf (#13672)

The new definition is defeq to the old one.





leanprover-community/mathlib,leanprover-community/mathlib