feat(Topology/Group/Profinite): Profinite group is limit of finite group

[Thmoas-Guan]

Prove that any profinite group is limit of finite groups.

---

• [ ] depends on: #16976
• [x] depends on: #16980
• [ ] depends on: #16991

[github-actions[bot]]

messageFile.md

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#16976~~
• ~~leanprover-community/mathlib4#16980~~
• ~~leanprover-community/mathlib4#16991~~
• ~~leanprover-community/mathlib4#20282~~ By Dependent Issues (🤖). Happy coding!

[faenuccio]

!bench

[leanprover-bot]

Here are the benchmark results for commit 4fbf384cba8d367bc420a304aae67b1c652b1257. There were no significant changes against commit e6e790275113b6bed3432cfc5a6929478604dc4e.

[github-actions[bot]]

File	Instructions	%
build	+20.253⬝10⁹	(+0.01%)
Mathlib.Data.Array.Lemmas	-1.669⬝10⁹	(-35.13%)
CI run

[kbuzzard]

I left one final nitpick comment. Many thanks! [edit: and I forgot to send it; it's sent now. Sorry for the delay.]

bors d+

[mathlib-bors[bot]]

:v: Thmoas-Guan can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[Thmoas-Guan]

Sorry, where is the "nitpick comment"? I didn't found it. Do you mean to use obtain rather than rcases?

[Thmoas-Guan]

bors r+

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style