(a :: l ++ [b]).last' does not simplify to some b

[jcpaik]

For a list with ends a and b, simp does not simplify its last' to some b:

import data.list

variable {α : Type*}
example (a b : α) (l : list α) : (a :: l ++ [b]).last' = some b :=
begin simp, sorry end

A possible workaround is to add the following simp lemma.

import data.list

variable {α : Type*}
@[simp]
theorem list.last'_cons_append_cons (a b : α) (l1 l2 : list α) : 
  (a :: (l1 ++ b :: l2)).last' = (b :: l2).last' := 
by revert a; induction l1 with c l1 ih; simp; intro; exact ih c

-- Now this works
example (a b : α) (l : list α) : (a :: l ++ [b]).last' = some b := by simp

How about we add the lemma above to mathlib?

I think a similar lemma for list.last (without ticks) can be also proved.