Unhelpful list deprecations

Stream: lean4

[Eric Wieser]

What's the intended replacement here?

import Lean

example := @List.get?_eq_some_iff

The deprecation message says

`List.get?_eq_some_iff` has been deprecated: Use `a[i]?` instead.

which isn't very helpful, as the first is a lemma and the second is a definition!

[Henrik Böving]

The corresponding getElem lemma.

[Eric Wieser]

Could the deprecations be changed to refer to those lemmas?

[Henrik Böving]

I guess? They are also up for deletion anyway though.

[Kim Morrison]

I'd merge a PR updating these deprecation messages, but don't have time to prepare such myself.