Delaboration of re-exported names

[hargoniX]

Description

Delaborating things that contain names of re-exported types can chose the wrong name for the type.
This most notably causes incorrect doc-gen4 renders: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Confusing.20delaboration.20in.20.20doc-gen/near/388158478

Steps to Reproduce

Delaboration of Lake.Name:

import Lean
import Lake

#eval show Lean.MetaM _ from do
  let ⟨fmt, _⟩ ← Lean.PrettyPrinter.ppExprWithInfos (Lean.mkConst ``Lean.Name)
  println! fmt

Further minified:

import Lean
import Lake

open Lean
#eval show MetaM _ from do
  unresolveNameGlobal ``Name

Expected behavior: We get Lean.Name

Actual behavior: We get Lake.Name

Reproduces how often: Always

[Kha]

@tydeu Let's just turn these into abbrevs? I'm not sure export is the right tool here. One of these names will always be printed as the other with it.

[tydeu]

@Kha Printing it always as Lean.Name would be what I would expect here (i.e., for the original name to be the canonical name rather than the alias). With Lake.Name, I am not trying to create a distinct type, but just have Lean.Name available when I open Lake. But it is certainly possible I misunderstand the proper use of export.

[kmill]

I have two competing solutions to this problem:

1. Change Lake. fix: have Lake not create core aliases into Lake namespace #5688 removes the exports and adds the relevant open commands.
2. Change pretty printing. fix: when pretty printing constant names, do not use aliases from "non-API exports" #5689 makes pretty printing only consider aliases into parent namespaces.

I'd prefer option 1 if @tydeu would be ok with it (and if it wouldn't cause problems for lakefiles), but otherwise I'll leave it to @Kha and the triage team to decide which of these two solutions (if either) might be acceptable.

There's a third option, which is to implement a scoped open command, which would have the effect that Mac wants but which wouldn't create global aliases into the Lake namespace.

[tydeu]

@kmill I am fine with a temporary stop-gap measure, but I would very much want this fixed in the future. Having to manually open common names is cumbersome. Furthermore, forgetting to do so can also lead to confusing problems with auto-implicits. Fortunately, your scoped open idea sounds like great solution!