Setting instance priorities

Stream: mathlib4

[Antoine Chambert-Loir]

I want to define a few instances but I wish that they have a smaller priority than any instance that the user would define as a […] parameter. And some of my instances should have a lower priority than the other ones, so that in some cases, the one which is synthesized is the good one.

What is the syntax for that ?

It is hard to propose a MWE, but basically, my instances are of the form Triple (f, g, h), and the goal is to fill h when f and g are known.
If there is an explicit Triple (f, g, h), it should be chosen.
Otherwise, two triples are good, Triple (id, g, g) and Triple (f, id, f).
And otherwise,when everything else fails, take Triple (f, g, g o f).

[Alex J. Best]

Sounds quite similar to dosc#RingHomCompTriple, where incidentally https://github.com/leanprover-community/mathlib4/blob/c13f0f5bfdf81a648b610b96e8381ccde5da237a/Mathlib/Algebra/Ring/CompTypeclasses.lean#L183 is an example of setting a priority

[Antoine Chambert-Loir]

It is indeed so similar, that it's made for the analogous CompTriple of #6057 ! Thanks.
What are the default priorities?
What is the ordering? — Just to check that an instance with priority 100 will be used after another with priority of 1000.

[Matthew Ballard]

Increasing number = increasing priority. Default is 1000 if I remember correctly