RFC: `List` lemmas for `tail`/`dropLast` applied to `take`/`drop`

Proposal

I propose adding these lemmas:

theorem tail_take (l : List α) (i : Nat) : (l.take i).tail = l.tail.take (i - 1) := by
  simp [← drop_one, drop_take]

theorem dropLast_take' (l : List α) (i : Nat) :
    (l.take i).dropLast = l.dropLast.take (i - 1) := by
  simp [dropLast_eq_take, take_take, Nat.sub_min_sub_right,
    Nat.le_trans (sub_le ..) (Nat.min_le_left ..)]

theorem tail_drop' (l : List α) (i : Nat) : (l.drop i).tail = l.tail.drop i := by
  simp

theorem dropLast_drop (l : List α) (i : Nat) : (l.drop i).dropLast = l.dropLast.drop i := by
  simp [dropLast_eq_take, Nat.sub_right_comm, drop_take]

Community Feedback

#Is there code for X? > List.tail/List.dropLast + List.take
(Kim supported adding these to core)

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

The proposal specifies four List lemmas: tail_take, dropLast_take', tail_drop', and dropLast_drop. Start by locating the core List API and its existing theorem organization, then check how these statements fit there. Done means the four lemmas are added with the supplied proofs and compile successfully.