mathlib3

chore(order/filter/n_ary): redefine, golf

#18258

Open