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

This is a stronger version of Array.extract_append_left, and should be upstreamed to replace that.

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)

This is a stronger version of Array.extract_append_right, and should be upstreamed to replace that.

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