"bad" simp lemmas can lead to `acyclic` tactic failure with `simp` recursion limit

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

I assume acyclic should now use omega instead of simp_arith

Context

Steps to Reproduce

import Mathlib.Algebra.Order.Monoid.Lemmas
import Mathlib.Data.Nat.Basic

@[simp] theorem succ_le_iff_lt: n + 1 ≤ k ↔ n < k := sorry

inductive Foo 
| mk (x y: Foo)

set_option trace.Meta.Tactic.acyclic true in
example {x y: Foo} (h: x = Foo.mk y x): False := nomatch h

Expected behavior: acyclic can handle such a goal

Actual behavior: acyclic tactic produces an error message:

[Meta.Tactic.acyclic] failed with
    tactic 'simp' failed, nested error:
    maximum recursion depth has been reached (use `set_option maxRecDepth <num>` to increase limit) 

Versions

4.7.0-rc2

Additional Information

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Reproduce the example using the listed Mathlib imports and set_option trace.Meta.Tactic.acyclic true. Start by tracing where acyclic invokes simp or simp_arith, then investigate the reported assumption that it should use omega; done means the example succeeds without increasing maxRecDepth and the recursion error no longer occurs.