chore: add missing simp for array size lemmas (#982)

Batteries/Data/Array/Lemmas.lean

@@ -78,7 +78,7 @@ theorem toList_zipWith (f : α → β → γ) (as : Array α) (bs : Array β) :
 @[deprecated (since := "2024-09-09")] alias data_zipWith := toList_zipWith
 @[deprecated (since := "2024-08-13")] alias zipWith_eq_zipWith_data := data_zipWith
 
-theorem size_zipWith (as : Array α) (bs : Array β) (f : α → β → γ) :
+@[simp] theorem size_zipWith (as : Array α) (bs : Array β) (f : α → β → γ) :
     (as.zipWith bs f).size = min as.size bs.size := by
   rw [size_eq_length_toList, toList_zipWith, List.length_zipWith]
 
@@ -88,7 +88,7 @@ theorem toList_zip (as : Array α) (bs : Array β) :
 @[deprecated (since := "2024-09-09")] alias data_zip := toList_zip
 @[deprecated (since := "2024-08-13")] alias zip_eq_zip_data := data_zip
 
-theorem size_zip (as : Array α) (bs : Array β) :
+@[simp] theorem size_zip (as : Array α) (bs : Array β) :
     (as.zip bs).size = min as.size bs.size :=
   as.size_zipWith bs Prod.mk
 
@@ -150,19 +150,23 @@ where
 /-! ### shrink -/
 
 theorem size_shrink_loop (a : Array α) (n) : (shrink.loop n a).size = a.size - n := by
-  induction n generalizing a with simp[shrink.loop]
-  | succ n ih =>
-      simp[ih]
-      omega
+  induction n generalizing a with simp only [shrink.loop, Nat.sub_zero]
+  | succ n ih => simp only [ih, size_pop]; omega
 
-theorem size_shrink (a : Array α) (n) : (a.shrink n).size = min a.size n := by
+@[simp] theorem size_shrink (a : Array α) (n) : (a.shrink n).size = min a.size n := by
   simp [shrink, size_shrink_loop]
   omega
 
 /-! ### set -/
 
-theorem size_set! (a : Array α) (i v) : (a.set! i v).size = a.size := by
-  rw [set!_is_setD, size_setD]
+theorem size_set! (a : Array α) (i v) : (a.set! i v).size = a.size := by simp
+
+/-! ### swapAt -/
+
+theorem size_swapAt (a : Array α) (x i) : (a.swapAt i x).snd.size = a.size := by simp
+
+@[simp] theorem size_swapAt! (a : Array α) (x) (h : i < a.size) :
+    (a.swapAt! i x).snd.size = a.size := by simp [h]
 
 /-! ### map -/
 
@@ -190,7 +194,7 @@ private theorem size_insertAt_loop (as : Array α) (i : Fin (as.size+1)) (j : Fi
   · rw [size_insertAt_loop, size_swap]
   · rfl
 
-theorem size_insertAt (as : Array α) (i : Fin (as.size+1)) (v : α) :
+@[simp] theorem size_insertAt (as : Array α) (i : Fin (as.size+1)) (v : α) :
     (as.insertAt i v).size = as.size + 1 := by
   rw [insertAt, size_insertAt_loop, size_push]