rw!: unknown free variable _fvar.423

Stream: mathlib4

[Shubakur Mitra]

After updating Lean from v4.24.0 to v4.27.0-rc1 and mathlib from a77a0aea to 1723eba8, tactic rw! started failing with unknown free variable _fvar.423

MWE:

import Mathlib.Tactic

example {xs : List (ℕ × ℕ)} (h₁ : xs.map (·.1) = [0])
(h₂ : 0 < (xs.map (·.1)).length) (h₃ : (xs.map (·.1))[0] = 0) : True := by
  rw! [h₁] at h₃ -- unknown free variable `_fvar.423`

[Snir Broshi]

A bit more minimized:

import Mathlib.Tactic.DepRewrite

/-- error: unknown free variable `_fvar.28` -/
#guard_msgs in
example {x : Bool} (h : x = x) : x = x := by
  rw! [h] at h

cc @Aaron Liu

[Aaron Liu]

oh I'll take a look

[Aaron Liu]

@𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒 might want to take a look too

[Aaron Liu]

looks like it's a problem with cleanup casts

[Aaron Liu]

until it's fixed you can use rewrite! instead

[Aaron Liu]

ah I fixed it

[Aaron Liu]

#33686