Lemmas about Array.extract

Some useful lemmas about Array.extract

@[simp]

theorem Array.extract_eq_nil_of_start_eq_end {α : Type u} {i : Nat} {a : Array α} : a.extract i i = #[]

theorem Array.extract_append_left {α : Type u} {a b : Array α} {i j : Nat} (h : j ≤ a.size) : (a ++ b).extract i j = a.extract i j

theorem Array.extract_append_right {α : Type u} {a b : Array α} {i j : Nat} (h : a.size ≤ i) : (a ++ b).extract i j = b.extract (i - a.size) (j - a.size)

theorem Array.extract_eq_of_size_le_end {α : Type u} {l p : Nat} {a : Array α} (h : a.size ≤ l) : a.extract p l = a.extract p a.size

theorem Array.extract_extract {α : Type u} {s1 e2 e1 s2 : Nat} {a : Array α} (h : s1 + e2 ≤ e1) : (a.extract s1 e1).extract s2 e2 = a.extract (s1 + s2) (s1 + e2)