Entries of a row read with a default

A list of lists, read with List.getD and the empty list as default, has every entry of each of its rows among the entries of its flattening.

theorem List.mem_flatten_of_mem_getD {α : Type u_1} {rows : List (List α)} {i : ℕ} {x : α} (hx : x ∈ rows.getD i []) : x ∈ rows.flatten

An entry of row i of a list of rows is an entry of the list. Rows beyond the last one are read as empty.