Array lemmas

@[simp]

theorem Array.getElem_map_fin {α β : Type} (f : α → β) (x : Array α) {n : ℕ} (i : Fin n) (h : ↑i < (map f x).size) : (map f x)[i] = f x[i]

theorem Array.getElem_eq_getElem! {α : Type} [Inhabited α] (d : Array α) {n : ℕ} (i : Fin n) (h : ↑i < d.size) : d[i] = d[i]!

@[simp]

theorem Fin.getElem_fin' {Cont Elem : Type} {Dom : Cont → ℕ → Prop} [GetElem Cont ℕ Elem Dom] (a : Cont) {n : ℕ} (i : Fin n) (h : Dom a ↑i) : a[i] = a[↑i]

ByteArray lemmas

@[simp]

theorem ByteArray.size_mkEmpty (c : ℕ) : (emptyWithCapacity c).size = 0

theorem ByteArray.getElem_eq_data_getElem' (d : ByteArray) (i : Fin d.size) : d[i] = d.data[i]

theorem ByteArray.getElem_eq_getElem! (d : ByteArray) (i : Fin d.size) : d[i] = d[i]!

theorem ByteArray.getElemNat_eq_getElem! {d : ByteArray} {i : ℕ} (h : i < d.size) : d[i] = d[i]!

theorem ByteArray.getElem!_push (d : ByteArray) (c : UInt8) (i : ℕ) : (d.push c)[i]! = if i < d.size then d[i]! else if i = d.size then c else default

theorem Array.getElem?_eq_toList_get?' {α : Type} (a : Array α) (i : ℕ) : a[i]? = a.toList[i]?

theorem ByteArray.getElem!_append (d0 d1 : ByteArray) (i : ℕ) : (d0 ++ d1)[i]! = if i < d0.size then d0[i]! else d1[i - d0.size]!