mathlib

e789ad31 - feat(group_theory/subgroup): mk lemmas (#9514)

feat(group_theory/subgroup): mk lemmas (#9514) See discussion at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/set_like.20idiom