create a type synonym and transfer a lot of stuff

Stream: mathlib4

[Antoine Chambert-Loir]

For PR #16177, I added some variant of the lexicographic order of monomials which led me to add a type synonym LexHom so that LexHom (Finsupp I Nat) would be endowed with that order (first on degree, then on lexicographic order). Here are my two questions.

1. Maybe I could/should have been content with typing something like Lex (Nat x Lex (Finsupp I Nat) all the time. Should I have?

2. On the other hand, if adding a type synonym is useful, then it requires to start adding a lot of equivalences (toLexHom, ofLexHom, etc., as there is for docs#Finsupp.Lex), functions and instances (endowing LexHom _ with a monoid structure when _ has, so that toLexHomis a morphism of monoids), a task which is rather uninteresting in itself. (Of course, I started by copy-pasting what exists for Lexand adjusted things afterwards according to my needs.)
   So the question is — what should be the proper way to have this boring code written automatically for us?

[Yaël Dillies]

Antoine Chambert-Loir said:

Maybe I could/should have been content with typing something like Lex (Nat x Lex (Finsupp I Nat) all the time. Should I have?

I would think so, yes. You are free to add notation for it, the same way as α ×ₗ β is notation for Lex (α × β)

[Antoine Chambert-Loir]

So I'll try adjusting my code in this direction and see if that makes it better. (You should like it, it's combinatorics after all!)

[Yaël Dillies]

What combinatorics, may I excitingly ask?

[Yaël Dillies]

Oh, the combinatorial nullstellensatz. Sorry, I should have clicked!

[Johan Commelin]

@Antoine Chambert-Loir If you use abbrev instead of def then typeclass synthesis will see through it and find all the instances that it would normally find for Lex (Nat x Lex (Finsupp I Nat). And then you shouldn't need all the equivalences and transferring...