# Documentation

Mathlib.Data.List.Perm

# List Permutations #

This file introduces the List.Perm relation, which is true if two lists are permutations of one another.

## Notation #

The notation ~ is used for permutation equivalence.

inductive List.Perm {α : Type uu} :
List αList αProp
• nil: ∀ {α : Type uu}, [] ~ []
• 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.

Instances For

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

Equations
@[simp]
theorem List.Perm.refl {α : Type uu} (l : List α) :
l ~ l
theorem List.Perm.symm {α : Type uu} {l₁ : List α} {l₂ : List α} (p : l₁ ~ l₂) :
l₂ ~ l₁
theorem List.perm_comm {α : Type uu} {l₁ : List α} {l₂ : List α} :
l₁ ~ l₂ l₂ ~ l₁
theorem List.Perm.swap' {α : Type uu} (x : α) (y : α) {l₁ : List α} {l₂ : List α} (p : l₁ ~ l₂) :
y :: x :: l₁ ~ x :: y :: l₂
theorem List.Perm.eqv (α : Type u_1) :
Equivalence List.Perm
theorem List.Perm.of_eq {α : Type uu} {l₁ : List α} {l₂ : List α} (h : l₁ = l₂) :
l₁ ~ l₂
instance List.isSetoid (α : Type u_1) :
Equations
theorem List.Perm.mem_iff {α : Type uu} {a : α} {l₁ : List α} {l₂ : List α} (p : l₁ ~ l₂) :
a l₁ a l₂
theorem List.Perm.subset {α : Type uu} {l₁ : List α} {l₂ : List α} (p : l₁ ~ l₂) :
l₁ l₂
theorem List.Perm.subset_congr_left {α : Type uu} {l₁ : List α} {l₂ : List α} {l₃ : List α} (h : l₁ ~ l₂) :
l₁ l₃ l₂ l₃
theorem List.Perm.subset_congr_right {α : Type uu} {l₁ : List α} {l₂ : List α} {l₃ : List α} (h : l₁ ~ l₂) :
l₃ l₁ l₃ l₂
theorem List.Perm.append_right {α : Type uu} {l₁ : List α} {l₂ : List α} (t₁ : List α) (p : l₁ ~ l₂) :
l₁ ++ t₁ ~ l₂ ++ t₁
theorem List.Perm.append_left {α : Type uu} {t₁ : List α} {t₂ : List α} (l : List α) :
t₁ ~ t₂l ++ t₁ ~ l ++ t₂
theorem List.Perm.append {α : Type uu} {l₁ : List α} {l₂ : List α} {t₁ : List α} {t₂ : List α} (p₁ : l₁ ~ l₂) (p₂ : t₁ ~ t₂) :
l₁ ++ t₁ ~ l₂ ++ t₂
theorem List.Perm.append_cons {α : Type uu} (a : α) {h₁ : List α} {h₂ : List α} {t₁ : List α} {t₂ : List α} (p₁ : h₁ ~ h₂) (p₂ : t₁ ~ t₂) :
h₁ ++ a :: t₁ ~ h₂ ++ a :: t₂
@[simp]
theorem List.perm_middle {α : Type uu} {a : α} {l₁ : List α} {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₁ : List α} {l₂ : List α} :
l₁ ++ l₂ ~ l₂ ++ l₁
theorem List.concat_perm {α : Type uu} (l : List α) (a : α) :
~ a :: l
theorem List.Perm.length_eq {α : Type uu} {l₁ : List α} {l₂ : List α} (p : l₁ ~ l₂) :
=
theorem List.Perm.eq_nil {α : Type uu} {l : List α} (p : l ~ []) :
l = []
theorem List.Perm.nil_eq {α : Type uu} {l : List α} (p : [] ~ l) :
[] = l
@[simp]
theorem List.perm_nil {α : Type uu} {l₁ : List α} :
l₁ ~ [] l₁ = []
@[simp]
theorem List.nil_perm {α : Type uu} {l₁ : List α} :
[] ~ l₁ l₁ = []
theorem List.not_perm_nil_cons {α : Type uu} (x : α) (l : List α) :
¬[] ~ x :: l
@[simp]
theorem List.reverse_perm {α : Type uu} (l : List α) :
theorem List.perm_cons_append_cons {α : Type uu} {l : List α} {l₁ : List α} {l₂ : List α} (a : α) (p : l ~ l₁ ++ l₂) :
a :: l ~ l₁ ++ a :: l₂
@[simp]
theorem List.perm_replicate {α : Type uu} {n : } {a : α} {l : List α} :
l ~ l =
@[simp]
theorem List.replicate_perm {α : Type uu} {n : } {a : α} {l : List α} :
~ l = l
@[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]

