mathlib3

4e8427ec - fix(data/list/defs): remove map_head; rename map_last to modify_last (#4507)

fix(data/list/defs): remove map_head; rename map_last to modify_last (#4507) `map_head` is removed in favour of the equivalent `modify_head`. `map_last` is renamed to `modify_last` for consistency with the other `modify_*` functions.