Timeouts when using simp on Fin inequalities

Stream: mathlib4

[Yakov Pechersky]

Is there a way to have the TC search to not be hit by simp here? You can imagine I had a more complex expression like (k + 0) + l < (l + 0) and wanted simp to simplify it.

import Mathlib.Data.Fin.Basic

example {n : ℕ} (k l : Fin (n + 1)) : k + l < l := by
  simp -- times out
  -- failed to synthesize
  -- CovariantClass (Fin (n + 1)) (Fin (n + 1)) (Function.swap fun x x_1 ↦ x + x_1) fun x x_1 ↦ x < x_1
  -- (deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit)

[Kevin Buzzard]

We could remove CovarianatClass...

[Yaël Dillies]

Agreed