LeanPool.ErdosTuzaValtr.Lib.List.Lemmas

Imported Lean Pool material for LeanPool.ErdosTuzaValtr.Lib.List.Lemmas.

theorem List.in_superset {α : Type u_1} {l : List α} {S T : Finset α} (h : S ⊆ T) : l.In S → l.In T

theorem List.subset_in {α : Type u_1} {l1 l2 : List α} {S : Finset α} (h : l1 ⊆ l2) (h_l2 : l2.In S) : l1.In S

@[simp]

theorem List.nil_in {α : Type u_1} {S : Finset α} : [].In S

@[simp]

theorem List.cons_in {α : Type u_1} {a : α} {l : List α} {S : Finset α} : (a :: l).In S ↔ a ∈ S ∧ l.In S

@[simp]

theorem List.append_in {α : Type u_1} {l1 l2 : List α} {S : Finset α} : (l1 ++ l2).In S ↔ l1.In S ∧ l2.In S

@[simp]

theorem List.reverse_in {α : Type u_1} {l : List α} {S : Finset α} : l.reverse.In S ↔ l.In S

theorem List.reverse_getLast {α : Type u_1} {l : List α} : l.reverse.getLast? = l.head?

theorem List.reverse_head {α : Type u_1} {l : List α} : l.reverse.head? = l.getLast?

@[simp]

theorem List.Mirror_nil {α : Type u_1} : [].Mirror = []

@[simp]

theorem List.Mirror_singleton {α : Type u_1} {a : α} : [a].Mirror = [OrderDual.toDual a]

@[simp]

theorem List.Mirror_cons {α : Type u_1} {a : α} {l : List α} : (a :: l).Mirror = l.Mirror ++ [OrderDual.toDual a]

@[simp]

theorem List.Mirror_append {α : Type u_1} {l1 l2 : List α} : (l1 ++ l2).Mirror = l2.Mirror ++ l1.Mirror

@[simp]

theorem List.ofMirror_nil {α : Type u_1} : [].ofMirror = []

@[simp]

theorem List.ofMirrorMirror {α : Type u_1} {l : List αᵒᵈ} : l.ofMirror.Mirror = l

@[simp]

theorem Finset.ofMirrorMirror {α : Type u_1} [LinearOrder α] {S : Finset αᵒᵈ} : S.ofMirror.Mirror = S

@[simp]

theorem List.Mirror_length {α : Type u_1} {l : List α} : l.Mirror.length = l.length

theorem List.chain'_mirror {α : Type u_1} [LinearOrder α] {l : List α} : IsChain (fun (x1 x2 : αᵒᵈ) => x1 < x2) l.Mirror ↔ IsChain (fun (x1 x2 : α) => x1 < x2) l

theorem List.Mirror_getLast {α : Type u_1} {l : List α} : l.Mirror.getLast? = Option.map (⇑OrderDual.toDual) l.head?

theorem List.Mirror_head {α : Type u_1} {l : List α} : l.Mirror.head? = Option.map (⇑OrderDual.toDual) l.getLast?

theorem List.ofMirror_getLast {α : Type u_1} {l : List αᵒᵈ} : l.ofMirror.getLast? = Option.map (⇑OrderDual.ofDual) l.head?

theorem List.ofMirror_head {α : Type u_1} {l : List αᵒᵈ} : l.ofMirror.head? = Option.map (⇑OrderDual.ofDual) l.getLast?

theorem List.Mirror_mem_getLast {α : Type u_1} {a : α} {l : List α} : OrderDual.toDual a ∈ l.Mirror.getLast? ↔ a ∈ l.head?

theorem List.Mirror_mem_head {α : Type u_1} {a : α} {l : List α} : OrderDual.toDual a ∈ l.Mirror.head? ↔ a ∈ l.getLast?

@[simp]

theorem List.Mirror_in {α : Type u_1} [LinearOrder α] {l : List α} {S : Finset α} : l.Mirror.In S.Mirror ↔ l.In S

@[simp]

theorem Finset.memMirror {α : Type u_1} [LinearOrder α] {a : α} {S : Finset α} : OrderDual.toDual a ∈ S.Mirror ↔ a ∈ S

@[simp]

theorem Finset.Mirror_card {α : Type u_1} [LinearOrder α] {S : Finset α} : S.Mirror.card = S.card

@[simp]

theorem List.getLast?_cons_append_cons {α : Type u_1} (a b : α) (l1 l2 : List α) : (a :: (l1 ++ b :: l2)).getLast? = (b :: l2).getLast?

