feat: Add getElem_swapIfInBounds* lemmas and deprecate getElem_swap'

src/Init/Data/Array/Lemmas.lean

@@ -4095,17 +4095,21 @@ theorem getElem?_modify {xs : Array α} {i : Nat} {f : α → α} {j : Nat} :
     (hi' : k ≠ i) (hj' : k ≠ j) : (xs.swap i j hi hj)[k]'(xs.size_swap .. |>.symm ▸ hp) = xs[k] := by
   simp [swap_def, getElem_set, hi'.symm, hj'.symm]
 
+@[grind]
+theorem getElem_swap {xs : Array α} {i j : Nat} (hi hj) {k : Nat} (hk : k < (xs.swap i j hi hj).size) :
+    (xs.swap i j hi hj)[k] = if k = i then xs[j] else if k = j then xs[i] else xs[k]'(by simp_all) := by
+  simp only [size_swap] at hk
+  split
+  · simp_all only [getElem_swap_left]
+  · split <;> simp_all
+
+@[deprecated getElem_swap (since := "2025-05-19")]
 theorem getElem_swap' {xs : Array α} {i j : Nat} {hi hj} {k : Nat} (hk : k < xs.size) :
     (xs.swap i j hi hj)[k]'(by simp_all) = if k = i then xs[j] else if k = j then xs[i] else xs[k] := by
   split
   · simp_all only [getElem_swap_left]
   · split <;> simp_all
 
-@[grind]
-theorem getElem_swap {xs : Array α} {i j : Nat} (hi hj) {k : Nat} (hk : k < (xs.swap i j hi hj).size) :
-    (xs.swap i j hi hj)[k] = if k = i then xs[j] else if k = j then xs[i] else xs[k]'(by simp_all) := by
-  apply getElem_swap'
-
 @[simp] theorem swap_swap {xs : Array α} {i j : Nat} (hi hj) :
     (xs.swap i j hi hj).swap i j ((xs.size_swap ..).symm ▸ hi) ((xs.size_swap ..).symm ▸ hj) = xs := by
   apply ext
@@ -4125,11 +4129,79 @@ theorem swap_comm {xs : Array α} {i j : Nat} (hi hj) : xs.swap i j hi hj = xs.s
     · split <;> simp_all
     · split <;> simp_all
 
+/-! ### swapIfInBounds -/
+
 @[simp] theorem size_swapIfInBounds {xs : Array α} {i j : Nat} :
     (xs.swapIfInBounds i j).size = xs.size := by unfold swapIfInBounds; split <;> (try split) <;> simp [size_swap]
 
 @[deprecated size_swapIfInBounds (since := "2024-11-24")] abbrev size_swap! := @size_swapIfInBounds
 
+@[simp]
+theorem getElem_swapIfInBounds_of_ge_left {xs : Array α} {i j k : Nat} (h : xs.size ≤ i)
+    (hk : k < (xs.swapIfInBounds i j).size) :
+    (xs.swapIfInBounds i j)[k] = xs[k]'(Nat.lt_of_lt_of_eq hk size_swapIfInBounds) := by
+  unfold swapIfInBounds
+  simp only [dif_neg (Nat.not_lt_of_le h)]
+
+@[simp]
+theorem getElem_swapIfInBounds_of_ge_right {xs : Array α} {i j k : Nat} (h : xs.size ≤ j)
+    (hk : k < (xs.swapIfInBounds i j).size) :
+    (xs.swapIfInBounds i j)[k] = xs[k]'(Nat.lt_of_lt_of_eq hk size_swapIfInBounds) := by
+  unfold swapIfInBounds
+  simp only [dif_neg (Nat.not_lt_of_le h), dite_eq_ite, ite_self]
+
+@[simp]
+theorem getElem_swapIfInBounds_left {xs : Array α} {i j : Nat} (hj : j < xs.size)
+    (hi : i < (xs.swapIfInBounds i j).size) : (xs.swapIfInBounds i j)[i] = xs[j] := by
+  simp only [size_swapIfInBounds] at hi
+  unfold swapIfInBounds
+  simp only [dif_pos hi, dif_pos hj]
+  exact getElem_swap_left
+
+@[simp]
+theorem getElem_swapIfInBounds_right {xs : Array α} {i j : Nat} (hi : i < xs.size)
+    (hj : j < (xs.swapIfInBounds i j).size) :
+    (xs.swapIfInBounds i j)[j] = xs[i] := by
+  simp only [size_swapIfInBounds] at hj
+  unfold swapIfInBounds
+  simp only [dif_pos hi, dif_pos hj]
+  exact getElem_swap_right
+
+@[simp]
+theorem getElem_swapIfInBounds_of_ne_ne {xs : Array α} {i j k : Nat} (hi : k ≠ i) (hj : k ≠ j)
+    (hk : k < (xs.swapIfInBounds i j).size) :
+    (xs.swapIfInBounds i j)[k] = xs[k]'(Nat.lt_of_lt_of_eq hk size_swapIfInBounds) := by
+  simp only [size_swapIfInBounds] at hk
+  unfold swapIfInBounds
+  split
+  · split
+    · exact getElem_swap_of_ne _ hi hj
+    · rfl
+  · rfl
+
+theorem getElem_swapIfInBounds {xs : Array α} {i j k : Nat}
+    (hk : k < (xs.swapIfInBounds i j).size) : (xs.swapIfInBounds i j)[k] =
+    if h : k = i ∧ j < xs.size then xs[j]'h.2
+    else  if h₂ : k = j ∧ i < xs.size then xs[i]'h₂.2
+          else xs[k]'(Nat.lt_of_lt_of_eq hk size_swapIfInBounds) := by
+  simp only [size_swapIfInBounds] at hk
+  split
+  · case isTrue hij =>
+    cases hij.1
+    exact getElem_swapIfInBounds_left _ _
+  · case isFalse hij =>
+    split
+    · case isTrue hij =>
+      cases hij.1
+      exact getElem_swapIfInBounds_right _ _
+    · case isFalse hji =>
+      simp only [not_and, Nat.not_lt] at hij hji
+      by_cases hki : k = i
+      · exact getElem_swapIfInBounds_of_ge_right (hij hki) _
+      · by_cases hkj : k = j
+        · exact getElem_swapIfInBounds_of_ge_left (hji hkj) _
+        · exact getElem_swapIfInBounds_of_ne_ne hki hkj _
+
 /-! ### swapAt -/
 
 @[simp] theorem swapAt_def {xs : Array α} {i : Nat} {v : α} (hi) :