fix: move Lean.List.toSMap to List.toSMap

[digama0]

This definition was clearly meant to be in the List namespace, but it is also in a namespace Lean so it ended up as Lean.List.toSMap instead of List.toSMap. It would be nice if #3031 made this unnecessary, but for now this seems to be the convention.

I noticed this because of another side effect: it defines Lean.List as a namespace, which means that

import Std

namespace Lean
open List

#check [1] <+ [2]

does not work as expected, it opens the Lean.List namespace instead of the List namespace. Should there be a regression test to ensure that the Lean.List namespace (and maybe others) are not accidentally created? (Unfortunately this puts a bit of a damper on #3031.)

[leanprover-community-mathlib4-bot]

• ❗ Mathlib CI will not be attempted unless you rebase your PR onto the 'nightly' branch. (2023-12-06 13:54:05)

[kim-em]

This needs to be rebased onto something more recent (e.g. nightly), so that the new CI requirements for the merge queue run.