Commit 2021-04-23 07:17 85df3a36

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