From e2f87ed2152344e4c93a135ec8c4470740aa943e Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Tue, 23 Sep 2025 23:08:41 +1000
Subject: [PATCH] chore: lemma for unfolding eraseIdxIfInBounds (#10520)

---
 src/Init/Data/Array/Basic.lean | 1 -
 src/Init/Data/Array/Erase.lean | 7 +++++++
 2 files changed, 7 insertions(+), 1 deletion(-)

diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index ebf062adb9..77ed69c4eb 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/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
 
diff --git a/src/Init/Data/Array/Erase.lean b/src/Init/Data/Array/Erase.lean
index 083f47cfc3..8194d36553 100644
--- a/src/Init/Data/Array/Erase.lean
+++ b/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) :