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