diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean
index 4b25a919e8c8..4f520ed30dae 100644
--- a/src/Init/Meta.lean
+++ b/src/Init/Meta.lean
@@ -431,21 +431,20 @@ def getSubstring? (stx : Syntax) (withLeading := true) (withTrailing := true) :
     }
   | _, _ => none
 
-@[specialize] private partial def updateLast {α} [Inhabited α] (a : Array α) (f : α → Option α) (i : Nat) : Option (Array α) :=
-  if i == 0 then
-    none
-  else
-    let i := i - 1
-    let v := a[i]!
+@[specialize] private partial def updateLast {α} (a : Array α) (f : α → Option α) (i : Fin (a.size + 1)) : Option (Array α) :=
+  match i with
+  | 0 => none
+  | ⟨i + 1, h⟩ =>
+    let v := a[i]'(Nat.succ_lt_succ_iff.mp h)
     match f v with
-    | some v => some <| a.set! i v
-    | none   => updateLast a f i
+    | some v => some <| a.set i v (Nat.succ_lt_succ_iff.mp h)
+    | none   => updateLast a f ⟨i, Nat.lt_of_succ_lt h⟩
 
 partial def setTailInfoAux (info : SourceInfo) : Syntax → Option Syntax
   | atom _ val             => some <| atom info val
   | ident _ rawVal val pre => some <| ident info rawVal val pre
   | node info' k args      =>
-    match updateLast args (setTailInfoAux info) args.size with
+    match updateLast args (setTailInfoAux info) ⟨args.size, by simp⟩ with
     | some args => some <| node info' k args
     | none      => none
   | _                      => none
diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean
index f8f0b7f0e4cd..5a8db9fb426e 100644
--- a/src/Init/NotationExtra.lean
+++ b/src/Init/NotationExtra.lean
@@ -22,28 +22,28 @@ syntax explicitBinders            := (ppSpace bracketedExplicitBinders)+ <|> unb
 
 open TSyntax.Compat in
 def expandExplicitBindersAux (combinator : Syntax) (idents : Array Syntax) (type? : Option Syntax) (body : Syntax) : MacroM Syntax :=
-  let rec loop (i : Nat) (acc : Syntax) := do
+  let rec loop (i : Nat) (h : i ≤ idents.size) (acc : Syntax) := do
     match i with
     | 0   => pure acc
-    | i+1 =>
-      let ident := idents[i]![0]
+    | i + 1 =>
+      let ident := idents[i][0]
       let acc ← match ident.isIdent, type? with
         | true,  none      => `($combinator fun $ident => $acc)
         | true,  some type => `($combinator fun $ident : $type => $acc)
         | false, none      => `($combinator fun _ => $acc)
         | false, some type => `($combinator fun _ : $type => $acc)
-      loop i acc
-  loop idents.size body
+      loop i (Nat.le_of_succ_le h) acc
+  loop idents.size (by simp) body
 
 def expandBrackedBindersAux (combinator : Syntax) (binders : Array Syntax) (body : Syntax) : MacroM Syntax :=
-  let rec loop (i : Nat) (acc : Syntax) := do
+  let rec loop (i : Nat) (h : i ≤ binders.size) (acc : Syntax) := do
     match i with
     | 0   => pure acc
     | i+1 =>
-      let idents := binders[i]![1].getArgs
-      let type   := binders[i]![3]
-      loop i (← expandExplicitBindersAux combinator idents (some type) acc)
-  loop binders.size body
+      let idents := binders[i][1].getArgs
+      let type   := binders[i][3]
+      loop i (Nat.le_of_succ_le h) (← expandExplicitBindersAux combinator idents (some type) acc)
+  loop binders.size (by simp) body
 
 def expandExplicitBinders (combinatorDeclName : Name) (explicitBinders : Syntax) (body : Syntax) : MacroM Syntax := do
   let combinator := mkCIdentFrom (← getRef) combinatorDeclName
diff --git a/src/Init/System/Uri.lean b/src/Init/System/Uri.lean
index 5e7cf47c3f52..03611839095d 100644
--- a/src/Init/System/Uri.lean
+++ b/src/Init/System/Uri.lean
@@ -29,13 +29,13 @@ def decodeUri (uri : String) : String := Id.run do
   let len := rawBytes.size
   let mut i := 0
   let percent := '%'.toNat.toUInt8
-  while i < len do
-    let c := rawBytes[i]!
-    (decoded, i) := if c == percent && i + 1 < len then
-      let h1 := rawBytes[i + 1]!
+  while h : i < len do
+    let c := rawBytes[i]
+    (decoded, i) := if h₁ : c == percent ∧ i + 1 < len then
+      let h1 := rawBytes[i + 1]
       if let some hd1 := hexDigitToUInt8? h1 then
-        if i + 2 < len then
-          let h2 := rawBytes[i + 2]!
+        if h₂ : i + 2 < len then
+          let h2 := rawBytes[i + 2]
           if let some hd2 := hexDigitToUInt8? h2 then
             -- decode the hex digits into a byte.
             (decoded.push (hd1 * 16 + hd2), i + 3)
diff --git a/src/Lean/Compiler/IR/EmitC.lean b/src/Lean/Compiler/IR/EmitC.lean
index 0300971705a9..505fd7533510 100644
--- a/src/Lean/Compiler/IR/EmitC.lean
+++ b/src/Lean/Compiler/IR/EmitC.lean
@@ -271,9 +271,9 @@ def emitTag (x : VarId) (xType : IRType) : M Unit := do
     emit x
 
 def isIf (alts : Array Alt) : Option (Nat × FnBody × FnBody) :=
