simp timeout at `whnf`

Stream: mathlib4

[thielema]

I have the following simplified code:

import Mathlib
import Lean

lemma injective_unit_pow
  {m : Nat} (is_prime : m.succ.Prime) (p : Units (Fin m.succ))
  : Function.Injective (p ^ ·)
  := by
  have p_order := orderOf_eq_card_powers (x := p)
  simp at p_order

Lean works several seconds on simp, then aborts with this error:

tactic 'simp' failed, nested error:
(deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached
Use `set_option maxHeartbeats <num>` to set the limit.
Additional diagnostic information may be available using the `set_option diagnostics true` command.

[Kim Morrison]

Have you tried the suggestion set_option diagnostics true that is shown in the error message yet? What does it say?

[Kevin Buzzard]

If I open this code in the web editor there's no problem with it (other than the fact that the lemma is false); there's no timeout. So maybe update your mathlib? You don't need import Lean by the way, you're not doing metaprogramming here.

[thielema]

It happened in Lean-4.14. Seems to have gone in 4.15.