panic with rw?

Stream: mathlib4

[Bhavik Mehta]

import Mathlib.Tactic

open List

#eval Lean.versionString

def foo : ℕ → ℕ
| 0 => 0
| (n + 1) => WithBot.unbot (minimum ([0].map (fun x => let y := foo x; y + 1))) (by rw?)

typing this gives the error
"Lean server printed an error: PANIC at Lean.Meta.whnfEasyCases Lean.Meta.WHNF:317:22: loose bvar in expression"
with the output page saying

PANIC at Lean.Meta.whnfEasyCases Lean.Meta.WHNF:317:22: loose bvar in expression
PANIC at Lean.Meta.whnfEasyCases Lean.Meta.WHNF:317:22: loose bvar in expression

This is on 4.0.0-nightly-2023-08-03

[Bhavik Mehta]

This seems superficially related to https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/panic.20and.20error.20with.20rw.3F, but this is on a version after the fix for that was merged

[Alex J. Best]

Made #6411 for this