Auxiliary lemmas for List

theorem List.append_getLast_dropLast {α : Type u} (l : List α) (h : l ≠ []) : l.dropLast ++ [l.getLast h] = l

theorem List.foldl_congr_of_mem {α : Type u} {β : Type v} {f g : α → β → α} (xs : List β) (acc : α) (h : ∀ (acc' : α), ∀ x ∈ xs, f acc' x = g acc' x) : foldl f acc xs = foldl g acc xs

theorem List.foldl_split_outer {α : Type u} {β : Type v} (f : α → β → α) (init : α) (l : List β) (h : l ≠ []) : foldl f init l = f (foldl f init l.dropLast) (l.getLast h)

theorem List.foldl_split_inner {α : Type u} {β : Type v} (f : α → β → α) (init : α) (l : List β) (h : l ≠ []) : foldl f init l = foldl f (f init (l.head h)) l.tail

theorem List.foldr_split_outer {α : Type u} {β : Type v} (f : α → β → β) (init : β) (l : List α) (h : l ≠ []) : foldr f init l = f (l.head h) (foldr f init l.tail)

theorem List.foldr_split_inner {α : Type u} {β : Type v} (f : α → β → β) (init : β) (l : List α) (h : l ≠ []) : foldr f init l = foldr f (f (l.getLast h) init) l.dropLast

theorem List.mapM_single {m : Type u → Type v} [Monad m] [LawfulMonad m] {α : Type w} {β : Type u} (f : α → m β) (a : α) : mapM f [a] = do let __do_lift ← f a pure [__do_lift]

@[simp]

theorem List.getLastI_append_single {α : Type w} (l : List α) [Inhabited α] (x : α) : (l ++ [x]).getLastI = x

@[simp]

theorem List.leftpad_eq_self {α : Type u_1} {unit : α} (l : List α) (n : ℕ) (h : l.length ≥ n) : leftpad n unit l = l

@[simp]

theorem List.rightpad_length {α : Type u_1} (n : ℕ) (unit : α) (l : List α) : (rightpad n unit l).length = max n l.length

@[simp]

theorem List.rightpad_prefix {α : Type u_1} (n : ℕ) (unit : α) (l : List α) : l <+: rightpad n unit l

@[simp]

theorem List.rightpad_suffix {α : Type u_1} (n : ℕ) (unit : α) (l : List α) : replicate (n - l.length) unit <:+ rightpad n unit l

@[simp]

theorem List.rightpad_eq_self {α : Type u_1} {unit : α} (l : List α) (n : ℕ) (h : n ≤ l.length) : rightpad n unit l = l

theorem List.rightpad_eq_rightpad_max {α : Type u_1} {unit : α} (l : List α) (n : ℕ) : rightpad n unit l = rightpad (max n l.length) unit l

theorem List.rightpad_eq_rightpad_append_replicate_of_ge {α : Type u_1} {unit : α} (l : List α) (m n : ℕ) (h : n ≤ m) : rightpad m unit l = rightpad n unit l ++ replicate (m - max n l.length) unit

theorem List.rightpad_eq_if_rightpad_eq_of_ge {α : Type u_1} {unit : α} (l l' : List α) (m n n' : ℕ) (h : n ≤ m) (h' : n' ≤ m) : rightpad n unit l = rightpad n' unit l' → rightpad m unit l = rightpad m unit l'

@[simp]

theorem List.rightpad_twice_eq_rightpad_max {α : Type u_1} (m n : ℕ) (unit : α) (l : List α) : rightpad n unit (rightpad m unit l) = rightpad (max m n) unit l

@[simp]

theorem List.rightpad_getD_eq_getD {α : Type u_1} (l : List α) (n : ℕ) (unit : α) (i : ℕ) : (rightpad n unit l).getD i unit = l.getD i unit

theorem List.rightpad_getElem_eq_getD {α : Type u_1} {a b : List α} {unit : α} {i : ℕ} (h : i < (rightpad b.length unit a).length) : (rightpad b.length unit a)[i] = a.getD i unit

def List.matchSize {α : Type u_1} (l₁ l₂ : List α) (unit : α) : List α × List α

Given two lists of potentially different lengths, right-pads the shorter list with unit elements until they are the same length.

theorem List.matchSize_comm {α : Type u_1} (l₁ l₂ : List α) (unit : α) : l₁.matchSize l₂ unit = (l₂.matchSize l₁ unit).swap

theorem List.matchSize_eq_iff_forall_eq {α : Type u_1} (l₁ l₂ : List α) (unit : α) : (fun (x : List α × List α) => match x with | (x, y) => x = y) (l₁.matchSize l₂ unit) ↔ ∀ (i : ℕ), l₁.getD i unit = l₂.getD i unit

List.matchSize returns two equal lists iff the two lists agree at every index i : Nat (extended by unit if necessary).

def List.dropLastWhile {α : Type u_1} (p : α → Bool) (l : List α) : List α

List.dropWhile but starting from the last element. Performed by dropWhile on the reversed list, followed by a reversal.

theorem List.zipWith_const {α : Type u_2} {β : Type u_3} {f : α → β → β} {l₁ : List α} {l₂ : List β} (h₁ : l₁.length = l₂.length) (h₂ : ∀ (a : α) (b : β), f a b = b) : zipWith f l₁ l₂ = l₂

theorem List.Nodup.pairwise_ne_map {α : Type u} {β : Type v} {l : List α} {f : α → β} (hf : Function.Injective f) (hl : l.Nodup) : Pairwise (fun (a b : α) => f a ≠ f b) l

An injective f separates the elements of a duplicate-free list pairwise.

This is List.Nodup.map transported along List.pairwise_map, stated in the unmapped form that Std.ExtTreeMap.getElem_ofList_of_mem and friends ask for.