feat(topology/algebra/open_subgroup): basics on open subgroups

[jcommelin]

From the perfectoid project.
Depends on #1066.
Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/open.20subgroups

[sgouezel]

This looks very good and very clean, except maybe the comment on Line 99 that you should remove. I have a question related to this comment: do you understand why the to_additive machinery sometimes works directly out of the box, and why sometimes you need to reprove the statements? Is that a hint that some previous lemmas are not tagged correctly, or simply that the machinery is not powerful enough?

[digama0]

The to_additive machinery is sometimes too aggressive in replacing multiplicative stuff with additive. In particular, whenever group_power gets involved, nat gets involved, and then you might not want to turn 1 : nat into 0 : nat and such, when you are trying to make the group A additive. I'm not sure if any such examples appear in this PR, though; mostly I discover the offenders by trial and error, although to_additive errors also tell you where to put more annotations.