Indexing a list gives you an element of the list

Stream: new members

[Mark Fischer]

I couldn't find anything that does this in std

example (l : List ℕ) (i : Fin l.length) : l[i] ∈ l := by sorry

It feels like it should be easy to prove for myself, but I get as far simplifying to List.Mem (List.get l i) l but then I get stuck. Where should I be looking?

[Matt Diamond]

docs#List.get_mem is in Std.Data.List.Init.Lemmas

[Matt Diamond]

in terms of advice, I would say that the way to find a membership lemma related to a given function is to just search mathlib for "[type] [function] mem", so in this case "list get mem" (and it turns out that's basically the name of the lemma)

[Matt Diamond]

(of course in retrospect this seems obvious but I understand it's tricky to know what the magic words are)

[Mark Fischer]

Thanks for all the help :)

I've been having some luck just re-wording stuff a few ways and using the apply? library search tactic. But yeah, so far I've been finding dependent types are intuitive enough, but all the naming conventions and simp-normal forms and such are a struggle for me. I suspect it takes time as with any library.