fix test

src/Init/Data/Array/Basic.lean

@@ -613,8 +613,15 @@ def findIdx? {α : Type u} (p : α → Bool) (as : Array α) : Option Nat :=
     decreasing_by simp_wf; decreasing_trivial_pre_omega
   loop 0
 
-def getIdx? [BEq α] (a : Array α) (v : α) : Option Nat :=
-  a.findIdx? fun a => a == v
+@[inline]
+def findFinIdx? {α : Type u} (p : α → Bool) (as : Array α) : Option (Fin as.size) :=
+  let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
+  loop (j : Nat) :=
+    if h : j < as.size then
+      if p as[j] then some ⟨j, h⟩ else loop (j + 1)
+    else none
+    decreasing_by simp_wf; decreasing_trivial_pre_omega
+  loop 0
 
 @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 def indexOfAux [BEq α] (a : Array α) (v : α) (i : Nat) : Option (Fin a.size) :=
@@ -627,6 +634,10 @@ decreasing_by simp_wf; decreasing_trivial_pre_omega
 def indexOf? [BEq α] (a : Array α) (v : α) : Option (Fin a.size) :=
   indexOfAux a v 0
 
+@[deprecated indexOf? (since := "2024-11-20")]
+def getIdx? [BEq α] (a : Array α) (v : α) : Option Nat :=
+  a.findIdx? fun a => a == v
+
 @[inline]
 def any (as : Array α) (p : α → Bool) (start := 0) (stop := as.size) : Bool :=
   Id.run <| as.anyM p start stop
@@ -766,48 +777,62 @@ def takeWhile (p : α → Bool) (as : Array α) : Array α :=
     decreasing_by simp_wf; decreasing_trivial_pre_omega
   go 0 #[]
 
-/-- Remove the element at a given index from an array without bounds checks, using a `Fin` index.
+/--
+Remove the element at a given index from an array without a runtime bounds checks,
+using a `Nat` index and a tactic-provided bound.
 
-  This function takes worst case O(n) time because
-  it has to backshift all elements at positions greater than `i`.-/
+This function takes worst case O(n) time because
+it has to backshift all elements at positions greater than `i`.-/
 @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
