Create a backbone of `Defs.lean` files

The import hierarchy in Mathlib is quite messy. A concrete issue we can focus on is that lot of files in Mathlib are structured around introducing a definition and then following up with a large collection of lemmas. This means that importing a definition often means also pulling in many unrelated definitions that interact with the intended result. Not only does this clustering make Mathlib slower to build after changes, it also means harder minimization of examples.

Ideally we'd maintain a stable "backbone" of Defs files, where each only contains definitions and the bare minimum of theory to get to the next level in the backbone. These could then be paired with Lemmas files that can be imported to get the full complement of results that would currently be imported alongside the defs.

Studying the import graph for a file can be a very useful tool in figuring out which bits of theory should be unnecessary for a definition.