mathlib3

85df3a36 - refactor(group_theory/submonoid/basic): merge together similar lemmas and definitions (#7280)

refactor(group_theory/submonoid/basic): merge together similar lemmas and definitions (#7280) This uses `simps` to generate lots of uninteresting coe lemmas, and removes the less-bundled versions of definitions. The main changes are: * `add_submonoid.to_submonoid_equiv` is now just called `add_submonoid.to_submonoid`. This means we can remove the `add_submonoid.to_submonoid_mono` lemma, as that's available as `add_submonoid.to_submonoid.monotone`. Ditto for the multiplicative version. * `simps` now knows how to handled `(add_)submonoid` objects. Unfortunately it uses `coe` as a suffix rather than a prefix, so we can't use it everywhere yet. For now we restrict its use to just these additive / multiplicative lemmas which already had `coe` as a suffix. * `submonoid.of_add_submonoid` has been renamed to `add_submonoid.to_submonoid'` to enable dot notation. * `add_submonoid.of_submonoid` has been renamed to `submonoid.to_add_submonoid'` to enable dot notation. * The above points, but applied to `(add_)subgroup` * Two new variants of the closure lemmas about `add_submonoid` (`add_submonoid.to_submonoid'_closure` and `submonoid.to_add_submonoid'_closure`), taken from #7279