getElem and List.get

Stream: lean4

[Eric Wieser]

Does this lemma exist anywhere?

example {α} {l : List α} (i : Fin l.length) : l[i] = l.get i := by
  sorry

It's true by rfl, which makes it hard to search for.

[Henrik Böving]

Why would it be heard to search for because of that?: https://loogle.lean-lang.org/?q=List.get%2C+GetElem.getElem, gets you docs#List.get_eq_getElem

[Eric Wieser]

That theorem doesn't close the goal here though

[Eric Wieser]

example {α} {l : List α} (i : Fin l.length) : l[i] = l.get i := by
  rw [List.get_eq_getElem]
  -- goal is `l[i] = l[↑i]`

[Eric Wieser]

Henrik Böving said:

Why would it be heard to search for because of that?:

Because exact? won't look beyond rfl, IIRC

[François G. Dorais]

@Kim Morrison There might be some specialized needs for fget after all.

[Markus Himmel]

The missing lemma to close the goal is docs#Fin.getElem_fin. simp finds both of these lemmas. I'm not sure whether there should be a lemma that combines the two, because docs#Fin.instGetElemFinVal is very general, so this lemma would need to be stated for a lot of other types with GetElem in addition to lists.