More general version of `list.map_const`?

Stream: Is there code for X?

[Michael Stoll]

There is

theorem list.map_const {α : Type u} {β : Type v} (l : list α) (b : β) :
  list.map (function.const α b) l = list.repeat b l.length

which clearly generalizes to

example {α β} {l : list α} {f : α → β} {b : β} (h : ∀ x ∈ l, f x = b) :
  l.map f = list.repeat b l.length :=

but I can't find this more general version. Is it really not there? And if so, would it make sense to add it? (I have a use case...)

[Scott Morrison]

Do you want this as a @[simp] lemma, in a situation where you expect simp to solve h as well?

Do you actually want a lemma that says (∀ x ∈ l, f x = b) → f = function.const α b?

[Michael Stoll]

Not sure it would make sense as a simplemma.

Scott Morrison said:

Do you actually want a lemma that says (∀ x ∈ l, f x = b) → f = function.const α b?

This will not be true in general: fcan take other values on elments that are not in the list.

[Michael Stoll]

(Which is precisely the point...)

[Eric Wieser]

Your version might be better as an `iff

[Michael Stoll]

OK; I'll do the iff version and PR it.

[Michael Stoll]

#17832

[Michael Stoll]

I think this can be merged now (before the tide rises :smile: ...).