Commit 2021-03-30 14:01 bcfaabfc

feat(data/set_like): remove repeated boilerplate from subobjects (#6768) This just scratches the surface, and removes all of the boilerplate that is just a consequence of the injective map to a set. Already this trims more than 150 lines. For every lemma of the form set_like.* added in this PR, the corresponding submonoid.*, add_submonoid.*, sub_mul_action.*, submodule.*, subsemiring.*, subring.*, subfield.*, subalgebra.*, and intermediate_field.* lemmas have been removed. Often these lemmas only existed for one or two of these subtypes, so this means that we have lemmas for more things not fewer. Note that while the ext_iff, ext', and ext'_iff lemmas have been removed, we still need the ext lemma as set_like.ext cannot directly be tagged @[ext].