Regression in v4.33.0-rc1: `simp` triggers a max heartbeats error

[sonmarcho]

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

example (x : Nat) :
    let v := Vector.ofFn fun k : Fin 5 => (x >>> k.val) % 2 != 0
    (Vector.ofFn fun i : Fin 1 =>
      Fin.foldl 5 (fun (acc : BitVec 1) j =>
        acc + v[i.val + j.val].toNat) 0)[0] = 0 := by
  -- The `simp only` works instantly in 4.32.0 but fails in 4.33.0-rc1 with:
  -- "timeout at `whnf`, maximum number of heartbeats (200000) has been reached"
  simp only [Vector.getElem_ofFn] -- 
  sorry