cleanup

cleanup

Author: kim-em

src/Init/Data/Range/Basic.lean

@@ -86,6 +86,3 @@ theorem Membership.get_elem_helper {i n : Nat} {r : Std.Range} (h₁ : i ∈ r)
 
 macro_rules
   | `(tactic| get_elem_tactic_extensible) => `(tactic| apply Membership.get_elem_helper; assumption; rfl)
-
-macro_rules
-  | `(tactic| get_elem_tactic_trivial) => `(tactic| apply Membership.get_elem_helper; assumption; rfl)

src/Init/GetElem.lean

@@ -283,9 +283,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

@@ -1933,9 +1933,7 @@ 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)
+macro_rules | `(tactic| get_elem_tactic_extensible) => `(tactic| trivial)
 
 /--
 `get_elem_tactic` is the tactic automatically called by the notation `arr[i]`

src/Lean/Elab/Tactic.lean

@@ -51,6 +51,3 @@ import Lean.Elab.Tactic.TreeTacAttr
 import Lean.Elab.Tactic.ExposeNames
 import Lean.Elab.Tactic.SimpArith
 import Lean.Elab.Tactic.Lets
-
-elab "get_elem_tactic_trivial" : tactic => do
-  throwError "`get_elem_tactic_trivial` has been renamed to `get_elem_tactic_extensible`"