grind clear error

Stream: lean4

[Aaron Liu]

I was initially baffled since I didn't use clear but then I figured out what was happening

/--
error: Tactic `clear` failed: target depends on 'w'

case grind
n m : Nat
a : Fin n
b : Fin m
w : [n] = [m]
⊢ n = m → [] = [] → ∀ (h : ⋯ ▸ a = b), ⋯ ▸ a = b
-/
#guard_msgs in
example (n m : Nat) (a : Fin n) (b : Fin m) (h : ∃ h : [n] = [m], (List.cons.inj h).1 ▸ a = b) :
    (List.cons.inj h.1).1 ▸ a = b := by
  grind

[Kim Morrison]

(Sorry about this delay to respond -- this is working on v4.26.0-rc1.)