fancy open/export options

[digama0]

open foo as bar (a b c) hiding d e renaming f->g

Lean 4 supports the (...) explicits, hiding and renaming each individually, but not in conjunction, and the as bar part is not supported at all. This is a relatively rare feature but we might run into it.

Lean 3 also supports export with the same syntax, while lean 4 has a much more restricted export grammar. But this is only used a small handful of times so it is probably not a concern.

[kim-em]

mathlib barely uses open ... as ...: only in the continued fractions development, and it's pretty easy to remove: https://github.com/leanprover-community/mathlib/pull/9847