diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index 48a57f4ff4..d064ad7d81 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -551,7 +551,7 @@ Note that the universe level is contrained to `Type` here,
 to avoid having to have the predicate live in `p : α → m (ULift Bool)`.
 -/
 @[inline]
-def findM? {α : Type} {m : Type → Type} [Monad m] (p : α → m Bool) (as : Array α) : m (Option α) := do
+def findM? {α : Type} [Monad m] (p : α → m Bool) (as : Array α) : m (Option α) := do
   for a in as do
     if (← p a) then
       return a
diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
index 27eaeeb2dd..1051c99585 100644
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -3525,7 +3525,7 @@ theorem getElem_modify {xs : Array α} {j i} (h : i < (xs.modify j f).size) :
   · rw [if_neg (mt (by rintro rfl; exact h) (by simp_all))]
 
 @[simp] theorem toList_modify (xs : Array α) (f : α → α) :
-    (xs.modify i f).toList = xs.toList.modify f i := by
+    (xs.modify i f).toList = xs.toList.modify i f := by
   apply List.ext_getElem
   · simp
   · simp [getElem_modify, List.getElem_modify]
@@ -4223,7 +4223,7 @@ theorem uset_toArray (l : List α) (i : USize) (a : α) (h : i.toNat < l.toArray
     l.toArray.uset i a h = (l.set i.toNat a).toArray := by simp
 
 @[simp] theorem modify_toArray (f : α → α) (l : List α) :
-    l.toArray.modify i f = (l.modify f i).toArray := by
+    l.toArray.modify i f = (l.modify i f).toArray := by
   apply ext'
   simp
 
diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index a3eea812a8..d06dfb7a12 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -1475,10 +1475,18 @@ Examples:
 ["circle", "square", "triangle"]
 ```
 -/
-@[simp] def modifyTailIdx (f : List α → List α) : (n : Nat) → (l : List α) → List α
+def modifyTailIdx (l : List α) (i : Nat) (f : List α → List α) : List α :=
+  go i l
+where
+  go : Nat → List α → List α
   | 0, l => f l
   | _+1, [] => []
-  | n+1, a :: l => a :: modifyTailIdx f n l
+  | i+1, a :: l => a :: go i l
+
+@[simp] theorem modifyTailIdx_zero {l : List α} : l.modifyTailIdx 0 f = f l := rfl
+@[simp] theorem modifyTailIdx_succ_nil {i : Nat} : ([] : List α).modifyTailIdx (i + 1) f = [] := rfl
+@[simp] theorem modifyTailIdx_succ_cons {i : Nat} {a : α} {l : List α} :
+    (a :: l).modifyTailIdx (i + 1) f = a :: l.modifyTailIdx i f := rfl
 
 /--
 Replace the head of the list with the result of applying `f` to it. Returns the empty list if the
@@ -1505,8 +1513,8 @@ Examples:
  * `[1, 2, 3].modify (· * 10) 2 = [1, 2, 30]`
  * `[1, 2, 3].modify (· * 10) 3 = [1, 2, 3]`
 -/
-def modify (f : α → α) : Nat → List α → List α :=
-  modifyTailIdx (modifyHead f)
+def modify (l : List α) (i : Nat) (f : α → α) : List α :=
+  l.modifyTailIdx i (modifyHead f)
 
 /-! ### insert -/
 
@@ -1536,8 +1544,8 @@ Examples:
  * `["tues", "thur", "sat"].insertIdx 3 "wed" = ["tues", "thur", "sat", "wed"]`
  * `["tues", "thur", "sat"].insertIdx 4 "wed" = ["tues", "thur", "sat"]`
 -/
-def insertIdx (i : Nat) (a : α) : (l : List α) → List α :=
-  modifyTailIdx (cons a) i
+def insertIdx (xs : List α) (i : Nat) (a : α) : List α :=
+  xs.modifyTailIdx i (cons a)
 
 /-! ### erase -/
 
diff --git a/src/Init/Data/List/Impl.lean b/src/Init/Data/List/Impl.lean
index bba8a026b1..104207df30 100644
--- a/src/Init/Data/List/Impl.lean
+++ b/src/Init/Data/List/Impl.lean
@@ -17,7 +17,8 @@ then at runtime you will get non-tail recursive versions of the following defini
 -/
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+-- TODO: restore after an update-stage0
+-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace List
 
@@ -300,20 +301,20 @@ Examples:
  * `[1, 2, 3].modifyTR (· * 10) 2 = [1, 2, 30]`
  * `[1, 2, 3].modifyTR (· * 10) 3 = [1, 2, 3]`
 -/
-def modifyTR (f : α → α) (n : Nat) (l : List α) : List α := go l n #[] where
-  /-- Auxiliary for `modifyTR`: `modifyTR.go f l n acc = acc.toList ++ modify f n l`. -/
+def modifyTR (l : List α) (i : Nat) (f : α → α) : List α := go l i #[] where
+  /-- Auxiliary for `modifyTR`: `modifyTR.go f l i acc = acc.toList ++ modify f i l`. -/
   go : List α → Nat → Array α → List α
   | [], _, acc => acc.toList
   | a :: l, 0, acc => acc.toListAppend (f a :: l)
-  | a :: l, n+1, acc => go l n (acc.push a)
+  | a :: l, i+1, acc => go l i (acc.push a)
 
-theorem modifyTR_go_eq : ∀ l i, modifyTR.go f l i acc = acc.toList ++ modify f i l
-  | [], n => by cases n <;> simp [modifyTR.go, modify]
+theorem modifyTR_go_eq : ∀ l i, modifyTR.go f l i acc = acc.toList ++ modify l i f
+  | [], i => by cases i <;> simp [modifyTR.go, modify]
   | a :: l, 0 => by simp [modifyTR.go, modify]
-  | a :: l, n+1 => by simp [modifyTR.go, modify, modifyTR_go_eq l]
+  | a :: l, i+1 => by simp [modifyTR.go, modify, modifyTR_go_eq l]
 
 @[csimp] theorem modify_eq_modifyTR : @modify = @modifyTR := by
-  funext α f n l; simp [modifyTR, modifyTR_go_eq]
+  funext α l i f; simp [modifyTR, modifyTR_go_eq]
 
 /-! ### insertIdx -/
 
@@ -332,19 +333,19 @@ Examples:
  * `["tues", "thur", "sat"].insertIdxTR 4 "wed" = ["tues", "thur", "sat"]`
 
 -/
-@[inline] def insertIdxTR (i : Nat) (a : α) (l : List α) : List α := go i l #[] where
+@[inline] def insertIdxTR (l : List α) (n : Nat) (a : α) : List α := go n l #[] where
   /-- Auxiliary for `insertIdxTR`: `insertIdxTR.go a n l acc = acc.toList ++ insertIdx n a l`. -/
   go : Nat → List α → Array α → List α
   | 0, l, acc => acc.toListAppend (a :: l)
   | _, [], acc => acc.toList
   | n+1, a :: l, acc => go n l (acc.push a)
 
-theorem insertIdxTR_go_eq : ∀ i l, insertIdxTR.go a i l acc = acc.toList ++ insertIdx i a l
+theorem insertIdxTR_go_eq : ∀ i l, insertIdxTR.go a i l acc = acc.toList ++ insertIdx l i a
   | 0, l | _+1, [] => by simp [insertIdxTR.go, insertIdx]
   | n+1, a :: l => by simp [insertIdxTR.go, insertIdx, insertIdxTR_go_eq n l]
 
 @[csimp] theorem insertIdx_eq_insertIdxTR : @insertIdx = @insertIdxTR := by
-  funext α f n l; simp [insertIdxTR, insertIdxTR_go_eq]
+  funext α l i a; simp [insertIdxTR, insertIdxTR_go_eq]
 
 /-! ### erase -/
 
diff --git a/src/Init/Data/List/Nat/InsertIdx.lean b/src/Init/Data/List/Nat/InsertIdx.lean
index 26c8aa8582..5ae2fe8404 100644
--- a/src/Init/Data/List/Nat/InsertIdx.lean
+++ b/src/Init/Data/List/Nat/InsertIdx.lean
@@ -13,7 +13,8 @@ Proves various lemmas about `List.insertIdx`.
 -/
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+-- TODO: restore after an update-stage0
+-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 open Function Nat
 
@@ -28,29 +29,29 @@ section InsertIdx
 variable {a : α}
 
 @[simp]
-theorem insertIdx_zero (s : List α) (x : α) : insertIdx 0 x s = x :: s :=
+theorem insertIdx_zero (xs : List α) (x : α) : xs.insertIdx 0 x = x :: xs :=
   rfl
 
 @[simp]
-theorem insertIdx_succ_nil (n : Nat) (a : α) : insertIdx (n + 1) a [] = [] :=
+theorem insertIdx_succ_nil (n : Nat) (a : α) : ([] : List α).insertIdx (n + 1) a = [] :=
   rfl
 
 @[simp]
-theorem insertIdx_succ_cons (s : List α) (hd x : α) (i : Nat) :
-    insertIdx (i + 1) x (hd :: s) = hd :: insertIdx i x s :=
+theorem insertIdx_succ_cons (xs : List α) (hd x : α) (i : Nat) :
+    (hd :: xs).insertIdx (i + 1) x = hd :: xs.insertIdx i x :=
   rfl
 
-theorem length_insertIdx : ∀ i as, (insertIdx i a as).length = if i ≤ as.length then as.length + 1 else as.length
+theorem length_insertIdx : ∀ i (as : List α), (as.insertIdx i a).length = if i ≤ as.length then as.length + 1 else as.length
   | 0, _ => by simp
   | n + 1, [] => by simp
   | n + 1, a :: as => by
     simp only [insertIdx_succ_cons, length_cons, length_insertIdx, Nat.add_le_add_iff_right]
     split <;> rfl
 
-theorem length_insertIdx_of_le_length (h : i ≤ length as) : length (insertIdx i a as) = length as + 1 := by
+theorem length_insertIdx_of_le_length (h : i ≤ length as) : (as.insertIdx i a).length = as.length + 1 := by
   simp [length_insertIdx, h]
 
-theorem length_insertIdx_of_length_lt (h : length as < i) : length (insertIdx i a as) = length as := by
+theorem length_insertIdx_of_length_lt (h : length as < i) : (as.insertIdx i a).length = as.length := by
   simp [length_insertIdx, h]
 
 @[simp]
@@ -60,7 +61,7 @@ theorem eraseIdx_insertIdx (i : Nat) (l : List α) : (l.insertIdx i a).eraseIdx
 
 theorem insertIdx_eraseIdx_of_ge :
     ∀ i m as,
-      i < length as → i ≤ m → insertIdx m a (as.eraseIdx i) = (as.insertIdx (m + 1) a).eraseIdx i
+      i < length as → i ≤ m → (as.eraseIdx i).insertIdx m a = (as.insertIdx (m + 1) a).eraseIdx i
   | 0, 0, [], has, _ => (Nat.lt_irrefl _ has).elim
   | 0, 0, _ :: as, _, _ => by simp [eraseIdx, insertIdx]
   | 0, _ + 1, _ :: _, _, _ => rfl
@@ -70,7 +71,7 @@ theorem insertIdx_eraseIdx_of_ge :
 
 theorem insertIdx_eraseIdx_of_le :
     ∀ i j as,
-      i < length as → j ≤ i → insertIdx j a (as.eraseIdx i) = (as.insertIdx j a).eraseIdx (i + 1)
+      i < length as → j ≤ i → (as.eraseIdx i).insertIdx j a = (as.insertIdx j a).eraseIdx (i + 1)
   | _, 0, _ :: _, _, _ => rfl
   | n + 1, m + 1, a :: as, has, hmn =>
     congrArg (cons a) <|
@@ -95,7 +96,7 @@ theorem mem_insertIdx {a b : α} :
       ← or_assoc, @or_comm (a = a'), or_assoc, mem_cons]
 
 theorem insertIdx_of_length_lt (l : List α) (x : α) (i : Nat) (h : l.length < i) :
-    insertIdx i x l = l := by
+    l.insertIdx i x = l := by
   induction l generalizing i with
   | nil =>
     cases i
@@ -108,24 +109,24 @@ theorem insertIdx_of_length_lt (l : List α) (x : α) (i : Nat) (h : l.length <
       simpa using ih _ h
 
 @[simp]
-theorem insertIdx_length_self (l : List α) (x : α) : insertIdx l.length x l = l ++ [x] := by
+theorem insertIdx_length_self (l : List α) (x : α) : l.insertIdx l.length x = l ++ [x] := by
   induction l with
   | nil => simp
   | cons x l ih => simpa using ih
 
 theorem length_le_length_insertIdx (l : List α) (x : α) (i : Nat) :
-    l.length ≤ (insertIdx i x l).length := by
+    l.length ≤ (l.insertIdx i x).length := by
   simp only [length_insertIdx]
   split <;> simp
 
 theorem length_insertIdx_le_succ (l : List α) (x : α) (i : Nat) :
-    (insertIdx i x l).length ≤ l.length + 1 := by
+    (l.insertIdx i x).length ≤ l.length + 1 := by
   simp only [length_insertIdx]
   split <;> simp
 
 theorem getElem_insertIdx_of_lt {l : List α} {x : α} {i j : Nat} (hn : j < i)
-    (hk : j < (insertIdx i x l).length) :
-    (insertIdx i x l)[j] = l[j]'(by simp [length_insertIdx] at hk; split at hk <;> omega) := by
+    (hk : j < (l.insertIdx i x).length) :
+    (l.insertIdx i x)[j] = l[j]'(by simp [length_insertIdx] at hk; split at hk <;> omega) := by
   induction i generalizing j l with
   | zero => simp at hn
   | succ n ih =>
@@ -138,8 +139,8 @@ theorem getElem_insertIdx_of_lt {l : List α} {x : α} {i j : Nat} (hn : j < i)
         simpa using ih hn _
 
 @[simp]
-theorem getElem_insertIdx_self {l : List α} {x : α} {i : Nat} (hi : i < (insertIdx i x l).length) :
-    (insertIdx i x l)[i] = x := by
+theorem getElem_insertIdx_self {l : List α} {x : α} {i : Nat} (hi : i < (l.insertIdx i x).length) :
+    (l.insertIdx i x)[i] = x := by
   induction l generalizing i with
   | nil =>
     simp [length_insertIdx] at hi
@@ -153,8 +154,8 @@ theorem getElem_insertIdx_self {l : List α} {x : α} {i : Nat} (hi : i < (inser
       simpa using ih hi
 
 theorem getElem_insertIdx_of_gt {l : List α} {x : α} {i j : Nat} (hn : i < j)
-    (hk : j < (insertIdx i x l).length) :
-    (insertIdx i x l)[j] = l[j - 1]'(by simp [length_insertIdx] at hk; split at hk <;> omega) := by
+    (hk : j < (l.insertIdx i x).length) :
+    (l.insertIdx i x)[j] = l[j - 1]'(by simp [length_insertIdx] at hk; split at hk <;> omega) := by
   induction l generalizing i j with
   | nil =>
     cases i with
@@ -182,8 +183,8 @@ theorem getElem_insertIdx_of_gt {l : List α} {x : α} {i j : Nat} (hn : i < j)
 @[deprecated getElem_insertIdx_of_gt (since := "2025-02-04")]
 abbrev getElem_insertIdx_of_ge := @getElem_insertIdx_of_gt
 
-theorem getElem_insertIdx {l : List α} {x : α} {i j : Nat} (h : j < (insertIdx i x l).length) :
-    (insertIdx i x l)[j] =
+theorem getElem_insertIdx {l : List α} {x : α} {i j : Nat} (h : j < (l.insertIdx i x).length) :
+    (l.insertIdx i x)[j] =
       if h₁ : j < i then
         l[j]'(by simp [length_insertIdx] at h; split at h <;> omega)
       else
@@ -199,7 +200,7 @@ theorem getElem_insertIdx {l : List α} {x : α} {i j : Nat} (h : j < (insertIdx
     · rw [getElem_insertIdx_of_gt (by omega)]
 
 theorem getElem?_insertIdx {l : List α} {x : α} {i j : Nat} :
-    (insertIdx i x l)[j]? =
+    (l.insertIdx i x)[j]? =
       if j < i then
         l[j]?
       else
@@ -230,16 +231,16 @@ theorem getElem?_insertIdx {l : List α} {x : α} {i j : Nat} :
         split at h <;> omega
 
 theorem getElem?_insertIdx_of_lt {l : List α} {x : α} {i j : Nat} (h : j < i) :
-    (insertIdx i x l)[j]? = l[j]? := by
+    (l.insertIdx i x)[j]? = l[j]? := by
   rw [getElem?_insertIdx, if_pos h]
 
 theorem getElem?_insertIdx_self {l : List α} {x : α} {i : Nat} :
-    (insertIdx i x l)[i]? = if i ≤ l.length then some x else none := by
+    (l.insertIdx i x)[i]? = if i ≤ l.length then some x else none := by
   rw [getElem?_insertIdx, if_neg (by omega)]
   simp
 
 theorem getElem?_insertIdx_of_gt {l : List α} {x : α} {i j : Nat} (h : i < j) :
-    (insertIdx i x l)[j]? = l[j - 1]? := by
+    (l.insertIdx i x)[j]? = l[j - 1]? := by
   rw [getElem?_insertIdx, if_neg (by omega), if_neg (by omega)]
 
 @[deprecated getElem?_insertIdx_of_gt (since := "2025-02-04")]
diff --git a/src/Init/Data/List/Nat/Modify.lean b/src/Init/Data/List/Nat/Modify.lean
index 8fe58713a0..c822cdcff0 100644
--- a/src/Init/Data/List/Nat/Modify.lean
+++ b/src/Init/Data/List/Nat/Modify.lean
@@ -87,75 +87,75 @@ theorem eraseIdx_modifyHead_zero {f : α → α} {l : List α} :
 
 /-! ### modifyTailIdx -/
 
-@[simp] theorem modifyTailIdx_id : ∀ n (l : List α), l.modifyTailIdx id n = l
+@[simp] theorem modifyTailIdx_id : ∀ i (l : List α), l.modifyTailIdx i id = l
   | 0, _ => rfl
   | _+1, [] => rfl
   | n+1, a :: l => congrArg (cons a) (modifyTailIdx_id n l)
 
-theorem eraseIdx_eq_modifyTailIdx : ∀ i (l : List α), eraseIdx l i = modifyTailIdx tail i l
+theorem eraseIdx_eq_modifyTailIdx : ∀ i (l : List α), eraseIdx l i = l.modifyTailIdx i tail
   | 0, l => by cases l <;> rfl
   | _+1, [] => rfl
   | _+1, _ :: _ => congrArg (cons _) (eraseIdx_eq_modifyTailIdx _ _)
 
-@[simp] theorem length_modifyTailIdx (f : List α → List α) (H : ∀ l, length (f l) = length l) :
-    ∀ n l, length (modifyTailIdx f n l) = length l
-  | 0, _ => H _
-  | _+1, [] => rfl
-  | _+1, _ :: _ => congrArg (·+1) (length_modifyTailIdx _ H _ _)
+@[simp] theorem length_modifyTailIdx (f : List α → List α) (H : ∀ l, (f l).length = l.length) :
+    ∀ (l : List α) i, (l.modifyTailIdx i f).length = l.length
+  | _, 0 => H _
+  | [], _+1 => rfl
+  | _ :: _, _+1 => congrArg (·+1) (length_modifyTailIdx _ H _ _)
 
-theorem modifyTailIdx_add (f : List α → List α) (n) (l₁ l₂ : List α) :
-    modifyTailIdx f (l₁.length + n) (l₁ ++ l₂) = l₁ ++ modifyTailIdx f n l₂ := by
+theorem modifyTailIdx_add (f : List α → List α) (i) (l₁ l₂ : List α) :
+    (l₁ ++ l₂).modifyTailIdx (l₁.length + i) f = l₁ ++ l₂.modifyTailIdx i f := by
   induction l₁ <;> simp [*, Nat.succ_add]
 
 theorem modifyTailIdx_eq_take_drop (f : List α → List α) (H : f [] = []) :
-    ∀ i l, modifyTailIdx f i l = take i l ++ f (drop i l)
-  | 0, _ => rfl
-  | _ + 1, [] => H.symm
-  | n + 1, b :: l => congrArg (cons b) (modifyTailIdx_eq_take_drop f H n l)
+    ∀ (l : List α) i, l.modifyTailIdx i f = l.take i ++ f (l.drop i)
+  | _, 0 => rfl
+  | [], _ + 1 => H.symm
+  | b :: l, i + 1 => congrArg (cons b) (modifyTailIdx_eq_take_drop f H l i)
 
-theorem exists_of_modifyTailIdx (f : List α → List α) {n} {l : List α} (h : n ≤ l.length) :
-    ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁.length = n ∧ modifyTailIdx f n l = l₁ ++ f l₂ :=
-  have ⟨_, _, eq, hl⟩ : ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁.length = n :=
-    ⟨_, _, (take_append_drop n l).symm, length_take_of_le h⟩
-  ⟨_, _, eq, hl, hl ▸ eq ▸ modifyTailIdx_add (n := 0) ..⟩
+theorem exists_of_modifyTailIdx (f : List α → List α) {i} {l : List α} (h : i ≤ l.length) :
+    ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁.length = i ∧ l.modifyTailIdx i f = l₁ ++ f l₂ := by
+  obtain ⟨l₁, l₂, rfl, rfl⟩ : ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁.length = i :=
+    ⟨_, _, (take_append_drop i l).symm, length_take_of_le h⟩
+  exact ⟨l₁, l₂, rfl, rfl, modifyTailIdx_add f 0 l₁ l₂⟩
 
-theorem modifyTailIdx_modifyTailIdx {f g : List α → List α} (m : Nat) :
-    ∀ (n) (l : List α),
-      (l.modifyTailIdx f n).modifyTailIdx g (m + n) =
-        l.modifyTailIdx (fun l => (f l).modifyTailIdx g m) n
+theorem modifyTailIdx_modifyTailIdx {f g : List α → List α} (i : Nat) :
+    ∀ (j) (l : List α),
+      (l.modifyTailIdx j f).modifyTailIdx (i + j) g =
+        l.modifyTailIdx j (fun l => (f l).modifyTailIdx i g)
   | 0, _ => rfl
   | _ + 1, [] => rfl
-  | n + 1, a :: l => congrArg (List.cons a) (modifyTailIdx_modifyTailIdx m n l)
+  | n + 1, a :: l => congrArg (List.cons a) (modifyTailIdx_modifyTailIdx i n l)
 
-theorem modifyTailIdx_modifyTailIdx_le {f g : List α → List α} (m n : Nat) (l : List α)
-    (h : n ≤ m) :
-    (l.modifyTailIdx f n).modifyTailIdx g m =
-      l.modifyTailIdx (fun l => (f l).modifyTailIdx g (m - n)) n := by
+theorem modifyTailIdx_modifyTailIdx_le {f g : List α → List α} (i j : Nat) (l : List α)
+    (h : j ≤ i) :
+    (l.modifyTailIdx j f).modifyTailIdx i g =
+      l.modifyTailIdx j (fun l => (f l).modifyTailIdx (i - j) g) := by
   rcases Nat.exists_eq_add_of_le h with ⟨m, rfl⟩
   rw [Nat.add_comm, modifyTailIdx_modifyTailIdx, Nat.add_sub_cancel]
 
-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
+theorem modifyTailIdx_modifyTailIdx_self {f g : List α → List α} (i : Nat) (l : List α) :
+    (l.modifyTailIdx i f).modifyTailIdx i g = l.modifyTailIdx i (g ∘ f) := by
+  rw [modifyTailIdx_modifyTailIdx_le i i l (Nat.le_refl i), Nat.sub_self]; rfl
 
 /-! ### modify -/
 
-@[simp] theorem modify_nil (f : α → α) (i) : [].modify f i = [] := by cases i <;> rfl
+@[simp] theorem modify_nil (f : α → α) (i) : [].modify i f = [] := by cases i <;> rfl
 
 @[simp] theorem modify_zero_cons (f : α → α) (a : α) (l : List α) :
-    (a :: l).modify f 0 = f a :: l := rfl
+    (a :: l).modify 0 f = f a :: l := rfl
 
 @[simp] theorem modify_succ_cons (f : α → α) (a : α) (l : List α) (i) :
-    (a :: l).modify f (i + 1) = a :: l.modify f i := by rfl
+    (a :: l).modify (i + 1) f = a :: l.modify i f := by rfl
 
 theorem modifyHead_eq_modify_zero (f : α → α) (l : List α) :
-    l.modifyHead f = l.modify f 0 := by cases l <;> simp
+    l.modifyHead f = l.modify 0 f := by cases l <;> simp
 
 @[simp] theorem modify_eq_nil_iff {f : α → α} {i} {l : List α} :
-    l.modify f i = [] ↔ l = [] := by cases l <;> cases i <;> simp
+    l.modify i f = [] ↔ l = [] := by cases l <;> cases i <;> simp
 
 theorem getElem?_modify (f : α → α) :
-    ∀ i (l : List α) j, (modify f i l)[j]? = (fun a => if i = j then f a else a) <$> l[j]?
+    ∀ i (l : List α) j, (l.modify i f)[j]? = (fun a => if i = j then f a else a) <$> l[j]?
   | n, l, 0 => by cases l <;> cases n <;> simp
   | n, [], _+1 => by cases n <;> rfl
   | 0, _ :: l, j+1 => by cases h : l[j]? <;> simp [h, modify, j.succ_ne_zero.symm]
@@ -165,32 +165,32 @@ theorem getElem?_modify (f : α → α) :
     cases h' : l[j]? <;> by_cases h : i = j <;>
       simp [h, if_pos, if_neg, Option.map, mt Nat.succ.inj, not_false_iff, h']
 
-@[simp] theorem length_modify (f : α → α) : ∀ i l, length (modify f i l) = length l :=
+@[simp] theorem length_modify (f : α → α) : ∀ (l : List α) i, (l.modify i f).length = l.length :=
   length_modifyTailIdx _ fun l => by cases l <;> rfl
 
 @[simp] theorem getElem?_modify_eq (f : α → α) (i) (l : List α) :
-    (modify f i l)[i]? = f <$> l[i]? := by
+    (l.modify i f)[i]? = f <$> l[i]? := by
   simp only [getElem?_modify, if_pos]
 
 @[simp] theorem getElem?_modify_ne (f : α → α) {i j} (l : List α) (h : i ≠ j) :
-    (modify f i l)[j]? = l[j]? := by
+    (l.modify i f)[j]? = l[j]? := by
   simp only [getElem?_modify, if_neg h, id_map']
 
-theorem getElem_modify (f : α → α) (i) (l : List α) (j) (h : j < (modify f i l).length) :
-    (modify f i l)[j] =
+theorem getElem_modify (f : α → α) (i) (l : List α) (j) (h : j < (l.modify i f).length) :
+    (l.modify i f)[j] =
       if i = j then f (l[j]'(by simp at h; omega)) else l[j]'(by simp at h; omega) := by
   rw [getElem_eq_iff, getElem?_modify]
   simp at h
   simp [h]
 
 @[simp] theorem getElem_modify_eq (f : α → α) (i) (l : List α) (h) :
-    (modify f i l)[i] = f (l[i]'(by simpa using h)) := by simp [getElem_modify]
+    (l.modify i f)[i] = f (l[i]'(by simpa using h)) := by simp [getElem_modify]
 
 @[simp] theorem getElem_modify_ne (f : α → α) {i j} (l : List α) (h : i ≠ j) (h') :
-    (modify f i l)[j] = l[j]'(by simpa using h') := by simp [getElem_modify, h]
+    (l.modify i f)[j] = l[j]'(by simpa using h') := by simp [getElem_modify, h]
 
 theorem modify_eq_self {f : α → α} {i} {l : List α} (h : l.length ≤ i) :
-    l.modify f i = l := by
+    l.modify i f = l := by
   apply ext_getElem
   · simp
   · intro m h₁ h₂
@@ -199,7 +199,7 @@ theorem modify_eq_self {f : α → α} {i} {l : List α} (h : l.length ≤ i) :
     omega
 
 theorem modify_modify_eq (f g : α → α) (i) (l : List α) :
-    (modify f i l).modify g i = modify (g ∘ f) i l := by
+    (l.modify i f).modify i g = l.modify i (g ∘ f) := by
   apply ext_getElem
   · simp
   · intro m h₁ h₂
@@ -207,7 +207,7 @@ theorem modify_modify_eq (f g : α → α) (i) (l : List α) :
     split <;> simp
 
 theorem modify_modify_ne (f g : α → α) {i j} (l : List α) (h : i ≠ j) :
-    (modify f i l).modify g j = (l.modify g j).modify f i := by
+    (l.modify i f).modify j g = (l.modify j g).modify i f := by
   apply ext_getElem
   · simp
   · intro m' h₁ h₂
@@ -215,7 +215,7 @@ theorem modify_modify_ne (f g : α → α) {i j} (l : List α) (h : i ≠ j) :
     split <;> split <;> first | rfl | omega
 
 theorem modify_eq_set [Inhabited α] (f : α → α) (i) (l : List α) :
-    modify f i l = l.set i (f (l[i]?.getD default)) := by
+    l.modify i f = l.set i (f (l[i]?.getD default)) := by
   apply ext_getElem
   · simp
   · intro m h₁ h₂
@@ -227,24 +227,24 @@ theorem modify_eq_set [Inhabited α] (f : α → α) (i) (l : List α) :
     · rfl
 
 theorem modify_eq_take_drop (f : α → α) :
-    ∀ i l, modify f i l = take i l ++ modifyHead f (drop i l) :=
+    ∀ (l : List α) i, l.modify i f = l.take i ++ modifyHead f (l.drop i) :=
   modifyTailIdx_eq_take_drop _ rfl
 
 theorem modify_eq_take_cons_drop {f : α → α} {i} {l : List α} (h : i < l.length) :
-    modify f i l = take i l ++ f l[i] :: drop (i + 1) l := by
+    l.modify i f = l.take i ++ f l[i] :: l.drop (i + 1) := by
   rw [modify_eq_take_drop, drop_eq_getElem_cons h]; rfl
 
 theorem exists_of_modify (f : α → α) {i} {l : List α} (h : i < l.length) :
-    ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ l₁.length = i ∧ modify f i l = l₁ ++ f a :: l₂ :=
+    ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ l₁.length = i ∧ l.modify i f = l₁ ++ f a :: l₂ :=
   match exists_of_modifyTailIdx _ (Nat.le_of_lt h) with
   | ⟨_, _::_, eq, hl, H⟩ => ⟨_, _, _, eq, hl, H⟩
   | ⟨_, [], eq, hl, _⟩ => nomatch Nat.ne_of_gt h (eq ▸ append_nil _ ▸ hl)
 
-@[simp] theorem modify_id (i) (l : List α) : l.modify id i = l := by
+@[simp] theorem modify_id (i) (l : List α) : l.modify i id = l := by
   simp [modify]
 
 theorem take_modify (f : α → α) (i j) (l : List α) :
-    (modify f i l).take j = (take j l).modify f i := by
+    (l.modify i f).take j = (l.take j).modify i f := by
   induction j generalizing l i with
   | zero => simp
   | succ n ih =>
@@ -256,7 +256,7 @@ theorem take_modify (f : α → α) (i j) (l : List α) :
       | succ i => simp [ih]
 
 theorem drop_modify_of_lt (f : α → α) (i j) (l : List α) (h : i < j) :
-    (modify f i l).drop j = l.drop j := by
+    (l.modify i f).drop j = l.drop j := by
   apply ext_getElem
   · simp
   · intro m' h₁ h₂
@@ -265,7 +265,7 @@ theorem drop_modify_of_lt (f : α → α) (i j) (l : List α) (h : i < j) :
     omega
 
 theorem drop_modify_of_ge (f : α → α) (i j) (l : List α) (h : i ≥ j) :
-    (modify f i l).drop j = modify f (i - j) (drop j l) := by
+    (l.modify i f).drop j = (l.drop j).modify (i - j) f  := by
   apply ext_getElem
   · simp
   · intro m' h₁ h₂
@@ -273,7 +273,7 @@ theorem drop_modify_of_ge (f : α → α) (i j) (l : List α) (h : i ≥ j) :
     split <;> split <;> first | rfl | omega
 
 theorem eraseIdx_modify_of_eq (f : α → α) (i) (l : List α) :
-    (modify f i l).eraseIdx i = l.eraseIdx i := by
+    (l.modify i f).eraseIdx i = l.eraseIdx i := by
   apply ext_getElem
   · simp [length_eraseIdx]
   · intro m h₁ h₂
@@ -281,7 +281,7 @@ theorem eraseIdx_modify_of_eq (f : α → α) (i) (l : List α) :
     split <;> split <;> first | rfl | omega
 
 theorem eraseIdx_modify_of_lt (f : α → α) (i j) (l : List α) (h : j < i) :
-    (modify f i l).eraseIdx j = (l.eraseIdx j).modify f (i - 1) := by
+    (l.modify i f).eraseIdx j = (l.eraseIdx j).modify (i - 1) f := by
   apply ext_getElem
   · simp [length_eraseIdx]
   · intro k h₁ h₂
@@ -291,7 +291,7 @@ theorem eraseIdx_modify_of_lt (f : α → α) (i j) (l : List α) (h : j < i) :
     all_goals (first | rfl | omega)
 
 theorem eraseIdx_modify_of_gt (f : α → α) (i j) (l : List α) (h : j > i) :
-    (modify f i l).eraseIdx j = (l.eraseIdx j).modify f i := by
+    (l.modify i f).eraseIdx j = (l.eraseIdx j).modify i f := by
   apply ext_getElem
   · simp [length_eraseIdx]
   · intro k h₁ h₂
@@ -301,7 +301,7 @@ theorem eraseIdx_modify_of_gt (f : α → α) (i j) (l : List α) (h : j > i) :
     all_goals (first | rfl | omega)
 
 theorem modify_eraseIdx_of_lt (f : α → α) (i j) (l : List α) (h : j < i) :
-    (l.eraseIdx i).modify f j = (l.modify f j).eraseIdx i := by
+    (l.eraseIdx i).modify j f = (l.modify j f).eraseIdx i := by
   apply ext_getElem
   · simp [length_eraseIdx]
   · intro k h₁ h₂
@@ -311,7 +311,7 @@ theorem modify_eraseIdx_of_lt (f : α → α) (i j) (l : List α) (h : j < i) :
     all_goals (first | rfl | omega)
 
 theorem modify_eraseIdx_of_ge (f : α → α) (i j) (l : List α) (h : j ≥ i) :
-    (l.eraseIdx i).modify f j = (l.modify f (j + 1)).eraseIdx i := by
+    (l.eraseIdx i).modify j f = (l.modify (j + 1) f).eraseIdx i := by
   apply ext_getElem
   · simp [length_eraseIdx]
   · intro k h₁ h₂
diff --git a/src/Init/Data/List/Perm.lean b/src/Init/Data/List/Perm.lean
index fcfa605dd6..ae2a3cb56e 100644
--- a/src/Init/Data/List/Perm.lean
+++ b/src/Init/Data/List/Perm.lean
@@ -19,7 +19,8 @@ The notation `~` is used for permutation equivalence.
 -/
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+-- TODO: restore after an update-stage0
+-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 open Nat
 
@@ -522,7 +523,7 @@ theorem Perm.eraseP (f : α → Bool) {l₁ l₂ : List α}
     exact fun h h₁ h₂ => h h₂ h₁
 
 theorem perm_insertIdx {α} (x : α) (l : List α) {i} (h : i ≤ l.length) :
-    insertIdx i x l ~ x :: l := by
+    l.insertIdx i x ~ x :: l := by
   induction l generalizing i with
   | nil =>
     cases i with
diff --git a/src/Init/Data/List/ToArray.lean b/src/Init/Data/List/ToArray.lean
index ed19b01dbb..46a98a858a 100644
--- a/src/Init/Data/List/ToArray.lean
+++ b/src/Init/Data/List/ToArray.lean
@@ -16,7 +16,8 @@ We prefer to pull `List.toArray` outwards past `Array` operations.
 -/
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+-- TODO: restore after an update-stage0
+-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace Array
 
diff --git a/src/Lean/Linter/List.lean b/src/Lean/Linter/List.lean
index 1ca61c9f3e..747978489f 100644
--- a/src/Lean/Linter/List.lean
+++ b/src/Lean/Linter/List.lean
@@ -52,7 +52,7 @@ def numericalIndices (t : InfoTree) : List (Syntax × Name) :=
       | List.take _ i _ => [i]
       | List.drop _ i _ => [i]
       | List.set _ _ i _ => [i]
-      | List.insertIdx _ i _ _ => [i]
+      | List.insertIdx _ _ i _ => [i]
       | List.eraseIdx _ _ i => [i]
       | List.modify _ _ i _ => [i]
       | List.zipIdx _ _ i => [i]