chore: remove redundant covariance instances, add priority

[astrainfinita]

trafficstars

I noticed that the following code is surprisingly slow.

import Mathlib

count_heartbeats in
example {n : ℕ} : CovariantClass (Fin (n + 1)) (Fin (n + 1)) (· + ·) (· < ·) := by
  try infer_instance
  sorry

This PR removed some redundant instances. The heartbeats have dropped from 19118 to 11450 (still too slow). Lean4 still seems to make some redundant attempts. See also https://github.com/leanprover-community/mathlib4/issues/6646#issuecomment-1691792488.

---

[astrainfinita]

!bench

[leanprover-bot]

Here are the benchmark results for commit a6e645f7c7c8d8c2f2f0b7facb405c6a7c8f1d20. There were significant changes against commit e9fb5b31bb918376a758dec1ff49931062deb8f4:

  Benchmark                                  Metric         Change
  ================================================================
- ~Mathlib.CategoryTheory.ComposableArrows   instructions     6.1%

[astrainfinita]

!bench

[leanprover-bot]

Here are the benchmark results for commit 1a749e0ff829652853aecae457336ffbeee6cb36. There were significant changes against commit e9fb5b31bb918376a758dec1ff49931062deb8f4:

  Benchmark                                  Metric         Change
  ================================================================
- ~Mathlib.CategoryTheory.ComposableArrows   instructions     5.3%

[urkud]

I'm changing it to awaiting-author because it's marked as a draft PR and as a WIP. If it's ready for review, then please change it from draft to a normal PR and adjust the labels.

[astrainfinita]

!bench

[leanprover-bot]

Here are the benchmark results for commit 45d4cccc28894bf4490178a81ffd4678a0ff11a7. There were no significant changes against commit 3502115bbf882ed91452052c41607a3e5139e1e1.