-  if alts.size != 2 then none
-  else match alts[0]! with
-    | Alt.ctor c b => some (c.cidx, b, alts[1]!.body)
+  if h : alts.size ≠ 2 then none
+  else match alts[0] with
+    | Alt.ctor c b => some (c.cidx, b, alts[1].body)
     | _            => none
 
 def emitInc (x : VarId) (n : Nat) (checkRef : Bool) : M Unit := do
diff --git a/src/Lean/Compiler/IR/EmitLLVM.lean b/src/Lean/Compiler/IR/EmitLLVM.lean
index 9bb129f0558c..fd2b19d26ebf 100644
--- a/src/Lean/Compiler/IR/EmitLLVM.lean
+++ b/src/Lean/Compiler/IR/EmitLLVM.lean
@@ -1172,8 +1172,8 @@ def emitFnArgs (builder : LLVM.Builder llvmctx)
     (needsPackedArgs? : Bool)  (llvmfn : LLVM.Value llvmctx) (params : Array Param) : M llvmctx Unit := do
   if needsPackedArgs? then do
       let argsp ← LLVM.getParam llvmfn 0 -- lean_object **args
-      for i in List.range params.size do
-          let param := params[i]!
+      for h : i in [:params.size] do
+          let param := params[i]
           -- argsi := (args + i)
           let argsi ← LLVM.buildGEP2 builder (← LLVM.voidPtrType llvmctx) argsp #[← constIntUnsigned i] s!"packed_arg_{i}_slot"
           let llvmty ← toLLVMType param.ty
@@ -1182,15 +1182,16 @@ def emitFnArgs (builder : LLVM.Builder llvmctx)
           -- slot for arg[i] which is always void* ?
           let alloca ← buildPrologueAlloca builder llvmty s!"arg_{i}"
           LLVM.buildStore builder pv alloca
-          addVartoState params[i]!.x alloca llvmty
+          addVartoState param.x alloca llvmty
   else
       let n ← LLVM.countParams llvmfn
-      for i in (List.range n.toNat) do
-        let llvmty ← toLLVMType params[i]!.ty
+      for i in [:n.toNat] do
+        let param := params[i]!
+        let llvmty ← toLLVMType param.ty
         let alloca ← buildPrologueAlloca builder  llvmty s!"arg_{i}"
         let arg ← LLVM.getParam llvmfn (UInt64.ofNat i)
         let _ ← LLVM.buildStore builder arg alloca
-        addVartoState params[i]!.x alloca llvmty
+        addVartoState param.x alloca llvmty
 
 def emitDeclAux (mod : LLVM.Module llvmctx) (builder : LLVM.Builder llvmctx) (d : Decl) : M llvmctx Unit := do
   let env ← getEnv
diff --git a/src/Lean/Compiler/IR/ExpandResetReuse.lean b/src/Lean/Compiler/IR/ExpandResetReuse.lean
index e2a1a8b38b6d..8afaf13c53b1 100644
--- a/src/Lean/Compiler/IR/ExpandResetReuse.lean
+++ b/src/Lean/Compiler/IR/ExpandResetReuse.lean
@@ -54,7 +54,7 @@ abbrev Mask := Array (Option VarId)
 partial def eraseProjIncForAux (y : VarId) (bs : Array FnBody) (mask : Mask) (keep : Array FnBody) : Array FnBody × Mask :=
   let done (_ : Unit)        := (bs ++ keep.reverse, mask)
   let keepInstr (b : FnBody) := eraseProjIncForAux y bs.pop mask (keep.push b)
-  if bs.size < 2 then done ()
+  if h : bs.size < 2 then done ()
   else
     let b := bs.back!
     match b with
