mathlib

587b312e - refactor(order/filter/basic): redefine `filter.pure` (#1889)

refactor(order/filter/basic): redefine `filter.pure` (#1889) * refactor(order/filter/basic): redefine `filter.pure` New definition has `s ∈ pure a` definitionally equal to `a ∈ s`. * Update src/order/filter/basic.lean Co-Authored-By: Gabriel Ebner <gebner@gebner.org> * Minor fixes suggested by @gebner * Fix compile * Update src/order/filter/basic.lean Co-authored-by: Gabriel Ebner <gebner@gebner.org> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>