mathlib documentation

data.list.perm

List permutations

inductive list.perm {α : Type uu} :
list αlist α → Prop
  • nil : ∀ {α : Type uu}, list.nil ~ list.nil
  • cons : ∀ {α : Type uu} (x : α) {l₁ l₂ : list α}, l₁ ~ l₂x :: l₁ ~ x :: l₂
  • swap : ∀ {α : Type uu} (x y : α) (l : list α), y :: x :: l ~ x :: y :: l
  • trans : ∀ {α : Type uu} {l₁ l₂ l₃ : list α}, l₁ ~ l₂l₂ ~ l₃l₁ ~ l₃

perm l₁ l₂ or l₁ ~ l₂ asserts that l₁ and l₂ are permutations of each other. This is defined by induction using pairwise swaps.

theorem list.perm.refl {α : Type uu} (l : list α) :
l ~ l

theorem list.perm.symm {α : Type uu} {l₁ l₂ : list α} :
l₁ ~ l₂l₂ ~ l₁

theorem list.perm_comm {α : Type uu} {l₁ l₂ : list α} :
l₁ ~ l₂ l₂ ~ l₁

theorem list.perm.swap' {α : Type uu} (x y : α) {l₁ l₂ : list α} :
l₁ ~ l₂y :: x :: l₁ ~ x :: y :: l₂

theorem list.perm.eqv (α : Type u_1) :

@[instance]
def list.is_setoid (α : Type u_1) :

Equations
theorem list.perm.subset {α : Type uu} {l₁ l₂ : list α} :
l₁ ~ l₂l₁ l₂

theorem list.perm.mem_iff {α : Type uu} {a : α} {l₁ l₂ : list α} :
l₁ ~ l₂(a l₁ a l₂)

theorem list.perm.append_right {α : Type uu} {l₁ l₂ : list α} (t₁ : list α) :
l₁ ~ l₂l₁ ++ t₁ ~ l₂ ++ t₁

theorem list.perm.append_left {α : Type uu} {t₁ t₂ : list α} (l : list α) :
t₁ ~ t₂l ++ t₁ ~ l ++ t₂

theorem list.perm.append {α : Type uu} {l₁ l₂ t₁ t₂ : list α} :
l₁ ~ l₂t₁ ~ t₂l₁ ++ t₁ ~ l₂ ++ t₂

theorem list.perm.append_cons {α : Type uu} (a : α) {h₁ h₂ t₁ t₂ : list α} :
h₁ ~ h₂t₁ ~ t₂h₁ ++ a :: t₁ ~ h₂ ++ a :: t₂

@[simp]
theorem list.perm_middle {α : Type uu} {a : α} {l₁ l₂ : list α} :
l₁ ++ a :: l₂ ~ a :: (l₁ ++ l₂)

@[simp]
theorem list.perm_append_singleton {α : Type uu} (a : α) (l : list α) :
l ++ [a] ~ a :: l

theorem list.perm_append_comm {α : Type uu} {l₁ l₂ : list α} :
l₁ ++ l₂ ~ l₂ ++ l₁

theorem list.concat_perm {α : Type uu} (l : list α) (a : α) :
l.concat a ~ a :: l

theorem list.perm.length_eq {α : Type uu} {l₁ l₂ : list α} :
l₁ ~ l₂l₁.length = l₂.length

theorem list.perm.eq_nil {α : Type uu} {l : list α} :

theorem list.perm.nil_eq {α : Type uu} {l : list α} :

theorem list.perm_nil {α : Type uu} {l₁ : list α} :
l₁ ~ list.nil l₁ = list.nil

theorem list.not_perm_nil_cons {α : Type uu} (x : α) (l : list α) :

@[simp]
theorem list.reverse_perm {α : Type uu} (l : list α) :

theorem list.perm_cons_append_cons {α : Type uu} {l l₁ l₂ : list α} (a : α) :
l ~ l₁ ++ l₂a :: l ~ l₁ ++ a :: l₂

@[simp]
theorem list.perm_repeat {α : Type uu} {a : α} {n : } {l : list α} :

@[simp]
theorem list.repeat_perm {α : Type uu} {a : α} {n : } {l : list α} :

