feat(Algebra/Group): Add translator tactic for Subgroup and subgroupOf

[FrederickPu]

Create translation tactic with similar user facing api to to_additive called to_subgroupOf that automatically converts theorems about Subgroup to theorems about subgroupOf. For example if we have:

@[to_subgroupOf]
theorem womp [Group G] (H1 H2 : Subgroup G) : H1 = H2 -> |H1| = |H2| := sorry

then,

theorem womp_synth [Group G] (K : Subgroup G) (H1 H2 : Subgroup G) (hH1 : H1.subgroupOf K) (hH2 : H2.subgroupOf K) :  H1 = H2 -> |H1| = |H2| := sorry

is created.
Note that this is not immediately possible with the current translation system since we need to introduce a new binder for the ambient group so we cannot simply perform constant rename like we do for to_additive. However, so long as we stick to instances where there is only one type implementing the Group type class translation should always be possible.

Based on discussion: https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/useful.20group.20theory.20lemmas/with/546738566

[FrederickPu]

one of doing this could be to just translate the declaration using the existing translation code (with a custom namedict that maps Subgroup to corresponding things in subgroupOf) and then add the binders for for the ambient group and the typeclass on the outside. The one issue with this is we will need to know the types of every sub expression (H : Subgroup G). So maybe running instantiateMvars on the expression first would help with that.

[FrederickPu]

ig this would also require replacing every (H : Subgroup G) with SubgroupDummy H G to work with the existing api

[SproutSeeds]

Hi all, I am planning a local first pass on this issue this week. I will run style preflight and local gate before opening any draft PR. If someone is already working on this, happy to coordinate and I can switch targets.

[FrederickPu]

I'd be willing to work together on this issue too. Although I'll be a bit busy the next couple weeks so I'll probably wait for your initial draft PR