Moved definition and module docstring

Stream: mathlib4

[Patrick Massot]

It would be really nice if people moving definitions around could pay attention to updating module docstring, especially when they move a very important definition. For instance the module docstring of https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Compactness/Compact.html is now a lie.