diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index 3e520e51b4..662f6cfd10 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -235,9 +235,11 @@ def range (n : Nat) : Array Nat :=
 def singleton (v : α) : Array α :=
   mkArray 1 v
 
-def back [Inhabited α] (a : Array α) : α :=
+def back! [Inhabited α] (a : Array α) : α :=
   a.get! (a.size - 1)
 
+@[deprecated back! (since := "2024-10-31")] abbrev back := @back!
+
 def get? (a : Array α) (i : Nat) : Option α :=
   if h : i < a.size then some a[i] else none
 
diff --git a/src/Init/Data/Array/BinSearch.lean b/src/Init/Data/Array/BinSearch.lean
index a3d7a488d9..d5f3cd23b3 100644
--- a/src/Init/Data/Array/BinSearch.lean
+++ b/src/Init/Data/Array/BinSearch.lean
@@ -69,8 +69,8 @@ namespace 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 (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
+  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
   else binInsertAux lt merge add as k 0 (as.size - 1)
 
 @[inline] def binInsert {α : Type u} (lt : α → α → Bool) (as : Array α) (k : α) : Array α :=
diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
index 1cecde08dc..d645fda2ee 100644
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -105,8 +105,8 @@ We prefer to pull `List.toArray` outwards.
 
 @[simp] theorem toArray_singleton (a : α) : (List.singleton a).toArray = singleton a := rfl
 
-@[simp] theorem back_toArray [Inhabited α] (l : List α) : l.toArray.back = l.getLast! := by
-  simp only [back, size_toArray, Array.get!_eq_getElem!, getElem!_toArray, getLast!_eq_getElem!]
+@[simp] theorem back!_toArray [Inhabited α] (l : List α) : l.toArray.back! = l.getLast! := by
+  simp only [back!, size_toArray, Array.get!_eq_getElem!, getElem!_toArray, getLast!_eq_getElem!]
 
 @[simp] theorem forIn'_loop_toArray [Monad m] (l : List α) (f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)) (i : Nat)
     (h : i ≤ l.length) (b : β) :
@@ -495,14 +495,14 @@ theorem getElem?_eq_some_iff {as : Array α} : as[n]? = some a ↔ ∃ h : n < a
   cases as
   simp [List.getElem?_eq_some_iff]
 
-theorem back_eq_back? [Inhabited α] (a : Array α) : a.back = a.back?.getD default := by
-  simp only [back, get!_eq_getElem?, get?_eq_getElem?, back?]
+theorem back!_eq_back? [Inhabited α] (a : Array α) : a.back! = a.back?.getD default := by
+  simp only [back!, get!_eq_getElem?, get?_eq_getElem?, back?]
 
 @[simp] theorem back?_push (a : Array α) : (a.push x).back? = some x := by
   simp [back?, getElem?_eq_getElem?_toList]
 
-@[simp] theorem back_push [Inhabited α] (a : Array α) : (a.push x).back = x := by
-  simp [back_eq_back?]
+@[simp] theorem back!_push [Inhabited α] (a : Array α) : (a.push x).back! = x := by
+  simp [back!_eq_back?]
 
 theorem getElem?_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
     (a.push x)[i]? = some a[i] := by
@@ -615,8 +615,8 @@ theorem eq_empty_of_size_eq_zero {as : Array α} (h : as.size = 0) : as = #[] :=
   · simp [h]
   · intros; contradiction
 
-theorem eq_push_pop_back_of_size_ne_zero [Inhabited α] {as : Array α} (h : as.size ≠ 0) :
-    as = as.pop.push as.back := by
+theorem eq_push_pop_back!_of_size_ne_zero [Inhabited α] {as : Array α} (h : as.size ≠ 0) :
+    as = as.pop.push as.back! := by
   apply ext
   · simp [Nat.sub_add_cancel (Nat.zero_lt_of_ne_zero h)]
   · intros i h h'
@@ -625,12 +625,12 @@ theorem eq_push_pop_back_of_size_ne_zero [Inhabited α] {as : Array α} (h : as.
     else
       have heq : i = as.pop.size :=
         Nat.le_antisymm (size_pop .. ▸ Nat.le_pred_of_lt h) (Nat.le_of_not_gt hlt)
-      cases heq; rw [getElem_push_eq, back, ←size_pop, get!_eq_getD, getD, dif_pos h]; rfl
+      cases heq; rw [getElem_push_eq, back!, ←size_pop, get!_eq_getD, getD, dif_pos h]; rfl
 
 theorem eq_push_of_size_ne_zero {as : Array α} (h : as.size ≠ 0) :
     ∃ (bs : Array α) (c : α), as = bs.push c :=
   let _ : Inhabited α := ⟨as[0]⟩
-  ⟨as.pop, as.back, eq_push_pop_back_of_size_ne_zero h⟩
+  ⟨as.pop, as.back!, eq_push_pop_back!_of_size_ne_zero h⟩
 
 theorem size_eq_length_toList (as : Array α) : as.size = as.toList.length := rfl
 
@@ -1621,6 +1621,8 @@ theorem toArray_concat {as : List α} {x : α} :
   apply ext'
   simp
 
+@[deprecated back!_toArray (since := "2024-10-31")] abbrev back_toArray := @back!_toArray
+
 end List
 
 namespace Array
@@ -1761,4 +1763,9 @@ abbrev get_swap := @getElem_swap
 @[deprecated getElem_swap' (since := "2024-09-30")]
 abbrev get_swap' := @getElem_swap'
 
+@[deprecated back!_eq_back? (since := "2024-10-31")] abbrev back_eq_back? := @back!_eq_back?
+@[deprecated back!_push (since := "2024-10-31")] abbrev back_push := @back!_push
+@[deprecated eq_push_pop_back!_of_size_ne_zero (since := "2024-10-31")]
+abbrev eq_push_pop_back_of_size_ne_zero := @eq_push_pop_back!_of_size_ne_zero
+
 end Array
diff --git a/src/Lean/Compiler/IR/ElimDeadVars.lean b/src/Lean/Compiler/IR/ElimDeadVars.lean
index da02b23dd8..e462e69192 100644
--- a/src/Lean/Compiler/IR/ElimDeadVars.lean
+++ b/src/Lean/Compiler/IR/ElimDeadVars.lean
@@ -13,7 +13,7 @@ partial def reshapeWithoutDead (bs : Array FnBody) (term : FnBody) : FnBody :=
   let rec reshape (bs : Array FnBody) (b : FnBody) (used : IndexSet) :=
     if bs.isEmpty then b
     else
-      let curr := bs.back
+      let curr := bs.back!
       let bs   := bs.pop
       let keep (_ : Unit) :=
         let used := curr.collectFreeIndices used
diff --git a/src/Lean/Compiler/IR/EmitLLVM.lean b/src/Lean/Compiler/IR/EmitLLVM.lean
index 2d6ba911b2..9bb129f055 100644
--- a/src/Lean/Compiler/IR/EmitLLVM.lean
+++ b/src/Lean/Compiler/IR/EmitLLVM.lean
@@ -1075,7 +1075,7 @@ def emitSetTag (builder : LLVM.Builder llvmctx) (x : VarId) (i : Nat) : M llvmct
 def ensureHasDefault' (alts : Array Alt) : Array Alt :=
   if alts.any Alt.isDefault then alts
   else
-    let last := alts.back
+    let last := alts.back!
     let alts := alts.pop
     alts.push (Alt.default last.body)
 
diff --git a/src/Lean/Compiler/IR/ExpandResetReuse.lean b/src/Lean/Compiler/IR/ExpandResetReuse.lean
index 2ac50dd7bc..e2a1a8b38b 100644
--- a/src/Lean/Compiler/IR/ExpandResetReuse.lean
+++ b/src/Lean/Compiler/IR/ExpandResetReuse.lean
@@ -56,7 +56,7 @@ partial def eraseProjIncForAux (y : VarId) (bs : Array FnBody) (mask : Mask) (ke
   let keepInstr (b : FnBody) := eraseProjIncForAux y bs.pop mask (keep.push b)
   if bs.size < 2 then done ()
   else
-    let b := bs.back
+    let b := bs.back!
     match b with
     | .vdecl _ _ (.sproj _ _ _) _ => keepInstr b
     | .vdecl _ _ (.uproj _ _) _   => keepInstr b
diff --git a/src/Lean/Compiler/IR/PushProj.lean b/src/Lean/Compiler/IR/PushProj.lean
index 04d7f02671..a7f2e9fdf5 100644
--- a/src/Lean/Compiler/IR/PushProj.lean
+++ b/src/Lean/Compiler/IR/PushProj.lean
@@ -13,7 +13,7 @@ namespace Lean.IR
 partial def pushProjs (bs : Array FnBody) (alts : Array Alt) (altsF : Array IndexSet) (ctx : Array FnBody) (ctxF : IndexSet) : Array FnBody × Array Alt :=
   if bs.isEmpty then (ctx.reverse, alts)
   else
-    let b    := bs.back
+    let b    := bs.back!
     let bs   := bs.pop
     let done (_ : Unit) := (bs.push b ++ ctx.reverse, alts)
     let skip (_ : Unit) := pushProjs bs alts altsF (ctx.push b) (b.collectFreeIndices ctxF)
diff --git a/src/Lean/Compiler/IR/SimpCase.lean b/src/Lean/Compiler/IR/SimpCase.lean
index 0276951e06..fe73f7e8f7 100644
--- a/src/Lean/Compiler/IR/SimpCase.lean
+++ b/src/Lean/Compiler/IR/SimpCase.lean
@@ -13,8 +13,8 @@ def ensureHasDefault (alts : Array Alt) : Array Alt :=
   if alts.any Alt.isDefault then alts
   else if alts.size < 2 then alts
   else
-    let last := alts.back;
-    let alts := alts.pop;
+    let last := alts.back!
+    let alts := alts.pop
     alts.push (Alt.default last.body)
 
 private def getOccsOf (alts : Array Alt) (i : Nat) : Nat := Id.run do
diff --git a/src/Lean/Data/Lsp/Utf16.lean b/src/Lean/Data/Lsp/Utf16.lean
index e6b214a3ba..e83fb043db 100644
--- a/src/Lean/Data/Lsp/Utf16.lean
+++ b/src/Lean/Data/Lsp/Utf16.lean
@@ -70,7 +70,7 @@ private def lineStartPos (text : FileMap) (line : Nat) : String.Pos :=
   else if text.positions.isEmpty then
     0
   else
-    text.positions.back
+    text.positions.back!
 
 /-- Computes an UTF-8 offset into `text.source`
 from an LSP-style 0-indexed (ln, col) position. -/
diff --git a/src/Lean/Data/Position.lean b/src/Lean/Data/Position.lean
index 7495b03f5d..28a27600f8 100644
--- a/src/Lean/Data/Position.lean
+++ b/src/Lean/Data/Position.lean
@@ -66,12 +66,12 @@ partial def ofString (s : String) : FileMap :=
       let i := s.next i
       if c == '\n' then loop i (line+1) (ps.push i)
       else loop i line ps
-  loop 0 1 (#[0])
+  loop 0 1 #[0]
 
 partial def toPosition (fmap : FileMap) (pos : String.Pos) : Position :=
   match fmap with
   | { source := str, positions := ps } =>
-    if ps.size >= 2 && pos <= ps.back then
+    if ps.size >= 2 && pos <= ps.back! then
       let rec toColumn (i : String.Pos) (c : Nat) : Nat :=
         if i == pos || str.atEnd i then c
         else toColumn (str.next i) (c+1)
@@ -84,14 +84,14 @@ partial def toPosition (fmap : FileMap) (pos : String.Pos) : Position :=
           if pos == posM then { line := fmap.getLine m, column := 0 }
           else if pos > posM then loop m e
           else loop b m
-      loop 0 (ps.size -1)
+      loop 0 (ps.size - 1)
     else if ps.isEmpty then
       ⟨0, 0⟩
     else
       -- Some systems like the delaborator use synthetic positions without an input file,
       -- which would violate `toPositionAux`'s invariant.
       -- Can also happen with EOF errors, which are not strictly inside the file.
-      ⟨fmap.getLastLine, (pos - ps.back).byteIdx⟩
+      ⟨fmap.getLastLine, (pos - ps.back!).byteIdx⟩
 
 /-- Convert a `Lean.Position` to a `String.Pos`. -/
 def ofPosition (text : FileMap) (pos : Position) : String.Pos :=
@@ -101,7 +101,7 @@ def ofPosition (text : FileMap) (pos : Position) : String.Pos :=
     else if text.positions.isEmpty then
       0
     else
-      text.positions.back
+      text.positions.back!
   String.Iterator.nextn ⟨text.source, colPos⟩ pos.column |>.pos
 
 /--
diff --git a/src/Lean/Data/Xml/Parser.lean b/src/Lean/Data/Xml/Parser.lean
index b5af3f347f..939bb3825f 100644
--- a/src/Lean/Data/Xml/Parser.lean
+++ b/src/Lean/Data/Xml/Parser.lean
@@ -463,7 +463,7 @@ mutual
     let mut res := #[]
     for x in xs do
       if res.size > 0 then
-        match res.back, x with
+        match res.back!, x with
         | Content.Character x, Content.Character y => res := res.set! (res.size - 1) (Content.Character $ x ++ y)
         | _, x => res := res.push x
       else res := res.push x
diff --git a/src/Lean/Elab/Arg.lean b/src/Lean/Elab/Arg.lean
index 79057d7ac3..3682f2766c 100644
--- a/src/Lean/Elab/Arg.lean
+++ b/src/Lean/Elab/Arg.lean
@@ -39,7 +39,7 @@ partial def expandArgs (args : Array Syntax) : MetaM (Array NamedArg × Array Ar
   let (args, ellipsis) :=
     if args.isEmpty then
       (args, false)
-    else if args.back.isOfKind ``Lean.Parser.Term.ellipsis then
+    else if args.back!.isOfKind ``Lean.Parser.Term.ellipsis then
       (args.pop, true)
     else
       (args, false)
diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index eb5ae628b0..08c3ccd2eb 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -226,7 +226,7 @@ partial def mkPairs (elems : Array Term) : MacroM Term :=
       loop i acc
     else
       pure acc
-  loop (elems.size - 1) elems.back
+  loop (elems.size - 1) elems.back!
 
 /-- Return syntax `PProd.mk elems[0] (PProd.mk elems[1] ... (PProd.mk elems[elems.size - 2] elems[elems.size - 1])))` -/
 partial def mkPPairs (elems : Array Term) : MacroM Term :=
@@ -238,7 +238,7 @@ partial def mkPPairs (elems : Array Term) : MacroM Term :=
       loop i acc
     else
       pure acc
-  loop (elems.size - 1) elems.back
+  loop (elems.size - 1) elems.back!
 
 /-- Return syntax `MProd.mk elems[0] (MProd.mk elems[1] ... (MProd.mk elems[elems.size - 2] elems[elems.size - 1])))` -/
 partial def mkMPairs (elems : Array Term) : MacroM Term :=
@@ -250,7 +250,7 @@ partial def mkMPairs (elems : Array Term) : MacroM Term :=
       loop i acc
     else
       pure acc
-  loop (elems.size - 1) elems.back
+  loop (elems.size - 1) elems.back!
 
 
 open Parser in
diff --git a/src/Lean/Elab/Calc.lean b/src/Lean/Elab/Calc.lean
index db51d8d2b2..923edae1f1 100644
--- a/src/Lean/Elab/Calc.lean
+++ b/src/Lean/Elab/Calc.lean
@@ -136,7 +136,7 @@ def throwCalcFailure (steps : Array CalcStepView) (expectedType result : Expr) :
           but is expected to be{indentD m!"{elhs} : {← inferType elhs}"}"
         failed := true
       unless ← isDefEqGuarded rhs erhs do
-        logErrorAt steps.back.term m!"\
+        logErrorAt steps.back!.term m!"\
           invalid 'calc' step, right-hand side is{indentD m!"{rhs} : {← inferType rhs}"}\n\
           but is expected to be{indentD m!"{erhs} : {← inferType erhs}"}"
         failed := true
diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean
index 3cc6fc02c9..48c4b400db 100644
--- a/src/Lean/Elab/Do.lean
+++ b/src/Lean/Elab/Do.lean
@@ -801,7 +801,7 @@ private def mkTuple (elems : Array Syntax) : MacroM Syntax := do
   else if elems.size == 1 then
     return elems[0]!
   else
-    elems.extract 0 (elems.size - 1) |>.foldrM (init := elems.back) fun elem tuple =>
+    elems.extract 0 (elems.size - 1) |>.foldrM (init := elems.back!) fun elem tuple =>
       ``(MProd.mk $elem $tuple)
 
 /-- Return `some action` if `doElem` is a `doExpr <action>`-/
diff --git a/src/Lean/Elab/Level.lean b/src/Lean/Elab/Level.lean
index cfeb5c74bf..5f9c56e001 100644
--- a/src/Lean/Elab/Level.lean
+++ b/src/Lean/Elab/Level.lean
@@ -60,11 +60,11 @@ partial def elabLevel (stx : Syntax) : LevelElabM Level := withRef stx do
     elabLevel (stx.getArg 1)
   else if kind == ``Lean.Parser.Level.max then
     let args := stx.getArg 1 |>.getArgs
-    args[:args.size - 1].foldrM (init := ← elabLevel args.back) fun stx lvl =>
+    args[:args.size - 1].foldrM (init := ← elabLevel args.back!) fun stx lvl =>
       return mkLevelMax' (← elabLevel stx) lvl
   else if kind == ``Lean.Parser.Level.imax then
     let args := stx.getArg 1 |>.getArgs
-    args[:args.size - 1].foldrM (init := ← elabLevel args.back) fun stx lvl =>
+    args[:args.size - 1].foldrM (init := ← elabLevel args.back!) fun stx lvl =>
       return mkLevelIMax' (← elabLevel stx) lvl
   else if kind == ``Lean.Parser.Level.hole then
     mkFreshLevelMVar
diff --git a/src/Lean/Elab/PreDefinition/Structural/IndGroupInfo.lean b/src/Lean/Elab/PreDefinition/Structural/IndGroupInfo.lean
index 457a406589..10f3c98d40 100644
--- a/src/Lean/Elab/PreDefinition/Structural/IndGroupInfo.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/IndGroupInfo.lean
@@ -105,6 +105,6 @@ def IndGroupInst.nestedTypeFormers (igi : IndGroupInst) : MetaM (Array Expr) :=
   auxMotives.mapM fun motive =>
     forallTelescopeReducing motive fun xs _ => do
       assert! xs.size > 0
-      mkForallFVars xs.pop (← inferType xs.back)
+      mkForallFVars xs.pop (← inferType xs.back!)
 
 end Lean.Elab.Structural
diff --git a/src/Lean/Elab/PreDefinition/TerminationArgument.lean b/src/Lean/Elab/PreDefinition/TerminationArgument.lean
index 0227908841..018057986f 100644
--- a/src/Lean/Elab/PreDefinition/TerminationArgument.lean
+++ b/src/Lean/Elab/PreDefinition/TerminationArgument.lean
@@ -118,7 +118,7 @@ def TerminationArgument.delab (arity : Nat) (extraParams : Nat) (termArg : Termi
         Array.map (fun (i : Ident) => if stxBody.raw.hasIdent i.getId then i else hole) vars
       -- drop trailing underscores
       let mut vars := vars
-      while ! vars.isEmpty && vars.back.raw.isOfKind ``hole do vars := vars.pop
+      while ! vars.isEmpty && vars.back!.raw.isOfKind ``hole do vars := vars.pop
       if termArg.structural then
         if vars.isEmpty then
           `(terminationBy|termination_by structural $stxBody)
diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean
index 305a96c1d2..71250fd73e 100644
--- a/src/Lean/Elab/Quotation.lean
+++ b/src/Lean/Elab/Quotation.lean
@@ -190,7 +190,7 @@ private partial def quoteSyntax : Syntax → TermElabM Term
                 | $[some $ids:ident],* => $(quote inner)
                 | $[_%$ids],*          => Array.empty)
             | _ =>
-              let arr ← ids[:ids.size-1].foldrM (fun id arr => `(Array.zip $id:ident $arr)) ids.back
+              let arr ← ids[:ids.size-1].foldrM (fun id arr => `(Array.zip $id:ident $arr)) ids.back!
               `(Array.map (fun $(← mkTuple ids) => $(inner[0]!)) $arr)
           let arr ← if k == `sepBy then
             `(mkSepArray $arr $(getSepStxFromSplice arg))
diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean
index 0a9866cfb0..9104923692 100644
--- a/src/Lean/Elab/Tactic/BuiltinTactic.lean
+++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean
@@ -465,7 +465,7 @@ def renameInaccessibles (mvarId : MVarId) (hs : TSyntaxArray ``binderIdent) : Ta
         let inaccessible := !(extractMacroScopes localDecl.userName |>.equalScope callerScopes)
         let shadowed := found.contains localDecl.userName
         if inaccessible || shadowed then
-          if let `(binderIdent| $h:ident) := hs.back then
+          if let `(binderIdent| $h:ident) := hs.back! then
             let newName := h.getId
             lctx := lctx.setUserName localDecl.fvarId newName
             info := info.push (localDecl.fvarId, h)
diff --git a/src/Lean/Meta/ArgsPacker.lean b/src/Lean/Meta/ArgsPacker.lean
index 6f2cd709de..27178ce08d 100644
--- a/src/Lean/Meta/ArgsPacker.lean
+++ b/src/Lean/Meta/ArgsPacker.lean
@@ -56,7 +56,7 @@ Given a telescope of FVars of type `tᵢ`, iterates `PSigma` to produce the type
 `t₁ ⊗' t₂ …`.
 -/
 def packType (xs : Array Expr) : MetaM Expr := do
-  let mut d ← inferType xs.back
+  let mut d ← inferType xs.back!
   for x in xs.pop.reverse do
     d ← mkAppOptM ``PSigma #[some (← inferType x), some (← mkLambdaFVars #[x] d)]
   return d
@@ -217,7 +217,7 @@ Helpers for iterated `PSum`.
 
 /-- Given types `#[t₁, t₂,…]`, returns the type `t₁ ⊕' t₂ …`. -/
 def packType (ds : Array Expr) : MetaM Expr := do
-  let mut r := ds.back
+  let mut r := ds.back!
   for d in ds.pop.reverse do
     r ← mkAppM ``PSum #[d, r]
   return r
@@ -335,7 +335,7 @@ def uncurryTypeND (types : Array Expr) : MetaM Expr := do
     unless type.isArrow do
       throwError "Mutual.uncurryTypeND: Expected non-dependent types, got {type}"
   let codomains := types.map (·.bindingBody!)
-  let t' := codomains.back
+  let t' := codomains.back!
   codomains.pop.forM fun t =>
     unless ← isDefEq t t' do
       throwError "Mutual.uncurryTypeND: Expected equal codomains, but got {t} and {t'}"
diff --git a/src/Lean/Meta/Closure.lean b/src/Lean/Meta/Closure.lean
index 289740b326..ba9b9456a6 100644
--- a/src/Lean/Meta/Closure.lean
+++ b/src/Lean/Meta/Closure.lean
@@ -239,7 +239,7 @@ def pickNextToProcess? : ClosureM (Option ToProcessElement) := do
     pure none
   else
     modifyGet fun s =>
-      let elem      := s.toProcess.back
+      let elem      := s.toProcess.back!
       let toProcess := s.toProcess.pop
       let (elem, toProcess) := pickNextToProcessAux lctx 0 toProcess elem
       (some elem, { s with toProcess := toProcess })
diff --git a/src/Lean/Meta/DiscrTree.lean b/src/Lean/Meta/DiscrTree.lean
index 79d2bff9f7..a3114086f7 100644
--- a/src/Lean/Meta/DiscrTree.lean
+++ b/src/Lean/Meta/DiscrTree.lean
@@ -426,7 +426,7 @@ partial def mkPathAux (root : Bool) (todo : Array Expr) (keys : Array Key) (conf
   if todo.isEmpty then
     return keys
   else
-    let e    := todo.back
+    let e    := todo.back!
     let todo := todo.pop
     let (k, todo) ← pushArgs root todo e config noIndexAtArgs
     mkPathAux false todo (keys.push k) config noIndexAtArgs
@@ -603,7 +603,7 @@ private partial def getMatchLoop (todo : Array Expr) (c : Trie α) (result : Arr
     else if cs.isEmpty then
       return result
     else
-      let e     := todo.back
+      let e     := todo.back!
       let todo  := todo.pop
       let first := cs[0]! /- Recall that `Key.star` is the minimal key -/
       let (k, args) ← getMatchKeyArgs e (root := false) config
@@ -748,7 +748,7 @@ where
       else if cs.isEmpty then
         return result
       else
-        let e     := todo.back
+        let e     := todo.back!
         let todo  := todo.pop
         let (k, args) ← getUnifyKeyArgs e (root := false) config
         let visitStar (result : Array α) : MetaM (Array α) :=
diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index de3bf2daf9..9a6e1b8077 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -430,7 +430,7 @@ where
   hasLetDeclsInBetween : MetaM Bool := do
     let check (lctx : LocalContext) : Bool := Id.run do
       let start := lctx.getFVar! xs[0]! |>.index
-      let stop  := lctx.getFVar! xs.back |>.index
+      let stop  := lctx.getFVar! xs.back! |>.index
       for i in [start+1:stop] do
         match lctx.getAt? i with
         | some localDecl =>
@@ -488,7 +488,7 @@ where
   collectLetDeps : MetaM FVarIdHashSet := do
     let lctx ← getLCtx
     let start := lctx.getFVar! xs[0]! |>.index
-    let stop  := lctx.getFVar! xs.back |>.index
+    let stop  := lctx.getFVar! xs.back! |>.index
     let s := xs.foldl (init := {}) fun s x => s.insert x.fvarId!
     let (_, s) ← collectLetDepsAux stop |>.run start |>.run s
     return s
@@ -500,7 +500,7 @@ where
     let s ← collectLetDeps
     /- Convert `s` into the array `ys` -/
     let start := lctx.getFVar! xs[0]! |>.index
-    let stop  := lctx.getFVar! xs.back |>.index
+    let stop  := lctx.getFVar! xs.back! |>.index
     let mut ys := #[]
     for i in [start:stop+1] do
       match lctx.getAt? i with
@@ -1072,7 +1072,7 @@ private def processAssignmentFOApproxAux (mvar : Expr) (args : Array Expr) (v :
     if args.isEmpty then
       pure false
     else
-      Meta.isExprDefEqAux args.back a <&&> Meta.isExprDefEqAux (mkAppRange mvar 0 (args.size - 1) args) f
+      Meta.isExprDefEqAux args.back! a <&&> Meta.isExprDefEqAux (mkAppRange mvar 0 (args.size - 1) args) f
   | _            => pure false
 
 /--
@@ -1178,7 +1178,7 @@ private partial def processConstApprox (mvar : Expr) (args : Array Expr) (patter
             if argsPrefix.isEmpty then
               defaultCase
             else
-              let some v ← mkLambdaFVarsWithLetDeps #[argsPrefix.back] v | defaultCase
+              let some v ← mkLambdaFVarsWithLetDeps #[argsPrefix.back!] v | defaultCase
               go argsPrefix.pop v
           match (← checkAssignment mvarId argsPrefix v) with
           | none      => cont
diff --git a/src/Lean/Meta/IndPredBelow.lean b/src/Lean/Meta/IndPredBelow.lean
index add31815ce..fc7433ec34 100644
--- a/src/Lean/Meta/IndPredBelow.lean
+++ b/src/Lean/Meta/IndPredBelow.lean
@@ -300,7 +300,7 @@ where
       let m ← introNPRec m
       (← m.getType).withApp fun below args =>
       m.withContext do
-        args.back.withApp fun ctor _ => do
+        args.back!.withApp fun ctor _ => do
         let ctorName := ctor.constName!.updatePrefix below.constName!
         let ctor := mkConst ctorName below.constLevels!
         let ctorInfo ← getConstInfoCtor ctorName
diff --git a/src/Lean/Meta/Injective.lean b/src/Lean/Meta/Injective.lean
index c59206c519..cd1fa2d57b 100644
--- a/src/Lean/Meta/Injective.lean
+++ b/src/Lean/Meta/Injective.lean
@@ -19,7 +19,7 @@ private def mkAnd? (args : Array Expr) : Option Expr := Id.run do
   if args.isEmpty then
     return none
   else
-    let mut result := args.back
+    let mut result := args.back!
     for arg in args.reverse[1:] do
       result := mkApp2 (mkConst ``And) arg result
     return result
@@ -122,7 +122,7 @@ private def solveEqOfCtorEq (ctorName : Name) (mvarId : MVarId) (h : FVarId) : M
 private def mkInjectiveTheoremValue (ctorName : Name) (targetType : Expr) : MetaM Expr :=
   forallTelescopeReducing targetType fun xs type => do
     let mvar ← mkFreshExprSyntheticOpaqueMVar type
-    solveEqOfCtorEq ctorName mvar.mvarId! xs.back.fvarId!
+    solveEqOfCtorEq ctorName mvar.mvarId! xs.back!.fvarId!
     mkLambdaFVars xs mvar
 
 def mkInjectiveTheoremNameFor (ctorName : Name) : Name :=
diff --git a/src/Lean/Meta/LazyDiscrTree.lean b/src/Lean/Meta/LazyDiscrTree.lean
index 6785377d62..29a37cdd82 100644
--- a/src/Lean/Meta/LazyDiscrTree.lean
+++ b/src/Lean/Meta/LazyDiscrTree.lean
@@ -396,7 +396,7 @@ private partial def buildPath (op : Bool → Array Expr → Expr → MetaM (Key
   if todo.isEmpty then
     return keys
   else
-    let e    := todo.back
+    let e    := todo.back!
     let todo := todo.pop
     let (k, todo) ← op root todo e
     buildPath op false todo (keys.push k)
@@ -454,7 +454,7 @@ private def evalLazyEntry (config : WhnfCoreConfig)
     let values := values.push v
     pure (values, starIdx, children)
   else
-    let e    := todo.back
+    let e    := todo.back!
     let todo := todo.pop
     let (k, todo) ← withLCtx lctx.1 lctx.2 $ pushArgs false todo e config
     if k == .star then
@@ -608,7 +608,7 @@ private partial def getMatchLoop (cases : Array PartialMatch) (result : MatchRes
   if cases.isEmpty then
     pure result
   else do
-    let ca := cases.back
+    let ca := cases.back!
     let cases := cases.pop
     let (vs, star, cs) ← evalNode ca.c
     if ca.todo.isEmpty then
@@ -617,7 +617,7 @@ private partial def getMatchLoop (cases : Array PartialMatch) (result : MatchRes
     else if star == 0 && cs.isEmpty then
       getMatchLoop cases result
     else
-      let e     := ca.todo.back
+      let e     := ca.todo.back!
       let todo  := ca.todo.pop
       /- We must always visit `Key.star` edges since they are wildcards.
           Thus, `todo` is not used linearly when there is `Key.star` edge
diff --git a/src/Lean/Meta/Match/MatchEqs.lean b/src/Lean/Meta/Match/MatchEqs.lean
index c4d288fff9..214a436859 100644
--- a/src/Lean/Meta/Match/MatchEqs.lean
+++ b/src/Lean/Meta/Match/MatchEqs.lean
@@ -431,7 +431,7 @@ where
   trimFalseTrail (argMask : Array Bool) : Array Bool :=
     if argMask.isEmpty then
       argMask
-    else if !argMask.back then
+    else if !argMask.back! then
       trimFalseTrail argMask.pop
     else
       argMask
diff --git a/src/Lean/Meta/PProdN.lean b/src/Lean/Meta/PProdN.lean
index 2ee96b944a..985b3d6e90 100644
--- a/src/Lean/Meta/PProdN.lean
+++ b/src/Lean/Meta/PProdN.lean
@@ -71,7 +71,7 @@ def pack (lvl : Level) (xs : Array Expr) : MetaM Expr := do
   if xs.size = 0 then
     if lvl matches .zero then return .const ``True []
                          else return .const ``PUnit [lvl]
-  let xBack := xs.back
+  let xBack := xs.back!
   xs.pop.foldrM mkPProd xBack
 
 /-- Given values `xᵢ` of type `tᵢ`, produces value of type `t₁ ×' t₂ ×' t₃` -/
@@ -79,7 +79,7 @@ def mk (lvl : Level) (xs : Array Expr) : MetaM Expr := do
   if xs.size = 0 then
     if lvl matches .zero then return .const ``True.intro []
                          else return .const ``PUnit.unit [lvl]
-  let xBack := xs.back
+  let xBack := xs.back!
   xs.pop.foldrM mkPProdMk xBack
 
 /-- Given a value of type `t₁ ×' … ×' tᵢ ×' … ×' tₙ`, return a value of type `tᵢ` -/
diff --git a/src/Lean/Meta/RecursorInfo.lean b/src/Lean/Meta/RecursorInfo.lean
index 1a8c76855a..14713d9663 100644
--- a/src/Lean/Meta/RecursorInfo.lean
+++ b/src/Lean/Meta/RecursorInfo.lean
@@ -107,7 +107,7 @@ private def getMajorPosDepElim (declName : Name) (majorPos? : Option Nat) (xs :
   | none => do
     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
+    let major := motiveArgs.back!
     match xs.getIdx? major with
     | some majorPos => pure (major, majorPos, true)
     | none          => throwError "ill-formed recursor '{declName}'"
diff --git a/src/Lean/Meta/SizeOf.lean b/src/Lean/Meta/SizeOf.lean
index 8b10e83220..367d5a549c 100644
--- a/src/Lean/Meta/SizeOf.lean
+++ b/src/Lean/Meta/SizeOf.lean
@@ -298,7 +298,7 @@ mutual
         for motiveFVar in motiveFVars do
           let motive ← forallTelescopeReducing (← inferType motiveFVar) fun ys _ => do
             let lhs ← mkSizeOf ys
-            let rhs ← mkAppM ``SizeOf.sizeOf #[ys.back]
+            let rhs ← mkAppM ``SizeOf.sizeOf #[ys.back!]
             mkLambdaFVars ys (← mkEq lhs rhs)
           r := mkApp r motive
         forallBoundedTelescope (← inferType r) recInfo.numMinors fun minorFVars _ => do
diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean
index 4a8ae7e697..2e16dbd2c2 100644
--- a/src/Lean/Meta/SynthInstance.lean
+++ b/src/Lean/Meta/SynthInstance.lean
@@ -534,7 +534,7 @@ def consume (cNode : ConsumerNode) : SynthM Unit := do
          tableEntries := s.tableEntries.insert key { entry with waiters := entry.waiters.push waiter } }
 
 def getTop : SynthM GeneratorNode :=
-  return (← get).generatorStack.back
+  return (← get).generatorStack.back!
 
 @[inline] def modifyTop (f : GeneratorNode → GeneratorNode) : SynthM Unit :=
   modify fun s => { s with generatorStack := s.generatorStack.modify (s.generatorStack.size - 1) f }
@@ -578,7 +578,7 @@ def generate : SynthM Unit := do
       return none
 
 def getNextToResume : SynthM (ConsumerNode × Answer) := do
-  let r := (← get).resumeStack.back
+  let r := (← get).resumeStack.back!
   modify fun s => { s with resumeStack := s.resumeStack.pop }
   return r
 
diff --git a/src/Lean/Meta/Tactic/FunInd.lean b/src/Lean/Meta/Tactic/FunInd.lean
index 19c167ec70..73e794381c 100644
--- a/src/Lean/Meta/Tactic/FunInd.lean
+++ b/src/Lean/Meta/Tactic/FunInd.lean
@@ -495,7 +495,7 @@ def mkLambdaFVarsMasked (xs : Array Expr) (e : Expr) : MetaM (Array Bool × Expr
   let mut xs := xs
   let mut mask := #[]
   while ! xs.isEmpty do
-    let discr := xs.back
+    let discr := xs.back!
     if discr.isFVar && e.containsFVar discr.fvarId! then
         e ← mkLambdaFVars #[discr] e
         mask := mask.push true
@@ -680,7 +680,7 @@ def deriveUnaryInduction (name : Name) : MetaM Name := do
   let e' ← lambdaTelescope e fun params funBody => MatcherApp.withUserNames params varNames do
     match_expr funBody with
     | fix@WellFounded.fix α _motive rel wf body target =>
-      unless params.back == target do
+      unless params.back! == target do
         throwError "functional induction: expected the target as last parameter{indentExpr e}"
       let fixedParams := params.pop
       let motiveType ← mkForallFVars #[target] (.sort levelZero)
@@ -806,7 +806,7 @@ def cleanPackedArgs (eqnInfo : WF.EqnInfo) (value : Expr) : MetaM Expr := do
     if e.isAppOf eqnInfo.declNameNonRec then
       let args := e.getAppArgs
       if eqnInfo.fixedPrefixSize + 1 ≤ args.size then
-        let packedArg := args.back
+        let packedArg := args.back!
           let (i, unpackedArgs) ← eqnInfo.argsPacker.unpack packedArg
           let e' := .const eqnInfo.declNames[i]! e.getAppFn.constLevels!
           let e' := mkAppN e' args.pop
@@ -836,7 +836,7 @@ def unpackMutualInduction (eqnInfo : WF.EqnInfo) (unaryInductName : Name) : Meta
     unless motive.isFVar && targets.size = 1 && targets.all (·.isFVar) do
       throwError "conclusion {concl} does not look like a packed motive application"
     let packedTarget := targets[0]!
-    unless xs.back == packedTarget do
+    unless xs.back! == packedTarget do
       throwError "packed target not last argument to {unaryInductName}"
     let some motivePos := xs.findIdx? (· == motive)
       | throwError "could not find motive {motive} in {xs}"
@@ -1054,7 +1054,7 @@ def deriveInductionStructural (names : Array Name) (numFixed : Nat) : MetaM Unit
                 pure e
               brecOnApps := brecOnApps.push e
             mkLetFVars minors' (← PProdN.mk 0 brecOnApps)
-          let e' ← abstractIndependentMVars mvars (← motives.back.fvarId!.getDecl).index e'
+          let e' ← abstractIndependentMVars mvars (← motives.back!.fvarId!.getDecl).index e'
           let e' ← mkLambdaFVars motives e'
 
           -- We could pass (usedOnly := true) below, and get nicer induction principles that
diff --git a/src/Lean/Meta/Tactic/LinearArith/Solver.lean b/src/Lean/Meta/Tactic/LinearArith/Solver.lean
index 9d00100491..cf367e49a4 100644
--- a/src/Lean/Meta/Tactic/LinearArith/Solver.lean
+++ b/src/Lean/Meta/Tactic/LinearArith/Solver.lean
@@ -47,10 +47,10 @@ abbrev Poly.size (e : Poly) : Nat :=
   e.val.size
 
 abbrev Poly.getMaxVarCoeff (e : Poly) : Int :=
-  e.val.back.1
+  e.val.back!.1
 
 abbrev Poly.getMaxVar (e : Poly) : Var :=
-  e.val.back.2
+  e.val.back!.2
 
 abbrev Poly.get (e : Poly) (i : Fin e.size) : Int × Var :=
   e.val.get i
@@ -152,7 +152,7 @@ def Cnstr.getBound (c : Cnstr) (a : Assignment) : Rat := Id.run do
       r := r - c*v
     else
       unreachable!
-  let k := c.lhs.val.back.1
+  let k := c.lhs.val.back!.1
   return r / k
 
 def Cnstr.isUnsat (c : Cnstr) (a : Assignment) : Bool :=
diff --git a/src/Lean/Meta/Tactic/Symm.lean b/src/Lean/Meta/Tactic/Symm.lean
index 449b1de39b..3d9072a698 100644
--- a/src/Lean/Meta/Tactic/Symm.lean
+++ b/src/Lean/Meta/Tactic/Symm.lean
@@ -65,7 +65,7 @@ def applySymm (e : Expr) : MetaM Expr := do
         restoreState s
         let lem ← mkConstWithFreshMVarLevels lem
         let (args, _, body) ← withReducible <| forallMetaTelescopeReducing (← inferType lem)
-        let .true ← isDefEq args.back e | failure
+        let .true ← isDefEq args.back! e | failure
         mkExpectedTypeHint (mkAppN lem args) (← instantiateMVars body)
   lems.toList.firstM act
     <|> throwError m!"no applicable symmetry lemma found for {indentExpr tgt}"
@@ -87,7 +87,7 @@ def applySymm (g : MVarId) : MetaM MVarId := do
         let (args, _, body) ← withReducible <| forallMetaTelescopeReducing (← inferType lem)
         let .true ← isDefEq (← g.getType) body | failure
         g.assign (mkAppN lem args)
-        let g' := args.back.mvarId!
+        let g' := args.back!.mvarId!
         g'.setTag (← g.getTag)
         pure g'
   lems.toList.firstM act
diff --git a/src/Lean/Parser/Types.lean b/src/Lean/Parser/Types.lean
index 9f6d8b3606..0598865677 100644
--- a/src/Lean/Parser/Types.lean
+++ b/src/Lean/Parser/Types.lean
@@ -173,7 +173,7 @@ def pop (stack : SyntaxStack) : SyntaxStack :=
 
 def back (stack : SyntaxStack) : Syntax :=
   if stack.size > 0 then
-    stack.raw.back
+    stack.raw.back!
   else
     panic! "SyntaxStack.back: element is inaccessible"
 
diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index 138bde803b..ccad1cea6c 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -868,7 +868,7 @@ def delabLam : Delab :=
               pure $ curNames.get! 0;
           `(funBinder| ($stxCurNames : $stxT))
         else
-          pure curNames.back  -- here `curNames.size == 1`
+          pure curNames.back!  -- here `curNames.size == 1`
       let group ← match e.binderInfo, ppTypes with
         | BinderInfo.default,        _      => defaultCase ()
         | BinderInfo.implicit,       true   => `(funBinder| {$curNames* : $stxT})
@@ -876,7 +876,7 @@ def delabLam : Delab :=
         | BinderInfo.strictImplicit, true   => `(funBinder| ⦃$curNames* : $stxT⦄)
         | BinderInfo.strictImplicit, false  => `(funBinder| ⦃$curNames*⦄)
         | BinderInfo.instImplicit,   _     =>
-          if usedDownstream then `(funBinder| [$curNames.back : $stxT])  -- here `curNames.size == 1`
+          if usedDownstream then `(funBinder| [$curNames.back! : $stxT])  -- here `curNames.size == 1`
           else  `(funBinder| [$stxT])
       let (binders, stxBody) :=
         match stxBody with
@@ -924,7 +924,7 @@ def delabForall : Delab := do
     | BinderInfo.implicit       => `(bracketedBinderF|{$curNames* : $stxT})
     | BinderInfo.strictImplicit => `(bracketedBinderF|⦃$curNames* : $stxT⦄)
     -- here `curNames.size == 1`
-    | BinderInfo.instImplicit   => `(bracketedBinderF|[$curNames.back : $stxT])
+    | BinderInfo.instImplicit   => `(bracketedBinderF|[$curNames.back! : $stxT])
     | _                         =>
       -- NOTE: non-dependent arrows are available only for the default binder info
       if dependent then
diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index 23f7ec3042..805bfd03a7 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -288,7 +288,7 @@ def categoryFormatter (cat : Name) : Formatter :=
 @[combinator_formatter parserOfStack]
 def parserOfStack.formatter (offset : Nat) (_prec : Nat := 0) : Formatter := do
   let st ← get
-  let stx := st.stxTrav.parents.back.getArg (st.stxTrav.idxs.back - offset)
+  let stx := st.stxTrav.parents.back!.getArg (st.stxTrav.idxs.back! - offset)
   formatterForKind stx.getKind
 
 @[combinator_formatter error]
diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean
index bb01b19be3..ab41996d70 100644
--- a/src/Lean/PrettyPrinter/Parenthesizer.lean
+++ b/src/Lean/PrettyPrinter/Parenthesizer.lean
@@ -342,7 +342,7 @@ def categoryParser.parenthesizer (cat : Name) (prec : Nat) : Parenthesizer := do
 @[combinator_parenthesizer parserOfStack]
 def parserOfStack.parenthesizer (offset : Nat) (_prec : Nat := 0) : Parenthesizer := do
   let st ← get
-  let stx := st.stxTrav.parents.back.getArg (st.stxTrav.idxs.back - offset)
+  let stx := st.stxTrav.parents.back!.getArg (st.stxTrav.idxs.back! - offset)
   parenthesizerForKind stx.getKind
 
 @[builtin_category_parenthesizer term]
diff --git a/src/Lean/Syntax.lean b/src/Lean/Syntax.lean
index 44cf9805b4..1790229e20 100644
--- a/src/Lean/Syntax.lean
+++ b/src/Lean/Syntax.lean
@@ -402,7 +402,7 @@ def down (t : Traverser) (idx : Nat) : Traverser :=
 /-- Advance to the parent of the current node, if any. -/
 def up (t : Traverser) : Traverser :=
   if t.parents.size > 0 then
-    let cur := if t.idxs.back < t.parents.back.getNumArgs then t.parents.back.setArg t.idxs.back t.cur else t.parents.back
+    let cur := if t.idxs.back! < t.parents.back!.getNumArgs then t.parents.back!.setArg t.idxs.back! t.cur else t.parents.back!
     { cur := cur, parents := t.parents.pop, idxs := t.idxs.pop }
   else
     t
@@ -410,14 +410,14 @@ def up (t : Traverser) : Traverser :=
 /-- Advance to the left sibling of the current node, if any. -/
 def left (t : Traverser) : Traverser :=
   if t.parents.size > 0 then
-    t.up.down (t.idxs.back - 1)
+    t.up.down (t.idxs.back! - 1)
   else
     t
 
 /-- Advance to the right sibling of the current node, if any. -/
 def right (t : Traverser) : Traverser :=
   if t.parents.size > 0 then
-    t.up.down (t.idxs.back + 1)
+    t.up.down (t.idxs.back! + 1)
   else
     t
 
diff --git a/src/Lean/Widget/TaggedText.lean b/src/Lean/Widget/TaggedText.lean
index c8c063a2bf..6ee95a3604 100644
--- a/src/Lean/Widget/TaggedText.lean
+++ b/src/Lean/Widget/TaggedText.lean
@@ -28,7 +28,7 @@ namespace TaggedText
 
 def appendText (s₀ : String) : TaggedText α → TaggedText α
   | text s    => text (s ++ s₀)
-  | append as => match as.back with
+  | append as => match as.back! with
     | text s => append <| as.set! (as.size - 1) <| text (s ++ s₀)
     | _      => append <| as.push (text s₀)
   | a         => append #[a, text s₀]
@@ -95,7 +95,7 @@ partial def stripTags (tt : TaggedText α) : String :=
   go "" #[tt]
 where go (acc : String) : Array (TaggedText α) → String
   | #[] => acc
-  | ts  => match ts.back with
+  | ts  => match ts.back! with
     | text s    => go (acc ++ s) ts.pop
     | append as => go acc (ts.pop ++ as.reverse)
     | tag _ a   => go acc (ts.set! (ts.size - 1) a)
diff --git a/src/lake/Lake/Toml/Elab/Expression.lean b/src/lake/Lake/Toml/Elab/Expression.lean
index f44c516de0..081a0b6684 100644
--- a/src/lake/Lake/Toml/Elab/Expression.lean
+++ b/src/lake/Lake/Toml/Elab/Expression.lean
@@ -75,7 +75,7 @@ def elabKeyval (kv : TSyntax ``keyval) : TomlElabM Unit := do
     | throwErrorAt kv "ill-formed key-value pair syntax"
   let `(key|$[$ks:simpleKey].*) := kStx
     | throwErrorAt kStx "ill-formed key syntax"
-  let tailKeyStx := ks.back
+  let tailKeyStx := ks.back!
   let k ← elabSubKeys ks.pop
   let k := k.str <| ← elabSimpleKey tailKeyStx
   if let some ty := (← get).keyTys.find? k then
@@ -116,7 +116,7 @@ def elabStdTable (x : TSyntax ``stdTable) : TomlElabM Unit := withRef x do
     | throwErrorAt x "ill-formed table syntax"
   let `(key|$[$ks:simpleKey].*) := kStx
     | throwErrorAt kStx "ill-formed key syntax"
-  let tailKey := ks.back
+  let tailKey := ks.back!
   let k ← elabHeaderKeys ks.pop
   let k ← k.str <$> elabSimpleKey tailKey
   if let some ty := (← get).keyTys.find? k then
@@ -134,7 +134,7 @@ def elabArrayTable (x : TSyntax ``arrayTable) : TomlElabM Unit := withRef x do
     | throwErrorAt x "ill-formed array table syntax"
   let `(key|$[$ks:simpleKey].*) := k
     | throwErrorAt x "ill-formed key syntax"
-  let tailKey := ks.back
+  let tailKey := ks.back!
   let k ← elabHeaderKeys ks.pop
   let k := k.str (← elabSimpleKey tailKey)
   if let some ty := (← get).keyTys.find? k then
diff --git a/src/lake/Lake/Toml/Elab/Value.lean b/src/lake/Lake/Toml/Elab/Value.lean
index 8288533880..7ba4a9085f 100644
--- a/src/lake/Lake/Toml/Elab/Value.lean
+++ b/src/lake/Lake/Toml/Elab/Value.lean
@@ -213,7 +213,7 @@ def elabInlineTable (x : TSyntax ``inlineTable) (elabVal : TSyntax ``val → Cor
       | throwErrorAt kv "ill-formed key-value pair syntax"
     let `(key|$[$ks].*) := k
       | throwErrorAt k "ill-formed key syntax"
-    let tailKey := ks.back
+    let tailKey := ks.back!
     let (k, t) ← StateT.run (s := t) <| ks.pop.foldlM (init := Name.anonymous) fun k p => do
       let k ← k.str <$> elabSimpleKey p
       if let some v := t.find? k then