Simplify head and tail of `List.map`

Stream: Is there code for X?

[Jakob von Raumer]

Should we have this?

@[simp]
lemma _root_.List.cons_map_tail_eq {α β : Type*} (f : α → β) (as : List α) (h : as ≠ []) :
    f (as.head h) :: (as.map f).tail = as.map f := by
  conv_rhs => rw [← List.head_cons_tail as h, List.map_cons, List.map_tail]

[Robin Arnez]

Whenever you are working with head and tail, you probably should instead match on the list:

theorem List.cons_map_tail_eq {α β : Type _} (f : α → β) (as : List α) (h : as ≠ []) :
    f (as.head h) :: (as.map f).tail = as.map f := by
  match as, h with
  | x :: l, _ => simp

I'm not sure if this really works well as a simp lemma though since List.map_cons basically goes the other way round (also the f on the left is a bit awkward). In most situations, you should be able to get away with

match as, h with
| x :: l, _ => ?_

and then just do stuff the other way round.

[Jakob von Raumer]

I'm not manipulating the Lists by hand, but inside a big aesop call, so matching at the use site of the lemma is difficult

[Jakob von Raumer]

But yea, List.map_cons being the other direction would cause a loop for as being a :: as

[Kim Morrison]

@Jakob von Raumer, if you're able to tell me about your use case either here or privately, I'd love to try out grind on it. It's nearly ready now for List oriented goals.