cleanup

Author: kim-em

src/Init/GetElem.lean

@@ -285,9 +285,6 @@ instance [GetElem? cont Nat elem dom] [h : LawfulGetElem cont Nat elem dom] :
 macro_rules
   | `(tactic| get_elem_tactic_extensible) => `(tactic| (with_reducible apply Fin.val_lt_of_le); get_elem_tactic_extensible; done)
 
-macro_rules
-  | `(tactic| get_elem_tactic_trivial) => `(tactic| (with_reducible apply Fin.val_lt_of_le); get_elem_tactic_trivial; done)
-
 end Fin
 
 namespace List

src/Init/Tactics.lean

@@ -1897,9 +1897,6 @@ syntax "get_elem_tactic_trivial" : tactic
 macro_rules | `(tactic| get_elem_tactic_extensible) => `(tactic| omega)
 macro_rules | `(tactic| get_elem_tactic_extensible) => `(tactic| simp +arith; done)
 
-macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| omega)
-macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| simp +arith; done)
-
 /--
 `get_elem_tactic` is the tactic automatically called by the notation `arr[i]`
 to prove any side conditions that arise when constructing the term