Quick style PRs

Stream: PR reviews

[Winston Yin (尹維晨)]

Two easy-to-review PRs for style:

• #8776 removes some namespace prefixes such as Set., Function., Filter, LocalHomeomorph when the namespace is already opened. E.g. Set.univ to univ. Edit: I went overboard!
• #8780 reorganises the variables in SmoothManifoldWithCorners to remove clutter.

Also #8702 (WIP) removes a bunch of explicit @foo _ _ _ _ in favour of Lean4's named arguments foo (x := y). I'd like to know what people think about this. I think it improves readability, reduces brittleness of code when argument order changes, and sets an example of the style of Lean4.

[Yaël Dillies]

Reviewed #8702