feat(data/list/basic): add lemma map_eq_repeat_iff (#17832)
This small PR adds the following API lemma for lists:
```lean
lemma map_eq_repeat_iff {α β} {l : list α} {f : α → β} {b : β} :
l.map f = repeat b l.length ↔ (∀ x ∈ l, f x = b)
```
See this [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/More.20general.20version.20of.20.60list.2Emap_const.60.3F/near/314118320).
(It also fixes a harmless typo in the proof of `last_map`.)
