recursive

Stream: mathlib4

[vxctyxeha]

maximum recursion depth has been reached？

import Mathlib
open Equiv Equiv.Perm Fin Finset -- 打开常用命名空间

example :
  let tau := c[0, 1] * c[2, 3, 4]
  let centralizerElements : Set (Perm (Fin 7)) :=
    { 1, c[0, 1], c[2, 3, 4], (c[2, 3, 4])^2, c[5, 6],
      c[0, 1] * c[2, 3, 4], c[0, 1] * (c[2, 3, 4])^2, c[0, 1] * c[5, 6],
      c[2, 3, 4] * c[5, 6], (c[2, 3, 4])^2 * c[5, 6],
      c[0, 1] * c[2, 3, 4] * c[5, 6], c[0, 1] * (c[2, 3, 4])^2 * c[5, 6]
    }
  ∀ σ ∈ centralizerElements, σ * tau = tau * σ :=
by
  decide

[Aaron Liu]

Try decide +kernel maybe?

[Edison Xie]

(deleted)