-def feraseIdx (a : Array α) (i : Fin a.size) : Array α :=
-  if h : i.val + 1 < a.size then
-    let a' := a.swap ⟨i.val + 1, h⟩ i
-    let i' : Fin a'.size := ⟨i.val + 1, by simp [a', h]⟩
-    a'.feraseIdx i'
+def eraseIdx (a : Array α) (i : Nat) (h : i < a.size := by get_elem_tactic) : Array α :=
+  if h' : i + 1 < a.size then
+    let a' := a.swap ⟨i + 1, h'⟩ ⟨i, h⟩
+    a'.eraseIdx (i + 1) (by simp [a', h'])
   else
     a.pop
-termination_by a.size - i.val
-decreasing_by simp_wf; exact Nat.sub_succ_lt_self _ _ i.isLt
+termination_by a.size - i
+decreasing_by simp_wf; exact Nat.sub_succ_lt_self _ _ h
 
 -- This is required in `Lean.Data.PersistentHashMap`.
-@[simp] theorem size_feraseIdx (a : Array α) (i : Fin a.size) : (a.feraseIdx i).size = a.size - 1 := by
-  induction a, i using Array.feraseIdx.induct with
-  | @case1 a i h a' _ ih =>
-    unfold feraseIdx
-    simp [h, a', ih]
-  | case2 a i h =>
-    unfold feraseIdx
-    simp [h]
+@[simp] theorem size_eraseIdx (a : Array α) (i : Nat) (h) : (a.eraseIdx i h).size = a.size - 1 := by
+  induction a, i, h using Array.eraseIdx.induct with
+  | @case1 a i h h' a' ih =>
+    unfold eraseIdx
+    simp [h', a', ih]
+  | case2 a i h h' =>
+    unfold eraseIdx
+    simp [h']
 
 /-- Remove the element at a given index from an array, or do nothing if the index is out of bounds.
 
   This function takes worst case O(n) time because
   it has to backshift all elements at positions greater than `i`.-/
-def eraseIdx (a : Array α) (i : Nat) : Array α :=
-  if h : i < a.size then a.feraseIdx ⟨i, h⟩ else a
+def eraseIdxIfInBounds (a : Array α) (i : Nat) : Array α :=
+  if h : i < a.size then a.eraseIdx i h else a
+
+/-- Remove the element at a given index from an array, or panic if the index is out of bounds.
+
+This function takes worst case O(n) time because
+it has to backshift all elements at positions greater than `i`. -/
+def eraseIdx! (a : Array α) (i : Nat) : Array α :=
+  if h : i < a.size then a.eraseIdx i h else panic! "invalid index"
 
 def erase [BEq α] (as : Array α) (a : α) : Array α :=
   match as.indexOf? a with
   | none   => as
-  | some i => as.feraseIdx i
+  | some i => as.eraseIdx i
+
+/-- Erase the first element that satisfies the predicate `p`. -/
+def eraseP (as : Array α) (p : α → Bool) : Array α :=
+  match as.findIdx? p with
+  | none   => as
+  | some i => as.eraseIdxIfInBounds i
 
 /-- Insert element `a` at position `i`. -/
-@[inline] def insertAt (as : Array α) (i : Fin (as.size + 1)) (a : α) : Array α :=
+@[inline] def insertIdx (as : Array α) (i : Nat) (a : α) (_ : i ≤ as.size := by get_elem_tactic) : Array α :=
   let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
   loop (as : Array α) (j : Fin as.size) :=
-    if i.1 < j then
+    if i < j then
       let j' := ⟨j-1, Nat.lt_of_le_of_lt (Nat.pred_le _) j.2⟩
       let as := as.swap j' j
       loop as ⟨j', by rw [size_swap]; exact j'.2⟩
@@ -818,12 +843,23 @@ def erase [BEq α] (as : Array α) (a : α) : Array α :=
   let as := as.push a
   loop as ⟨j, size_push .. ▸ j.lt_succ_self⟩
 
+@[deprecated insertIdx (since := "2024-11-20")] abbrev insertAt := @insertIdx
+
 /-- Insert element `a` at position `i`. Panics if `i` is not `i ≤ as.size`. -/
-def insertAt! (as : Array α) (i : Nat) (a : α) : Array α :=
+def insertIdx! (as : Array α) (i : Nat) (a : α) : Array α :=
   if h : i ≤ as.size then
-    insertAt as ⟨i, Nat.lt_succ_of_le h⟩ a
+    insertIdx as i a
   else panic! "invalid index"
 
+@[deprecated insertIdx! (since := "2024-11-20")] abbrev insertAt! := @insertIdx!
+
+/-- Insert element `a` at position `i`, or do nothing if `as.size < i`. -/
+def insertIdxIfInBounds (as : Array α) (i : Nat) (a : α) : Array α :=
+  if h : i ≤ as.size then
+    insertIdx as i a
+  else
+    as
+
 @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 def isPrefixOfAux [BEq α] (as bs : Array α) (hle : as.size ≤ bs.size) (i : Nat) : Bool :=
   if h : i < as.size then

src/Init/Data/Array/BinSearch.lean

@@ -52,7 +52,7 @@ namespace Array
     let mid    := (lo + hi)/2
     let midVal := as.get! mid
     if lt midVal k then
-      if mid == lo then do let v ← add (); pure <| as.insertAt! (lo+1) v
+      if mid == lo then do let v ← add (); pure <| as.insertIdx! (lo+1) v
       else binInsertAux lt merge add as k mid hi
     else if lt k midVal then
       binInsertAux lt merge add as k lo mid
@@ -67,7 +67,7 @@ namespace Array
     (k : α) : m (Array α) :=
   let _ := Inhabited.mk k
   if as.isEmpty then do let v ← add (); pure <| as.push v
-  else if lt k (as.get! 0) then do let v ← add (); pure <| as.insertAt! 0 v
+  else if lt k (as.get! 0) then do let v ← add (); pure <| as.insertIdx! 0 v
   else if !lt (as.get! 0) k then as.modifyM 0 <| merge
   else if lt as.back! k then do let v ← add (); pure <| as.push v
   else if !lt k as.back! then as.modifyM (as.size - 1) <| merge

src/Init/Data/Array/Lemmas.lean

@@ -1602,9 +1602,9 @@ theorem swap_comm (a : Array α) {i j : Fin a.size} : a.swap i j = a.swap j i :=
 
 /-! ### eraseIdx -/
 
-theorem feraseIdx_eq_eraseIdx {a : Array α} {i : Fin a.size} :
-    a.feraseIdx i = a.eraseIdx i.1 := by
-  simp [eraseIdx]
+theorem eraseIdx_eq_eraseIdxIfInBounds {a : Array α} {i : Nat} (h : i < a.size) :
+    a.eraseIdx i h = a.eraseIdxIfInBounds i := by
+  simp [eraseIdxIfInBounds, h]
 
 /-! ### isPrefixOf -/
 
@@ -1834,16 +1834,15 @@ theorem takeWhile_go_toArray (p : α → Bool) (l : List α) (i : Nat) :
     l.toArray.takeWhile p = (l.takeWhile p).toArray := by
   simp [Array.takeWhile, takeWhile_go_toArray]
 
-@[simp] theorem feraseIdx_toArray (l : List α) (i : Fin l.toArray.size) :
-    l.toArray.feraseIdx i = (l.eraseIdx i).toArray := by
-  rw [feraseIdx]
-  split <;> rename_i h
-  · rw [feraseIdx_toArray]
+@[simp] theorem eraseIdx_toArray (l : List α) (i : Nat) (h : i < l.toArray.size) :
+    l.toArray.eraseIdx i h = (l.eraseIdx i).toArray := by
+  rw [Array.eraseIdx]
+  split <;> rename_i h'
+  · rw [eraseIdx_toArray]
     simp only [swap_toArray, Fin.getElem_fin, toList_toArray, mk.injEq]
     rw [eraseIdx_set_gt (by simp), eraseIdx_set_eq]
     simp
-  · rcases i with ⟨i, w⟩
-    simp at h w
+  · simp at h h'
     have t : i = l.length - 1 := by omega
     simp [t]
 termination_by l.length - i
@@ -1853,9 +1852,9 @@ decreasing_by
   simp
   omega
 
-@[simp] theorem eraseIdx_toArray (l : List α) (i : Nat) :
-    l.toArray.eraseIdx i = (l.eraseIdx i).toArray := by
-  rw [Array.eraseIdx]
+@[simp] theorem eraseIdxIfInBounds_toArray (l : List α) (i : Nat) :
+    l.toArray.eraseIdxIfInBounds i = (l.eraseIdx i).toArray := by
+  rw [Array.eraseIdxIfInBounds]
   split
   · simp
   · simp_all [eraseIdx_eq_self.2]
@@ -1874,13 +1873,13 @@ namespace Array
     (as.takeWhile p).toList = as.toList.takeWhile p := by
   induction as; simp
 
-@[simp] theorem toList_feraseIdx (as : Array α) (i : Fin as.size) :
-    (as.feraseIdx i).toList = as.toList.eraseIdx i.1 := by
+@[simp] theorem toList_eraseIdx (as : Array α) (i : Nat) (h : i < as.size) :
+    (as.eraseIdx i h).toList = as.toList.eraseIdx i := by
   induction as
   simp
 
-@[simp] theorem toList_eraseIdx (as : Array α) (i : Nat) :
-    (as.eraseIdx i).toList = as.toList.eraseIdx i := by
+@[simp] theorem toList_eraseIdxIfInBounds (as : Array α) (i : Nat) :
+    (as.eraseIdxIfInBounds i).toList = as.toList.eraseIdx i := by
   induction as
   simp
 

src/Lean/Compiler/LCNF/Basic.lean

@@ -366,10 +366,10 @@ to be updated.
 @[implemented_by updateFunDeclCoreImp] opaque FunDeclCore.updateCore (decl: FunDecl) (type : Expr) (params : Array Param) (value : Code) : FunDecl
 
 def CasesCore.extractAlt! (cases : Cases) (ctorName : Name) : Alt × Cases :=
-  let found (i : Nat) := (cases.alts[i]!, { cases with alts := cases.alts.eraseIdx i })
-  if let some i := cases.alts.findIdx? fun | .alt ctorName' .. => ctorName == ctorName' | _ => false then
+  let found i := (cases.alts[i], { cases with alts := cases.alts.eraseIdx i })
+  if let some i := cases.alts.findFinIdx? fun | .alt ctorName' .. => ctorName == ctorName' | _ => false then
     found i
-  else if let some i := cases.alts.findIdx? fun | .default _ => true | _ => false then
+  else if let some i := cases.alts.findFinIdx? fun | .default _ => true | _ => false then
     found i
   else
     unreachable!

src/Lean/Compiler/LCNF/PassManager.lean

@@ -134,9 +134,9 @@ def withEachOccurrence (targetName : Name) (f : Nat → PassInstaller) : PassIns
 
 def installAfter (targetName : Name) (p : Pass → Pass) (occurrence : Nat := 0) : PassInstaller where
   install passes :=
-    if let some idx := passes.findIdx? (fun p => p.name == targetName && p.occurrence == occurrence) then
-      let passUnderTest := passes[idx]!
-      return passes.insertAt! (idx + 1) (p passUnderTest)
+    if let some idx := passes.findFinIdx? (fun p => p.name == targetName && p.occurrence == occurrence) then
+      let passUnderTest := passes[idx]
+      return passes.insertIdx (idx + 1) (p passUnderTest)
     else
       throwError s!"Tried to insert pass after {targetName}, occurrence {occurrence} but {targetName} is not in the pass list"
 
@@ -145,9 +145,9 @@ def installAfterEach (targetName : Name) (p : Pass → Pass) : PassInstaller :=
 
 def installBefore (targetName : Name) (p : Pass → Pass) (occurrence : Nat := 0): PassInstaller where
   install passes :=
-    if let some idx := passes.findIdx? (fun p => p.name == targetName && p.occurrence == occurrence) then
-      let passUnderTest := passes[idx]!
-      return passes.insertAt! idx (p passUnderTest)
+    if let some idx := passes.findFinIdx? (fun p => p.name == targetName && p.occurrence == occurrence) then
+      let passUnderTest := passes[idx]
+      return passes.insertIdx idx (p passUnderTest)
     else
       throwError s!"Tried to insert pass after {targetName}, occurrence {occurrence} but {targetName} is not in the pass list"
 

src/Lean/Compiler/Specialize.lean

@@ -32,7 +32,7 @@ private def elabSpecArgs (declName : Name) (args : Array Syntax) : MetaM (Array
         result := result.push idx
       else
         let argName := arg.getId
-        if let some idx := argNames.getIdx? argName then
+        if let some idx := argNames.indexOf? argName then
           if result.contains idx then throwErrorAt arg "invalid specialization argument name `{argName}`, it has already been specified as a specialization candidate"
           result := result.push idx
         else

src/Lean/Data/PersistentHashMap.lean

@@ -233,10 +233,10 @@ partial def eraseAux [BEq α] : Node α β → USize → α → Node α β
   | n@(Node.collision keys vals heq), _, k =>
     match keys.indexOf? k with
     | some idx =>
-      let keys' := keys.feraseIdx idx
-      have keq := keys.size_feraseIdx idx
-      let vals' := vals.feraseIdx (Eq.ndrec idx heq)
-      have veq := vals.size_feraseIdx (Eq.ndrec idx heq)
+      let keys' := keys.eraseIdx idx
+      have keq := keys.size_eraseIdx idx _
+      let vals' := vals.eraseIdx (Eq.ndrec idx heq)
+      have veq := vals.size_eraseIdx (Eq.ndrec idx heq) _
       have : keys.size - 1 = vals.size - 1 := by rw [heq]
       Node.collision keys' vals' (keq.trans (this.trans veq.symm))
     | none     => n

src/Lean/Elab/App.lean

@@ -1347,7 +1347,7 @@ where
     let mut unusableNamedArgs := unusableNamedArgs
     for x in xs, bInfo in bInfos do
       let xDecl ← x.mvarId!.getDecl
-      if let some idx := remainingNamedArgs.findIdx? (·.name == xDecl.userName) then
+      if let some idx := remainingNamedArgs.findFinIdx? (·.name == xDecl.userName) then
         /- If there is named argument with name `xDecl.userName`, then it is accounted for and we can't make use of it. -/
         remainingNamedArgs := remainingNamedArgs.eraseIdx idx
       else
@@ -1355,9 +1355,9 @@ where
           /- We found a type of the form (baseName ...).
              First, we check if the current argument is an explicit one,
              and if the current explicit position "fits" at `args` (i.e., it must be ≤ arg.size) -/
-          if argIdx ≤ args.size && bInfo.isExplicit then
+          if h : argIdx ≤ args.size ∧ bInfo.isExplicit then
             /- We can insert `e` as an explicit argument -/
-            return (args.insertAt! argIdx (Arg.expr e), namedArgs)
+            return (args.insertIdx argIdx (Arg.expr e), namedArgs)
           else
             /- If we can't add `e` to `args`, we try to add it using a named argument, but this is only possible
                if there isn't an argument with the same name occurring before it. -/

src/Lean/Elab/BuiltinCommand.lean

@@ -211,7 +211,7 @@ private def replaceBinderAnnotation (binder : TSyntax ``Parser.Term.bracketedBin
         else
           `(bracketedBinderF| {$id $[: $ty?]?})
       for id in ids.reverse do
-        if let some idx := binderIds.findIdx? fun binderId => binderId.raw.isIdent && binderId.raw.getId == id.raw.getId then
+        if let some idx := binderIds.findFinIdx? fun binderId => binderId.raw.isIdent && binderId.raw.getId == id.raw.getId then
           binderIds := binderIds.eraseIdx idx
           modifiedVarDecls := true
           varDeclsNew := varDeclsNew.push (← mkBinder id explicit)

src/Lean/Elab/Do.lean

@@ -1518,7 +1518,7 @@ mutual
   -/
   partial def doForToCode (doFor : Syntax) (doElems : List Syntax) : M CodeBlock := do
     let doForDecls := doFor[1].getSepArgs
-    if doForDecls.size > 1 then
+    if h : doForDecls.size > 1 then
       /-
         Expand
         ```

src/Lean/Elab/PatternVar.lean

@@ -332,9 +332,9 @@ where
     else
       let accessible := isNextArgAccessible ctx
       let (d, ctx)   := getNextParam ctx
-      match ctx.namedArgs.findIdx? fun namedArg => namedArg.name == d.1 with
+      match ctx.namedArgs.findFinIdx? fun namedArg => namedArg.name == d.1 with
       | some idx =>
-        let arg := ctx.namedArgs[idx]!
+        let arg := ctx.namedArgs[idx]
         let ctx := { ctx with namedArgs := ctx.namedArgs.eraseIdx idx }
         let ctx ← pushNewArg accessible ctx arg.val
         processCtorAppContext ctx

src/Lean/Elab/PreDefinition/Structural/BRecOn.lean

@@ -292,9 +292,9 @@ def mkBrecOnApp (positions : Positions) (fnIdx : Nat) (brecOnConst : Nat → Exp
     let packedFTypes ← inferArgumentTypesN positions.size brecOn
     let packedFArgs ← positions.mapMwith PProdN.mkLambdas packedFTypes FArgs
     let brecOn := mkAppN brecOn packedFArgs
-    let some poss := positions.find? (·.contains fnIdx)
+    let some (size, idx) := positions.findSome? fun pos => (pos.size, ·) <$> pos.indexOf? fnIdx
       | throwError "mkBrecOnApp: Could not find {fnIdx} in {positions}"
-    let brecOn ← PProdN.proj poss.size (poss.getIdx? fnIdx).get! brecOn
+    let brecOn ← PProdN.proj size idx brecOn
     mkLambdaFVars ys (mkAppN brecOn otherArgs)
 
 end Lean.Elab.Structural

src/Lean/Elab/PreDefinition/WF/PackMutual.lean

@@ -40,7 +40,7 @@ private partial def post (fixedPrefix : Nat) (argsPacker : ArgsPacker) (funNames
     return TransformStep.done e
   let declName := f.constName!
   let us       := f.constLevels!
-  if let some fidx := funNames.getIdx? declName then
+  if let some fidx := funNames.indexOf? declName then
     let arity := fixedPrefix + argsPacker.varNamess[fidx]!.size
     let e' ← withAppN arity e fun args => do
       let fixedArgs := args[:fixedPrefix]

src/Lean/Elab/Quotation.lean

@@ -58,7 +58,7 @@ partial def mkTuple : Array Syntax → TermElabM Syntax
   | #[]  => `(Unit.unit)
   | #[e] => return e
   | es   => do
-    let stx ← mkTuple (es.eraseIdx 0)
+    let stx ← mkTuple (es.eraseIdxIfInBounds 0)
     `(Prod.mk $(es[0]!) $stx)
 
 def resolveSectionVariable (sectionVars : NameMap Name) (id : Name) : List (Name × List String) :=

src/Lean/Elab/Syntax.lean

@@ -142,7 +142,7 @@ where
     let args := stx.getArgs
     if (← checkLeftRec stx[0]) then
       if args.size == 1 then throwErrorAt stx "invalid atomic left recursive syntax"
-      let args := args.eraseIdx 0
+      let args := args.eraseIdxIfInBounds 0
       let args ← args.mapM fun arg => withNestedParser do process arg
       mkParserSeq args
     else

src/Lean/Elab/Tactic/Induction.lean

@@ -340,9 +340,9 @@ where
     for h : altStxIdx in [0:altStxs.size] do
       let altStx := altStxs[altStxIdx]
       let altName := getAltName altStx
-      if let some i := alts.findIdx? (·.1 == altName) then
+      if let some i := alts.findFinIdx? (·.1 == altName) then
         -- cover named alternative
-        applyAltStx tacSnaps altStxIdx altStx alts[i]!
+        applyAltStx tacSnaps altStxIdx altStx alts[i]
         alts := alts.eraseIdx i
       else if !alts.isEmpty && isWildcard altStx then
         -- cover all alternatives

src/Lean/Meta/IndPredBelow.lean

@@ -83,7 +83,7 @@ where
       forallTelescopeReducing t fun xs s => do
         let motiveType ← instantiateForall motive xs[:numParams]
         withLocalDecl motiveName BinderInfo.implicit motiveType fun motive => do
-          mkForallFVars (xs.insertAt! numParams motive) s)
+          mkForallFVars (xs.insertIdxIfInBounds numParams motive) s)
 
   motiveType (indVal : InductiveVal) : MetaM Expr :=
     forallTelescopeReducing indVal.type fun xs _ => do

src/Lean/Meta/Match/MatchEqs.lean

@@ -129,9 +129,9 @@ where
           let typeNew := b.instantiate1 y
           if let some (_, lhs, rhs) ← matchEq? d then
             if lhs.isFVar && ys.contains lhs && args.contains lhs && isNamedPatternProof typeNew y then
-               let some j  := ys.getIdx? lhs | unreachable!
+               let some j  := ys.indexOf? lhs | unreachable!
                let ys      := ys.eraseIdx j
-               let some k  := args.getIdx? lhs | unreachable!
+               let some k  := args.indexOf? lhs | unreachable!
                let mask    := mask.set! k false
                let args    := args.map fun arg => if arg == lhs then rhs else arg
                let arg     ← mkEqRefl rhs

src/Lean/Meta/RecursorInfo.lean

@@ -107,7 +107,7 @@ private def getMajorPosDepElim (declName : Name) (majorPos? : Option Nat) (xs :
     if motiveArgs.isEmpty then
       throwError "invalid user defined recursor, '{declName}' does not support dependent elimination, and position of the major premise was not specified (solution: set attribute '[recursor <pos>]', where <pos> is the position of the major premise)"
     let major := motiveArgs.back!
-    match xs.getIdx? major with
+    match xs.indexOf? major with
     | some majorPos => pure (major, majorPos, true)
     | none          => throwError "ill-formed recursor '{declName}'"
 

src/Lean/Meta/Tactic/Clear.lean

@@ -27,7 +27,7 @@ def _root_.Lean.MVarId.clear (mvarId : MVarId) (fvarId : FVarId) : MetaM MVarId
       throwTacticEx `clear mvarId m!"target depends on '{mkFVar fvarId}'"
     let lctx := lctx.erase fvarId
     let localInsts ← getLocalInstances
-    let localInsts := match localInsts.findIdx? fun localInst => localInst.fvar.fvarId! == fvarId with
+    let localInsts := match localInsts.findFinIdx? fun localInst => localInst.fvar.fvarId! == fvarId with
       | none => localInsts
       | some idx => localInsts.eraseIdx idx
     let newMVar ← mkFreshExprMVarAt lctx localInsts mvarDecl.type MetavarKind.syntheticOpaque tag

src/Lean/MetavarContext.lean

@@ -248,9 +248,7 @@ instance : Hashable LocalInstance where
 
 /-- Remove local instance with the given `fvarId`. Do nothing if `localInsts` does not contain any free variable with id `fvarId`. -/
 def LocalInstances.erase (localInsts : LocalInstances) (fvarId : FVarId) : LocalInstances :=
-  match localInsts.findIdx? (fun inst => inst.fvar.fvarId! == fvarId) with
-  | some idx => localInsts.eraseIdx idx
-  | _        => localInsts
+  localInsts.eraseP (fun inst => inst.fvar.fvarId! == fvarId)
 
 /-- A kind for the metavariable that determines its unification behaviour.
 For more information see the large comment at the beginning of this file. -/

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -349,7 +349,7 @@ def delabAppExplicitCore (fieldNotation : Bool) (numArgs : Nat) (delabHead : (in
     if idx == 0 then
       -- If it's the first argument, then we can tag `obj.field` with the first app.
       head ← withBoundedAppFn (numArgs - 1) <| annotateTermInfo head
-    return Syntax.mkApp head (argStxs.eraseIdx idx)
+    return Syntax.mkApp head (argStxs.eraseIdxIfInBounds idx)
   else
     return Syntax.mkApp fnStx argStxs
 
@@ -876,7 +876,7 @@ def delabLam : Delab :=
           -- "default" binder group is the only one that expects binder names
           -- as a term, i.e. a single `Syntax.ident` or an application thereof
           let stxCurNames ←
-            if curNames.size > 1 then
+            if h : curNames.size > 1 then
               `($(curNames.get! 0) $(curNames.eraseIdx 0)*)
             else
               pure $ curNames.get! 0;

src/Lean/Structure.lean

@@ -383,7 +383,7 @@ partial def computeStructureResolutionOrder [Monad m] [MonadEnv m]
   -- `resOrders` contains the resolution orders to merge.
   -- The parent list is inserted as a pseudo resolution order to ensure immediate parents come out in order,
   -- and it is added first to be the primary ordering constraint when there are ordering errors.
-  let mut resOrders := parentResOrders.insertAt 0 parentNames |>.filter (!·.isEmpty)
+  let mut resOrders := parentResOrders.insertIdx 0 parentNames |>.filter (!·.isEmpty)
 
   let mut resOrder : Array Name := #[structName]
   let mut defects : Array StructureResolutionOrderConflict := #[]

tests/lean/interactive/completionDocString.lean

@@ -1,2 +1,2 @@
-#eval Array.insertAt
-                  --^ textDocument/completion
+#eval Array.insertIdx
+                   --^ textDocument/completion

tests/lean/interactive/completionDocString.lean.expected.out

@@ -1,19 +1,32 @@
 {"textDocument": {"uri": "file:///completionDocString.lean"},
- "position": {"line": 0, "character": 20}}
+ "position": {"line": 0, "character": 21}}
 {"items":
  [{"sortText": "0",
-   "label": "insertAt",
+   "label": "insertIdx",
    "kind": 3,
    "documentation":
    {"value": "Insert element `a` at position `i`. ", "kind": "markdown"},
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completionDocString.lean"},
-     "position": {"line": 0, "character": 20}},
-    "id": {"const": {"declName": "Array.insertAt"}},
+     "position": {"line": 0, "character": 21}},
+    "id": {"const": {"declName": "Array.insertIdx"}},
     "cPos": 0}},
   {"sortText": "1",
-   "label": "insertAt!",
+   "label": "insertIdxIfInBounds",
+   "kind": 3,
+   "documentation":
+   {"value":
+    "Insert element `a` at position `i`, or do nothing if `as.size < i`. ",
+    "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionDocString.lean"},
+     "position": {"line": 0, "character": 21}},
+    "id": {"const": {"declName": "Array.insertIdxIfInBounds"}},
+    "cPos": 0}},
+  {"sortText": "2",
+   "label": "insertIdx!",
    "kind": 3,
    "documentation":
    {"value":
@@ -22,7 +35,7 @@
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completionDocString.lean"},
-     "position": {"line": 0, "character": 20}},
-    "id": {"const": {"declName": "Array.insertAt!"}},
+     "position": {"line": 0, "character": 21}},
+    "id": {"const": {"declName": "Array.insertIdx!"}},
     "cPos": 0}}],
  "isIncomplete": true}

tests/lean/run/array_isEqvAux.lean

@@ -36,9 +36,9 @@ example : #[0, 1, 2].popWhile (· % 2 = 0) = #[0, 1] := by decide
 
 example : #[0, 1, 2].takeWhile (· % 2 = 0) = #[0] := by decide
 
-example : #[0, 1, 2].feraseIdx ⟨1, by decide⟩ = #[0, 2] := by decide
+example : #[0, 1, 2].eraseIdx 1 = #[0, 2] := by decide
 
-example : #[0, 1, 2].insertAt ⟨1, by decide⟩ 3 = #[0, 3, 1, 2] := by decide
+example : #[0, 1, 2].insertIdx 1 3 = #[0, 3, 1, 2] := by decide
 
 example : #[0, 1, 2].isPrefixOf #[0, 1, 2, 3] = true := by decide