feat: more lemmas

Batteries/Data/DArray/Lemmas.lean

@@ -73,3 +73,14 @@ theorem umodify_eq_modify (a : DArray n α) (i : USize) (h : i.toNat < n)
 
 @[simp]
 theorem copy_eq (a : DArray n α) : a.copy = a := rfl
+
+theorem get_map {β : Fin n → Type _} (f : {i : Fin n} → α i → β i) (a : DArray n α) (i : Fin n) :
+    (a.map f).get i = f (a.get i) := rfl
+
+@[simp]
+theorem size_amap (f : {i : Fin n} → α i → β) (a : DArray n α) :
+    (a.amap f).size = n := Array.size_ofFn ..
+
+theorem getElem_amap (f : {i : Fin n} → α i → β) (a : DArray n α) (i : Fin n)
+    (h : i.val < (a.amap f).size := (a.size_amap f).symm ▸ i.is_lt) :
+    (a.amap f)[i] = f (a.get i) := by simp [amap]