Join of a list of lists

This file proves basic properties of List.flatten, which concatenates a list of lists. It is defined in Init.Prelude.

theorem List.Sublist.flatten {α : Type u_1} {l₁ l₂ : List (List α)} (h : l₁.Sublist l₂) : l₁.flatten.Sublist l₂.flatten

theorem List.Sublist.flatMap {α : Type u_1} {β : Type u_2} {l₁ l₂ : List α} (h : l₁.Sublist l₂) (f : α → List β) : (flatMap f l₁).Sublist (flatMap f l₂)

theorem List.Sublist.flatMap_right {α : Type u_1} {β : Type u_2} (l : List α) {f g : α → List β} (h : ∀ (a : α), a ∈ l → (f a).Sublist (g a)) : (flatMap f l).Sublist (flatMap g l)

theorem List.drop_take_succ_eq_cons_getElem {α : Type u_1} (L : List α) (i : Nat) (h : i < L.length) : drop i (take (i + 1) L) = [L[i]]

Taking only the first i+1 elements in a list, and then dropping the first i ones, one is left with a list of length 1 made of the i-th element of the original list.

theorem List.append_flatten_map_append {α : Type u_1} (L : List (List α)) (x : List α) : x ++ (map (fun (x_1 : List α) => x_1 ++ x) L).flatten = (map (fun (x_1 : List α) => x ++ x_1) L).flatten ++ x

We can rebracket x ++ (l₁ ++ x) ++ (l₂ ++ x) ++ ... ++ (lₙ ++ x) to (x ++ l₁) ++ (x ++ l₂) ++ ... ++ (x ++ lₙ) ++ x where L = [l₁, l₂, ..., lₙ].

theorem List.head_head_eq_head_flatten {α : Type u_1} {l : List (List α)} (hl : l ≠ []) (hl' : l.head hl ≠ []) : (l.head hl).head hl' = l.flatten.head ⋯

See also head_flatten_eq_head_head, which switches around the proof obligations.

theorem List.head_flatten_eq_head_head {α : Type u_1} {l : List (List α)} (hl : l.flatten ≠ []) (hl' : l.head ⋯ ≠ []) : l.flatten.head hl = (l.head ⋯).head hl'

See also head_head_eq_head_flatten, which switches around the proof obligations.

theorem List.getLast_getLast_eq_getLast_flatten {α : Type u_1} {l : List (List α)} (hl : l ≠ []) (hl' : l.getLast hl ≠ []) : (l.getLast hl).getLast hl' = l.flatten.getLast ⋯

See also getLast_flatten_eq_getLast_getLast, which switches around the proof obligations.

@[deprecated List.getLast_getLast_eq_getLast_flatten (since := "2026-01-31")]

theorem List.getLast_flatten_of_getLast_ne_nil {α : Type u_1} {l : List (List α)} (hl : l ≠ []) (hl' : l.getLast hl ≠ []) : (l.getLast hl).getLast hl' = l.flatten.getLast ⋯

Alias of List.getLast_getLast_eq_getLast_flatten.

---

See also getLast_flatten_eq_getLast_getLast, which switches around the proof obligations.

theorem List.getLast_flatten_eq_getLast_getLast {α : Type u_1} {l : List (List α)} (hl : l.flatten ≠ []) (hl' : l.getLast ⋯ ≠ []) : l.flatten.getLast hl = (l.getLast ⋯).getLast hl'

See also getLast_getLast_eq_getLast_flatten, which switches around the proof obligations.

@[deprecated List.getLast_flatten_eq_getLast_getLast (since := "2026-01-31")]

theorem List.getLast_flatten_of_flatten_ne_nil {α : Type u_1} {l : List (List α)} (hl : l.flatten ≠ []) (hl' : l.getLast ⋯ ≠ []) : l.flatten.getLast hl = (l.getLast ⋯).getLast hl'

Alias of List.getLast_flatten_eq_getLast_getLast.

---

See also getLast_getLast_eq_getLast_flatten, which switches around the proof obligations.