theorem List.singleton_val_of {α : Type u_1} (a : α) (arr : List α) (h1 : arr = [a]) (h2 : 0 < arr.length) : arr.get ⟨0, h2⟩ = a

theorem List.singleton_val {α : Type u_1} (a : α) (h : 0 < [a].length) : [a].get ⟨0, h⟩ = a

theorem List.get_of_fun_eq {α : Type u_1} {l1 : List α} {l2 : List α} {f : List α → List α} (h : f l1 = f l2) (n : Fin (f l1).length) : (f l1).get n = (f l2).get ⟨↑n, ⋯⟩

theorem List.eq_of_dropLast_eq_last_eq {α : Type u_1} {l1 : List α} {l2 : List α} (hd : l1.dropLast = l2.dropLast) (hl1 : l1.length - 1 < l1.length) (hl2 : l2.length - 1 < l2.length) (heq : l1.get ⟨l1.length - 1, hl1⟩ = l2.get ⟨l2.length - 1, hl2⟩) : l1 = l2

theorem List.get_last_of_concat {α : Type u_1} {last : α} {l : List α} (h : (l ++ [last]).length - 1 < (l ++ [last]).length) : (l ++ [last]).get ⟨(l ++ [last]).length - 1, h⟩ = last

theorem List.eq_succ_of_tail_nth {α : Type u_1} {n : Nat} {head : α} {tail : List α} (data : List α) (h1 : n + 1 < data.length) (h2 : data = head :: tail) (h3 : n < tail.length) : tail.get ⟨n, h3⟩ = data.get ⟨n + 1, h1⟩

theorem List.eq_succ_of_tail_nth_pred {α : Type u_1} {n : Nat} {head : α} {tail : List α} (data : List α) (h0 : n ≠ 0) (h1 : n < data.length) (h2 : data = head :: tail) (h3 : n - 1 < tail.length) : tail.get ⟨n - 1, h3⟩ = data.get ⟨n, h1⟩

theorem List.chain_split {α : Type u_1} {R : α → α → Prop} {a : α} {b : α} {l₁ : List α} {l₂ : List α} : List.Chain R a (l₁ ++ b :: l₂) ↔ List.Chain R a (l₁ ++ [b]) ∧ List.Chain R b l₂

theorem List.chain_append_cons_cons {α : Type u_1} {R : α → α → Prop} {a : α} {b : α} {c : α} {l₁ : List α} {l₂ : List α} : List.Chain R a (l₁ ++ b :: c :: l₂) ↔ List.Chain R a (l₁ ++ [b]) ∧ R b c ∧ List.Chain R c l₂

theorem List.chain_iff_get {α : Type u_1} {R : α → α → Prop} {a : α} {l : List α} : List.Chain R a l ↔ (∀ (h : 0 < l.length), R a (l.get ⟨0, h⟩)) ∧ ∀ (i : Nat) (h : i < l.length - 1), R (l.get ⟨i, ⋯⟩) (l.get ⟨i + 1, ⋯⟩)