@[simp]
theorem list.perm_singleton {α : Type uu} {a : α} {l : list α} :
l ~ [a] l = [a]

@[simp]
theorem list.singleton_perm {α : Type uu} {a : α} {l : list α} :
[a] ~ l [a] = l

theorem list.perm.eq_singleton {α : Type uu} {a : α} {l : list α} :
l ~ [a]l = [a]

theorem list.perm.singleton_eq {α : Type uu} {a : α} {l : list α} :
[a] ~ l[a] = l

theorem list.singleton_perm_singleton {α : Type uu} {a b : α} :
[a] ~ [b] a = b

theorem list.perm_cons_erase {α : Type uu} [decidable_eq α] {a : α} {l : list α} :
a ll ~ a :: l.erase a

theorem list.perm_induction_on {α : Type uu} {P : list αlist α → Prop} {l₁ l₂ : list α} :
l₁ ~ l₂P list.nil list.nil(∀ (x : α) (l₁ l₂ : list α), l₁ ~ l₂P l₁ l₂P (x :: l₁) (x :: l₂))(∀ (x y : α) (l₁ l₂ : list α), l₁ ~ l₂P l₁ l₂P (y :: x :: l₁) (x :: y :: l₂))(∀ (l₁ l₂ l₃ : list α), l₁ ~ l₂l₂ ~ l₃P l₁ l₂P l₂ l₃P l₁ l₃)P l₁ l₂

theorem list.perm.filter_map {α : Type uu} {β : Type vv} (f : α → option β) {l₁ l₂ : list α} :
l₁ ~ l₂list.filter_map f l₁ ~ list.filter_map f l₂

theorem list.perm.map {α : Type uu} {β : Type vv} (f : α → β) {l₁ l₂ : list α} :
l₁ ~ l₂list.map f l₁ ~ list.map f l₂

theorem list.perm.pmap {α : Type uu} {β : Type vv} {p : α → Prop} (f : Π (a : α), p a → β) {l₁ l₂ : list α} (p_1 : l₁ ~ l₂) {H₁ : ∀ (a : α), a l₁p a} {H₂ : ∀ (a : α), a l₂p a} :
list.pmap f l₁ H₁ ~ list.pmap f l₂ H₂

theorem list.perm.filter {α : Type uu} (p : α → Prop) [decidable_pred p] {l₁ l₂ : list α} :
l₁ ~ l₂list.filter p l₁ ~ list.filter p l₂

