List lemmas

theorem PhysLean.List.insertIdx_map {I J : Type} (f : I → J) (i : ℕ) (r : List I) (r0 : I) : List.map f (List.insertIdx i r0 r) = List.insertIdx i (f r0) (List.map f r)

theorem PhysLean.List.eraseIdx_sorted {I : Type} (le : I → I → Prop) (r : List I) (n : ℕ) : List.Sorted le r → List.Sorted le (r.eraseIdx n)

theorem PhysLean.List.mem_eraseIdx_nodup {I : Type} (i : I) (l : List I) (n : ℕ) (hn : n < l.length) (h : l.Nodup) : i ∈ l.eraseIdx n ↔ i ∈ l ∧ i ≠ l[n]

theorem PhysLean.List.insertIdx_eq_take_drop {I : Type} (i : I) (r : List I) (n : Fin r.length.succ) : List.insertIdx (↑n) i r = List.take (↑n) r ++ i :: List.drop (↑n) r

@[simp]

theorem PhysLean.List.insertIdx_length_fin {I : Type} (i : I) (r : List I) (n : Fin r.length.succ) : (List.insertIdx (↑n) i r).length = r.length.succ

@[simp]

theorem PhysLean.List.insertIdx_getElem_fin {I : Type} (i : I) (r : List I) (k : Fin r.length.succ) (m : Fin r.length) : (List.insertIdx (↑k) i r)[↑(k.succAbove m)] = r[↑m]

theorem PhysLean.List.insertIdx_eraseIdx_fin {I : Type} (r : List I) (k : Fin r.length) : List.insertIdx (↑k) r[k] (r.eraseIdx ↑k) = r

theorem PhysLean.List.insertIdx_length_fst_append {I : Type} (φ : I) (φs φs' : List I) : List.insertIdx φs.length φ (φs ++ φs') = φs ++ φ :: φs'

theorem PhysLean.List.get_eq_insertIdx_succAbove {I : Type} (i : I) (r : List I) (k : Fin r.length.succ) : r.get = (List.insertIdx (↑k) i r).get ∘ ⇑(finCongr ⋯) ∘ k.succAbove

theorem PhysLean.List.take_insert_same {I : Type} (i : I) (n : ℕ) (r : List I) : List.take n (List.insertIdx n i r) = List.take n r

theorem PhysLean.List.take_eraseIdx_same {I : Type} (n : ℕ) (r : List I) : List.take n (r.eraseIdx n) = List.take n r

theorem PhysLean.List.drop_eraseIdx_succ {I : Type} (n : ℕ) (r : List I) (hn : n < r.length) : r[n] :: List.drop n (r.eraseIdx n) = List.drop n r

theorem PhysLean.List.take_insert_gt {I : Type} (i : I) (n m : ℕ) (h : n < m) (r : List I) : List.take n (List.insertIdx m i r) = List.take n r

theorem PhysLean.List.take_insert_let {I : Type} (i : I) (n m : ℕ) (h : m ≤ n) (r : List I) (hm : m ≤ r.length) : (List.take (n + 1) (List.insertIdx m i r)).Perm (i :: List.take n r)