Commit 2022-12-11 18:31 cf9386b5

feat(data/list/basic): add lemma map_eq_repeat_iff (#17832) This small PR adds the following API lemma for lists:

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. (It also fixes a harmless typo in the proof of last_map.)