theorem List.Perm.two_iff {α : Type u_1} {a b : α} {l : List α} : l.Perm [a, b] ↔ l = [a, b] ∨ l = [b, a]

inductive List.CompSubset {α : Type u_1} : List α → List α → Type u_1

• refl {α : Type u_1} (l : List α) : l.CompSubset l
• perm {α : Type u_1} {l₁ l₂ l₃ : List α} : l₁.CompSubset l₂ → l₂.Perm l₃ → l₁.CompSubset l₃
• add {α : Type u_1} {l₁ l₂ : List α} (a : α) : l₁.CompSubset l₂ → l₁.CompSubset (a :: l₂)
• double {α : Type u_1} {l₁ l₂ : List α} {a : α} : l₁.CompSubset (a :: a :: l₂) → l₁.CompSubset (a :: l₂)

theorem List.remove_def {α : Type u_1} [DecidableEq α] (a b : α) (l : List α) : remove a (b :: l) = if a = b then remove a l else b :: remove a l

theorem List.count_def {α : Type u_1} [DecidableEq α] (a b : α) (l : List α) : count a (b :: l) = if a = b then count a l + 1 else count a l

theorem List.perm_normalize {α : Type u_1} [DecidableEq α] (l : List α) (a : α) : l.Perm (replicate (count a l) a ++ remove a l)

def List.CompSubset.iterated_double {α : Type u_1} {k : ℕ} {l₁ l₂ : List α} {a : α} (h : k > 0) (c : l₁.CompSubset (replicate k a ++ l₂)) : l₁.CompSubset (a :: l₂)

Equations

• List.CompSubset.iterated_double h_2 c_2 = c_2
• List.CompSubset.iterated_double h_2 c_2 = List.CompSubset.iterated_double ⋯ c_2.double

def List.CompSubset.trans {α : Type u_1} {l₁ l₂ l₃ : List α} (c₁ : l₁.CompSubset l₂) (c₂ : l₂.CompSubset l₃) : l₁.CompSubset l₃

Equations

• c₁.trans (List.CompSubset.refl l₂) = c₁
• c₁.trans (c₂_2.perm hp) = (c₁.trans c₂_2).perm hp
• c₁.trans (List.CompSubset.add b c₂_2) = List.CompSubset.add b (c₁.trans c₂_2)
• c₁.trans c₂_2.double = (c₁.trans c₂_2).double

def List.CompSubset.cons {α : Type u_1} [DecidableEq α] {l₁ l₂ : List α} (c : l₁.CompSubset l₂) (a : α) : (a :: l₁).CompSubset (a :: l₂)

Equations

• (List.CompSubset.refl l₁).cons a = List.CompSubset.refl (a :: l₁)
• (c₂_1.perm hp).cons a = (c₂_1.cons a).perm ⋯
• (List.CompSubset.add b c₂_1).cons a = (List.CompSubset.add b (c₂_1.cons a)).perm ⋯
• c₂_1.double.cons a = ((c₂_1.cons a).perm ⋯).double.perm ⋯

def List.Subset.toCompSubst {α : Type u_1} [DecidableEq α] {l₁ l₂ : List α} (h : l₁ ⊆ l₂) : l₁.CompSubset l₂

Equations

• One or more equations did not get rendered due to their size.
• List.Subset.toCompSubst h_2 = ⋯ ▸ ⋯ ▸ List.CompSubset.refl []