Membership and extensionality for take and drop by index

The getElem? forms of List.mem_take_iff_getElem and List.mem_drop_iff_getElem: an element of a prefix or suffix is an entry of the original list at an index on that side of the cut. Alongside, the extensionality lemmas List.ext_take_getElem? and List.ext_drop_getElem?: two lists agreeing at every index below n have the same take n, and agreeing from n on have the same drop n; and List.take_append_take, truncating the right operand before taking a prefix is a no-op. [UPSTREAM] candidates for Init/Data/List/Nat/TakeDrop.lean, beside their getElem counterparts and List.ext_getElem?.

theorem List.mem_take_iff_getElem? {α : Type u_1} {l : List α} {a : α} {n : ℕ} : a ∈ take n l ↔ ∃ (i : ℕ), i < n ∧ l[i]? = some a

An element of l.take n is an entry of l at an index below n.

theorem List.mem_drop_iff_getElem? {α : Type u_1} {l : List α} {a : α} {n : ℕ} : a ∈ drop n l ↔ ∃ (i : ℕ), i ≥ n ∧ l[i]? = some a

An element of l.drop n is an entry of l at an index at least n. Unlike List.mem_drop_iff_getElem, the index is into l, not into the suffix.

theorem List.ext_take_getElem? {α : Type u_1} {l₁ l₂ : List α} {n : ℕ} (h : ∀ (k : ℕ), k < n → l₁[k]? = l₂[k]?) : take n l₁ = take n l₂

Lists agreeing at every index below n have the same prefix of length n.

theorem List.ext_drop_getElem? {α : Type u_1} {l₁ l₂ : List α} {n : ℕ} (h : ∀ (k : ℕ), n ≤ k → l₁[k]? = l₂[k]?) : drop n l₁ = drop n l₂

Lists agreeing at every index from n on have the same suffix from n.

theorem List.take_append_take {α : Type u_1} (n : ℕ) (l₁ l₂ : List α) : take n (l₁ ++ take n l₂) = take n (l₁ ++ l₂)

Truncating the right operand to length n before taking the length-n prefix of an append is a no-op.

theorem List.lt_length_of_mem_drop {α : Type u_1} {l : List α} {a : α} {n : ℕ} (h : a ∈ drop n l) : n < l.length

A nonempty suffix starts inside the list.