@@ -62,7 +62,7 @@ partial def eraseProjIncForAux (y : VarId) (bs : Array FnBody) (mask : Mask) (ke
     | .vdecl _ _ (.uproj _ _) _   => keepInstr b
     | .inc z n c p _ =>
       if n == 0 then done () else
-      let b' := bs[bs.size - 2]!
+      let b' := bs[bs.size - 2]
       match b' with
       | .vdecl w _ (.proj i x) _ =>
         if w == z && y == x then
diff --git a/src/Lean/Compiler/LCNF/SpecInfo.lean b/src/Lean/Compiler/LCNF/SpecInfo.lean
index ed8594f16ed8..0e7f2cefa77d 100644
--- a/src/Lean/Compiler/LCNF/SpecInfo.lean
+++ b/src/Lean/Compiler/LCNF/SpecInfo.lean
@@ -152,8 +152,8 @@ def saveSpecParamInfo (decls : Array Decl) : CompilerM Unit := do
       let specArgs? := getSpecializationArgs? (← getEnv) decl.name
       let contains (i : Nat) : Bool := specArgs?.getD #[] |>.contains i
       let mut paramsInfo : Array SpecParamInfo := #[]
-      for i in [:decl.params.size] do
-        let param := decl.params[i]!
+      for h :i in [:decl.params.size] do
+        let param := decl.params[i]
         let info ←
           if contains i then
             pure .user
@@ -181,14 +181,14 @@ def saveSpecParamInfo (decls : Array Decl) : CompilerM Unit := do
       declsInfo := declsInfo.push paramsInfo
   if declsInfo.any fun paramsInfo => paramsInfo.any (· matches .user | .fixedInst | .fixedHO) then
     let m := mkFixedParamsMap decls
-    for i in [:decls.size] do
-      let decl := decls[i]!
+    for hi : i in [:decls.size] do
+      let decl := decls[i]
       let mut paramsInfo := declsInfo[i]!
       let some mask := m.find? decl.name | unreachable!
       trace[Compiler.specialize.info] "{decl.name} {mask}"
       paramsInfo := paramsInfo.zipWith mask fun info fixed => if fixed || info matches .user then info else .other
       for j in [:paramsInfo.size] do
-        let mut info  := paramsInfo[j]!
+        let mut info := paramsInfo[j]!
         if info matches .fixedNeutral && !hasFwdDeps decl paramsInfo j then
           paramsInfo := paramsInfo.set! j .other
       if paramsInfo.any fun info => info matches .fixedInst | .fixedHO | .user then
diff --git a/src/Lean/Compiler/LCNF/ToLCNF.lean b/src/Lean/Compiler/LCNF/ToLCNF.lean
index aa5d65d2fab6..fc5408c3a1f4 100644
--- a/src/Lean/Compiler/LCNF/ToLCNF.lean
+++ b/src/Lean/Compiler/LCNF/ToLCNF.lean
@@ -499,8 +499,8 @@ where
       match app with
       | .fvar f =>
         let mut argsNew := #[]
-        for i in [arity : args.size] do
-          argsNew := argsNew.push (← visitAppArg args[i]!)
+        for h :i in [arity : args.size] do
+          argsNew := argsNew.push (← visitAppArg args[i])
         letValueToArg <| .fvar f argsNew
       | .erased | .type .. => return .erased
 
diff --git a/src/Lean/Compiler/Specialize.lean b/src/Lean/Compiler/Specialize.lean
index e59a3229d00b..ad3747e0904d 100644
--- a/src/Lean/Compiler/Specialize.lean
+++ b/src/Lean/Compiler/Specialize.lean
@@ -26,10 +26,11 @@ private def elabSpecArgs (declName : Name) (args : Array Syntax) : MetaM (Array
       if let some idx := arg.isNatLit? then
         if idx == 0 then throwErrorAt arg "invalid specialization argument index, index must be greater than 0"
         let idx := idx - 1
-        if idx >= argNames.size then
+        if h : idx >= argNames.size then
           throwErrorAt arg "invalid argument index, `{declName}` has #{argNames.size} arguments"
-        if result.contains idx then throwErrorAt arg "invalid specialization argument index, `{argNames[idx]!}` has already been specified as a specialization candidate"
-        result := result.push idx
+        else
+          if result.contains idx then throwErrorAt arg "invalid specialization argument index, `{argNames[idx]}` has already been specified as a specialization candidate"
+          result := result.push idx
       else
         let argName := arg.getId
         if let some idx := argNames.indexOf? argName then
diff --git a/src/Lean/Elab/Deriving/Util.lean b/src/Lean/Elab/Deriving/Util.lean
index 03f7eecae200..29f925ee1478 100644
--- a/src/Lean/Elab/Deriving/Util.lean
+++ b/src/Lean/Elab/Deriving/Util.lean
@@ -49,9 +49,9 @@ invoking ``mkInstImplicitBinders `BarClass foo #[`α, `n, `β]`` gives `` `([Bar
 def mkInstImplicitBinders (className : Name) (indVal : InductiveVal) (argNames : Array Name) : TermElabM (Array Syntax) :=
   forallBoundedTelescope indVal.type indVal.numParams fun xs _ => do
     let mut binders := #[]
-    for i in [:xs.size] do
+    for h : i in [:xs.size] do
       try
-        let x := xs[i]!
+        let x := xs[i]
         let c ← mkAppM className #[x]
         if (← isTypeCorrect c) then
           let argName := argNames[i]!
@@ -86,8 +86,8 @@ def mkContext (fnPrefix : String) (typeName : Name) : TermElabM Context := do
 
 def mkLocalInstanceLetDecls (ctx : Context) (className : Name) (argNames : Array Name) : TermElabM (Array (TSyntax ``Parser.Term.letDecl)) := do
   let mut letDecls := #[]
-  for i in [:ctx.typeInfos.size] do
-    let indVal       := ctx.typeInfos[i]!
+  for h : i in [:ctx.typeInfos.size] do
+    let indVal       := ctx.typeInfos[i]
     let auxFunName   := ctx.auxFunNames[i]!
     let currArgNames ← mkInductArgNames indVal
     let numParams    := indVal.numParams
diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean
index 5ba538704221..57ba1d890ceb 100644
--- a/src/Lean/Elab/Do.lean
+++ b/src/Lean/Elab/Do.lean
@@ -796,10 +796,10 @@ Note that we are not restricting the macro power since the
 actions to be in the same universe.
 -/
 private def mkTuple (elems : Array Syntax) : MacroM Syntax := do
-  if elems.size == 0 then
+  if elems.size = 0 then
     mkUnit
-  else if elems.size == 1 then
-    return elems[0]!
+  else if h : elems.size = 1 then
+    return elems[0]
   else
     elems.extract 0 (elems.size - 1) |>.foldrM (init := elems.back!) fun elem tuple =>
       ``(MProd.mk $elem $tuple)
@@ -831,10 +831,10 @@ def isDoExpr? (doElem : Syntax) : Option Syntax :=
   We use this method when expanding the `for-in` notation.
 -/
 private def destructTuple (uvars : Array Var) (x : Syntax) (body : Syntax) : MacroM Syntax := do
-  if uvars.size == 0 then
+  if uvars.size = 0 then
     return body
-  else if uvars.size == 1 then
-    `(let $(uvars[0]!):ident := $x; $body)
+  else if h : uvars.size = 1 then
+    `(let $(uvars[0]):ident := $x; $body)
   else
     destruct uvars.toList x body
 where
@@ -1314,9 +1314,9 @@ private partial def expandLiftMethodAux (inQuot : Bool) (inBinder : Bool) : Synt
     else if liftMethodDelimiter k then
       return stx
     -- For `pure` if-then-else, we only lift `(<- ...)` occurring in the condition.
-    else if args.size >= 2 && (k == ``termDepIfThenElse || k == ``termIfThenElse) then do
+    else if h : args.size >= 2 ∧ (k == ``termDepIfThenElse || k == ``termIfThenElse) then do
       let inAntiquot := stx.isAntiquot && !stx.isEscapedAntiquot
-      let arg1 ← expandLiftMethodAux (inQuot && !inAntiquot || stx.isQuot) inBinder args[1]!
+      let arg1 ← expandLiftMethodAux (inQuot && !inAntiquot || stx.isQuot) inBinder args[1]
       let args := args.set! 1 arg1
       return Syntax.node i k args
     else if k == ``Parser.Term.liftMethod && !inQuot then withFreshMacroScope do
diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean
index 6ce61d1b1063..813fbafd952b 100644
--- a/src/Lean/Elab/Inductive.lean
+++ b/src/Lean/Elab/Inductive.lean
@@ -173,15 +173,15 @@ private def checkUnsafe (rs : Array ElabHeaderResult) : TermElabM Unit := do
       throwErrorAt r.view.ref "invalid inductive type, cannot mix unsafe and safe declarations in a mutually inductive datatypes"
 
 private def InductiveView.checkLevelNames (views : Array InductiveView) : TermElabM Unit := do
-  if views.size > 1 then
-    let levelNames := views[0]!.levelNames
+  if h : views.size > 1 then
+    let levelNames := views[0].levelNames
     for view in views do
       unless view.levelNames == levelNames do
         throwErrorAt view.ref "invalid inductive type, universe parameters mismatch in mutually inductive datatypes"
 
 private def ElabHeaderResult.checkLevelNames (rs : Array ElabHeaderResult) : TermElabM Unit := do
-  if rs.size > 1 then
-    let levelNames := rs[0]!.levelNames
+  if h : rs.size > 1 then
+    let levelNames := rs[0].levelNames
     for r in rs do
       unless r.levelNames == levelNames do
         throwErrorAt r.view.ref "invalid inductive type, universe parameters mismatch in mutually inductive datatypes"
@@ -433,8 +433,8 @@ where
         let mut args := e.getAppArgs
         unless args.size ≥ params.size do
           throwError "unexpected inductive type occurrence{indentExpr e}"
-        for i in [:params.size] do
-          let param := params[i]!
+        for h : i in [:params.size] do
+          let param := params[i]
           let arg := args[i]!
           unless (← isDefEq param arg) do
             throwError "inductive datatype parameter mismatch{indentExpr arg}\nexpected{indentExpr param}"
@@ -694,8 +694,8 @@ private def collectLevelParamsInInductive (indTypes : List InductiveType) : Arra
 private def mkIndFVar2Const (views : Array InductiveView) (indFVars : Array Expr) (levelNames : List Name) : ExprMap Expr := Id.run do
   let levelParams := levelNames.map mkLevelParam;
   let mut m : ExprMap Expr := {}
-  for i in [:views.size] do
-    let view    := views[i]!
+  for h : i in [:views.size] do
+    let view    := views[i]
     let indFVar := indFVars[i]!
     m := m.insert indFVar (mkConst view.declName levelParams)
   return m
@@ -856,9 +856,9 @@ private def mkInductiveDecl (vars : Array Expr) (views : Array InductiveView) :
     withInductiveLocalDecls rs fun params indFVars => do
       trace[Elab.inductive] "indFVars: {indFVars}"
       let mut indTypesArray := #[]
-      for i in [:views.size] do
+      for h : i in [:views.size] do
         let indFVar := indFVars[i]!
-        Term.addLocalVarInfo views[i]!.declId indFVar
+        Term.addLocalVarInfo views[i].declId indFVar
         let r     := rs[i]!
         /- At this point, because of `withInductiveLocalDecls`, the only fvars that are in context are the ones related to the first inductive type.
            Because of this, we need to replace the fvars present in each inductive type's header of the mutual block with those of the first inductive.
diff --git a/src/Lean/Elab/LetRec.lean b/src/Lean/Elab/LetRec.lean
index 22663d005548..45b257462956 100644
--- a/src/Lean/Elab/LetRec.lean
+++ b/src/Lean/Elab/LetRec.lean
@@ -87,8 +87,8 @@ private def elabLetRecDeclValues (view : LetRecView) : TermElabM (Array Expr) :=
   view.decls.mapM fun view => do
     forallBoundedTelescope view.type view.binderIds.size fun xs type => do
       -- Add new info nodes for new fvars. The server will detect all fvars of a binder by the binder's source location.
-      for i in [0:view.binderIds.size] do
-        addLocalVarInfo view.binderIds[i]! xs[i]!
+      for h : i in [0:view.binderIds.size] do
+        addLocalVarInfo view.binderIds[i] xs[i]!
       withDeclName view.declName do
         withInfoContext' view.valStx
           (mkInfo := (pure <| .inl <| mkBodyInfo view.valStx ·))
diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean
index 3fb9c33c86ce..9a3d2665b971 100644
--- a/src/Lean/Elab/Match.lean
+++ b/src/Lean/Elab/Match.lean
@@ -282,8 +282,8 @@ where
         let dArg := dArgs[i]!
         unless (← isDefEq tArg dArg) do
           return i :: (← goType tArg dArg)
-      for i in [info.numParams : tArgs.size] do
-        let tArg := tArgs[i]!
+      for h : i in [info.numParams : tArgs.size] do
+        let tArg := tArgs[i]
         let dArg := dArgs[i]!
         unless (← isDefEq tArg dArg) do
           return i :: (← goIndex tArg dArg)
diff --git a/src/Lean/Elab/Open.lean b/src/Lean/Elab/Open.lean
index 2dc2813db391..e0279afe8b83 100644
--- a/src/Lean/Elab/Open.lean
+++ b/src/Lean/Elab/Open.lean
@@ -49,12 +49,12 @@ private def resolveNameUsingNamespacesCore (nss : List Name) (idStx : Syntax) :
       exs := exs.push ex
   if exs.size == nss.length then
     withRef idStx do
-      if exs.size == 1 then
-        throw exs[0]!
+      if h : exs.size = 1 then
+        throw exs[0]
       else
         throwErrorWithNestedErrors "failed to open" exs
-  if result.size == 1 then
-    return result[0]!
+  if h : result.size = 1 then
+    return result[0]
   else
     withRef idStx do throwError "ambiguous identifier '{idStx.getId}', possible interpretations: {result.map mkConst}"
 
diff --git a/src/Lean/Elab/PreDefinition/Basic.lean b/src/Lean/Elab/PreDefinition/Basic.lean
index 3d874f88aa31..b1b78b1a9aa5 100644
--- a/src/Lean/Elab/PreDefinition/Basic.lean
+++ b/src/Lean/Elab/PreDefinition/Basic.lean
@@ -244,8 +244,8 @@ def checkCodomainsLevel (preDefs : Array PreDefinition) : MetaM Unit := do
     lambdaTelescope preDef.value fun xs _ => return xs.size
   forallBoundedTelescope preDefs[0]!.type arities[0]!  fun _ type₀ => do
     let u₀ ← getLevel type₀
-    for i in [1:preDefs.size] do
-      forallBoundedTelescope preDefs[i]!.type arities[i]! fun _ typeᵢ =>
+    for h : i in [1:preDefs.size] do
+      forallBoundedTelescope preDefs[i].type arities[i]! fun _ typeᵢ =>
       unless ← isLevelDefEq u₀ (← getLevel typeᵢ) do
         withOptions (fun o => pp.sanitizeNames.set o false) do
           throwError m!"invalid mutual definition, result types must be in the same universe " ++
diff --git a/src/Lean/Elab/PreDefinition/TerminationArgument.lean b/src/Lean/Elab/PreDefinition/TerminationArgument.lean
index 018057986f51..5998666b7828 100644
--- a/src/Lean/Elab/PreDefinition/TerminationArgument.lean
+++ b/src/Lean/Elab/PreDefinition/TerminationArgument.lean
@@ -53,10 +53,10 @@ def TerminationArgument.elab (funName : Name) (type : Expr) (arity extraParams :
     (hint : TerminationBy) : TermElabM TerminationArgument := withDeclName funName do
   assert! extraParams ≤ arity
 
-  if hint.vars.size > extraParams then
+  if h : hint.vars.size > extraParams then
     let mut msg := m!"{parameters hint.vars.size} bound in `termination_by`, but the body of " ++
       m!"{funName} only binds {parameters extraParams}."
-    if let `($ident:ident) := hint.vars[0]! then
+    if let `($ident:ident) := hint.vars[0] then
       if ident.getId.isSuffixOf funName then
           msg := msg ++ m!" (Since Lean v4.6.0, the `termination_by` clause no longer " ++
             "expects the function name here.)"
diff --git a/src/Lean/Elab/PreDefinition/TerminationHint.lean b/src/Lean/Elab/PreDefinition/TerminationHint.lean
index 29ce520555d3..9243c3349477 100644
--- a/src/Lean/Elab/PreDefinition/TerminationHint.lean
+++ b/src/Lean/Elab/PreDefinition/TerminationHint.lean
@@ -90,10 +90,10 @@ lambda of `value`, and throws appropriate errors.
 -/
 def TerminationBy.checkVars (funName : Name) (extraParams : Nat) (tb : TerminationBy) : MetaM Unit := do
   unless tb.synthetic do
-    if tb.vars.size > extraParams then
+    if h : tb.vars.size > extraParams then
       let mut msg := m!"{parameters tb.vars.size} bound in `termination_by`, but the body of " ++
         m!"{funName} only binds {parameters extraParams}."
-      if let `($ident:ident) := tb.vars[0]! then
+      if let `($ident:ident) := tb.vars[0] then
         if ident.getId.isSuffixOf funName then
             msg := msg ++ m!" (Since Lean v4.6.0, the `termination_by` clause no longer " ++
               "expects the function name here.)"
diff --git a/src/Lean/Elab/PreDefinition/WF/Main.lean b/src/Lean/Elab/PreDefinition/WF/Main.lean
index 9302132f5df5..6aacb9c2cec2 100644
--- a/src/Lean/Elab/PreDefinition/WF/Main.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Main.lean
@@ -21,8 +21,8 @@ open Meta
 private partial def addNonRecPreDefs (fixedPrefixSize : Nat) (argsPacker : ArgsPacker) (preDefs : Array PreDefinition) (preDefNonRec : PreDefinition)  : TermElabM Unit := do
   let us := preDefNonRec.levelParams.map mkLevelParam
   let all := preDefs.toList.map (·.declName)
-  for fidx in [:preDefs.size] do
-    let preDef := preDefs[fidx]!
+  for h : fidx in [:preDefs.size] do
+    let preDef := preDefs[fidx]
     let value ← forallBoundedTelescope preDef.type (some fixedPrefixSize) fun xs _ => do
       let value := mkAppN (mkConst preDefNonRec.declName us) xs
       let value ← argsPacker.curryProj value fidx
diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean
index 91ba8b37dd09..1e0f21691ba8 100644
--- a/src/Lean/Elab/Syntax.lean
+++ b/src/Lean/Elab/Syntax.lean
@@ -19,12 +19,12 @@ def expandOptPrecedence (stx : Syntax) : MacroM (Option Nat) :=
     return some (← evalPrec stx[0][1])
 
 private def mkParserSeq (ds : Array (Term × Nat)) : TermElabM (Term × Nat) := do
-  if ds.size == 0 then
+  if h₀ : ds.size = 0 then
     throwUnsupportedSyntax
-  else if ds.size == 1 then
-    pure ds[0]!
+  else if h₁ : ds.size = 1 then
+    pure ds[0]
   else
-    let mut (r, stackSum) := ds[0]!
+    let mut (r, stackSum) := ds[0]
     for (d, stackSz) in ds[1:ds.size] do
       r ← `(ParserDescr.binary `andthen $r $d)
       stackSum := stackSum + stackSz
diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean
index 5a6eeda9fa7d..bf045692f328 100644
--- a/src/Lean/Elab/SyntheticMVars.lean
+++ b/src/Lean/Elab/SyntheticMVars.lean
@@ -149,8 +149,8 @@ where
         -- Succeeded. Collect new TC problems
         trace[Elab.defaultInstance] "isDefEq worked {mkMVar mvarId} : {← inferType (mkMVar mvarId)} =?= {candidate} : {← inferType candidate}"
         let mut pending := []
-        for i in [:bis.size] do
-          if bis[i]! == BinderInfo.instImplicit then
+        for h : i in [:bis.size] do
+          if bis[i] == BinderInfo.instImplicit then
             pending := mvars[i]!.mvarId! :: pending
         synthesizePending pending
       else
diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index 2448fc859bfb..4e0b8ceef688 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -317,8 +317,8 @@ partial def ensureExtensionsArraySize (exts : Array EnvExtensionState) : IO (Arr
 where
   loop (i : Nat) (exts : Array EnvExtensionState) : IO (Array EnvExtensionState) := do
     let envExtensions ← envExtensionsRef.get
-    if i < envExtensions.size then
-      let s ← envExtensions[i]!.mkInitial
+    if h : i < envExtensions.size then
+      let s ← envExtensions[i].mkInitial
       let exts := exts.push s
       loop (i + 1) exts
     else
@@ -726,7 +726,6 @@ def mkExtNameMap (startingAt : Nat) : IO (Std.HashMap Name Nat) := do
   let descrs ← persistentEnvExtensionsRef.get
   let mut result := {}
   for h : i in [startingAt : descrs.size] do
-    have : i < descrs.size := h.upper
     let descr := descrs[i]
     result := result.insert descr.name i
   return result
@@ -740,7 +739,6 @@ private def setImportedEntries (env : Environment) (mods : Array ModuleData) (st
   /- For each module `mod`, and `mod.entries`, if the extension name is one of the extensions after `startingAt`, set `entries` -/
   let extNameIdx ← mkExtNameMap startingAt
   for h : modIdx in [:mods.size] do
-    have : modIdx < mods.size := h.upper
     let mod := mods[modIdx]
     for (extName, entries) in mod.entries do
       if let some entryIdx := extNameIdx[extName]? then
@@ -860,7 +858,7 @@ def finalizeImport (s : ImportState) (imports : Array Import) (opts : Options) (
   let mut const2ModIdx : Std.HashMap Name ModuleIdx := Std.HashMap.empty (capacity := numConsts)
   let mut constantMap : Std.HashMap Name ConstantInfo := Std.HashMap.empty (capacity := numConsts)
   for h : modIdx in [0:s.moduleData.size] do
-    let mod := s.moduleData[modIdx]'h.upper
+    let mod := s.moduleData[modIdx]
     for cname in mod.constNames, cinfo in mod.constants do
       match constantMap.getThenInsertIfNew? cname cinfo with
       | (cinfoPrev?, constantMap') =>
diff --git a/src/Lean/Meta/CongrTheorems.lean b/src/Lean/Meta/CongrTheorems.lean
index f5818f1dfd60..e517f9a64dae 100644
--- a/src/Lean/Meta/CongrTheorems.lean
+++ b/src/Lean/Meta/CongrTheorems.lean
@@ -122,8 +122,8 @@ def mkHCongr (f : Expr) : MetaM CongrTheorem := do
 private def fixKindsForDependencies (info : FunInfo) (kinds : Array CongrArgKind) : Array CongrArgKind := Id.run do
   let mut kinds := kinds
   for i in [:info.paramInfo.size] do
-    for j in [i+1:info.paramInfo.size] do
-      if info.paramInfo[j]!.backDeps.contains i then
+    for hj : j in [i+1:info.paramInfo.size] do
+      if info.paramInfo[j].backDeps.contains i then
         if kinds[j]! matches CongrArgKind.eq || kinds[j]! matches CongrArgKind.fixed then
           -- We must fix `i` because there is a `j` that depends on `i` and `j` is not cast-fixed.
           kinds := kinds.set! i CongrArgKind.fixed
diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index 1a7fabfcc0d9..b9e8bd9016fe 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -255,8 +255,8 @@ private def isDefEqArgsFirstPass
     (paramInfo : Array ParamInfo) (args₁ args₂ : Array Expr) : MetaM DefEqArgsFirstPassResult := do
   let mut postponedImplicit := #[]
   let mut postponedHO := #[]
-  for i in [:paramInfo.size] do
-    let info := paramInfo[i]!
+  for h : i in [:paramInfo.size] do
+    let info := paramInfo[i]
     let a₁ := args₁[i]!
     let a₂ := args₂[i]!
     if info.dependsOnHigherOrderOutParam || info.higherOrderOutParam then
diff --git a/src/Lean/Meta/ForEachExpr.lean b/src/Lean/Meta/ForEachExpr.lean
index cc73c7810b73..7617dfc7106d 100644
--- a/src/Lean/Meta/ForEachExpr.lean
+++ b/src/Lean/Meta/ForEachExpr.lean
@@ -93,8 +93,8 @@ def setMVarUserNamesAt (e : Expr) (isTarget : Array Expr) : MetaM (Array MVarId)
   forEachExpr (← instantiateMVars e) fun e => do
     if e.isApp then
       let args := e.getAppArgs
-      for i in [:args.size] do
-        let arg := args[i]!
+      for h : i in [:args.size] do
+        let arg := args[i]
         if arg.isMVar && isTarget.contains arg then
           let mvarId := arg.mvarId!
           if (← mvarId.getDecl).userName.isAnonymous then
diff --git a/src/Lean/Meta/Match/MatchEqs.lean b/src/Lean/Meta/Match/MatchEqs.lean
index d3cfd47ae7bf..728c09462be3 100644
--- a/src/Lean/Meta/Match/MatchEqs.lean
+++ b/src/Lean/Meta/Match/MatchEqs.lean
@@ -557,8 +557,8 @@ where
         let mut minorBodyNew := minor
         -- We have to extend the mapping to make sure `convertTemplate` can "fix" occurrences of the refined minor premises
         let mut m ← read
-        for i in [:isAlt.size] do
-          if isAlt[i]! then
+        for h : i in [:isAlt.size] do
+          if isAlt[i] then
             -- `convertTemplate` will correct occurrences of the alternative
             let alt := args[6+i]! -- Recall that `Eq.ndrec` has 6 arguments
             let some (_, numParams, argMask) := m.find? alt.fvarId! | unreachable!
diff --git a/src/Lean/Meta/Tactic/ElimInfo.lean b/src/Lean/Meta/Tactic/ElimInfo.lean
index 0ada47e2eedf..630b30017d56 100644
--- a/src/Lean/Meta/Tactic/ElimInfo.lean
+++ b/src/Lean/Meta/Tactic/ElimInfo.lean
@@ -148,13 +148,13 @@ def mkCustomEliminator (elimName : Name) (induction : Bool) : MetaM CustomElimin
   let info ← getConstInfo elimName
   forallTelescopeReducing info.type fun xs _ => do
     let mut typeNames := #[]
-    for i in [:elimInfo.targetsPos.size] do
-      let targetPos := elimInfo.targetsPos[i]!
+    for hi : i in [:elimInfo.targetsPos.size] do
+      let targetPos := elimInfo.targetsPos[i]
       let x := xs[targetPos]!
       /- Return true if there is another target that depends on `x`. -/
       let isImplicitTarget : MetaM Bool := do
-        for j in [i+1:elimInfo.targetsPos.size] do
-          let y := xs[elimInfo.targetsPos[j]!]!
+        for hj : j in [i+1:elimInfo.targetsPos.size] do
+          let y := xs[elimInfo.targetsPos[j]]!
           let yType ← inferType y
           if (← dependsOn yType x.fvarId!) then
             return true
diff --git a/src/Lean/Meta/Tactic/Simp/SimpAll.lean b/src/Lean/Meta/Tactic/Simp/SimpAll.lean
index 4841665737b5..cefc68f5703c 100644
--- a/src/Lean/Meta/Tactic/Simp/SimpAll.lean
+++ b/src/Lean/Meta/Tactic/Simp/SimpAll.lean
@@ -58,8 +58,9 @@ private partial def loop : M Bool := do
   modify fun s => { s with modified := false }
   let simprocs := (← get).simprocs
   -- simplify entries
-  for i in [:(← get).entries.size] do
-    let entry := (← get).entries[i]!
+  let entries := (← get).entries
+  for h : i in [:entries.size] do
+    let entry := entries[i]
     let ctx := (← get).ctx
     -- We disable the current entry to prevent it to be simplified to `True`
     let simpThmsWithoutEntry := (← getSimpTheorems).eraseTheorem entry.id
diff --git a/src/Lean/Meta/Tactic/Split.lean b/src/Lean/Meta/Tactic/Split.lean
index 0ebcda9ccc0f..be116ed428e1 100644
--- a/src/Lean/Meta/Tactic/Split.lean
+++ b/src/Lean/Meta/Tactic/Split.lean
@@ -140,8 +140,8 @@ private partial def generalizeMatchDiscrs (mvarId : MVarId) (matcherDeclName : N
           let matcherApp := { matcherApp with discrs := discrVars }
           foundRef.set true
           let mut altsNew := #[]
-          for i in [:matcherApp.alts.size] do
-            let alt := matcherApp.alts[i]!
+          for h : i in [:matcherApp.alts.size] do
+            let alt := matcherApp.alts[i]
             let altNumParams := matcherApp.altNumParams[i]!
             let altNew ← lambdaTelescope alt fun xs body => do
               if xs.size < altNumParams || xs.size < numDiscrEqs then
diff --git a/src/Lean/Meta/Tactic/TryThis.lean b/src/Lean/Meta/Tactic/TryThis.lean
index a5df5057331a..04845bf3fa11 100644
--- a/src/Lean/Meta/Tactic/TryThis.lean
+++ b/src/Lean/Meta/Tactic/TryThis.lean
@@ -114,7 +114,7 @@ apply the replacement.
     unless params.range.start.line ≤ stxRange.end.line do return result
     let mut result := result
     for h : i in [:suggestionTexts.size] do
-      let (newText, title?) := suggestionTexts[i]'h.2
+      let (newText, title?) := suggestionTexts[i]
       let title := title?.getD <| (codeActionPrefix?.getD "Try this: ") ++ newText
       result := result.push {
         eager.title := title
diff --git a/src/Lean/PrettyPrinter/Delaborator/FieldNotation.lean b/src/Lean/PrettyPrinter/Delaborator/FieldNotation.lean
index 84aefe4b1916..7209d7de5380 100644
--- a/src/Lean/PrettyPrinter/Delaborator/FieldNotation.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/FieldNotation.lean
@@ -57,8 +57,8 @@ private def generalizedFieldInfo (c : Name) (args : Array Expr) : MetaM (Name ×
   -- Search for the first argument that could be used for field notation
   -- and make sure it is the first explicit argument.
   forallBoundedTelescope info.type args.size fun params _ => do
-    for i in [0:params.size] do
-      let fvarId := params[i]!.fvarId!
+    for h : i in [0:params.size] do
+      let fvarId := params[i].fvarId!
       -- If there is a motive, we will treat this as a sort of control flow structure and so we won't use field notation.
       -- Plus, recursors tend to be riskier when using dot notation.
       if (← fvarId.getUserName) == `motive then
diff --git a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
index 6b69c498b062..0a2aed6e1a2c 100644
--- a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
@@ -308,12 +308,12 @@ partial def canBottomUp (e : Expr) (mvar? : Option Expr := none) (fuel : Nat :=
     let args := e.getAppArgs
     let fType ← replaceLPsWithVars (← inferType e.getAppFn)
     let (mvars, bInfos, resultType) ← forallMetaBoundedTelescope fType e.getAppArgs.size
-    for i in [:mvars.size] do
+    for h : i in [:mvars.size] do
       if bInfos[i]! == BinderInfo.instImplicit then
-        inspectOutParams args[i]! mvars[i]!
+        inspectOutParams args[i]! mvars[i]
       else if bInfos[i]! == BinderInfo.default then
-        if ← isTrivialBottomUp args[i]! then tryUnify args[i]! mvars[i]!
-        else if ← typeUnknown mvars[i]! <&&> canBottomUp args[i]! (some mvars[i]!) fuel then tryUnify args[i]! mvars[i]!
+        if ← isTrivialBottomUp args[i]! then tryUnify args[i]! mvars[i]
+        else if ← typeUnknown mvars[i] <&&> canBottomUp args[i]! (some mvars[i]) fuel then tryUnify args[i]! mvars[i]
     if ← (pure (isHBinOp e) <&&> (valUnknown mvars[0]! <||> valUnknown mvars[1]!)) then tryUnify mvars[0]! mvars[1]!
     if mvar?.isSome then tryUnify resultType (← inferType mvar?.get!)
     return !(← valUnknown resultType)
@@ -487,22 +487,22 @@ mutual
     collectBottomUps := do
       let { args, mvars, bInfos, ..} ← read
       for target in [fun _ => none, fun i => some mvars[i]!] do
-        for i in [:args.size] do
+        for h : i in [:args.size] do
           if bInfos[i]! == BinderInfo.default then
-            if ← typeUnknown mvars[i]! <&&> canBottomUp args[i]! (target i) then
+            if ← typeUnknown mvars[i]! <&&> canBottomUp args[i] (target i) then
               tryUnify args[i]! mvars[i]!
               modify fun s => { s with bottomUps := s.bottomUps.set! i true }
 
     checkOutParams := do
       let { args, mvars, bInfos, ..} ← read
-      for i in [:args.size] do
-        if bInfos[i]! == BinderInfo.instImplicit then inspectOutParams args[i]! mvars[i]!
+      for h : i in [:args.size] do
+        if bInfos[i]! == BinderInfo.instImplicit then inspectOutParams args[i] mvars[i]!
 
     collectHigherOrders := do
       let { args, mvars, bInfos, ..} ← read
-      for i in [:args.size] do
+      for h : i in [:args.size] do
         if !(bInfos[i]! == BinderInfo.implicit || bInfos[i]! == BinderInfo.strictImplicit) then continue
-        if !(← isHigherOrder (← inferType args[i]!)) then continue
+        if !(← isHigherOrder (← inferType args[i])) then continue
         if getPPAnalyzeTrustId (← getOptions) && isIdLike args[i]! then continue
 
         if getPPAnalyzeTrustKnownFOType2TypeHOFuns (← getOptions) && !(← valUnknown mvars[i]!)
@@ -520,9 +520,9 @@ mutual
       -- motivation: prevent levels from printing in
       -- Boo.mk : {α : Type u_1} → {β : Type u_2} → α → β → Boo.{u_1, u_2} α β
       let { args, mvars, bInfos, ..} ← read
-      for i in [:args.size] do
+      for h : i in [:args.size] do
         if bInfos[i]! == BinderInfo.default then
-          if ← valUnknown mvars[i]! <&&> isTrivialBottomUp args[i]! then
+          if ← valUnknown mvars[i]! <&&> isTrivialBottomUp args[i] then
             tryUnify args[i]! mvars[i]!
             modify fun s => { s with bottomUps := s.bottomUps.set! i true }
 
diff --git a/src/Lean/Syntax.lean b/src/Lean/Syntax.lean
index 1790229e20bf..6e487ff0e8d4 100644
--- a/src/Lean/Syntax.lean
+++ b/src/Lean/Syntax.lean
@@ -248,11 +248,11 @@ partial def updateTrailing (trailing : Substring) : Syntax → Syntax
   | Syntax.atom info val               => Syntax.atom (info.updateTrailing trailing) val
   | Syntax.ident info rawVal val pre   => Syntax.ident (info.updateTrailing trailing) rawVal val pre
   | n@(Syntax.node info k args)        =>
-    if args.size == 0 then n
+    if h : args.size = 0 then n
     else
      let i    := args.size - 1
-     let last := updateTrailing trailing args[i]!
-     let args := args.set! i last;
+     let last := updateTrailing trailing args[i]
+     let args := args.set i last;
      Syntax.node info k args
   | s => s
 
diff --git a/src/lake/Lake/Toml/Data/Dict.lean b/src/lake/Lake/Toml/Data/Dict.lean
index ee7685c84543..de40e3163bed 100644
--- a/src/lake/Lake/Toml/Data/Dict.lean
+++ b/src/lake/Lake/Toml/Data/Dict.lean
@@ -36,7 +36,7 @@ def mkEmpty (capacity : Nat) : RBDict α β cmp :=
 def ofArray (items : Array (α × β)) : RBDict α β cmp := Id.run do
   let mut indices := mkRBMap α Nat cmp
   for h : i in [0:items.size] do
-    indices := indices.insert (items[i]'h.upper).1 i
+    indices := indices.insert items[i].1 i
   return {items, indices}
 
 protected def beq [BEq (α × β)] (self other : RBDict α β cmp) : Bool :=