mathlib3

efab188a - refactor(group_theory/{submonoid, subsemigroup}/basic): move `mul_mem_class` (#13559)

refactor(group_theory/{submonoid, subsemigroup}/basic): move `mul_mem_class` (#13559) This moves `mul_mem_class` (and `add_mem_class`) from `group_theory/submonoid/basic` to `group_theory/subsemigroup/basic` so that `subsemigroup` can be an instance. We then protect `subsemigroup.mul_mem`. In addition, we add an induction principle for binary predicates to better parallel `group_theory/submonoid/basic`.