mathlib3

refactor(order/filter/basic): redefine `filter.pure`

#1889

Merged