theorem list.exists_perm_sublist {α : Type uu} {l₁ l₂ l₂' : list α} :
l₁ <+ l₂l₂ ~ l₂'(∃ (l₁' : list α) (H : l₁' ~ l₁), l₁' <+ l₂')

theorem list.perm.sizeof_eq_sizeof {α : Type uu} [has_sizeof α] {l₁ l₂ : list α} :
l₁ ~ l₂l₁.sizeof = l₂.sizeof

theorem list.perm_comp_forall₂ {α : Type uu} {β : Type vv} {r : α → β → Prop} {l u : list α} {v : list β} :

theorem list.forall₂_comp_perm_eq_perm_comp_forall₂ {α : Type uu} {β : Type vv} {r : α → β → Prop} :

theorem list.rel_perm_imp {α : Type uu} {β : Type vv} {r : α → β → Prop} :

theorem list.rel_perm {α : Type uu} {β : Type vv} {r : α → β → Prop} :

def list.subperm {α : Type uu} :
list αlist α → Prop

subperm l₁ l₂, denoted l₁ <+~ l₂, means that l₁ is a sublist of a permutation of l₂. This is an analogue of l₁ ⊆ l₂ which respects multiplicities of elements, and is used for the relation on multisets.

Equations
  • l₁ <+~ l₂ = ∃ (l : list α) (H : l ~ l₁), l <+ l₂
theorem list.nil_subperm {α : Type uu} {l : list α} :

theorem list.perm.subperm_left {α : Type uu} {l l₁ l₂ : list α} :
l₁ ~ l₂(l <+~ l₁ l <+~ l₂)

theorem list.perm.subperm_right {α : Type uu} {l₁ l₂ l : list α} :
l₁ ~ l₂(l₁ <+~ l l₂ <+~ l)

theorem list.sublist.subperm {α : Type uu} {l₁ l₂ : list α} :
l₁ <+ l₂l₁ <+~ l₂

theorem list.perm.subperm {α : Type uu} {l₁ l₂ : list α} :
l₁ ~ l₂l₁ <+~ l₂

theorem list.subperm.refl {α : Type uu} (l : list α) :
l <+~ l

theorem list.subperm.trans {α : Type uu} {l₁ l₂ l₃ : list α} :
l₁ <+~ l₂l₂ <+~ l₃l₁ <+~ l₃

theorem list.subperm.length_le {α : Type uu} {l₁ l₂ : list α} :
l₁ <+~ l₂l₁.length l₂.length

theorem list.subperm.perm_of_length_le {α : Type uu} {l₁ l₂ : list α} :
l₁ <+~ l₂l₂.length l₁.lengthl₁ ~ l₂

theorem list.subperm.antisymm {α : Type uu} {l₁ l₂ : list α} :
l₁ <+~ l₂l₂ <+~ l₁l₁ ~ l₂

theorem list.subperm.subset {α : Type uu} {l₁ l₂ : list α} :
l₁ <+~ l₂l₁ l₂

theorem list.sublist.exists_perm_append {α : Type uu} {l₁ l₂ : list α} :
l₁ <+ l₂(∃ (l : list α), l₂ ~ l₁ ++ l)

theorem list.perm.countp_eq {α : Type uu} (p : α → Prop) [decidable_pred p] {l₁ l₂ : list α} :
l₁ ~ l₂list.countp p l₁ = list.countp p l₂

theorem list.subperm.countp_le {α : Type uu} (p : α → Prop) [decidable_pred p] {l₁ l₂ : list α} :
l₁ <+~ l₂list.countp p l₁ list.countp p l₂

theorem list.perm.count_eq {α : Type uu} [decidable_eq α] {l₁ l₂ : list α} (p : l₁ ~ l₂) (a : α) :
list.count a l₁ = list.count a l₂

theorem list.subperm.count_le {α : Type uu} [decidable_eq α] {l₁ l₂ : list α} (s : l₁ <+~ l₂) (a : α) :
list.count a l₁ list.count a l₂

theorem list.perm.foldl_eq' {α : Type uu} {β : Type vv} {f : β → α → β} {l₁ l₂ : list α} (p : l₁ ~ l₂) (a : ∀ (x : α), x l₁∀ (y : α), y l₁∀ (z : β), f (f z x) y = f (f z y) x) (b : β) :
list.foldl f b l₁ = list.foldl f b l₂

theorem list.perm.foldl_eq {α : Type uu} {β : Type vv} {f : β → α → β} {l₁ l₂ : list α} (rcomm : right_commutative f) (p : l₁ ~ l₂) (b : β) :
list.foldl f b l₁ = list.foldl f b l₂

theorem list.perm.foldr_eq {α : Type uu} {β : Type vv} {f : α → β → β} {l₁ l₂ : list α} (lcomm : left_commutative f) (p : l₁ ~ l₂) (b : β) :
list.foldr f b l₁ = list.foldr f b l₂

theorem list.perm.rec_heq {α : Type uu} {β : list αSort u_1} {f : Π (a : α) (l : list α), β lβ (a :: l)} {b : β list.nil} {l l' : list α} :
l ~ l'(∀ {a : α} {l l' : list α} {b : β l} {b' : β l'}, l ~ l'b == b'f a l b == f a l' b')(∀ {a a' : α} {l : list α} {b : β l}, f a (a' :: l) (f a' l b) == f a' (a :: l) (f a l b))list.rec b f l == list.rec b f l'

theorem list.perm.fold_op_eq {α : Type uu} {op : α → α → α} [is_associative α op] [is_commutative α op] {l₁ l₂ : list α} {a : α} :
l₁ ~ l₂list.foldl op a l₁ = list.foldl op a l₂

theorem list.perm.prod_eq' {α : Type uu} [monoid α] {l₁ l₂ : list α} :
l₁ ~ l₂list.pairwise (λ (x y : α), x * y = y * x) l₁l₁.prod = l₂.prod

If elements of a list commute with each other, then their product does not depend on the order of elements

theorem list.perm.sum_eq' {α : Type uu} [add_monoid α] {l₁ l₂ : list α} :
l₁ ~ l₂list.pairwise (λ (x y : α), x + y = y + x) l₁l₁.sum = l₂.sum

theorem list.perm.prod_eq {α : Type uu} [comm_monoid α] {l₁ l₂ : list α} :
l₁ ~ l₂l₁.prod = l₂.prod

theorem list.perm.sum_eq {α : Type uu} [add_comm_monoid α] {l₁ l₂ : list α} :
l₁ ~ l₂l₁.sum = l₂.sum

theorem list.sum_reverse {α : Type uu} [add_comm_monoid α] (l : list α) :

theorem list.prod_reverse {α : Type uu} [comm_monoid α] (l : list α) :

theorem list.perm_inv_core {α : Type uu} {a : α} {l₁ l₂ r₁ r₂ : list α} :
l₁ ++ a :: r₁ ~ l₂ ++ a :: r₂l₁ ++ r₁ ~ l₂ ++ r₂

theorem list.perm.cons_inv {α : Type uu} {a : α} {l₁ l₂ : list α} :
a :: l₁ ~ a :: l₂l₁ ~ l₂

@[simp]
theorem list.perm_cons {α : Type uu} (a : α) {l₁ l₂ : list α} :
a :: l₁ ~ a :: l₂ l₁ ~ l₂

theorem list.perm_append_left_iff {α : Type uu} {l₁ l₂ : list α} (l : list α) :
l ++ l₁ ~ l ++ l₂ l₁ ~ l₂

theorem list.perm_append_right_iff {α : Type uu} {l₁ l₂ : list α} (l : list α) :
l₁ ++ l ~ l₂ ++ l l₁ ~ l₂

theorem list.perm_option_to_list {α : Type uu} {o₁ o₂ : option α} :
o₁.to_list ~ o₂.to_list o₁ = o₂

theorem list.subperm_cons {α : Type uu} (a : α) {l₁ l₂ : list α} :
a :: l₁ <+~ a :: l₂ l₁ <+~ l₂

theorem list.cons_subperm_of_mem {α : Type uu} {a : α} {l₁ l₂ : list α} :
l₁.nodupa l₁a l₂l₁ <+~ l₂a :: l₁ <+~ l₂

theorem list.subperm_append_left {α : Type uu} {l₁ l₂ : list α} (l : list α) :
l ++ l₁ <+~ l ++ l₂ l₁ <+~ l₂

theorem list.subperm_append_right {α : Type uu} {l₁ l₂ : list α} (l : list α) :
l₁ ++ l <+~ l₂ ++ l l₁ <+~ l₂

theorem list.subperm.exists_of_length_lt {α : Type uu} {l₁ l₂ : list α} :
l₁ <+~ l₂l₁.length < l₂.length(∃ (a : α), a :: l₁ <+~ l₂)

theorem list.subperm_of_subset_nodup {α : Type uu} {l₁ l₂ : list α} :
l₁.nodupl₁ l₂l₁ <+~ l₂

theorem list.perm_ext {α : Type uu} {l₁ l₂ : list α} :
l₁.nodupl₂.nodup(l₁ ~ l₂ ∀ (a : α), a l₁ a l₂)

theorem list.nodup.sublist_ext {α : Type uu} {l₁ l₂ l : list α} :
l.nodupl₁ <+ ll₂ <+ l(l₁ ~ l₂ l₁ = l₂)

theorem list.perm.erase {α : Type uu} [decidable_eq α] (a : α) {l₁ l₂ : list α} :
l₁ ~ l₂l₁.erase a ~ l₂.erase a

theorem list.subperm_cons_erase {α : Type uu} [decidable_eq α] (a : α) (l : list α) :
l <+~ a :: l.erase a

theorem list.erase_subperm {α : Type uu} [decidable_eq α] (a : α) (l : list α) :
l.erase a <+~ l

theorem list.subperm.erase {α : Type uu} [decidable_eq α] {l₁ l₂ : list α} (a : α) :
l₁ <+~ l₂l₁.erase a <+~ l₂.erase a

theorem list.perm.diff_right {α : Type uu} [decidable_eq α] {l₁ l₂ : list α} (t : list α) :
l₁ ~ l₂l₁.diff t ~ l₂.diff t

theorem list.perm.diff_left {α : Type uu} [decidable_eq α] (l : list α) {t₁ t₂ : list α} :
t₁ ~ t₂l.diff t₁ = l.diff t₂

theorem list.perm.diff {α : Type uu} [decidable_eq α] {l₁ l₂ t₁ t₂ : list α} :
l₁ ~ l₂t₁ ~ t₂l₁.diff t₁ ~ l₂.diff t₂

theorem list.subperm.diff_right {α : Type uu} [decidable_eq α] {l₁ l₂ : list α} (h : l₁ <+~ l₂) (t : list α) :
l₁.diff t <+~ l₂.diff t

theorem list.erase_cons_subperm_cons_erase {α : Type uu} [decidable_eq α] (a b : α) (l : list α) :
(a :: l).erase b <+~ a :: l.erase b

theorem list.subperm_cons_diff {α : Type uu} [decidable_eq α] {a : α} {l₁ l₂ : list α} :
(a :: l₁).diff l₂ <+~ a :: l₁.diff l₂

theorem list.subset_cons_diff {α : Type uu} [decidable_eq α] {a : α} {l₁ l₂ : list α} :
(a :: l₁).diff l₂ a :: l₁.diff l₂

theorem list.perm.bag_inter_right {α : Type uu} [decidable_eq α] {l₁ l₂ : list α} (t : list α) :
l₁ ~ l₂l₁.bag_inter t ~ l₂.bag_inter t

theorem list.perm.bag_inter_left {α : Type uu} [decidable_eq α] (l : list α) {t₁ t₂ : list α} :
t₁ ~ t₂l.bag_inter t₁ = l.bag_inter t₂

theorem list.perm.bag_inter {α : Type uu} [decidable_eq α] {l₁ l₂ t₁ t₂ : list α} :
l₁ ~ l₂t₁ ~ t₂l₁.bag_inter t₁ ~ l₂.bag_inter t₂

theorem list.cons_perm_iff_perm_erase {α : Type uu} [decidable_eq α] {a : α} {l₁ l₂ : list α} :
a :: l₁ ~ l₂ a l₂ l₁ ~ l₂.erase a

theorem list.perm_iff_count {α : Type uu} [decidable_eq α] {l₁ l₂ : list α} :
l₁ ~ l₂ ∀ (a : α), list.count a l₁ = list.count a l₂

@[instance]
def list.decidable_perm {α : Type uu} [decidable_eq α] (l₁ l₂ : list α) :
decidable (l₁ ~ l₂)

Equations
theorem list.perm.erase_dup {α : Type uu} [decidable_eq α] {l₁ l₂ : list α} :
l₁ ~ l₂l₁.erase_dup ~ l₂.erase_dup

theorem list.perm.insert {α : Type uu} [decidable_eq α] (a : α) {l₁ l₂ : list α} :
l₁ ~ l₂insert a l₁ ~ insert a l₂

theorem list.perm_insert_swap {α : Type uu} [decidable_eq α] (x y : α) (l : list α) :
insert x (insert y l) ~ insert y (insert x l)

theorem list.perm_insert_nth {α : Type u_1} (x : α) (l : list α) {n : } :
n l.lengthlist.insert_nth n x l ~ x :: l

theorem list.perm.union_right {α : Type uu} [decidable_eq α] {l₁ l₂ : list α} (t₁ : list α) :
l₁ ~ l₂l₁ t₁ ~ l₂ t₁

theorem list.perm.union_left {α : Type uu} [decidable_eq α] (l : list α) {t₁ t₂ : list α} :
t₁ ~ t₂l t₁ ~ l t₂

theorem list.perm.union {α : Type uu} [decidable_eq α] {l₁ l₂ t₁ t₂ : list α} :
l₁ ~ l₂t₁ ~ t₂l₁ t₁ ~ l₂ t₂

theorem list.perm.inter_right {α : Type uu} [decidable_eq α] {l₁ l₂ : list α} (t₁ : list α) :
l₁ ~ l₂l₁ t₁ ~ l₂ t₁

theorem list.perm.inter_left {α : Type uu} [decidable_eq α] (l : list α) {t₁ t₂ : list α} :
t₁ ~ t₂l t₁ = l t₂

theorem list.perm.inter {α : Type uu} [decidable_eq α] {l₁ l₂ t₁ t₂ : list α} :
l₁ ~ l₂t₁ ~ t₂l₁ t₁ ~ l₂ t₂

theorem list.perm.inter_append {α : Type uu} [decidable_eq α] {l t₁ t₂ : list α} :
t₁.disjoint t₂l (t₁ ++ t₂) ~ l t₁ ++ l t₂

theorem list.perm.pairwise_iff {α : Type uu} {R : α → α → Prop} (S : symmetric R) {l₁ l₂ : list α} :
l₁ ~ l₂(list.pairwise R l₁ list.pairwise R l₂)

theorem list.perm.nodup_iff {α : Type uu} {l₁ l₂ : list α} :
l₁ ~ l₂(l₁.nodup l₂.nodup)

theorem list.perm.bind_right {α : Type uu} {β : Type vv} {l₁ l₂ : list α} (f : α → list β) :
l₁ ~ l₂l₁.bind f ~ l₂.bind f

theorem list.perm.bind_left {α : Type uu} {β : Type vv} (l : list α) {f g : α → list β} :
(∀ (a : α), f a ~ g a)l.bind f ~ l.bind g

theorem list.perm.product_right {α : Type uu} {β : Type vv} {l₁ l₂ : list α} (t₁ : list β) :
l₁ ~ l₂l₁.product t₁ ~ l₂.product t₁

theorem list.perm.product_left {α : Type uu} {β : Type vv} (l : list α) {t₁ t₂ : list β} :
t₁ ~ t₂l.product t₁ ~ l.product t₂

theorem list.perm.product {α : Type uu} {β : Type vv} {l₁ l₂ : list α} {t₁ t₂ : list β} :
l₁ ~ l₂t₁ ~ t₂l₁.product t₁ ~ l₂.product t₂

theorem list.sublists_cons_perm_append {α : Type uu} (a : α) (l : list α) :

theorem list.sublists_perm_sublists' {α : Type uu} (l : list α) :

theorem list.revzip_sublists {α : Type uu} (l l₁ l₂ : list α) :
(l₁, l₂) l.sublists.revzipl₁ ++ l₂ ~ l

theorem list.revzip_sublists' {α : Type uu} (l l₁ l₂ : list α) :
(l₁, l₂) l.sublists'.revzipl₁ ++ l₂ ~ l

theorem list.perm_lookmap {α : Type uu} (f : α → option α) {l₁ l₂ : list α} :
list.pairwise (λ (a b : α), ∀ (c : α), c f a∀ (d : α), d f ba = b c = d) l₁l₁ ~ l₂list.lookmap f l₁ ~ list.lookmap f l₂

theorem list.perm.erasep {α : Type uu} (f : α → Prop) [decidable_pred f] {l₁ l₂ : list α} :
list.pairwise (λ (a b : α), f af bfalse) l₁l₁ ~ l₂list.erasep f l₁ ~ list.erasep f l₂

theorem list.perm.take_inter {α : Type u_1} [decidable_eq α] {xs ys : list α} (n : ) :
xs ~ ysys.noduplist.take n xs ~ ys.inter (list.take n xs)

theorem list.perm.drop_inter {α : Type u_1} [decidable_eq α] {xs ys : list α} (n : ) :
xs ~ ysys.noduplist.drop n xs ~ ys.inter (list.drop n xs)

theorem list.perm.slice_inter {α : Type u_1} [decidable_eq α] {xs ys : list α} (n m : ) :
xs ~ ysys.noduplist.slice n m xs ~ ys list.slice n m xs

theorem list.permutations_aux2_fst {α : Type uu} {β : Type vv} (t : α) (ts : list α) (r : list β) (ys : list α) (f : list α → β) :
(list.permutations_aux2 t ts r ys f).fst = ys ++ ts

@[simp]
theorem list.permutations_aux2_snd_nil {α : Type uu} {β : Type vv} (t : α) (ts : list α) (r : list β) (f : list α → β) :

@[simp]
theorem list.permutations_aux2_snd_cons {α : Type uu} {β : Type vv} (t : α) (ts : list α) (r : list β) (y : α) (ys : list α) (f : list α → β) :
(list.permutations_aux2 t ts r (y :: ys) f).snd = f (t :: y :: ys ++ ts) :: (list.permutations_aux2 t ts r ys (λ (x : list α), f (y :: x))).snd

theorem list.permutations_aux2_append {α : Type uu} {β : Type vv} (t : α) (ts : list α) (r : list β) (ys : list α) (f : list α → β) :

theorem list.mem_permutations_aux2 {α : Type uu} {t : α} {ts ys l l' : list α} :
l' (list.permutations_aux2 t ts list.nil ys (append l)).snd ∃ (l₁ l₂ : list α), l₂ list.nil ys = l₁ ++ l₂ l' = l ++ l₁ ++ t :: l₂ ++ ts

theorem list.mem_permutations_aux2' {α : Type uu} {t : α} {ts ys l : list α} :
l (list.permutations_aux2 t ts list.nil ys id).snd ∃ (l₁ l₂ : list α), l₂ list.nil ys = l₁ ++ l₂ l = l₁ ++ t :: l₂ ++ ts

theorem list.length_permutations_aux2 {α : Type uu} {β : Type vv} (t : α) (ts ys : list α) (f : list α → β) :

theorem list.foldr_permutations_aux2 {α : Type uu} (t : α) (ts : list α) (r L : list (list α)) :
list.foldr (λ (y : list α) (r : list (list α)), (list.permutations_aux2 t ts r y id).snd) r L = L.bind (λ (y : list α), (list.permutations_aux2 t ts list.nil y id).snd) ++ r

theorem list.mem_foldr_permutations_aux2 {α : Type uu} {t : α} {ts : list α} {r L : list (list α)} {l' : list α} :
l' list.foldr (λ (y : list α) (r : list (list α)), (list.permutations_aux2 t ts r y id).snd) r L l' r ∃ (l₁ l₂ : list α), l₁ ++ l₂ L l₂ list.nil l' = l₁ ++ t :: l₂ ++ ts

theorem list.length_foldr_permutations_aux2 {α : Type uu} (t : α) (ts : list α) (r L : list (list α)) :
(list.foldr (λ (y : list α) (r : list (list α)), (list.permutations_aux2 t ts r y id).snd) r L).length = (list.map list.length L).sum + r.length

theorem list.length_foldr_permutations_aux2' {α : Type uu} (t : α) (ts : list α) (r L : list (list α)) (n : ) :
(∀ (l : list α), l Ll.length = n)(list.foldr (λ (y : list α) (r : list (list α)), (list.permutations_aux2 t ts r y id).snd) r L).length = n * L.length + r.length

theorem list.perm_of_mem_permutations_aux {α : Type uu} {ts is l : list α} :
l ts.permutations_aux isl ~ ts ++ is

theorem list.perm_of_mem_permutations {α : Type uu} {l₁ l₂ : list α} :
l₁ l₂.permutationsl₁ ~ l₂

theorem list.length_permutations_aux {α : Type uu} (ts is : list α) :

theorem list.length_permutations {α : Type uu} (l : list α) :

theorem list.mem_permutations_of_perm_lemma {α : Type uu} {is l : list α} :
(l ~ list.nil ++ is(∃ (ts' : list α) (H : ts' ~ list.nil), l = ts' ++ is) l is.permutations_aux list.nil)l ~ isl is.permutations

theorem list.mem_permutations_aux_of_perm {α : Type uu} {ts is l : list α} :
l ~ is ++ ts(∃ (is' : list α) (H : is' ~ is), l = is' ++ ts) l ts.permutations_aux is

@[simp]
theorem list.mem_permutations {α : Type uu} (s t : list α) :