Sections of a replicated list

This file proves facts about List.sections of replicate n l, the list of words of length n over the alphabet l: membership, compatibility with map, and the recursion in the length as a multiset bind.

theorem List.sections_map_map {α : Type u_1} {β : Type u_2} (f : α → β) (L : List (List α)) : (map (map f) L).sections = map (map f) L.sections

theorem List.sections_replicate_map {α : Type u_1} {β : Type u_2} (f : α → β) (n : ℕ) (l : List α) : (replicate n (map f l)).sections = map (map f) (replicate n l).sections

theorem List.mem_sections_replicate {α : Type u_1} {n : ℕ} {l s : List α} : s ∈ (replicate n l).sections ↔ s.length = n ∧ ∀ (a : α), a ∈ s → a ∈ l

@[simp]

theorem List.sections_replicate_singleton {α : Type u_1} (a : α) (n : ℕ) : (replicate n [a]).sections = [replicate n a]

theorem List.sections_singleton {α : Type u_1} (l : List α) : [l].sections = map (fun (x : α) => [x]) l

theorem List.coe_sections_replicate_succ {α : Type u_1} (n : ℕ) (l : List α) : ↑(replicate (n + 1) l).sections = (↑l).bind fun (a : α) => Multiset.map (fun (x : List α) => a :: x) ↑(replicate n l).sections