Map eq cons

Stream: Is there code for X?

[Marcus Rossel]

I have a proof that hd :: tl = l.map f for hd : X, tl : list X, l : List Y, f : Y -> X.
How can I show that l must be equal to some a :: b where f a = hd and b.map f = tl?

[Yaël Dillies]

You can do cases l, get rid of the first goal because [].map f = [] and then rw list.map_cons (or something like that) in your second goal.

[Floris van Doorn]

Though feel free to add a lemma to mathlib of the form lemma map_eq_cons : l.map f = hd :: tl \iff \exists x l', l = x :: l' \and f x = hd \and l'.map f = tl

[Floris van Doorn]

(and while we're at it map_eq_append)

[Eric Wieser]

Should it be map_eq_cons_iff? What does #naming have to say about trailing _iffs?