feat: Array lemma for empty map added (#877)

Co-authored-by: François G. Dorais <fgdorais@gmail.com>

Batteries/Data/Array/Lemmas.lean

@@ -126,3 +126,10 @@ theorem size_shrink_loop (a : Array α) (n) : (shrink.loop n a).size = a.size -
 theorem size_shrink (a : Array α) (n) : (a.shrink n).size = min a.size n := by
   simp [shrink, size_shrink_loop]
   omega
+
+/-! ### map -/
+
+theorem mapM_empty [Monad m] (f : α → m β) : mapM f #[] = pure #[] := by
+  rw [mapM, mapM.map]; rfl
+
+@[simp] theorem map_empty (f : α → β) : map f #[] = #[] := mapM_empty ..