slow typeclass synthesis: takes 15000 heartbeats in fail in ZeroHomClass (Perm (Fin (Nat.succ n))) ?m ?m

[semorrison]

import Mathlib

open Equiv in
/--
error: failed to synthesize
  ZeroHomClass (Perm (Fin (Nat.succ n))) ?m.21038 ?m.21039
(deterministic) timeout at 'typeclass', maximum number of heartbeats (15000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit)
-/
#guard_msgs in
set_option synthInstance.maxHeartbeats 15000 in
example {n : ℕ} (p : Fin (n + 1)) (e : Perm (Fin n)) :
    Equiv.Perm.decomposeFin.symm (p, e) 0 = p := by simp

This then gets slightly worse after leanprover/lean4#3807, and thereafter causes the simpNF linter to fail on Equiv.Perm.decomposeFin_symm_apply_zero and Equiv.Perm.decomposeFin_symm_apply_one.

[mattrobball]

This one also seems fixed by leanprover/lean4#4085