chore(group_theory/congruence): lower priority for `con.quotient.deci…

…dable_eq` (#9826)

I was debugging some slow typeclass searches, and it turns out (`add_`)`con.quotient.decidable_eq` wants to be applied to all quotient types, causing a search for a `has_mul` instance before the elaborator can try unifying the `con.to_setoid` relation with the quotient type's relation, so e.g. `decidable_eq (multiset α)` first tries going all the way up to searching for a `linear_ordered_normed_etc_field (list α)` before even trying `multiset.decidable_eq`.

Another approach would be to make `multiset` and/or `con.quotient` irreducible, but that would require a lot more work to ensure we don't break the irreducibility barrier.

src/group_theory/congruence.lean

@@ -208,7 +208,8 @@ relation", priority 0]
 instance : has_coe_t M c.quotient := ⟨@quotient.mk _ c.to_setoid⟩
 
 /-- The quotient by a decidable congruence relation has decidable equality. -/
-@[to_additive "The quotient by a decidable additive congruence relation has decidable equality."]
+@[to_additive "The quotient by a decidable additive congruence relation has decidable equality.",
+  priority 500] -- Lower the priority since it unifies with any quotient type.
 instance [d : ∀ a b, decidable (c a b)] : decidable_eq c.quotient :=
 @quotient.decidable_eq M c.to_setoid d