[Merged by Bors] - feat(data/(d)finsupp): well-foundedness of lexicographic and product orders

[alreadydone]

condition on domain	finsupp/dfinsupp	function/pi
arbitrary (prod) / has well_founded_gt (lex)	0 is a bottom elem in codomain (e.g. canonically_ordered) + well_founded_lt	invalid
finite (prod) / finite with linear_order (lex)	codomain has well_founded_lt	same as (d)finsupp

• (prod) means the product order and (lex) means the lexicographic order.

All results are provided in two forms whenever possible: a general form where the relations can be arbitrary (not the (<) of a preorder, or not even transitive, etc.) and a specialized form provided as well_founded_lt instances where the (d)finsupp/pi type (or their lex type synonyms) carries a natural (<).

---

• depends on: [Merged by Bors] - feat(data): port finsupp.ne_locus/lex to dfinsupp #16777
• depends on: [Merged by Bors] - feat(order/antisymmetrization): (<) is well-founded for a preorder iff well-founded on its antisymmetrization #16741

[YaelDillies]

I'm happy with this PR overall but there is a lot going on and I would feel more comfortable with a second pair of eyes reviewing it (@eric-wieser maybe?). But I recognize I'm probably the reviewer the closest to this kind of maths...

[alreadydone]

@eric-wieser @YaelDillies Any further comments?

[YaelDillies]

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

[jcommelin]

Thanks 🎉

bors merge

[Vierkantor]

Since the build hasn't finished I'll delegate just in case you need to fix it.

bors d+

[bors]

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

[YaelDillies]

Seems to have been forborsgotten!

[alreadydone]

bors r+

[bors]

Build failed (retrying...):

• Run tests

[bors]

Build failed (retrying...):

• Run tests

[bors]

Pull request successfully merged into master.

Build succeeded:

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