Alias of the forward direction of List.perm_singleton.

theorem List.Perm.singleton_eq {α : Type uu} {a : α} {l : List α} :
[a] ~ l[a] = l

Alias of the forward direction of List.singleton_perm.

theorem List.singleton_perm_singleton {α : Type uu} {a : α} {b : α} :
[a] ~ [b] a = b
theorem List.perm_cons_erase {α : Type uu} [inst : ] {a : α} {l : List α} (h : a l) :
l ~ a ::
theorem List.perm_induction_on {α : Type uu} {P : List αList αProp} {l₁ : List α} {l₂ : List α} (p : l₁ ~ l₂) (h₁ : P [] []) (h₂ : (x : α) → (l₁ l₂ : List α) → l₁ ~ l₂P l₁ l₂P (x :: l₁) (x :: l₂)) (h₃ : (x y : α) → (l₁ l₂ : List α) → l₁ ~ l₂P l₁ l₂P (y :: x :: l₁) (x :: y :: l₂)) (h₄ : (l₁ l₂ l₃ : List α) → l₁ ~ l₂l₂ ~ l₃P l₁ l₂P l₂ l₃P l₁ l₃) :
P l₁ l₂
theorem List.Perm.filterMap {α : Type uu} {β : Type vv} (f : α) {l₁ : List α} {l₂ : List α} (p : l₁ ~ l₂) :
~
theorem List.Perm.map {α : Type uu} {β : Type vv} (f : αβ) {l₁ : List α} {l₂ : List α} (p : 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₁ : List α} {l₂ : List α} (p : 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 : αBool) {l₁ : List α} {l₂ : List α} (s : l₁ ~ l₂) :
List.filter p l₁ ~ List.filter p l₂
theorem List.filter_append_perm {α : Type uu} (p : αBool) (l : List α) :
++ List.filter (fun x => decide ¬p x = true) l ~ l
theorem List.exists_perm_sublist {α : Type uu} {l₁ : List α} {l₂ : List α} {l₂' : List α} (s : List.Sublist l₁ l₂) (p : l₂ ~ l₂') :
l₁' x, List.Sublist l₁' l₂'
theorem List.Perm.sizeOf_eq_sizeOf {α : Type uu} [inst : ] {l₁ : List α} {l₂ : List α} (h : l₁ ~ l₂) :
sizeOf l₁ = sizeOf l₂
theorem List.perm_comp_perm {α : Type uu} :
Relation.Comp List.Perm List.Perm = List.Perm
theorem List.perm_comp_forall₂ {α : Type uu} {β : Type vv} {r : αβProp} {l : List α} {u : List α} {v : List β} (hlu : l ~ u) (huv : List.Forall₂ r u v) :
Relation.Comp () List.Perm l v
theorem List.forall₂_comp_perm_eq_perm_comp_forall₂ {α : Type uu} {β : Type vv} {r : αβProp} :
Relation.Comp () List.Perm = Relation.Comp List.Perm ()
theorem List.rel_perm_imp {α : Type uu} {β : Type vv} {r : αβProp} (hr : ) :
fun x x_1 => xx_1) List.Perm List.Perm
theorem List.rel_perm {α : Type uu} {β : Type vv} {r : αβProp} (hr : ) :
fun x x_1 => x x_1) List.Perm List.Perm
def List.Subperm {α : Type uu} (l₁ : List α) (l₂ : List α) :

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

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
theorem List.nil_subperm {α : Type uu} {l : List α} :
[] <+~ l
theorem List.Perm.subperm_left {α : Type uu} {l : List α} {l₁ : List α} {l₂ : List α} (p : l₁ ~ l₂) :
l <+~ l₁ l <+~ l₂
theorem List.Perm.subperm_right {α : Type uu} {l₁ : List α} {l₂ : List α} {l : List α} (p : l₁ ~ l₂) :
l₁ <+~ l l₂ <+~ l
theorem List.Sublist.subperm {α : Type uu} {l₁ : List α} {l₂ : List α} (s : List.Sublist l₁ l₂) :
l₁ <+~ l₂
theorem List.Perm.subperm {α : Type uu} {l₁ : List α} {l₂ : List α} (p : l₁ ~ l₂) :
l₁ <+~ l₂
theorem List.Subperm.refl {α : Type uu} (l : List α) :
l <+~ l
theorem List.Subperm.trans {α : Type uu} {l₁ : List α} {l₂ : List α} {l₃ : List α} :
l₁ <+~ l₂l₂ <+~ l₃l₁ <+~ l₃
theorem List.Subperm.length_le {α : Type uu} {l₁ : List α} {l₂ : List α} :
l₁ <+~ l₂
theorem List.Subperm.perm_of_length_le {α : Type uu} {l₁ : List α} {l₂ : List α} :
l₁ <+~ l₂ l₁ ~ l₂
theorem List.Subperm.antisymm {α : Type uu} {l₁ : List α} {l₂ : List α} (h₁ : l₁ <+~ l₂) (h₂ : l₂ <+~ l₁) :
l₁ ~ l₂
theorem List.Subperm.subset {α : Type uu} {l₁ : List α} {l₂ : List α} :
l₁ <+~ l₂l₁ l₂
theorem List.Subperm.filter {α : Type uu} (p : αBool) ⦃l : List α ⦃l' : List α (h : l <+~ l') :
theorem List.Sublist.exists_perm_append {α : Type uu} {l₁ : List α} {l₂ : List α} :
List.Sublist l₁ l₂l, l₂ ~ l₁ ++ l
theorem List.Perm.countp_eq {α : Type uu} (p : αBool) {l₁ : List α} {l₂ : List α} (s : l₁ ~ l₂) :
List.countp p l₁ = List.countp p l₂
theorem List.Subperm.countp_le {α : Type uu} (p : αBool) {l₁ : List α} {l₂ : List α} :
l₁ <+~ l₂List.countp p l₁ List.countp p l₂
theorem List.Perm.countp_congr {α : Type uu} {l₁ : List α} {l₂ : List α} (s : l₁ ~ l₂) {p : αBool} {p' : αBool} (hp : ∀ (x : α), x l₁p x = p' x) :
List.countp p l₁ = List.countp p' l₂
theorem List.countp_eq_countp_filter_add {α : Type uu} (l : List α) (p : αBool) (q : αBool) :
= List.countp p () + List.countp p (List.filter (fun a => decide ¬q a = true) l)
theorem List.Perm.count_eq {α : Type uu} [inst : ] {l₁ : List α} {l₂ : List α} (p : l₁ ~ l₂) (a : α) :
List.count a l₁ = List.count a l₂
theorem List.Subperm.count_le {α : Type uu} [inst : ] {l₁ : List α} {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₁ : List α} {l₂ : List α} (p : l₁ ~ l₂) :
(∀ (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₁ : List α} {l₂ : List α} (rcomm : ) (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₁ : List α} {l₂ : List α} (lcomm : ) (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 : β []} {l : List α} {l' : List α} (hl : l ~ l') (f_congr : ∀ {a : α} {l l' : List α} {b : β l} {b' : β l'}, l ~ l'HEq b b'HEq (f a l b) (f a l' b')) (f_swap : ∀ {a a' : α} {l : List α} {b : β l}, HEq (f a (a' :: l) (f a' l b)) (f a' (a :: l) (f a l b))) :
HEq (List.rec b f l) (List.rec b f l')
theorem List.Perm.fold_op_eq {α : Type uu} {op : ααα} [IA : ] [IC : ] {l₁ : List α} {l₂ : List α} {a : α} (h : l₁ ~ l₂) :
List.foldl op a l₁ = List.foldl op a l₂
theorem List.Perm.sum_eq' {α : Type uu} [M : ] {l₁ : List α} {l₂ : List α} (h : l₁ ~ l₂) (hc : List.Pairwise AddCommute l₁) :
List.sum l₁ = List.sum l₂

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

theorem List.Perm.prod_eq' {α : Type uu} [M : ] {l₁ : List α} {l₂ : List α} (h : l₁ ~ l₂) (hc : List.Pairwise Commute l₁) :
=

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} [inst : ] {l₁ : List α} {l₂ : List α} (h : l₁ ~ l₂) :
List.sum l₁ = List.sum l₂
theorem List.Perm.prod_eq {α : Type uu} [inst : ] {l₁ : List α} {l₂ : List α} (h : l₁ ~ l₂) :
=
theorem List.sum_reverse {α : Type uu} [inst : ] (l : List α) :
theorem List.prod_reverse {α : Type uu} [inst : ] (l : List α) :
theorem List.perm_inv_core {α : Type uu} {a : α} {l₁ : List α} {l₂ : List α} {r₁ : List α} {r₂ : List α} :
l₁ ++ a :: r₁ ~ l₂ ++ a :: r₂l₁ ++ r₁ ~ l₂ ++ r₂
theorem List.Perm.cons_inv {α : Type uu} {a : α} {l₁ : List α} {l₂ : List α} :
a :: l₁ ~ a :: l₂l₁ ~ l₂
@[simp]
theorem List.perm_cons {α : Type uu} (a : α) {l₁ : List α} {l₂ : List α} :
a :: l₁ ~ a :: l₂ l₁ ~ l₂
theorem List.perm_append_left_iff {α : Type uu} {l₁ : List α} {l₂ : List α} (l : List α) :
l ++ l₁ ~ l ++ l₂ l₁ ~ l₂
theorem List.perm_append_right_iff {α : Type uu} {l₁ : List α} {l₂ : List α} (l : List α) :
l₁ ++ l ~ l₂ ++ l l₁ ~ l₂
theorem List.perm_option_to_list {α : Type uu} {o₁ : } {o₂ : } :
o₁ = o₂
theorem List.subperm_cons {α : Type uu} (a : α) {l₁ : List α} {l₂ : List α} :
a :: l₁ <+~ a :: l₂ l₁ <+~ l₂
theorem List.subperm.of_cons {α : Type uu} (a : α) {l₁ : List α} {l₂ : List α} :
a :: l₁ <+~ a :: l₂l₁ <+~ l₂

Alias of the forward direction of List.subperm_cons.

theorem List.subperm.cons {α : Type uu} (a : α) {l₁ : List α} {l₂ : List α} :
l₁ <+~ l₂a :: l₁ <+~ a :: l₂

Alias of the reverse direction of List.subperm_cons.

theorem List.cons_subperm_of_mem {α : Type uu} {a : α} {l₁ : List α} {l₂ : List α} (d₁ : ) (h₁ : ¬a l₁) (h₂ : a l₂) (s : l₁ <+~ l₂) :
a :: l₁ <+~ l₂
theorem List.subperm_append_left {α : Type uu} {l₁ : List α} {l₂ : List α} (l : List α) :
l ++ l₁ <+~ l ++ l₂ l₁ <+~ l₂
theorem List.subperm_append_right {α : Type uu} {l₁ : List α} {l₂ : List α} (l : List α) :
l₁ ++ l <+~ l₂ ++ l l₁ <+~ l₂
theorem List.Subperm.exists_of_length_lt {α : Type uu} {l₁ : List α} {l₂ : List α} :
l₁ <+~ l₂ < a, a :: l₁ <+~ l₂
theorem List.Nodup.subperm {α : Type uu} {l₁ : List α} {l₂ : List α} (d : ) (H : l₁ l₂) :
l₁ <+~ l₂
theorem List.perm_ext {α : Type uu} {l₁ : List α} {l₂ : List α} (d₁ : ) (d₂ : ) :
l₁ ~ l₂ ∀ (a : α), a l₁ a l₂
theorem List.Nodup.sublist_ext {α : Type uu} {l₁ : List α} {l₂ : List α} {l : List α} (d : ) (s₁ : List.Sublist l₁ l) (s₂ : List.Sublist l₂ l) :
l₁ ~ l₂ l₁ = l₂
theorem List.Perm.erase {α : Type uu} [inst : ] (a : α) {l₁ : List α} {l₂ : List α} (p : l₁ ~ l₂) :
List.erase l₁ a ~ List.erase l₂ a
theorem List.subperm_cons_erase {α : Type uu} [inst : ] (a : α) (l : List α) :
l <+~ a ::
theorem List.erase_subperm {α : Type uu} [inst : ] (a : α) (l : List α) :
<+~ l
theorem List.Subperm.erase {α : Type uu} [inst : ] {l₁ : List α} {l₂ : List α} (a : α) (h : l₁ <+~ l₂) :
List.erase l₁ a <+~ List.erase l₂ a
theorem List.Perm.diff_right {α : Type uu} [inst : ] {l₁ : List α} {l₂ : List α} (t : List α) (h : l₁ ~ l₂) :
List.diff l₁ t ~ List.diff l₂ t
theorem List.Perm.diff_left {α : Type uu} [inst : ] (l : List α) {t₁ : List α} {t₂ : List α} (h : t₁ ~ t₂) :
List.diff l t₁ = List.diff l t₂
theorem List.Perm.diff {α : Type uu} [inst : ] {l₁ : List α} {l₂ : List α} {t₁ : List α} {t₂ : List α} (hl : l₁ ~ l₂) (ht : t₁ ~ t₂) :
List.diff l₁ t₁ ~ List.diff l₂ t₂
theorem List.Subperm.diff_right {α : Type uu} [inst : ] {l₁ : List α} {l₂ : List α} (h : l₁ <+~ l₂) (t : List α) :
List.diff l₁ t <+~ List.diff l₂ t
theorem List.erase_cons_subperm_cons_erase {α : Type uu} [inst : ] (a : α) (b : α) (l : List α) :
List.erase (a :: l) b <+~ a ::
theorem List.subperm_cons_diff {α : Type uu} [inst : ] {a : α} {l₁ : List α} {l₂ : List α} :
List.diff (a :: l₁) l₂ <+~ a :: List.diff l₁ l₂
theorem List.subset_cons_diff {α : Type uu} [inst : ] {a : α} {l₁ : List α} {l₂ : List α} :
List.diff (a :: l₁) l₂ a :: List.diff l₁ l₂
theorem List.Perm.bagInter_right {α : Type uu} [inst : ] {l₁ : List α} {l₂ : List α} (t : List α) (h : l₁ ~ l₂) :
~
theorem List.Perm.bagInter_left {α : Type uu} [inst : ] (l : List α) {t₁ : List α} {t₂ : List α} (p : t₁ ~ t₂) :
=
theorem List.Perm.bagInter {α : Type uu} [inst : ] {l₁ : List α} {l₂ : List α} {t₁ : List α} {t₂ : List α} (hl : l₁ ~ l₂) (ht : t₁ ~ t₂) :
List.bagInter l₁ t₁ ~ List.bagInter l₂ t₂
theorem List.cons_perm_iff_perm_erase {α : Type uu} [inst : ] {a : α} {l₁ : List α} {l₂ : List α} :
a :: l₁ ~ l₂ a l₂ l₁ ~ List.erase l₂ a
theorem List.perm_iff_count {α : Type uu} [inst : ] {l₁ : List α} {l₂ : List α} :
l₁ ~ l₂ ∀ (a : α), List.count a l₁ = List.count a l₂
theorem List.perm_replicate_append_replicate {α : Type uu} [inst : ] {l : List α} {a : α} {b : α} {m : } {n : } (h : a b) :
l ~ ++ = m = n l [a, b]
theorem List.Subperm.cons_right {α : Type u_1} {l : List α} {l' : List α} (x : α) (h : l <+~ l') :
l <+~ x :: l'
theorem List.subperm_append_diff_self_of_count_le {α : Type uu} [inst : ] {l₁ : List α} {l₂ : List α} (h : ∀ (x : α), x l₁List.count x l₁ List.count x l₂) :
l₁ ++ List.diff l₂ l₁ ~ l₂

The list version of add_tsub_cancel_of_le for multisets.

theorem List.subperm_ext_iff {α : Type uu} [inst : ] {l₁ : List α} {l₂ : List α} :
l₁ <+~ l₂ ∀ (x : α), x l₁List.count x l₁ List.count x l₂

The list version of Multiset.le_iff_count.

instance List.decidableSubperm {α : Type uu} [inst : ] :
DecidableRel fun x x_1 => x <+~ x_1
Equations
@[simp]
theorem List.subperm_singleton_iff {α : Type u_1} {l : List α} {a : α} :
[a] <+~ l a l
theorem List.Subperm.cons_left {α : Type uu} [inst : ] {l₁ : List α} {l₂ : List α} (h : l₁ <+~ l₂) (x : α) (hx : List.count x l₁ < List.count x l₂) :
x :: l₁ <+~ l₂
instance List.decidablePerm {α : Type uu} [inst : ] (l₁ : List α) (l₂ : List α) :
Decidable (l₁ ~ l₂)
Equations
theorem List.Perm.dedup {α : Type uu} [inst : ] {l₁ : List α} {l₂ : List α} (p : l₁ ~ l₂) :
~
theorem List.Perm.insert {α : Type uu} [inst : ] (a : α) {l₁ : List α} {l₂ : List α} (p : l₁ ~ l₂) :
List.insert a l₁ ~ List.insert a l₂
theorem List.perm_insert_swap {α : Type uu} [inst : ] (x : α) (y : α) (l : List α) :
theorem List.perm_insertNth {α : Type u_1} (x : α) (l : List α) {n : } (h : n ) :
~ x :: l
theorem List.Perm.union_right {α : Type uu} [inst : ] {l₁ : List α} {l₂ : List α} (t₁ : List α) (h : l₁ ~ l₂) :
List.union l₁ t₁ ~ List.union l₂ t₁
theorem List.Perm.union_left {α : Type uu} [inst : ] (l : List α) {t₁ : List α} {t₂ : List α} (h : t₁ ~ t₂) :
List.union l t₁ ~ List.union l t₂
theorem List.Perm.union {α : Type uu} [inst : ] {l₁ : List α} {l₂ : List α} {t₁ : List α} {t₂ : List α} (p₁ : l₁ ~ l₂) (p₂ : t₁ ~ t₂) :
List.union l₁ t₁ ~ List.union l₂ t₂
theorem List.Perm.inter_right {α : Type uu} [inst : ] {l₁ : List α} {l₂ : List α} (t₁ : List α) :
l₁ ~ l₂l₁ t₁ ~ l₂ t₁
theorem List.Perm.inter_left {α : Type uu} [inst : ] (l : List α) {t₁ : List α} {t₂ : List α} (p : t₁ ~ t₂) :
l t₁ = l t₂
theorem List.Perm.inter {α : Type uu} [inst : ] {l₁ : List α} {l₂ : List α} {t₁ : List α} {t₂ : List α} (p₁ : l₁ ~ l₂) (p₂ : t₁ ~ t₂) :
l₁ t₁ ~ l₂ t₂
theorem List.Perm.inter_append {α : Type uu} [inst : ] {l : List α} {t₁ : List α} {t₂ : List α} (h : List.Disjoint t₁ t₂) :
l (t₁ ++ t₂) ~ l t₁ ++ l t₂
theorem List.Perm.pairwise_iff {α : Type uu} {R : ααProp} (S : ) {l₁ : List α} {l₂ : List α} (_p : l₁ ~ l₂) :
theorem List.Pairwise.perm {α : Type uu} {R : ααProp} {l : List α} {l' : List α} (hR : ) (hl : l ~ l') (hsymm : ) :
theorem List.Perm.pairwise {α : Type uu} {R : ααProp} {l : List α} {l' : List α} (hl : l ~ l') (hR : ) (hsymm : ) :
theorem List.Perm.nodup_iff {α : Type uu} {l₁ : List α} {l₂ : List α} :
l₁ ~ l₂ → ( )
theorem List.Perm.join {α : Type uu} {l₁ : List (List α)} {l₂ : List (List α)} (h : l₁ ~ l₂) :
~
theorem List.Perm.bind_right {α : Type uu} {β : Type vv} {l₁ : List α} {l₂ : List α} (f : αList β) (p : l₁ ~ l₂) :
List.bind l₁ f ~ List.bind l₂ f
theorem List.Perm.join_congr {α : Type uu} {l₁ : List (List α)} {l₂ : List (List α)} :
List.Forall₂ (fun x x_1 => x ~ x_1) l₁ l₂ ~
theorem List.Perm.bind_left {α : Type uu} {β : Type vv} (l : List α) {f : αList β} {g : αList β} (h : ∀ (a : α), a lf a ~ g a) :
~
theorem List.bind_append_perm {α : Type uu} {β : Type vv} (l : List α) (f : αList β) (g : αList β) :
++ ~ List.bind l fun x => f x ++ g x
theorem List.map_append_bind_perm {α : Type uu} {β : Type vv} (l : List α) (f : αβ) (g : αList β) :
List.map f l ++ ~ List.bind l fun x => f x :: g x
theorem List.Perm.product_right {α : Type uu} {β : Type vv} {l₁ : List α} {l₂ : List α} (t₁ : List β) (p : l₁ ~ l₂) :
l₁ ×ˢ t₁ ~ l₂ ×ˢ t₁
theorem List.Perm.product_left {α : Type uu} {β : Type vv} (l : List α) {t₁ : List β} {t₂ : List β} (p : t₁ ~ t₂) :
l ×ˢ t₁ ~ l ×ˢ t₂
theorem List.Perm.product {α : Type uu} {β : Type vv} {l₁ : List α} {l₂ : List α} {t₁ : List β} {t₂ : List β} (p₁ : l₁ ~ l₂) (p₂ : t₁ ~ t₂) :
l₁ ×ˢ t₁ ~ l₂ ×ˢ t₂
theorem List.perm_lookmap {α : Type uu} (f : α) {l₁ : List α} {l₂ : List α} (H : List.Pairwise (fun a b => ∀ (c : α), c f a∀ (d : α), d f ba = b c = d) l₁) (p : l₁ ~ l₂) :
theorem List.Perm.erasep {α : Type uu} (f : αProp) [inst : ] {l₁ : List α} {l₂ : List α} (H : List.Pairwise (fun a b => f af bFalse) l₁) (p : l₁ ~ l₂) :
List.eraseP (fun b => decide (f b)) l₁ ~ List.eraseP (fun b => decide (f b)) l₂
theorem List.Perm.take_inter {α : Type u_1} [inst : ] {xs : List α} {ys : List α} (n : ) (h : xs ~ ys) (h' : ) :
theorem List.Perm.drop_inter {α : Type u_1} [inst : ] {xs : List α} {ys : List α} (n : ) (h : xs ~ ys) (h' : ) :
theorem List.Perm.dropSlice_inter {α : Type u_1} [inst : ] {xs : List α} {ys : List α} (n : ) (m : ) (h : xs ~ ys) (h' : ) :
theorem List.perm_of_mem_permutationsAux {α : Type uu} {ts : List α} {is : List α} {l : List α} :
l l ~ ts ++ is
theorem List.perm_of_mem_permutations {α : Type uu} {l₁ : List α} {l₂ : List α} (h : l₁ ) :
l₁ ~ l₂
theorem List.length_permutationsAux {α : Type uu} (ts : List α) (is : List α) :
theorem List.length_permutations {α : Type uu} (l : List α) :
theorem List.mem_permutations_of_perm_lemma {α : Type uu} {is : List α} {l : List α} (H : l ~ [] ++ is(ts' x, l = ts' ++ is) l ) :
l ~ is
theorem List.mem_permutationsAux_of_perm {α : Type uu} {ts : List α} {is : List α} {l : List α} :
l ~ is ++ ts(is' x, l = is' ++ ts) l
@[simp]
theorem List.mem_permutations {α : Type uu} {s : List α} {t : List α} :
s ~ t
theorem List.perm_permutations'Aux_comm {α : Type uu} (a : α) (b : α) (l : List α) :
theorem List.Perm.permutations' {α : Type uu} {s : List α} {t : List α} (p : s ~ t) :
@[simp]
theorem List.mem_permutations' {α : Type uu} {s : List α} {t : List α} :
s ~ t
theorem List.Perm.permutations {α : Type uu} {s : List α} {t : List α} (h : s ~ t) :
@[simp]
theorem List.perm_permutations_iff {α : Type uu} {s : List α} {t : List α} :
s ~ t
@[simp]
theorem List.perm_permutations'_iff {α : Type uu} {s : List α} {t : List α} :
s ~ t
theorem List.nthLe_permutations'Aux {α : Type uu} (s : List α) (x : α) (n : ) (hn : ) :
List.nthLe () n hn =
theorem List.count_permutations'Aux_self {α : Type uu} [inst : ] (l : List α) (x : α) :
List.count (x :: l) () = List.length (List.takeWhile (fun b => decide ((fun x x_1 => x = x_1) x b)) l) + 1
@[simp]
theorem List.length_permutations'Aux {α : Type uu} (s : List α) (x : α) :
= + 1
@[simp]
theorem List.permutations'Aux_nthLe_zero {α : Type uu} (s : List α) (x : α) (hn : optParam () (_ : )) :
List.nthLe () 0 hn = x :: s
theorem List.injective_permutations'Aux {α : Type uu} (x : α) :
theorem List.nodup_permutations'Aux_of_not_mem {α : Type uu} (s : List α) (x : α) (hx : ¬x s) :
theorem List.nodup_permutations'Aux_iff {α : Type uu} {s : List α} {x : α} :
¬x s
theorem List.nodup_permutations {α : Type uu} (s : List α) (hs : ) :