mathlib

dcb28262 - feat(order/filter/basic): add eventually_eq.(smul/const_smul/sup/inf) (#12101)