List Take/Join Lemma

This file packages a reusable list lemma imported from an external public-domain source.

Main declarations

• take_join_of_lt

theorem List.take_join_of_lt {α : Type u_1} {L : List (List α)} {n : ℕ} (notall : n < L.flatten.length) : ∃ (m : ℕ) (k : ℕ) (mlt : m < L.length), k < (L.get ⟨m, mlt⟩).length ∧ take n L.flatten = (take m L).flatten ++ take k (L.get ⟨m, mlt⟩)