Taking prefix of concatenated lists returns the first list
Provedtake_append_selfTaking the first n elements from the concatenation of two lists, where n is the length of the first list, returns exactly the first list.
Formal statement
theorem take_append_self {α : Type} (l1 l2 : List α) :
(l1 ++ l2).take l1.length = l1 := by sorry