diff --git a/src/Init/Data/List/Nat/InsertIdx.lean b/src/Init/Data/List/Nat/InsertIdx.lean
index 3fcda63c25..ab86095a05 100644
--- a/src/Init/Data/List/Nat/InsertIdx.lean
+++ b/src/Init/Data/List/Nat/InsertIdx.lean
@@ -53,7 +53,7 @@ theorem length_insertIdx_of_length_lt (h : length as < n) : length (insertIdx n
   simp [length_insertIdx, h]
 
 theorem eraseIdx_insertIdx (n : Nat) (l : List α) : (l.insertIdx n a).eraseIdx n = l := by
-  rw [eraseIdx_eq_modifyTailIdx, insertIdx, modifyTailIdx_modifyTailIdx_eq]
+  rw [eraseIdx_eq_modifyTailIdx, insertIdx, modifyTailIdx_modifyTailIdx_self]
   exact modifyTailIdx_id _ _
 
 theorem insertIdx_eraseIdx_of_ge :
diff --git a/src/Init/Data/List/Nat/Modify.lean b/src/Init/Data/List/Nat/Modify.lean
index 9f88f5ed36..60dc4e3fa3 100644
--- a/src/Init/Data/List/Nat/Modify.lean
+++ b/src/Init/Data/List/Nat/Modify.lean
@@ -125,7 +125,7 @@ theorem modifyTailIdx_modifyTailIdx_le {f g : List α → List α} (m n : Nat) (
   rcases Nat.exists_eq_add_of_le h with ⟨m, rfl⟩
   rw [Nat.add_comm, modifyTailIdx_modifyTailIdx, Nat.add_sub_cancel]
 
-theorem modifyTailIdx_modifyTailIdx_eq {f g : List α → List α} (n : Nat) (l : List α) :
+theorem modifyTailIdx_modifyTailIdx_self {f g : List α → List α} (n : Nat) (l : List α) :
     (l.modifyTailIdx f n).modifyTailIdx g n = l.modifyTailIdx (g ∘ f) n := by
   rw [modifyTailIdx_modifyTailIdx_le n n l (Nat.le_refl n), Nat.sub_self]; rfl