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

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

Begin by examining the existing translation system and the to_additive implementation referenced in the issue, then compare how Subgroup and subgroupOf are represented. Done means providing the illustrated to_subgroupOf API with the required ambient-group binder and hypotheses, under the stated single-Group limitation. Use the linked Zulip discussion to resolve the design questions before implementation.