fix: invalid namespace completions (#5322)

This PR fixes an issue reported a while ago at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60Monad.2Emap.60.20is.20a.20namespace.3F/near/425662846
where `Monad.map` was incorrectly reported by the autocompletion as a
namespace.

The underlying issue is that `Monad.map` contains an internal
declaration `_default`. This PR ensures that no namespaces are
registered that only contain internal declarations.

This also means that `open`ing namespaces that only contain internal
declarations will now fail.

The Mathlib adaption for this is a minor change where a declaration
(i.e. a namespace that only contains internal declarations) was `open`ed
by accident.

src/Lean/Environment.lean

@@ -1016,7 +1016,15 @@ private def registerNamePrefixes : Environment → Name → Environment
 
 @[export lean_environment_add]
 private def add (env : Environment) (cinfo : ConstantInfo) : Environment :=
-  let env := registerNamePrefixes env cinfo.name
+  let name := cinfo.name
+  let env := match name with
+    | .str _ s =>
+      if s.get 0 == '_' then
+        -- Do not register namespaces that only contain internal declarations.
+        env
+      else
+        registerNamePrefixes env name
+    | _ => env
   env.addAux cinfo
 
 @[export lean_display_stats]

tests/lean/stdio.lean

@@ -10,7 +10,7 @@ out.putStrLn "print stdout"
 let err ← IO.getStderr;
 (err.putStr "print stderr" : IO Unit)
 
-open usingIO IO
+open IO
 
 def test : IO Unit := do
 FS.withFile "stdout1.txt" IO.FS.Mode.write $ fun h₁ => do