(1 2 3 4)^4 = 1 is slow

Stream: mathlib4

[Yongyi Chen]

It appears that if a permutation on a set with a small number of elements (4 in this case) is defined using Cycle.fromPerm, evaluating its powers using #eval is fine but deciding whether its power is equal to 1 is very slow. See below.

Minimal working example:

import Mathlib

set_option trace.profiler true

open Equiv

def g : Perm (Fin 4) := Cycle.formPerm [(0 : Fin 4), 1, 2, 3] (by trivial)
def h : Perm (Fin 4) := ⟨![1, 2, 3, 0], ![3, 0, 1, 2], by decide, by decide⟩
-- These are both fast enough.
#eval g^4
#eval h^4

example : g^4 = 1 := by decide -- (deterministic) timeout at 'whnf', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
example : h^4 = 1 := by decide -- [0.185449s]

[Thomas Browning]

Here's an example from mathlib: https://github.com/leanprover-community/mathlib4/blob/6af751e84a5e8d15f0d0d2d1b279ad4f7da7f28e/Mathlib/GroupTheory/Solvable.lean#L211-L220

[Kevin Buzzard]

Could this be lean4#2564 again?