chore: lemma for unfolding eraseIdxIfInBounds (#10520)

src/Init/Data/Array/Basic.lean

@@ -1799,7 +1799,6 @@ Examples:
 * `#["apple", "pear", "orange"].eraseIdxIfInBounds 3 = #["apple", "pear", "orange"]`
 * `#["apple", "pear", "orange"].eraseIdxIfInBounds 5 = #["apple", "pear", "orange"]`
 -/
-@[grind]
 def eraseIdxIfInBounds (xs : Array α) (i : Nat) : Array α :=
   if h : i < xs.size then xs.eraseIdx i h else xs
 

src/Init/Data/Array/Erase.lean

@@ -324,6 +324,13 @@ abbrev erase_mkArray_ne := @erase_replicate_ne
 
 end erase
 
+/-! ### eraseIdxIfInBounds -/
+
+@[grind =]
+theorem eraseIdxIfInBounds_eq {xs : Array α} {i : Nat} :
+    xs.eraseIdxIfInBounds i = if h : i < xs.size then xs.eraseIdx i else xs := by
+  simp [eraseIdxIfInBounds]
+
 /-! ### eraseIdx -/
 
 theorem eraseIdx_eq_eraseIdxIfInBounds {xs : Array α} {i : Nat} (h : i < xs.size) :