feat(topology/category/profinite): Initial work to show that profinite sets are limits of finite discrete sets

[callesonne]

Initial work to show that profinite sets are limits of finite discrete sets. Formalizes the diagram of discrete sets over which a given profinite set will be the limit, and shows that this profinite set gives a cone over the diagram.

---

This is the first of probably 3 PRs, the full formalization, although for now messy, can be found on the branch Profinite2.

• [x] depends on: #6219

[kim-em]

@callesonne, just checking if there's been any progress on this, if there are any blockers, or if you want help with it.

[callesonne]

@callesonne, just checking if there's been any progress on this, if there are any blockers, or if you want help with it.

No progress sadly, I was busy with other things for a bit. There are no blockers for this PR itself, but before I push the remaining PRs of the full proof I think that I need to rewrite the old implementation of limits in Profinite to use the fact that its reflective in Top. I plan to do that this weekend hopefully, and after that I can work on this PR again.

[github-actions[bot]]

This PR/issue depends on:

• ~~leanprover-community/mathlib#6219~~ By Dependent Issues (🤖). Happy coding!