fix: namespace completion to only use the short name#8350

mhuisi merged 5 commits intoleanprover:masterleanprover/lean4:masterfrom

Rob23oba:no-namespace-dupRob23oba/lean4:no-namespace-dupCopy head branch name to clipboard