[Merged by Bors] - feat(data/set_like): remove repeated boilerplate from subobjects

[eric-wieser]

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].

---

• depends on: [Merged by Bors] - chore(algebra/algebra/subalgebra): Add missing coe_sort for subalgebra #6800

[Vierkantor]

I think this is a very good idea! One note, in category theory terms, coe here is exactly the forgetful functor subobject -> subset. It might make sense to give it as an order preserving map subobject -> subset rather than "just" a function. (But you define the order in terms of coe, so that might be too confusing.)

Did you already consider how this would integrate with subobjects that use galois_insertion to define their lattice structure? E.g. intermediate_field.complete_lattice? This should give a complete lattice structure for free on everything with a "free subobject".

[eric-wieser]

But you define the order in terms of coe, so that might be too confusing.

The duplication I'm trying to eliminate always picks an order that matches coe; I think exposing an order-embedding as part of the API is sensible, but I don't think it should be part of the construction of the structure

Did you already consider how this would integrate with subobjects that use galois_insertion to define their lattice structure? E.g. intermediate_field.complete_lattice? This should give a complete lattice structure for free on everything with a "free subobject".

I was thinking about this, yes; but I figured I'd try and keep the scope of this PR somewhat constrained for now. I think my intent with this PR is to just propagate the lemma removals and see if typeclass resolution gets stuck anywhere. There's almost certainly a more powerful generalization to be made, but that will be much easier to build on top of the weak generalization with half the lemmas already deduplicated.

[eric-wieser]

I had a quick go with affine_subspace, but the whole API seems to be centered around expressions of the form a ∈ ↑b instead of a ∈ b, so I think it makes sense to try and fix that separately.

[eric-wieser]

I fear this will go stale quite quickly, as PRs seem to appear that use the mem_coe lemmas all the time.

[Vierkantor]

Thanks! 🎉

bors r+

[bors]

Build failed (retrying...):

• Build mathlib

[bors]

Build failed:

• Build mathlib

[Vierkantor]

Let's try it again:

bors merge
bors d+

[bors]

✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests