doc-next-gen

Mathlib.Data.List.Sublists

Module docstring

{"# sublists

List.Sublists gives a list of all (not necessarily contiguous) sublists of a list.

This file contains basic results on this function. ","### sublists ","### sublistsLen "}

List.sublists'_nil theorem
: sublists' (@nil α) = [[]]
Full source 
@[simp]
theorem sublists'_nil : sublists' (@nil α) = [[]] :=
  rfl
Sublists of Empty List
Informal description
The list of all sublists of the empty list `[]` is the singleton list containing only the empty list, i.e., `sublists' [] = [[]]`.
List.sublists'_singleton theorem
(a : α) : sublists' [a] = [[], [a]]
Full source 
@[simp]
theorem sublists'_singleton (a : α) : sublists' [a] = [[], [a]] :=
  rfl
Sublists of Singleton List
Informal description
For any element $a$ of type $\alpha$, the list of all sublists of the singleton list $[a]$ is $[[], [a]]$.
List.sublists'Aux definition
(a : α) (r₁ r₂ : List (List α)) : List (List α)
Full source 
/-- Auxiliary helper definition for `sublists'` -/
def sublists'Aux (a : α) (r₁ r₂ : List (List α)) : List (List α) :=
  r₁.foldl (init := r₂) fun r l => r ++ [a :: l]
Auxiliary sublist construction function
Informal description
Given an element `a` of type `α` and two lists `r₁`, `r₂` of lists of `α`, the function returns the list obtained by prepending `a` to each element of `r₁` and appending these new lists to `r₂`. This is an auxiliary function used in the definition of `sublists'` which generates all sublists of a list.
List.sublists'Aux_eq_array_foldl theorem
(a : α) : ∀ (r₁ r₂ : List (List α)), sublists'Aux a r₁ r₂ = ((r₁.toArray).foldl (init := r₂.toArray) (fun r l => r.push (a :: l))).toList
Full source 
theorem sublists'Aux_eq_array_foldl (a : α) : ∀ (r₁ r₂ : List (List α)),
    sublists'Aux a r₁ r₂ = ((r₁.toArray).foldl (init := r₂.toArray)
      (fun r l => r.push (a :: l))).toList := by
  intro r₁ r₂
  rw [sublists'Aux, Array.foldl_toList]
  have := List.foldl_hom Array.toList (g₁ := fun r l => r.push (a :: l))
    (g₂ := fun r l => r ++ [a :: l]) (l := r₁) (init := r₂.toArray) (by simp)
  simpa using this
Equivalence of Sublist Auxiliary Function and Array Fold Operation
Informal description
For any element $a$ of type $\alpha$ and any lists $r_1, r_2$ of lists of $\alpha$, the auxiliary sublist construction function `sublists'Aux` applied to $a$, $r_1$, and $r_2$ is equal to converting $r_1$ and $r_2$ to arrays, performing a left fold operation on $r_1$'s array (initialized with $r_2$'s array) where each step appends the list obtained by prepending $a$ to the current element of $r_1$, and then converting the resulting array back to a list. In mathematical notation: $$\text{sublists'Aux}(a, r_1, r_2) = \text{toList}\left(\text{foldl}\left(\text{init} := \text{toArray}(r_2), \text{fun } r \, l \Rightarrow r.\text{push}(a :: l)\right)(\text{toArray}(r_1))\right)$$
List.sublists'_eq_sublists'Aux theorem
(l : List α) : sublists' l = l.foldr (fun a r => sublists'Aux a r r) [[]]
Full source 
theorem sublists'_eq_sublists'Aux (l : List α) :
    sublists' l = l.foldr (fun a r => sublists'Aux a r r) [[]] := by
  simp only [sublists', sublists'Aux_eq_array_foldl]
  rw [← List.foldr_hom Array.toList]
  · intros _ _; congr
