chore: alignment of a List/Array/Vector.reverse lemma

src/Init/Data/Array/Lemmas.lean

@@ -2435,6 +2435,12 @@ theorem getElem?_swap (xs : Array α) (i j : Nat) (hi hj) (k : Nat) : (xs.swap i
   cases xs
   simp
 
+theorem getElem_eq_getElem_reverse {xs : Array α} {i} (h : i < xs.size) :
+    xs[i] = xs.reverse[xs.size - 1 - i]'(by simpa using Nat.sub_one_sub_lt_of_lt h) := by
+  rw [getElem_reverse]
+  congr
+  omega
+
 @[simp] theorem reverse_eq_empty_iff {xs : Array α} : xs.reverse = #[] ↔ xs = #[] := by
   cases xs
   simp

src/Init/Data/Vector/Lemmas.lean

@@ -2068,6 +2068,12 @@ theorem flatMap_mkArray {β} (f : α → Vector β m) : (mkVector n a).flatMap f
   rcases xs with ⟨xs, rfl⟩
   simp
 
+theorem getElem_eq_getElem_reverse {xs : Vector α n} {i} (h : i < n) :
+    xs[i] = xs.reverse[n - 1 - i] := by
+  rw [getElem_reverse]
+  congr
+  omega
+
 /-- Variant of `getElem?_reverse` with a hypothesis giving the linear relation between the indices. -/
 theorem getElem?_reverse' {xs : Vector α n} (i j) (h : i + j + 1 = n) : xs.reverse[i]? = xs[j]? := by
   rcases xs with ⟨xs, rfl⟩