Tabulating a list by defaulted lookup

Reading every index of a list of length n with List.getD and tabulating the result over Fin n gives back the list. These are the getD forms of core's List.ofFn_getElem and Mathlib's List.ofFn_getElem_eq_map, for when the length is only known to be n.

Main results

• List.ofFn_getD_eq_of_length: List.ofFn (fun i : Fin n => l.getD i d) = l when l.length = n.
• List.ofFn_getD_eq_map_of_length: the same after applying f to every entry.

theorem List.ofFn_getD_eq_of_length {α : Type u_1} (d : α) {n : ℕ} {l : List α} (hl : l.length = n) : (ofFn fun (i : Fin n) => l.getD (↑i) d) = l

Tabulating the defaulted lookups of a list of length n over Fin n gives back the list.

theorem List.ofFn_getD_eq_map_of_length {α : Type u_1} {β : Type u_2} (f : α → β) (d : α) {n : ℕ} {l : List α} (hl : l.length = n) : (ofFn fun (i : Fin n) => f (l.getD (↑i) d)) = map f l

Tabulating f of the defaulted lookups of a list of length n over Fin n maps f over the list.