mathlib

a2e76391 - feat(order/filter): more eventually/frequently API (#2330)

feat(order/filter): more eventually/frequently API (#2330) * feat(order/filter): more eventually/frequently API * Update after review * Add simp attribute * Update src/order/filter/basic.lean Co-Authored-By: Yury G. Kudryashov <urkud@urkud.name> * Update src/order/filter/basic.lean Co-Authored-By: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>