[Merged by Bors] - chore: golf using filter_upwards

[grunweg]

This is presumably not exhaustive, but covers about a hundred instances.

Style opinions (e.g., why a particular change is great/not a good idea) are very welcome; I'm still forming my own.

---

[loefflerd]

This PR is definitely an improvement but I saw a couple of points where it can be improved further using the filter_upwards [foo] with bar syntax. There might be more, so have a look for cases where Eventually.mp (or Eventually.and etc) is used just before a filter_upwards.

[grunweg]

Thanks for the hint: I pushed a few more golfs, including looking for occurrences of Eventually.{mp,and}.
awaiting-review

[loefflerd]

I've checked through all of these now. Most of them look great. I have, however, flagged up a few instances where I think you've been a bit trigger-happy. In particular, if eventually_of_forall or ae_of_all is one ingredient in a long compound proof term (as argument to refine or exact), using the filter_upwards tactic requires breaking this into two tactic calls, and in many cases the result is longer than the original (as well as being, I suspect, fractionally slower to compile).

[grunweg]

Thank you, all fixed. (Sorry for going overboard - I rather wanted you to tell me "this is not better" than the other way. Now I know.)
awaiting-review

[loefflerd]

This looks good now. There are surely further golfs that are possible; but this PR certainly is a substantial improvement on the existing code, and given that it touches rather a lot of files, it will rot quickly if we try to make it perfect.

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by loefflerd.

[fpvandoorn]

This looks good, thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style