RFC for the `export` command

Stream: mathlib4

[Kyle Miller]

(The discussion thread for RFC lean4#6394 is #lean4 > RFC: let `export` create namespace aliases @ 💬)

The proposed change has some affects on mathlib. With the change, export can create namespace aliases too. For example, since docs#HasSubset.Subset has an export HasSubset (Subset) and HasSubset.Subset is used as a namespace, then if you write Subset.trans it can now resolve to HasSubset.Subset.trans.

This is causing a small problem, where there are a number of instances where, with open Set, people would write Subset.trans and want it to resolve to Set.Subset.trans, but now it resolves to HasSubset.Subset.trans as well, causing an "ambiguous identifiers" error. The fixes are to write either Set.Subset.trans explicitly or to use subset_trans, which avoids the issue.

Arguably it's odd that Subset.trans ever worked since Set.Subset is protected; however, name resolution doesn't have a concept of a protected namespace.

Annoyingly, the ambiguity ought to be harmless, since both interpretations of Subset.trans give defeq elaboration results. Maybe it would be worth allowing ambiguity in this case? (That would be a separate RFC.)

[Kyle Miller]

Anyway, the purpose of this thread is to get some feedback, both for my mathlib fixes, commit 1 and commit 2 (whether my workarounds are acceptable; like whether Set.Subset.trans would be better than subset_trans for example), and to get a sense of whether we need to find better solutions to this problem (like the "ambiguity is OK if results are defeq" proposal, or maybe introducing protected namespaces).

[Kevin Buzzard]

Those commits look fine to me -- in fact I'd say that moving more towards dot notation is a strict improvement.

[Johan Commelin]

These diffs look perfectly fine to me! Thanks for these improvements!