Basic topological properties of manifolds

Topological manifolds inherit properties from their model space, such as the following. Let $M$ be a topological manifold.

1. If $M$ is finite-dimensional, it is locally compact (if $M$ is modelled on e.g. the reals).
2. $M$ is locally connected.
3. $M$ is locally path-connected.
4. Deduce that $M$ is connected iff it is path-connected.
5. $M$ is locally simply connected.
6. $M$ is semi-locally simply connected.

Current status (December 2024):

• (1) is shown, and its converse also
• (3) is proven also, as are the implications (3) => (2) and step (4) --- both in general, specific lemmas for manifolds are not worth it
• (5) and (6) are not defined in mathlib yet; mathlib has simply connected spaces, though

Start by reviewing the existing manifold results for local compactness and local path-connectedness, then consult the linked PathConnected documentation and the SimplyConnectedSpace definition. Determine which listed properties remain formalized and whether the missing locally and semi-locally simply connected notions are available; done means the remaining applicable manifold properties are represented in mathlib.