feat: second countable finite-dimensional manifolds are sigma-compact

[grunweg]

This uses their local compactness, in particular also requires them to be modelled on a locally compact field.

• part of the road towards Sard's theorem
• depends on: [Merged by Bors] - feat: finite-dimensional manifolds are locally compact #7822

---

Likewise, I'm open moving this result to a new file about topological properties of (topological or smooth) manifolds.

[digama0]

Note: I have pushed an update to the lean toolchain because this PR was on a buggy version of the toolchain. WARNING: checking out old commits of this PR using v4.2.0-rc2 or v4.2.0-rc3 can cause lake clean to delete your mathlib folder! If you need to do so, make sure to delete lakefile.olean manually before running any lake commands.

[ghost]

This PR/issue depends on:

• [Merged by Bors] - feat: finite-dimensional manifolds are locally compact #7822
  By Dependent Issues (🤖). Happy coding!

[sgouezel]

I am not convinced this PR is really useful: you can not declare this as an instance as the field k and the model space E can not be guessed by the system by just looking at M, so you would need to invoke the theorem by hand. But at this point you might as well just invoke by hand the theorem that says that M is locally compact (which you have proved in a previous PR), and then typeclass inference will automatically kick in and provide for you the information that M is sigma-compact.

Do you have a use case where you think that the theorem in this PR would be more useful? Maybe I have overlooked some possible application.

[grunweg]

Makes sense! I'm still grappling with the typeclass system - I agree that in given this, this doesn't make sense.

I've checked: for the use case I have in mind (Sard's theorem), invoking local compactness is sufficient. Thanks for the careful look!