feat: use omega in the get_elem tactic

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]`