Rewriting/simplification issue in v4.29.0-rc2

Stream: mathlib4

[Palalansoukî]

In v4.29.0-rc2, I encountered a strange change in behavior regarding rewriting/simplification. Previously (at least v4.28.0-rc1), the following theorem could be proven just using simp, but in v4.29.0-rc2, it cannot be rewritten even using rw or grind. congr and try? also fails.

import Mathlib

open List List.Vector

example (P : ℕ → Prop) (v : List.Vector ℕ (n + 1)) (i : Fin n) :
    P (v.get i.succ) ↔ P (v.tail.get i) := by
  simp [get_tail_succ] -- fail
  rw [get_tail_succ] -- fail
  grind [get_tail_succ] -- fail
  sorry

Is this change in behavior intentional? Also, what method should be used in such cases?

[Violeta Hernández]

set_option backward.isDefEq.respectTransparency false

[Violeta Hernández]

#general > backward.isDefEq.respectTransparency

[Eric Wieser]

Is this one reported in that thread?

[Violeta Hernández]

Seems very similar to this