Regression: rw works, but simp fails

Stream: mathlib4

[Shubakur Mitra]

After updating Lean from v4.27.0-rc1 to v4.29.0-rc1 and mathlib from 1723eba8 to 7f14c970, the following proof started failing:

import Mathlib
open List in example {α : Type*} {xs : List α} {p : α → Bool} :
    xs.findIdx p = 0 ↔ xs = [] ∨ ∃ (h : 0 < xs.length), p xs[0] := by
  rcases xs with _ | ⟨x, xs⟩ <;> simp; rw [findIdx_eq] <;> simp

Further investigation shows that here rw works, but simp fails to close the goal:

import Mathlib
open List in example {α : Type*} {xs : List α} {p : α → Bool} :
    xs.findIdx p = 0 ↔ xs = [] ∨ ∃ (h : 0 < xs.length), p xs[0] := by
  rcases xs with _ | ⟨x, xs⟩ <;> simp; rw [findIdx_eq]; simp
  · simp --fails
    rw [getElem_cons_zero] --works
  · sorry

Simp was working in the old version.

[Yury G. Kudryashov]

Use set_option backward.isDefEq.respectTransparency false

[Yury G. Kudryashov]

See the announcement, the FRO doesn't recommend downstream projects to update yet.