diff --git a/src/Init/Data/Range/Basic.lean b/src/Init/Data/Range/Basic.lean
index 8d14e06976..de84cc57e7 100644
--- a/src/Init/Data/Range/Basic.lean
+++ b/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)
diff --git a/src/Init/GetElem.lean b/src/Init/GetElem.lean
index 708c55f3c6..29419aaeb7 100644
--- a/src/Init/GetElem.lean
+++ b/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
diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index 654ebeec6d..eace359b94 100644
--- a/src/Init/Tactics.lean
+++ b/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]`
diff --git a/src/Lean/Elab/Tactic.lean b/src/Lean/Elab/Tactic.lean
index 497280dcd2..9036f1cb0c 100644
--- a/src/Lean/Elab/Tactic.lean
+++ b/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`"
diff --git a/tests/lean/run/grind_indexmap.lean b/tests/lean/run/grind_indexmap.lean
index 66fb944e24..35f76738b7 100644
--- a/tests/lean/run/grind_indexmap.lean
+++ b/tests/lean/run/grind_indexmap.lean
@@ -6,7 +6,7 @@ import Std.Data.HashMap
 
 set_option grind.warning false
 
-macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| grind)
+macro_rules | `(tactic| get_elem_tactic_extensible) => `(tactic| grind)
 
 open Std