List lemmas

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

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) : r.insertIdx (↑n) i = 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) : (r.insertIdx (↑n) i).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) : (r.insertIdx (↑k) i)[↑(k.succAbove m)] = r[↑m]

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

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

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

theorem PhysLean.List.take_insert_same {I : Type} (i : I) (n : ℕ) (r : List I) : List.take n (r.insertIdx n i) = 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 (r.insertIdx m i) = 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) (r.insertIdx m i)).Perm (i :: List.take n r)