feat: use omega in the get_elem tactic (#3515)

with this, hopefully more obvious array accesses will be handled
automatically.

Just like #3503, this PR does not investiate which of the exitsting
tactics in `get_elem_tactic_trivial` are subsumed now and could be
dropped without (too much) breakage.

src/Init/Tactics.lean

@@ -1425,13 +1425,14 @@ macro_rules | `(‹$type›) => `((by assumption : $type))
 by the notation `arr[i]` to prove any side conditions that arise when
 constructing the term (e.g. the index is in bounds of the array).
 The default behavior is to just try `trivial` (which handles the case
-where `i < arr.size` is in the context) and `simp_arith`
+where `i < arr.size` is in the context) and `simp_arith` and `omega`
 (for doing linear arithmetic in the index).
 -/
 syntax "get_elem_tactic_trivial" : tactic
 
 macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| trivial)
 macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| simp (config := { arith := true }); done)
+macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| omega)
 
 /--
 `get_elem_tactic` is the tactic automatically called by the notation `arr[i]`

tests/lean/getElem.lean

@@ -42,3 +42,10 @@ def withTwoRanges (xs : Array Nat) : Option Nat := Id.run do
       if xs[i] == xs[j] then
         return i
   return none
+
+def palindromeNeedsOmega (xs : Array Nat) : Bool := Id.run do
+  for h : i in [:xs.size/2] do
+    have : i < xs.size/2 := h.2 -- omega does not understand range yet
+    if xs[xs.size - 1 - i] ≠ xs[i] then
+      return false
+  return true