diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index f6657f147c..7e4abb955f 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -703,7 +703,7 @@ def erase [BEq α] (as : Array α) (a : α) : Array α :=
   | some i => as.feraseIdx i
 
 /-- Insert element `a` at position `i`. -/
-@[inline] def insertAt' (as : Array α) (i : Fin (as.size + 1)) (a : α) : Array α :=
+@[inline] def insertAt (as : Array α) (i : Fin (as.size + 1)) (a : α) : Array α :=
   let rec loop (as : Array α) (j : Fin as.size) :=
     if i.1 < j then
       let j' := ⟨j-1, Nat.lt_of_le_of_lt (Nat.pred_le _) j.2⟩
@@ -717,9 +717,9 @@ def erase [BEq α] (as : Array α) (a : α) : Array α :=
 termination_by _ _ _ j => j.1
 
 /-- Insert element `a` at position `i`. Panics if `i` is not `i ≤ as.size`. -/
-def insertAt (as : Array α) (i : Nat) (a : α) : Array α :=
+def insertAt! (as : Array α) (i : Nat) (a : α) : Array α :=
   if h : i ≤ as.size then
-    insertAt' as ⟨i, Nat.lt_succ_of_le h⟩ a
+    insertAt as ⟨i, Nat.lt_succ_of_le h⟩ a
   else panic! "invalid index"
 termination_by _ _ _ j => j.1
 
diff --git a/src/Init/Data/Array/BinSearch.lean b/src/Init/Data/Array/BinSearch.lean
index 362f8de849..34b940ff8e 100644
--- a/src/Init/Data/Array/BinSearch.lean
+++ b/src/Init/Data/Array/BinSearch.lean
@@ -50,7 +50,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.insertAt! (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
@@ -64,7 +64,7 @@ namespace Array
     (as : Array α)
     (k : α) : m (Array α) :=
   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.insertAt! 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
diff --git a/src/Lean/Compiler/LCNF/PassManager.lean b/src/Lean/Compiler/LCNF/PassManager.lean
index 13d2bb95fe..d5a0505b3d 100644
--- a/src/Lean/Compiler/LCNF/PassManager.lean
+++ b/src/Lean/Compiler/LCNF/PassManager.lean
@@ -143,7 +143,7 @@ def installAfter (targetName : Name) (p : Pass → Pass) (occurrence : Nat := 0)
   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)
+      return passes.insertAt! (idx + 1) (p passUnderTest)
     else
       throwError s!"Tried to insert pass after {targetName}, occurrence {occurrence} but {targetName} is not in the pass list"
 
@@ -154,7 +154,7 @@ def installBefore (targetName : Name) (p : Pass → Pass) (occurrence : Nat := 0
   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)
+      return passes.insertAt! idx (p passUnderTest)
     else
       throwError s!"Tried to insert pass after {targetName}, occurrence {occurrence} but {targetName} is not in the pass list"
 
diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index a45e511f3a..b4834dddab 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -1109,7 +1109,7 @@ private def addLValArg (baseName : Name) (fullName : Name) (e : Expr) (args : Ar
              and the current explicit position "fits" at `args` (i.e., it must be ≤ arg.size) -/
           if argIdx ≤ args.size && xDecl.binderInfo.isExplicit then
             /- We insert `e` as an explicit argument -/
-            return (args.insertAt argIdx (Arg.expr e), namedArgs)
+            return (args.insertAt! argIdx (Arg.expr e), namedArgs)
           /- 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. -/
           for j in [:i] do
diff --git a/src/Lean/Linter/UnusedVariables.lean b/src/Lean/Linter/UnusedVariables.lean
index e41df7900b..0766abeaa8 100644
--- a/src/Lean/Linter/UnusedVariables.lean
+++ b/src/Lean/Linter/UnusedVariables.lean
@@ -186,7 +186,7 @@ def unusedVariables : Linter := fun cmdStx => do
 
   -- collect ignore functions
   let ignoreFns := (← getUnusedVariablesIgnoreFns)
-    |>.insertAt 0 (isTopLevelDecl constDecls)
+    |>.insertAt! 0 (isTopLevelDecl constDecls)
 
   -- determine unused variables
   for (id, ⟨decl?, uses⟩) in vars.toList do
diff --git a/src/Lean/Meta/IndPredBelow.lean b/src/Lean/Meta/IndPredBelow.lean
index 59e5af2235..3145f29d31 100644
--- a/src/Lean/Meta/IndPredBelow.lean
+++ b/src/Lean/Meta/IndPredBelow.lean
@@ -82,7 +82,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.insertAt! numParams motive) s)
 
   motiveType (indVal : InductiveVal) : MetaM Expr :=
     forallTelescopeReducing indVal.type fun xs _ => do