mathlib

d287d345 - refactor(order/filter/basic): define `filter.eventually_eq` (#3134)

refactor(order/filter/basic): define `filter.eventually_eq` (#3134) * Define `eventually_eq` (`f =^f[l] g`) and `eventually_le` (`f ≤^f[l] g`). * Use new notation and definitions in some files.