def List.takeHead' {α : Type u_1} {a : α} {l : List α} : a ∈ l.head? → (t : List α) ×' l = a :: t

Split off the head of a list given a witness that a is its head.

Equations

• List.takeHead' h = absurd h ⋯
• List.takeHead' h = ⟨t, ⋯⟩

def List.takeHead {α : Type u_1} {l : List α} : l ≠ [] → (h1 : α) ×' (t : List α) ×' l = h1 :: t

Split a nonempty list into its head and tail.

Equations

• List.takeHead h = absurd ⋯ h
• List.takeHead x_2 = ⟨h1, ⟨t, ⋯⟩⟩

def List.takeHead2 {α : Type u_1} {l : List α} : 2 ≤ l.length → (h1 : α) ×' (h2 : α) ×' (t : List α) ×' l = h1 :: h2 :: t

Split a list of length at least 2 into its first two elements and the rest.

Equations

• List.takeHead2 h = absurd h ⋯
• List.takeHead2 h = absurd h ⋯
• List.takeHead2 x_2 = ⟨a, ⟨b, ⟨t, ⋯⟩⟩⟩

def List.takeHead3 {α : Type u_1} {l : List α} : 3 ≤ l.length → (h1 : α) ×' (h2 : α) ×' (h3 : α) ×' (t : List α) ×' l = h1 :: h2 :: h3 :: t

Split a list of length at least 3 into its first three elements and the rest.

Equations

• List.takeHead3 h = absurd h ⋯
• List.takeHead3 h = absurd h ⋯
• List.takeHead3 h = absurd h ⋯
• List.takeHead3 x_2 = ⟨a, ⟨b, ⟨c, ⟨t, ⋯⟩⟩⟩⟩

def List.takeLast' {α : Type u_1} {a : α} {l : List α} : a ∈ l.getLast? → (l' : List α) ×' l = l' ++ [a]

Split off the last element of a list given a witness that a is its last element.

Equations

• List.takeLast' h = absurd h ⋯
• List.takeLast' h = ⟨[], ⋯⟩
• List.takeLast' h = match List.takeLast' ⋯ with | ⟨l'', hl''⟩ => ⟨b :: l'', ⋯⟩

def List.takeLast {α : Type u_1} {l : List α} : l ≠ [] → (e1 : α) ×' (m : List α) ×' l = m ++ [e1]

Split a nonempty list into its last element and the preceding prefix.

Equations

• List.takeLast h = absurd ⋯ h
• List.takeLast x_2 = ⟨a, ⟨[], ⋯⟩⟩
• List.takeLast x_2 = match List.takeLast ⋯ with | ⟨e1, ⟨m', eq_l'⟩⟩ => ⟨e1, ⟨a :: m', ⋯⟩⟩

def List.takeLast2 {α : Type u_1} {l : List α} : 2 ≤ l.length → (e1 : α) ×' (e2 : α) ×' (m : List α) ×' l = m ++ [e1, e2]

Split a list of length at least 2 into its last two elements and the preceding prefix.

Equations

• List.takeLast2 h = absurd h ⋯
• List.takeLast2 h = absurd h ⋯
• List.takeLast2 x_2 = ⟨a, ⟨b, ⟨[], ⋯⟩⟩⟩
• List.takeLast2 x_2 = match List.takeLast2 ⋯ with | ⟨e1, ⟨e2, ⟨m', eq_l'⟩⟩⟩ => ⟨e1, ⟨e2, ⟨a :: m', ⋯⟩⟩⟩

def List.takeLast3 {α : Type u_1} {l : List α} : 3 ≤ l.length → (e1 : α) ×' (e2 : α) ×' (e3 : α) ×' (m : List α) ×' l = m ++ [e1, e2, e3]

Split a list of length at least 3 into its last three elements and the preceding prefix.

Equations

• List.takeLast3 h = absurd h ⋯
• List.takeLast3 h = absurd h ⋯
• List.takeLast3 h = absurd h ⋯
• List.takeLast3 x_2 = ⟨a, ⟨b, ⟨c, ⟨[], ⋯⟩⟩⟩⟩
• List.takeLast3 x_2 = match List.takeLast3 ⋯ with | ⟨e1, ⟨e2, ⟨e3, ⟨m', eq_l'⟩⟩⟩⟩ => ⟨e1, ⟨e2, ⟨e3, ⟨a :: m', ⋯⟩⟩⟩⟩