lemmas for `getElem! `

Stream: Is there code for X?

[Moritz Firsching]

What would be a good place for the following two lemmas for getElem!:

lemma getElem_cons_zero (tl : List ℕ) (hd : ℕ) : hd = (hd :: tl)[0]! := by
  unfold getElem!
  simp

and

lemma getElem_cons (n : ℕ) (tl : List ℕ) (hd : ℕ) : tl[n]! = (hd :: tl)[n + 1]! := by

?
It seems like getElem! is defined in lean4 and I can't find where basic theorems for that definition are.

[Alex J. Best]

Probably in Std.Data.List.Lemmas (suitably generalized). I also can't find lemmas for it, perhaps as it isn't used as much for proving as its friends getElem and getElem?

[Moritz Firsching]

https://github.com/leanprover/std4/pull/214 for the first one
right next to get_cons_zero

[Alex J. Best]

Definitely it seems we should have getElem!_eq_get! along with get!_eq_getD get!_eq_get? for listst also