mathlib3

f5d916a6 - feat(data/vector/mem): Lemmas about membership in a vector (#15154)

feat(data/vector/mem): Lemmas about membership in a vector (#15154) Add a number of lemmas about membership in different `vector`s. Some just wrap the `list` versions but some of the `n+1` cases are more general.