Equivalence of Sublist Generation via Fold and Auxiliary Function
Informal description
For any list $l$ of elements of type $\alpha$, the list of all sublists of $l$ (denoted as $\text{sublists'}(l)$) is equal to the right fold of $l$ using the auxiliary function $\text{sublists'Aux}$, starting with the singleton list containing the empty list. More precisely: $$\text{sublists'}(l) = \text{foldr} \left(\lambda a \, r \mapsto \text{sublists'Aux}(a, r, r)\right) \left[ \left[ \right] \right] l$$
List.sublists'Aux_eq_map theorem
(a : α) (r₁ : List (List α)) : ∀ (r₂ : List (List α)), sublists'Aux a r₁ r₂ = r₂ ++ map (cons a) r₁
Full source 
theorem sublists'Aux_eq_map (a : α) (r₁ : List (List α)) : ∀ (r₂ : List (List α)),
    sublists'Aux a r₁ r₂ = r₂ ++ map (cons a) r₁ :=
  List.reverseRecOn r₁ (fun _ => by simp [sublists'Aux]) fun r₁ l ih r₂ => by
    rw [map_append, map_singleton, ← append_assoc, ← ih, sublists'Aux, foldl_append, foldl]
    simp [sublists'Aux]
Auxiliary Sublist Construction via Concatenation and Mapping
Informal description
For any element $a$ of type $\alpha$ and any list $r_1$ of lists of $\alpha$, the auxiliary function `sublists'Aux` satisfies the equation: \[ \text{sublists'Aux}(a, r_1, r_2) = r_2 \mathbin{+\kern-1.5ex+} \text{map} (\text{cons } a) r_1 \] for any list $r_2$ of lists of $\alpha$, where $\mathbin{+\kern-1.5ex+}$ denotes list concatenation and $\text{cons } a$ denotes prepending $a$ to a list.
List.sublists'_cons theorem
(a : α) (l : List α) : sublists' (a :: l) = sublists' l ++ map (cons a) (sublists' l)
Full source 
@[simp 900]
theorem sublists'_cons (a : α) (l : List α) :
    sublists' (a :: l) = sublists' l ++ map (cons a) (sublists' l) := by
  simp [sublists'_eq_sublists'Aux, foldr_cons, sublists'Aux_eq_map]
Sublist Generation for Cons List: $\text{sublists'}(a :: l) = \text{sublists'}(l) \mathbin{+\kern-1.5ex+} \text{map} (\text{cons } a) (\text{sublists'}(l))$
Informal description
For any element $a$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the list of all sublists of $a :: l$ is equal to the concatenation of the list of all sublists of $l$ with the list obtained by prepending $a$ to each sublist of $l$. More precisely: $$\text{sublists'}(a :: l) = \text{sublists'}(l) \mathbin{+\kern-1.5ex+} \text{map} (\text{cons } a) (\text{sublists'}(l))$$
List.mem_sublists' theorem
{s t : List α} : s ∈ sublists' t ↔ s <+ t
Full source 
@[simp]
theorem mem_sublists' {s t : List α} : s ∈ sublists' ts ∈ sublists' t ↔ s <+ t := by
  induction' t with a t IH generalizing s
  · simp only [sublists'_nil, mem_singleton]
    exact ⟨fun h => by rw [h], eq_nil_of_sublist_nil⟩
  simp only [sublists'_cons, mem_append, IH, mem_map]
  constructor <;> intro h
  · rcases h with (h | ⟨s, h, rfl⟩)
    · exact sublist_cons_of_sublist _ h
    · exact h.cons_cons _
  · obtain - | ⟨-, h⟩ | ⟨-, h⟩ := h
    · exact Or.inl h
    · exact Or.inr ⟨_, h, rfl⟩
Sublist Membership Characterization: $s \in \text{sublists'}(t) \leftrightarrow s \subseteq t$
Informal description
For any two lists $s$ and $t$ of elements of type $\alpha$, the list $s$ is an element of the list of all sublists of $t$ if and only if $s$ is a sublist of $t$ (not necessarily contiguous).
List.length_sublists' theorem
: ∀ l : List α, length (sublists' l) = 2 ^ length l
Full source 
@[simp]
theorem length_sublists' : ∀ l : List α, length (sublists' l) = 2 ^ length l
  | [] => rfl
  | a :: l => by
    simp +arith only [sublists'_cons, length_append, length_sublists' l,
      length_map, length, Nat.pow_succ']
Cardinality of Sublists: $|\text{sublists'}(l)| = 2^{|l|}$
Informal description
For any list $l$ of elements of type $\alpha$, the length of the list of all sublists of $l$ is equal to $2$ raised to the power of the length of $l$, i.e., $$|\text{sublists'}(l)| = 2^{|l|}.$$
List.sublists_nil theorem
: sublists (@nil α) = [[]]
Full source 
@[simp]
theorem sublists_nil : sublists (@nil α) = [[]] :=
  rfl
Sublists of Empty List
Informal description
The list of all sublists of the empty list `[]` is the singleton list containing only the empty list, i.e., `sublists([]) = [[]]`.
List.sublists_singleton theorem
(a : α) : sublists [a] = [[], [a]]
Full source 
@[simp]
theorem sublists_singleton (a : α) : sublists [a] = [[], [a]] :=
  rfl
Sublists of Singleton List
Informal description
For any element $a$ of type $\alpha$, the list of all sublists of the singleton list $[a]$ is equal to the list $[[], [a]]$.
List.sublistsAux definition
(a : α) (r : List (List α)) : List (List α)
Full source 
/-- Auxiliary helper function for `sublists` -/
def sublistsAux (a : α) (r : List (List α)) : List (List α) :=
  r.foldl (init := []) fun r l => r ++ [l, a :: l]
Auxiliary function for generating sublists
Informal description
The auxiliary function `sublistsAux` takes an element `a` of type `α` and a list of lists `r : List (List α)`, and returns a new list of lists obtained by appending to `r` each list in `r` both as-is and with `a` prepended.
List.sublistsAux_eq_array_foldl theorem
: sublistsAux = fun (a : α) (r : List (List α)) => (r.toArray.foldl (init := #[]) fun r l => (r.push l).push (a :: l)).toList
Full source 
theorem sublistsAux_eq_array_foldl :
    sublistsAux = fun (a : α) (r : List (List α)) =>
      (r.toArray.foldl (init := #[])
        fun r l => (r.push l).push (a :: l)).toList := by
  funext a r
  simp only [sublistsAux, Array.foldl_toList, Array.mkEmpty]
  have := foldl_hom Array.toList (g₁ := fun r l => (r.push l).push (a :: l))
    (g₂ := fun r l => r ++ [l, a :: l]) (l := r) (init := #[]) (by simp)
  simpa using this
Equivalence of Sublist Generation via Array Fold
Informal description
The auxiliary function `sublistsAux` is equal to the function that converts the input list `r` to an array, folds over it starting with an empty array, and for each sublist `l` in `r`, appends both `l` and `a :: l` to the accumulator, then converts the result back to a list. In other words, `sublistsAux a r` is equivalent to `(r.toArray.foldl (init := #[]) fun r l => (r.push l).push (a :: l)).toList`.
List.sublistsAux_eq_flatMap theorem
: sublistsAux = fun (a : α) (r : List (List α)) => r.flatMap fun l => [l, a :: l]
Full source 
theorem sublistsAux_eq_flatMap :
    sublistsAux = fun (a : α) (r : List (List α)) => r.flatMap fun l => [l, a :: l] :=
  funext fun a => funext fun r =>
  List.reverseRecOn r
    (by simp [sublistsAux])
    (fun r l ih => by
      rw [flatMap_append, ← ih, flatMap_singleton, sublistsAux, foldl_append]
      simp [sublistsAux])
Sublist Auxiliary Function as FlatMap
Informal description
The auxiliary function `sublistsAux` for generating sublists is equal to the function that takes an element $a$ of type $\alpha$ and a list of lists $r$, and returns the concatenation of all lists obtained by mapping each list $l$ in $r$ to both $l$ itself and the list $a :: l$ (i.e., $l$ with $a$ prepended).
List.sublists_eq_sublistsFast theorem
: @sublists = @sublistsFast
Full source 
@[csimp] theorem sublists_eq_sublistsFast : @sublists = @sublistsFast := by
  ext α l : 2
  trans l.foldr sublistsAux [[]]
  · rw [sublistsAux_eq_flatMap, sublists]
  · simp only [sublistsFast, sublistsAux_eq_array_foldl, Array.foldr_toList]
    rw [← foldr_hom Array.toList]
    · intros _ _; congr
Equality of Sublist Generation Functions: `sublists = sublistsFast`
Informal description
The function `sublists` that generates all sublists of a given list is equal to the optimized function `sublistsFast` for the same purpose.
List.sublists_append theorem
(l₁ l₂ : List α) : sublists (l₁ ++ l₂) = (sublists l₂) >>= (fun x => (sublists l₁).map (· ++ x))
Full source 
theorem sublists_append (l₁ l₂ : List α) :
    sublists (l₁ ++ l₂) = (sublists l₂) >>= (fun x => (sublists l₁).map (· ++ x)) := by
  simp only [sublists, foldr_append]
  induction l₁ with
  | nil => simp
  | cons a l₁ ih =>
    rw [foldr_cons, ih]
    simp [List.flatMap, flatten_flatten, Function.comp_def]
Sublists of Concatenated Lists
Informal description
For any two lists $l₁$ and $l₂$ of elements of type $\alpha$, the list of all sublists of the concatenated list $l₁ ++ l₂$ is equal to the concatenation of all lists obtained by appending each sublist of $l₂$ to each sublist of $l₁$. More formally, $\text{sublists}(l₁ ++ l₂) = \text{sublists}(l₂) \gg= (\lambda x, \text{sublists}(l₁).\text{map}(\cdot ++ x))$.
List.sublists_cons theorem
(a : α) (l : List α) : sublists (a :: l) = sublists l >>= (fun x => [x, a :: x])
Full source 
theorem sublists_cons (a : α) (l : List α) :
    sublists (a :: l) = sublistssublists l >>= (fun x => [x, a :: x]) :=
  show sublists ([a] ++ l) = _ by
  rw [sublists_append]
  simp only [sublists_singleton, map_cons, bind_eq_flatMap, nil_append, cons_append, map_nil]
Sublists of a Cons List
Informal description
For any element $a$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the list of all sublists of the list $a :: l$ is equal to the concatenation of all lists obtained by taking each sublist $x$ of $l$ and producing both $x$ and $a :: x$. More formally, $\text{sublists}(a :: l) = \text{sublists}(l) \gg= (\lambda x, [x, a :: x])$.
List.sublists_concat theorem
(l : List α) (a : α) : sublists (l ++ [a]) = sublists l ++ map (fun x => x ++ [a]) (sublists l)
Full source 
@[simp]
theorem sublists_concat (l : List α) (a : α) :
    sublists (l ++ [a]) = sublists l ++ map (fun x => x ++ [a]) (sublists l) := by
  rw [sublists_append, sublists_singleton, bind_eq_flatMap, flatMap_cons, flatMap_cons, flatMap_nil,
     map_id'' append_nil, append_nil]
Sublists of List Concatenated with Singleton
Informal description
For any list $l$ of elements of type $\alpha$ and any element $a : \alpha$, the list of all sublists of the concatenated list $l ++ [a]$ is equal to the concatenation of the list of sublists of $l$ and the list obtained by appending $[a]$ to each sublist of $l$. More formally, $\text{sublists}(l ++ [a]) = \text{sublists}(l) ++ \text{map}(\lambda x, x ++ [a]) (\text{sublists}(l))$.
List.sublists_reverse theorem
(l : List α) : sublists (reverse l) = map reverse (sublists' l)
Full source 
theorem sublists_reverse (l : List α) : sublists (reverse l) = map reverse (sublists' l) := by
  induction' l with hd tl ih <;> [rfl;
    simp only [reverse_cons, sublists_append, sublists'_cons, map_append, ih, sublists_singleton,
      map_eq_map, bind_eq_flatMap, map_map, flatMap_cons, append_nil, flatMap_nil,
      Function.comp_def]]
Sublists of Reversed List via Reversed Sublists'
Informal description
For any list $l$ of elements of type $\alpha$, the list of all sublists of the reversed list $\text{reverse}(l)$ is equal to the list obtained by reversing each sublist in the list of all sublists of $l$ (computed via $\text{sublists'}$). More formally: $$\text{sublists}(\text{reverse}(l)) = \text{map reverse} (\text{sublists'}(l))$$
List.sublists_eq_sublists' theorem
(l : List α) : sublists l = map reverse (sublists' (reverse l))
Full source 
theorem sublists_eq_sublists' (l : List α) : sublists l = map reverse (sublists' (reverse l)) := by
  rw [← sublists_reverse, reverse_reverse]
Equivalence of Sublists and Reversed Sublists' of Reversed List
Informal description
For any list $l$ of elements of type $\alpha$, the list of all sublists of $l$ is equal to the list obtained by reversing each sublist in the list of all sublists (computed via $\text{sublists'}$) of the reversed list $\text{reverse}(l)$. More formally: $$\text{sublists}(l) = \text{map reverse} (\text{sublists'}(\text{reverse}(l)))$$
List.sublists'_reverse theorem
(l : List α) : sublists' (reverse l) = map reverse (sublists l)
Full source 
theorem sublists'_reverse (l : List α) : sublists' (reverse l) = map reverse (sublists l) := by
  simp only [sublists_eq_sublists', map_map, map_id'' reverse_reverse, Function.comp_def]
Sublists' of Reversed List Equals Reversed Sublists
Informal description
For any list $l$ of elements of type $\alpha$, the list of all sublists (computed via $\text{sublists'}$) of the reversed list $\text{reverse}(l)$ is equal to the list obtained by reversing each sublist in the list of all sublists of $l$. More formally: $$\text{sublists'}(\text{reverse}(l)) = \text{map reverse} (\text{sublists}(l))$$
List.sublists'_eq_sublists theorem
(l : List α) : sublists' l = map reverse (sublists (reverse l))
Full source 
theorem sublists'_eq_sublists (l : List α) : sublists' l = map reverse (sublists (reverse l)) := by
  rw [← sublists'_reverse, reverse_reverse]
Equivalence of Sublists' and Reversed Sublists of Reversed List
Informal description
For any list $l$ of elements of type $\alpha$, the list of all sublists (computed via $\text{sublists'}$) of $l$ is equal to the list obtained by reversing each sublist in the list of all sublists of the reversed list $\text{reverse}(l)$. More formally: $$\text{sublists'}(l) = \text{map reverse} (\text{sublists}(\text{reverse}(l)))$$
List.mem_sublists theorem
{s t : List α} : s ∈ sublists t ↔ s <+ t
Full source 
@[simp]
theorem mem_sublists {s t : List α} : s ∈ sublists ts ∈ sublists t ↔ s <+ t := by
  rw [← reverse_sublist, ← mem_sublists', sublists'_reverse,
    mem_map_of_injective reverse_injective]
Sublist Membership Characterization: $s \in \text{sublists}(t) \leftrightarrow s \subseteq t$
Informal description
For any two lists $s$ and $t$ of elements of type $\alpha$, the list $s$ is an element of the list of all sublists of $t$ if and only if $s$ is a sublist of $t$ (not necessarily contiguous). More formally: $$s \in \text{sublists}(t) \leftrightarrow s \subseteq t$$
List.length_sublists theorem
(l : List α) : length (sublists l) = 2 ^ length l
Full source 
@[simp]
theorem length_sublists (l : List α) : length (sublists l) = 2 ^ length l := by
  simp only [sublists_eq_sublists', length_map, length_sublists', length_reverse]
Cardinality of Sublists: $|\text{sublists}(l)| = 2^{|l|}$
Informal description
For any list $l$ of elements of type $\alpha$, the length of the list of all sublists of $l$ is equal to $2$ raised to the power of the length of $l$, i.e., $$|\text{sublists}(l)| = 2^{|l|}.$$
List.map_pure_sublist_sublists theorem
(l : List α) : map pure l <+ sublists l
Full source 
theorem map_pure_sublist_sublists (l : List α) : mapmap pure l <+ sublists l := by
  induction' l using reverseRecOn with l a ih <;> simp only [map, map_append, sublists_concat]
  · simp only [sublists_nil, sublist_cons_self]
  exact ((append_sublist_append_left _).2 <|
              singleton_sublist.2 <| mem_map.2 ⟨[], mem_sublists.2 (nil_sublist _), by rfl⟩).trans
          ((append_sublist_append_right _).2 ih)
Inclusion of Singleton Sublists in All Sublists: $\text{map}(\text{pure}, l) \subseteq \text{sublists}(l)$
Informal description
For any list $l$ of elements of type $\alpha$, the list obtained by mapping the singleton list constructor $\text{pure}$ over $l$ is a sublist of the list of all sublists of $l$. In other words, the list of all single-element sublists of $l$ is a sublist of the list of all possible sublists of $l$. More formally: $$\text{map}(\text{pure}, l) \subseteq \text{sublists}(l)$$
List.sublistsLenAux definition
: ℕ → List α → (List α → β) → List β → List β
Full source 
/-- Auxiliary function to construct the list of all sublists of a given length. Given an
integer `n`, a list `l`, a function `f` and an auxiliary list `L`, it returns the list made of
`f` applied to all sublists of `l` of length `n`, concatenated with `L`. -/
def sublistsLenAux : ℕ → List α → (List α → β) → List β → List β
  | 0, _, f, r => f [] :: r
  | _ + 1, [], _, r => r
  | n + 1, a :: l, f, r => sublistsLenAux (n + 1) l f (sublistsLenAux n l (f ∘ List.cons a) r)
Auxiliary function for generating length-`n` sublists
Informal description
The auxiliary function `sublistsLenAux` constructs the list of all sublists of a given length `n` from a list `l`. It takes as input: - A natural number `n` (the desired sublist length) - A list `l` of type `α` - A function `f` that processes each sublist (of type `List α → β`) - An accumulator list `r` of type `List β` The function returns a new list where: 1. When `n = 0`, it prepends `f []` to `r` (the empty sublist) 2. When the input list is empty (and `n > 0`), it returns `r` unchanged 3. Otherwise, it recursively processes: - All sublists containing the head element `a` (via composition with `List.cons a`) - All sublists not containing the head element (via direct recursion on the tail) The results are accumulated in `r` through the recursion.
List.sublistsLen definition
(n : ℕ) (l : List α) : List (List α)
Full source 
/-- The list of all sublists of a list `l` that are of length `n`. For instance, for
`l = [0, 1, 2, 3]` and `n = 2`, one gets
`[[2, 3], [1, 3], [1, 2], [0, 3], [0, 2], [0, 1]]`. -/
def sublistsLen (n : ℕ) (l : List α) : List (List α) :=
  sublistsLenAux n l id []
List of length-$n$ sublists
Informal description
For a given natural number $n$ and a list $l$ of elements of type $\alpha$, the function returns the list of all sublists of $l$ that have length exactly $n$. The sublists are not necessarily contiguous in the original list. For example, for $l = [0, 1, 2, 3]$ and $n = 2$, the result would be $[[2, 3], [1, 3], [1, 2], [0, 3], [0, 2], [0, 1]]$.
List.sublistsLenAux_append theorem
: ∀ (n : ℕ) (l : List α) (f : List α → β) (g : β → γ) (r : List β) (s : List γ), sublistsLenAux n l (g ∘ f) (r.map g ++ s) = (sublistsLenAux n l f r).map g ++ s
Full source 
theorem sublistsLenAux_append :
    ∀ (n : ℕ) (l : List α) (f : List α → β) (g : β → γ) (r : List β) (s : List γ),
      sublistsLenAux n l (g ∘ f) (r.map g ++ s) = (sublistsLenAux n l f r).map g ++ s
  | 0, l, f, g, r, s => by unfold sublistsLenAux; simp
  | _ + 1, [], _, _, _, _ => rfl
  | n + 1, a :: l, f, g, r, s => by
    unfold sublistsLenAux
    simp only [show (g ∘ f) ∘ List.cons a = g ∘ f ∘ List.cons a by rfl, sublistsLenAux_append,
      sublistsLenAux_append]
Composition and Concatenation Property of sublistsLenAux
Informal description
For any natural number $n$, list $l$ of type $\alpha$, functions $f : \text{List } \alpha \to \beta$ and $g : \beta \to \gamma$, and lists $r$ of type $\text{List } \beta$ and $s$ of type $\text{List } \gamma$, the following equality holds: $$\text{sublistsLenAux } n\ l\ (g \circ f)\ (\text{map } g\ r \mathbin{+\!\!+} s) = \text{map } g\ (\text{sublistsLenAux } n\ l\ f\ r) \mathbin{+\!\!+} s$$ where: - $\text{sublistsLenAux}$ is the auxiliary function that generates all sublists of length $n$ from $l$ - $\circ$ denotes function composition - $\mathbin{+\!\!+}$ denotes list concatenation - $\text{map } g\ r$ applies $g$ to each element of $r$
List.sublistsLenAux_eq theorem
(l : List α) (n) (f : List α → β) (r) : sublistsLenAux n l f r = (sublistsLen n l).map f ++ r
Full source 
theorem sublistsLenAux_eq (l : List α) (n) (f : List α → β) (r) :
    sublistsLenAux n l f r = (sublistsLen n l).map f ++ r := by
  rw [sublistsLen, ← sublistsLenAux_append]; rfl
Equivalence of sublistsLenAux and Mapping sublistsLen
Informal description
For any list $l$ of elements of type $\alpha$, natural number $n$, function $f : \text{List } \alpha \to \beta$, and accumulator list $r$ of type $\text{List } \beta$, the auxiliary function `sublistsLenAux` satisfies: $$\text{sublistsLenAux } n\ l\ f\ r = \text{map } f\ (\text{sublistsLen } n\ l) \mathbin{+\!\!+} r$$ where: - $\text{sublistsLen } n\ l$ generates all sublists of $l$ with length exactly $n$ - $\mathbin{+\!\!+}$ denotes list concatenation - $\text{map } f$ applies $f$ to each sublist in $\text{sublistsLen } n\ l$
List.sublistsLenAux_zero theorem
(l : List α) (f : List α → β) (r) : sublistsLenAux 0 l f r = f [] :: r
Full source 
theorem sublistsLenAux_zero (l : List α) (f : List α → β) (r) :
    sublistsLenAux 0 l f r = f [] :: r := by cases l <;> rfl
Base case of sublistsLenAux for length zero
Informal description
For any list $l$ of type $\alpha$, any function $f$ from lists of $\alpha$ to $\beta$, and any accumulator list $r$ of type $\beta$, the auxiliary function `sublistsLenAux` with length parameter $0$ satisfies: $$\text{sublistsLenAux}\ 0\ l\ f\ r = f([]) :: r$$
List.sublistsLen_zero theorem
(l : List α) : sublistsLen 0 l = [[]]
Full source 
@[simp]
theorem sublistsLen_zero (l : List α) : sublistsLen 0 l = [[]] :=
  sublistsLenAux_zero _ _ _
Zero-length Sublists are Only the Empty List
Informal description
For any list $l$ of elements of type $\alpha$, the list of all sublists of $l$ with length exactly $0$ is the singleton list containing the empty list, i.e., $\text{sublistsLen}\ 0\ l = [[]]$.
List.sublistsLen_succ_nil theorem
(n) : sublistsLen (n + 1) (@nil α) = []
Full source 
@[simp]
theorem sublistsLen_succ_nil (n) : sublistsLen (n + 1) (@nil α) = [] :=
  rfl
No Sublists of Positive Length in Empty List
Informal description
For any natural number $n$, the list of all sublists of length $n+1$ of the empty list is the empty list, i.e., $\text{sublistsLen}(n+1, []) = []$.
List.sublistsLen_succ_cons theorem
(n) (a : α) (l) : sublistsLen (n + 1) (a :: l) = sublistsLen (n + 1) l ++ (sublistsLen n l).map (cons a)
Full source 
@[simp]
theorem sublistsLen_succ_cons (n) (a : α) (l) :
    sublistsLen (n + 1) (a :: l) = sublistsLen (n + 1) l ++ (sublistsLen n l).map (cons a) := by
  rw [sublistsLen, sublistsLenAux, sublistsLenAux_eq, sublistsLenAux_eq, map_id,
      append_nil]; rfl
Recursive Construction of Sublists of Length $n+1$ via Cons
Informal description
For any natural number $n$, element $a$ of type $\alpha$, and list $l$ of elements of type $\alpha$, the list of all sublists of length $n+1$ of the list $a :: l$ is equal to the concatenation of: 1. The list of all sublists of length $n+1$ of $l$, and 2. The list obtained by prepending $a$ to each sublist of length $n$ of $l$. In symbols: $$\text{sublistsLen}(n+1, a :: l) = \text{sublistsLen}(n+1, l) \mathbin{+\!\!+} \text{map}\ (\text{cons}\ a)\ (\text{sublistsLen}\ n\ l)$$
List.sublistsLen_one theorem
(l : List α) : sublistsLen 1 l = l.reverse.map ([·])
Full source 
theorem sublistsLen_one (l : List α) : sublistsLen 1 l = l.reverse.map ([·]) :=
  l.rec (by rw [sublistsLen_succ_nil, reverse_nil, map_nil]) fun a s ih ↦ by
    rw [sublistsLen_succ_cons, ih, reverse_cons, map_append, sublistsLen_zero]; rfl
Sublists of Length One are Singletons of Reversed List Elements
Informal description
For any list $l$ of elements of type $\alpha$, the list of all sublists of $l$ with length exactly 1 is equal to the list obtained by reversing $l$ and then mapping each element $x$ to the singleton list $[x]$.
List.length_sublistsLen theorem
: ∀ (n) (l : List α), length (sublistsLen n l) = Nat.choose (length l) n
Full source 
@[simp]
theorem length_sublistsLen :
    ∀ (n) (l : List α), length (sublistsLen n l) = Nat.choose (length l) n
  | 0, l => by simp
  | _ + 1, [] => by simp
  | n + 1, a :: l => by
    rw [sublistsLen_succ_cons, length_append, length_sublistsLen (n+1) l,
      length_map, length_sublistsLen n l, length_cons, Nat.choose_succ_succ, Nat.add_comm]
Cardinality of Length-$n$ Sublists: $\text{length}(\text{sublistsLen}(n, l)) = \binom{\text{length}(l)}{n}$
Informal description
For any natural number $n$ and any list $l$ of elements of type $\alpha$, the number of sublists of $l$ with length exactly $n$ is equal to the binomial coefficient $\binom{\text{length}(l)}{n}$.
List.sublistsLen_sublist_sublists' theorem
: ∀ (n) (l : List α), sublistsLen n l <+ sublists' l
Full source 
theorem sublistsLen_sublist_sublists' :
    ∀ (n) (l : List α), sublistsLensublistsLen n l <+ sublists' l
  | 0, l => by simp
  | _ + 1, [] => nil_sublist _
  | n + 1, a :: l => by
    rw [sublistsLen_succ_cons, sublists'_cons]
    exact (sublistsLen_sublist_sublists' _ _).append ((sublistsLen_sublist_sublists' _ _).map _)
Sublists of Fixed Length are Sublists of All Sublists
Informal description
For any natural number $n$ and any list $l$ of elements of type $\alpha$, the list of all sublists of $l$ with length exactly $n$ is a sublist of the list of all (not necessarily contiguous) sublists of $l$. In symbols: $$\text{sublistsLen}(n, l) \subseteq \text{sublists'}(l)$$
List.sublistsLen_sublist_of_sublist theorem
(n) {l₁ l₂ : List α} (h : l₁ <+ l₂) : sublistsLen n l₁ <+ sublistsLen n l₂
Full source 
theorem sublistsLen_sublist_of_sublist (n) {l₁ l₂ : List α} (h : l₁ <+ l₂) :
    sublistsLensublistsLen n l₁ <+ sublistsLen n l₂ := by
  induction' n with n IHn generalizing l₁ l₂; · simp
  induction h with
  | slnil => rfl
  | cons a _ IH =>
    refine IH.trans ?_
    rw [sublistsLen_succ_cons]
    apply sublist_append_left
  | cons₂ a s IH => simpa only [sublistsLen_succ_cons] using IH.append ((IHn s).map _)
Sublist Preservation under Length-$n$ Sublists Construction
Informal description
For any natural number $n$ and lists $l₁, l₂$ of elements of type $\alpha$, if $l₁$ is a sublist of $l₂$, then the list of all length-$n$ sublists of $l₁$ is a sublist of the list of all length-$n$ sublists of $l₂$.
List.length_of_sublistsLen theorem
: ∀ {n} {l l' : List α}, l' ∈ sublistsLen n l → length l' = n
Full source 
theorem length_of_sublistsLen :
    ∀ {n} {l l' : List α}, l' ∈ sublistsLen n l → length l' = n
  | 0, l, l', h => by simp_all
  | n + 1, a :: l, l', h => by
    rw [sublistsLen_succ_cons, mem_append, mem_map] at h
    rcases h with (h | ⟨l', h, rfl⟩)
    · exact length_of_sublistsLen h
    · exact congr_arg (· + 1) (length_of_sublistsLen h)
Sublists in $\text{sublistsLen}\ n\ l$ have length $n$
Informal description
For any natural number $n$ and lists $l, l'$ of elements of type $\alpha$, if $l'$ is in the list of sublists of $l$ with length $n$, then the length of $l'$ is equal to $n$. In other words, all sublists in $\text{sublistsLen}\ n\ l$ have length exactly $n$.
List.mem_sublistsLen_self theorem
{l l' : List α} (h : l' <+ l) : l' ∈ sublistsLen (length l') l
Full source 
theorem mem_sublistsLen_self {l l' : List α} (h : l' <+ l) :
    l' ∈ sublistsLen (length l') l := by
  induction h with
  | slnil => simp
  | @cons l₁ l₂ a s IH =>
    rcases l₁ with - | ⟨b, l₁⟩
    · simp
    · rw [length, sublistsLen_succ_cons]
      exact mem_append_left _ IH
  | cons₂ a s IH =>
    rw [length, sublistsLen_succ_cons]
    exact mem_append_right _ (mem_map.2 ⟨_, IH, rfl⟩)
Sublist Membership in Sublists of Matching Length
Informal description
For any lists $l$ and $l'$ of elements of type $\alpha$, if $l'$ is a sublist of $l$, then $l'$ is contained in the list of all sublists of $l$ that have length equal to the length of $l'$. In other words, $l' \in \text{sublistsLen}\ (\text{length}\ l')\ l$.
List.mem_sublistsLen theorem
{n} {l l' : List α} : l' ∈ sublistsLen n l ↔ l' <+ l ∧ length l' = n
Full source 
@[simp]
theorem mem_sublistsLen {n} {l l' : List α} :
    l' ∈ sublistsLen n ll' ∈ sublistsLen n l ↔ l' <+ l ∧ length l' = n :=
  ⟨fun h =>
    ⟨mem_sublists'.1 ((sublistsLen_sublist_sublists' _ _).subset h), length_of_sublistsLen h⟩,
    fun ⟨h₁, h₂⟩ => h₂ ▸ mem_sublistsLen_self h₁⟩
Characterization of Membership in Length-$n$ Sublists: $l' \in \text{sublistsLen}(n, l) \leftrightarrow (l' \subseteq l) \land (\text{length}(l') = n)$
Informal description
For any natural number $n$ and lists $l, l'$ of elements of type $\alpha$, the list $l'$ is in the list of all length-$n$ sublists of $l$ if and only if $l'$ is a sublist of $l$ and the length of $l'$ is equal to $n$. In symbols: $$l' \in \text{sublistsLen}(n, l) \leftrightarrow (l' \subseteq l) \land (\text{length}(l') = n)$$
List.sublistsLen_of_length_lt theorem
{n} {l : List α} (h : l.length < n) : sublistsLen n l = []
Full source 
theorem sublistsLen_of_length_lt {n} {l : List α} (h : l.length < n) : sublistsLen n l = [] :=
  eq_nil_iff_forall_not_mem.mpr fun _ =>
    mem_sublistsLen.not.mpr fun ⟨hs, hl⟩ => (h.trans_eq hl.symm).not_le (Sublist.length_le hs)
Empty Sublists for Length Exceeding List Size
Informal description
For any natural number $n$ and list $l$ of elements of type $\alpha$, if the length of $l$ is strictly less than $n$, then the list of all length-$n$ sublists of $l$ is empty. In symbols: $$\text{length}(l) < n \implies \text{sublistsLen}(n, l) = []$$
List.sublistsLen_length theorem
: ∀ l : List α, sublistsLen l.length l = [l]
Full source 
@[simp]
theorem sublistsLen_length : ∀ l : List α, sublistsLen l.length l = [l]
  | [] => rfl
  | a :: l => by
    simp only [length, sublistsLen_succ_cons, sublistsLen_length, map,
      sublistsLen_of_length_lt (lt_succ_self _), nil_append]
Only the Full List is a Sublist of Its Own Length
Informal description
For any list $l$ of elements of type $\alpha$, the list of all sublists of $l$ that have the same length as $l$ is exactly the singleton list containing $l$ itself. In symbols: $$\text{sublistsLen}(\text{length}(l), l) = [l]$$
List.Pairwise.sublists' theorem
{R} : ∀ {l : List α}, Pairwise R l → Pairwise (Lex (swap R)) (sublists' l)
Full source 
theorem Pairwise.sublists' {R} :
    ∀ {l : List α}, Pairwise R l → Pairwise (Lex (swap R)) (sublists' l)
  | _, Pairwise.nil => pairwise_singleton _ _
  | _, @Pairwise.cons _ _ a l H₁ H₂ => by
    simp only [sublists'_cons, pairwise_append, pairwise_map, mem_sublists', mem_map, exists_imp,
      and_imp]
    refine ⟨H₂.sublists', H₂.sublists'.imp fun l₁ => Lex.cons l₁, ?_⟩
    rintro l₁ sl₁ x l₂ _ rfl
    rcases l₁ with - | ⟨b, l₁⟩; · constructor
    exact Lex.rel (H₁ _ <| sl₁.subset mem_cons_self)
Pairwise Sublists under Lexicographic Order of Swapped Relation
Informal description
For any binary relation $R$ on a type $\alpha$ and any list $l$ of elements of type $\alpha$, if $l$ is pairwise with respect to $R$, then the list of all sublists of $l$ is pairwise with respect to the lexicographic order of the swapped relation $\operatorname{swap} R$. More precisely: If $\text{Pairwise } R\, l$ holds, then $\text{Pairwise } (\text{Lex } (\operatorname{swap} R))\, (\text{sublists' } l)$ also holds.
List.pairwise_sublists theorem
{R} {l : List α} (H : Pairwise R l) : Pairwise (Lex R on reverse) (sublists l)
Full source 
theorem pairwise_sublists {R} {l : List α} (H : Pairwise R l) :
    Pairwise (LexLex R on reverse) (sublists l) := by
  have := (pairwise_reverse.2 H).sublists'
  rwa [sublists'_reverse, pairwise_map] at this
Pairwise Sublists under Lexicographic Order of Relation Composed with Reverse
Informal description
For any binary relation $R$ on a type $\alpha$ and any list $l$ of elements of type $\alpha$, if $l$ is pairwise with respect to $R$, then the list of all sublists of $l$ is pairwise with respect to the lexicographic order of $R$ composed with the reverse operation on lists. More precisely, if $\text{Pairwise } R\, l$ holds, then $\text{Pairwise } (\text{Lex } R \text{ on reverse})\, (\text{sublists } l)$ also holds.
List.nodup_sublists theorem
{l : List α} : Nodup (sublists l) ↔ Nodup l
Full source 
@[simp]
theorem nodup_sublists {l : List α} : NodupNodup (sublists l) ↔ Nodup l :=
  ⟨fun h => (h.sublist (map_pure_sublist_sublists _)).of_map _, fun h =>
    (pairwise_sublists h).imp @fun l₁ l₂ h => by simpa using h.to_ne⟩
Distinctness of Sublists is Equivalent to Distinctness of Original List
Informal description
For any list $l$ of elements of type $\alpha$, the list of all sublists of $l$ has no duplicate elements if and only if $l$ itself has no duplicate elements.
List.nodup_sublists' theorem
{l : List α} : Nodup (sublists' l) ↔ Nodup l
Full source 
@[simp]
theorem nodup_sublists' {l : List α} : NodupNodup (sublists' l) ↔ Nodup l := by
  rw [sublists'_eq_sublists, nodup_map_iff reverse_injective, nodup_sublists, nodup_reverse]
Distinctness of Sublists' is Equivalent to Distinctness of Original List
Informal description
For any list $l$ of elements of type $\alpha$, the list of all sublists of $l$ (computed via `sublists'`) has no duplicate elements if and only if $l$ itself has no duplicate elements.
List.nodup_sublistsLen theorem
(n : ℕ) {l : List α} (h : Nodup l) : (sublistsLen n l).Nodup
Full source 
theorem nodup_sublistsLen (n : ℕ) {l : List α} (h : Nodup l) : (sublistsLen n l).Nodup := by
  have : Pairwise (· ≠ ·) l.sublists' := Pairwise.imp
    (fun h => Lex.to_ne (by convert h using 3; simp [swap, eq_comm])) h.sublists'
  exact this.sublist (sublistsLen_sublist_sublists' _ _)
Distinctness of Fixed-Length Sublists from Distinct Lists
Informal description
For any natural number $n$ and any list $l$ of distinct elements of type $\alpha$, the list of all sublists of $l$ with length exactly $n$ consists of distinct elements.
List.sublists_map theorem
(f : α → β) : ∀ (l : List α), sublists (map f l) = map (map f) (sublists l)
Full source 
theorem sublists_map (f : α → β) : ∀ (l : List α),
    sublists (map f l) = map (map f) (sublists l)
  | [] => by simp
  | a::l => by
    rw [map_cons, sublists_cons, bind_eq_flatMap, sublists_map f l, sublists_cons,
      bind_eq_flatMap, map_eq_flatMap, map_eq_flatMap]
    induction sublists l <;> simp [*]
Mapping Preserves Sublists: $\text{sublists}(\text{map}\,f\,l) = \text{map}\,(\text{map}\,f)\,(\text{sublists}\,l)$
Informal description
For any function $f : \alpha \to \beta$ and any list $l$ of elements of type $\alpha$, the list of all sublists of the mapped list $\text{map}\,f\,l$ is equal to the list obtained by applying $\text{map}\,f$ to each sublist of $l$. More formally, $\text{sublists}(\text{map}\,f\,l) = \text{map}\,(\text{map}\,f)\,(\text{sublists}\,l)$.
List.sublists'_map theorem
(f : α → β) : ∀ (l : List α), sublists' (map f l) = map (map f) (sublists' l)
Full source 
theorem sublists'_map (f : α → β) : ∀ (l : List α),
    sublists' (map f l) = map (map f) (sublists' l)
  | [] => by simp
  | a::l => by simp [map_cons, sublists'_cons, sublists'_map f l, Function.comp]
Sublist Mapping Preservation: $\text{sublists'}(\text{map}\,f\,l) = \text{map}\,(\text{map}\,f)\,(\text{sublists'}\,l)$
Informal description
For any function $f : \alpha \to \beta$ and any list $l$ of elements of type $\alpha$, the list of all sublists of the mapped list $\text{map}\,f\,l$ is equal to the list obtained by applying $\text{map}\,f$ to each sublist of $l$. More formally, $\text{sublists'}(\text{map}\,f\,l) = \text{map}\,(\text{map}\,f)\,(\text{sublists'}\,l)$.
List.sublists_perm_sublists' theorem
(l : List α) : sublists l ~ sublists' l
Full source 
theorem sublists_perm_sublists' (l : List α) : sublistssublists l ~ sublists' l := by
  rw [← finRange_map_get l, sublists_map, sublists'_map]
  apply Perm.map
  apply (perm_ext_iff_of_nodup _ _).mpr
  · simp
  · exact nodup_sublists.mpr (nodup_finRange _)
  · exact (nodup_sublists'.mpr (nodup_finRange _))
Permutation of Sublists Computations: $\text{sublists}(l) \sim \text{sublists'}(l)$
Informal description
For any list $l$ of elements of type $\alpha$, the list of all sublists of $l$ (computed via `sublists`) is a permutation of the list of all sublists of $l$ (computed via `sublists'`). In other words, $\text{sublists}(l) \sim \text{sublists'}(l)$, where $\sim$ denotes the permutation relation between lists.
List.sublists_cons_perm_append theorem
(a : α) (l : List α) : sublists (a :: l) ~ sublists l ++ map (cons a) (sublists l)
Full source 
theorem sublists_cons_perm_append (a : α) (l : List α) :
    sublistssublists (a :: l) ~ sublists l ++ map (cons a) (sublists l) :=
  Perm.trans (sublists_perm_sublists' _) <| by
  rw [sublists'_cons]
  exact Perm.append (sublists_perm_sublists' _).symm (Perm.map _ (sublists_perm_sublists' _).symm)
Permutation of Sublists for Cons List: $\text{sublists}(a :: l) \sim \text{sublists}(l) \mathbin{+\kern-1.5ex+} \text{map} (\text{cons } a) (\text{sublists}(l))$
Informal description
For any element $a$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the list of all sublists of $a :: l$ is a permutation of the concatenation of the list of all sublists of $l$ with the list obtained by prepending $a$ to each sublist of $l$. In other words: $$\text{sublists}(a :: l) \sim \text{sublists}(l) \mathbin{+\kern-1.5ex+} \text{map} (\text{cons } a) (\text{sublists}(l))$$ where $\sim$ denotes the permutation relation between lists.
List.revzip_sublists theorem
(l : List α) : ∀ l₁ l₂, (l₁, l₂) ∈ revzip l.sublists → l₁ ++ l₂ ~ l
Full source 
theorem revzip_sublists (l : List α) : ∀ l₁ l₂, (l₁, l₂)(l₁, l₂) ∈ revzip l.sublists → l₁ ++ l₂ ~ l := by
  rw [revzip]
  induction' l using List.reverseRecOn with l' a ih
  · intro l₁ l₂ h
    simp? at h says
      simp only [sublists_nil, reverse_cons, reverse_nil, nil_append, zip_cons_cons, zip_nil_right,
        mem_cons, Prod.mk.injEq, not_mem_nil, or_false] at h
    simp [h]
  · intro l₁ l₂ h
    rw [sublists_concat, reverse_append, zip_append (by simp), ← map_reverse, zip_map_right,
      zip_map_left] at *
    simp only [Prod.mk_inj, mem_map, mem_append, Prod.map_apply, Prod.exists] at h
    rcases h with (⟨l₁, l₂', h, rfl, rfl⟩ | ⟨l₁', l₂, h, rfl, rfl⟩)
    · rw [← append_assoc]
      exact (ih _ _ h).append_right _
    · rw [append_assoc]
      apply (perm_append_comm.append_left _).trans
      rw [← append_assoc]
      exact (ih _ _ h).append_right _
Concatenation of Sublist Pairs in Reverse Zip is Permutation of Original List
Informal description
For any list $l$ of elements of type $\alpha$, and for any two sublists $l_1$ and $l_2$ such that $(l_1, l_2)$ is in the reverse zip of the list of all sublists of $l$, the concatenation of $l_1$ and $l_2$ is a permutation of $l$. In other words, if $(l_1, l_2) \in \text{revzip}(\text{sublists}(l))$, then $l_1 \mathbin{+\kern-1.5ex+} l_2$ is a permutation of $l$.
List.revzip_sublists' theorem
(l : List α) : ∀ l₁ l₂, (l₁, l₂) ∈ revzip l.sublists' → l₁ ++ l₂ ~ l
Full source 
theorem revzip_sublists' (l : List α) : ∀ l₁ l₂, (l₁, l₂)(l₁, l₂) ∈ revzip l.sublists' → l₁ ++ l₂ ~ l := by
  rw [revzip]
  induction' l with a l IH <;> intro l₁ l₂ h
  · simp_all only [sublists'_nil, reverse_cons, reverse_nil, nil_append, zip_cons_cons,
      zip_nil_right, mem_singleton, Prod.mk.injEq, append_nil, Perm.refl]
  · rw [sublists'_cons, reverse_append, zip_append, ← map_reverse, zip_map_right, zip_map_left] at *
      <;> [simp only [mem_append, mem_map, Prod.map_apply, id_eq, Prod.mk.injEq, Prod.exists,
        exists_eq_right_right] at h; simp]
    rcases h with (⟨l₁, l₂', h, rfl, rfl⟩ | ⟨l₁', h, rfl⟩)
    · exact perm_middle.trans ((IH _ _ h).cons _)
    · exact (IH _ _ h).cons _
Concatenation of Sublist Pairs in Reverse Zip is Permutation of Original List
Informal description
For any list $l$ of elements of type $\alpha$, and for any two sublists $l_1$ and $l_2$ such that $(l_1, l_2)$ is in the reverse zip of the list of all sublists of $l$, the concatenation of $l_1$ and $l_2$ is a permutation of $l$. In other words, if $(l_1, l_2)$ is a pair in $\text{revzip}(\text{sublists'}(l))$, then $l_1 \mathbin{+\kern-1.5ex+} l_2$ is a permutation of $l$.
List.range_bind_sublistsLen_perm theorem
(l : List α) : ((List.range (l.length + 1)).flatMap fun n => sublistsLen n l) ~ sublists' l
Full source 
theorem range_bind_sublistsLen_perm (l : List α) :
    ((List.range (l.length + 1)).flatMap fun n => sublistsLen n l) ~ sublists' l := by
  induction' l with h tl l_ih
  · simp [range_succ]
  · simp_rw [range_succ_eq_map, length, flatMap_cons, flatMap_map, sublistsLen_succ_cons,
      sublists'_cons, List.sublistsLen_zero, List.singleton_append]
    refine ((flatMap_append_perm (range (tl.length + 1)) _ _).symm.cons _).trans ?_
    simp_rw [← List.map_flatMap, ← cons_append]
    rw [← List.singleton_append, ← List.sublistsLen_zero tl]
    refine Perm.append ?_ (l_ih.map _)
    rw [List.range_succ, flatMap_append, flatMap_singleton,
      sublistsLen_of_length_lt (Nat.lt_succ_self _), append_nil,
      ← List.flatMap_map Nat.succ fun n => sublistsLen n tl,
      ← flatMap_cons (f := fun n => sublistsLen n tl), ← range_succ_eq_map]
    exact l_ih
Permutation Equivalence of Sublists via Length Partitioning
Informal description
For any list $l$ of elements of type $\alpha$, the concatenation of all sublists of $l$ of lengths ranging from $0$ to $\text{length}(l)$ is permutation-equivalent to the list of all sublists of $l$. In symbols: $$\text{flatMap}\ (\lambda n, \text{sublistsLen}\ n\ l)\ (\text{range}\ (\text{length}\ l + 1)) \sim \text{sublists'}\ l$$