mathlib

951a60ea - chore(data/list/basic): golf a proof (#9949)

chore(data/list/basic): golf a proof (#9949) Prove `list.mem_map` directly, get `list.exists_of_mem_map` and `list.mem_map_of_mem` as corollaries.