Filter.EventuallyEq and Sets

Stream: mathlib4

[Yury G. Kudryashov]

Back in Lean 3, I introduced a hack to use docs#Fitler.EventuallyEq and docs#Filter.EventuallyLE for sets, casting them to α → Prop behind the scenes. It caused issues back then, it causes issues today. E.g., s =ᶠ[l] ∅ fails without extra type annotation. Also, calc doesn't work with sets and EventuallyEq. Should we migrate to set-specific notation?

[Yury G. Kudryashov]

If yes, should we let it reduce to (· ∈ s) =ᶠ[l] (· t) and deal with possible @[simp]lifications for ∈, or introduce a new definition and repeat some API?

[Yaël Dillies]

I would like us to try the former before trying to repeat API

[Patrick Massot]

What are examples of statements you want to use this trick?

[Yaël Dillies]

docs#MeasureTheory.setAverage_congr is a good example

[Yury G. Kudryashov]

It's very useful in measure theory, where you can say that the sets are a.e. equal. In topology/analysis, you can say that s belongs to nhdsWithin x t or t is eventually less than s along nhds x, or write an inequality between nhdsWithin filters, and we don't have a normal form.