mathlib3

a6158f19 - feat(group_theory/subgroup/basic): One-sided closure induction lemmas (#12725)

feat(group_theory/subgroup/basic): One-sided closure induction lemmas (#12725) This PR adds one-sided closure induction lemmas, which I will need for Schreier's lemma. Co-authored-by: tb65536 <tb65536@users.noreply.github.com>