diff --git a/src/Lean/Compiler/IR/SimpCase.lean b/src/Lean/Compiler/IR/SimpCase.lean
index c293de19db..7bbfbe57c2 100644
--- a/src/Lean/Compiler/IR/SimpCase.lean
+++ b/src/Lean/Compiler/IR/SimpCase.lean
@@ -20,18 +20,18 @@ def ensureHasDefault (alts : Array Alt) : Array Alt :=
 private def getOccsOf (alts : Array Alt) (i : Nat) : Nat := Id.run do
   let aBody := (alts.get! i).body
   let mut n := 1
-  for j in [i+1:alts.size] do
-    if alts[j]!.body == aBody then
+  for h: j in [i+1:alts.size] do
+    if alts[j].body == aBody then
       n := n+1
   return n
 
 private def maxOccs (alts : Array Alt) : Alt × Nat := Id.run do
   let mut maxAlt := alts[0]!
   let mut max    := getOccsOf alts 0
-  for i in [1:alts.size] do
+  for h: i in [1:alts.size] do
     let curr := getOccsOf alts i
     if curr > max then
-       maxAlt := alts[i]!
+       maxAlt := alts[i]
        max    := curr
   return (maxAlt, max)
 
diff --git a/src/Lean/Compiler/LCNF/Check.lean b/src/Lean/Compiler/LCNF/Check.lean
index a1b75c1f98..c591d14ce1 100644
--- a/src/Lean/Compiler/LCNF/Check.lean
+++ b/src/Lean/Compiler/LCNF/Check.lean
@@ -110,8 +110,8 @@ def isCtorParam (f : Expr) (i : Nat) : CoreM Bool := do
 def checkAppArgs (f : Expr) (args : Array Arg) : CheckM Unit := do
   let mut fType ← inferType f
   let mut j := 0
-  for i in [:args.size] do
-    let arg := args[i]!
+  for h: i in [:args.size] do
+    let arg := args[i]
     if fType.isErased then
       return ()
     fType := fType.headBeta
diff --git a/src/Lean/Compiler/LCNF/ElimDeadBranches.lean b/src/Lean/Compiler/LCNF/ElimDeadBranches.lean
index 60eef13dbe..31f2e5fa49 100644
--- a/src/Lean/Compiler/LCNF/ElimDeadBranches.lean
+++ b/src/Lean/Compiler/LCNF/ElimDeadBranches.lean
@@ -505,8 +505,8 @@ ones. Return whether any `Value` got updated in the process.
 -/
 def inferStep : InterpM Bool := do
   let ctx ← read
-  for idx in [0:ctx.decls.size] do
-    let decl := ctx.decls[idx]!
+  for h: idx in [0:ctx.decls.size] do
+    let decl := ctx.decls[idx]
     if !decl.safe then
       continue
 
diff --git a/src/Lean/Compiler/LCNF/MonoTypes.lean b/src/Lean/Compiler/LCNF/MonoTypes.lean
index 4f609b3f9b..7b0bddd50f 100644
--- a/src/Lean/Compiler/LCNF/MonoTypes.lean
+++ b/src/Lean/Compiler/LCNF/MonoTypes.lean
@@ -48,8 +48,8 @@ def hasTrivialStructure? (declName : Name) : CoreM (Option TrivialStructureInfo)
   let [ctorName] := info.ctors | return none
   let mask ← getRelevantCtorFields ctorName
   let mut result := none
-  for i in [:mask.size] do
-    if mask[i]! then
+  for h: i in [:mask.size] do
+    if mask[i] then
       if result.isSome then return none
       result := some { ctorName, fieldIdx := i, numParams := info.numParams }
   return result
@@ -129,4 +129,4 @@ def getOtherDeclMonoType (declName : Name) : CoreM Expr := do
     modifyEnv fun env => monoTypeExt.modifyState env fun s => { s with mono := s.mono.insert declName type }
     return type
 
-end Lean.Compiler.LCNF
\ No newline at end of file
+end Lean.Compiler.LCNF
diff --git a/src/Lean/Compiler/LCNF/PullFunDecls.lean b/src/Lean/Compiler/LCNF/PullFunDecls.lean
index e1162ac6fe..8dd0781017 100644
--- a/src/Lean/Compiler/LCNF/PullFunDecls.lean
+++ b/src/Lean/Compiler/LCNF/PullFunDecls.lean
@@ -96,9 +96,9 @@ where
     unless (← visited i) do
       modify fun (k, visited) => (k, visited.set! i true)
       let pi := ps[i]!
-      for j in [:ps.size] do
+      for h: j in [:ps.size] do
         unless (← visited j) do
-          let pj := ps[j]!
+          let pj := ps[j]
           if pj.used.contains pi.decl.fvarId then
             visit j
       modify fun (k, visited) => (pi.attach k, visited)
diff --git a/src/Lean/Compiler/LCNF/Simp/DefaultAlt.lean b/src/Lean/Compiler/LCNF/Simp/DefaultAlt.lean
index 8b2a6587dd..1374067cf6 100644
--- a/src/Lean/Compiler/LCNF/Simp/DefaultAlt.lean
+++ b/src/Lean/Compiler/LCNF/Simp/DefaultAlt.lean
@@ -18,10 +18,10 @@ or not.
 private def getMaxOccs (alts : Array Alt) : Alt × Nat := Id.run do
   let mut maxAlt := alts[0]!
   let mut max    := getNumOccsOf alts 0
-  for i in [1:alts.size] do
+  for h: i in [1:alts.size] do
     let curr := getNumOccsOf alts i
     if curr > max then
-       maxAlt := alts[i]!
+       maxAlt := alts[i]
        max    := curr
   return (maxAlt, max)
 where
@@ -34,8 +34,8 @@ where
   getNumOccsOf (alts : Array Alt) (i : Nat) : Nat := Id.run do
     let code := alts[i]!.getCode
     let mut n := 1
-    for j in [i+1:alts.size] do
-      if Code.alphaEqv alts[j]!.getCode code then
+    for h: j in [i+1:alts.size] do
+      if Code.alphaEqv alts[j].getCode code then
         n := n+1
     return n
 
diff --git a/src/Lean/Compiler/LCNF/Simp/JpCases.lean b/src/Lean/Compiler/LCNF/Simp/JpCases.lean
index 5986ba8c37..e249b6e994 100644
--- a/src/Lean/Compiler/LCNF/Simp/JpCases.lean
+++ b/src/Lean/Compiler/LCNF/Simp/JpCases.lean
@@ -121,8 +121,8 @@ where
     let mut paramsNew := #[]
     let singleton : FVarIdSet := ({} : FVarIdSet).insert params[targetParamIdx]!.fvarId
     let dependsOnDiscr := k.dependsOn singleton || decls.any (·.dependsOn singleton)
-    for i in [:params.size] do
-      let param := params[i]!
+    for h: i in [:params.size] do
+      let param := params[i]
       if targetParamIdx == i then
         if dependsOnDiscr then
           paramsNew := paramsNew.push (← internalizeParam param)
@@ -300,4 +300,3 @@ builtin_initialize
   registerTraceClass `Compiler.simp.jpCases
 
 end Lean.Compiler.LCNF
-
diff --git a/src/Lean/Compiler/LCNF/SpecInfo.lean b/src/Lean/Compiler/LCNF/SpecInfo.lean
index 530ef482d5..3688e0e349 100644
--- a/src/Lean/Compiler/LCNF/SpecInfo.lean
+++ b/src/Lean/Compiler/LCNF/SpecInfo.lean
@@ -129,9 +129,9 @@ See comment at `.fixedNeutral`.
 -/
 private def hasFwdDeps (decl : Decl) (paramsInfo : Array SpecParamInfo) (j : Nat) : Bool := Id.run do
   let param := decl.params[j]!
-  for k in [j+1 : decl.params.size] do
+  for h: k in [j+1 : decl.params.size] do
     if paramsInfo[k]! matches .user | .fixedHO | .fixedInst then
-      let param' := decl.params[k]!
+      let param' := decl.params[k]
       if param'.type.containsFVar param.fvarId then
         return true
   return false
@@ -214,4 +214,3 @@ builtin_initialize
   registerTraceClass `Compiler.specialize.info
 
 end Lean.Compiler.LCNF
-
diff --git a/src/Lean/Compiler/LCNF/ToDecl.lean b/src/Lean/Compiler/LCNF/ToDecl.lean
index a8369e8e6f..ec0485cde5 100644
--- a/src/Lean/Compiler/LCNF/ToDecl.lean
+++ b/src/Lean/Compiler/LCNF/ToDecl.lean
@@ -50,9 +50,9 @@ partial def inlineMatchers (e : Expr) : CoreM Expr :=
       let numAlts := info.numAlts
       let altNumParams := info.altNumParams
       let rec inlineMatcher (i : Nat) (args : Array Expr) (letFVars : Array Expr) : MetaM Expr := do
-        if i < numAlts then
+        if h: i < numAlts then
           let altIdx := i + info.getFirstAltPos
-          let numParams := altNumParams[i]!
+          let numParams := altNumParams[i]
           let alt ← normalizeAlt args[altIdx]! numParams
           Meta.withLetDecl (← mkFreshUserName `_alt) (← Meta.inferType alt) alt fun altFVar =>
             inlineMatcher (i+1) (args.set! altIdx altFVar) (letFVars.push altFVar)
diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 5f9e18e959..b74230c0da 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -421,8 +421,8 @@ private def findNamedArgDependsOnCurrent? : M (Option NamedArg) := do
   else
     forallTelescopeReducing s.fType fun xs _ => do
       let curr := xs[0]!
-      for i in [1:xs.size] do
-        let xDecl ← xs[i]!.fvarId!.getDecl
+      for h: i in [1:xs.size] do
+        let xDecl ← xs[i].fvarId!.getDecl
         if let some arg := s.namedArgs.find? fun arg => arg.name == xDecl.userName then
           /- Remark: a default value at `optParam` does not count as a dependency -/
           if (← exprDependsOn xDecl.type.cleanupAnnotations curr.fvarId!) then
@@ -800,8 +800,8 @@ def getElabElimExprInfo (elimExpr : Expr) : MetaM ElabElimInfo := do
         return s
     /- Collect the major parameter positions -/
     let mut majorsPos := #[]
-    for i in [:xs.size] do
-      let x := xs[i]!
+    for h: i in [:xs.size] do
+      let x := xs[i]
       unless motivePos == i do
         let xType ← x.fvarId!.getType
         /-
@@ -1301,8 +1301,8 @@ private def addLValArg (baseName : Name) (fullName : Name) (e : Expr) (args : Ar
   forallTelescopeReducing fType fun xs _ => do
     let mut argIdx := 0 -- position of the next explicit argument
     let mut remainingNamedArgs := namedArgs
-    for i in [:xs.size] do
-      let x := xs[i]!
+    for h: i in [:xs.size] do
+      let x := xs[i]
       let xDecl ← x.fvarId!.getDecl
       /- If there is named argument with name `xDecl.userName`, then we skip it. -/
       match remainingNamedArgs.findIdx? (fun namedArg => namedArg.name == xDecl.userName) with
diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index df8f0bed27..4f592d3911 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -55,8 +55,8 @@ open Meta
             let cinfo ← getConstInfoCtor ctor
             let numExplicitFields ← forallTelescopeReducing cinfo.type fun xs _ => do
               let mut n := 0
-              for i in [cinfo.numParams:xs.size] do
-                if (← getFVarLocalDecl xs[i]!).binderInfo.isExplicit then
+              for h: i in [cinfo.numParams:xs.size] do
+                if (← getFVarLocalDecl xs[i]).binderInfo.isExplicit then
                   n := n + 1
               return n
             let args := args.getElems
diff --git a/src/Lean/Elab/DeclNameGen.lean b/src/Lean/Elab/DeclNameGen.lean
index 2d6f97b413..db0a08cabc 100644
--- a/src/Lean/Elab/DeclNameGen.lean
+++ b/src/Lean/Elab/DeclNameGen.lean
@@ -64,13 +64,13 @@ private partial def winnowExpr (e : Expr) : MetaM Expr := do
         let mut fty ← inferType f
         let mut j := 0
         let mut e' ← visit f
-        for i in [0:args.size] do
+        for h: i in [0:args.size] do
           unless fty.isForall do
             fty ← withTransparency .all <| whnf <| fty.instantiateRevRange j i args
             j := i
           let .forallE _ _ fty' bi := fty | failure
           fty := fty'
-          let arg := args[i]!
+          let arg := args[i]
           if ← pure bi.isExplicit <||> (pure !arg.isSort <&&> isTypeFormer arg) then
             unless (← isProof arg) do
               e' := .app e' (← visit arg)
diff --git a/src/Lean/Elab/Deriving/Inhabited.lean b/src/Lean/Elab/Deriving/Inhabited.lean
index 61b786e174..b1655fb15d 100644
--- a/src/Lean/Elab/Deriving/Inhabited.lean
+++ b/src/Lean/Elab/Deriving/Inhabited.lean
@@ -86,8 +86,8 @@ where
       addLocalInstancesForParams xs[:ctorVal.numParams] fun localInst2Index => do
         let mut usedInstIdxs := {}
         let mut ok := true
-        for i in [ctorVal.numParams:xs.size] do
-          let x := xs[i]!
+        for h: i in [ctorVal.numParams:xs.size] do
+          let x := xs[i]
           let instType ← mkAppM `Inhabited #[(← inferType x)]
           trace[Elab.Deriving.inhabited] "checking {instType} for '{ctorName}'"
           match (← trySynthInstance instType) with
diff --git a/src/Lean/Elab/Deriving/Repr.lean b/src/Lean/Elab/Deriving/Repr.lean
index 18ebfd8501..38122252af 100644
--- a/src/Lean/Elab/Deriving/Repr.lean
+++ b/src/Lean/Elab/Deriving/Repr.lean
@@ -29,8 +29,8 @@ def mkBodyForStruct (header : Header) (indVal : InductiveVal) : TermElabM Term :
     let mut fields ← `(Format.nil)
     if xs.size != numParams + fieldNames.size then
       throwError "'deriving Repr' failed, unexpected number of fields in structure"
-    for i in [:fieldNames.size] do
-      let fieldName := fieldNames[i]!
+    for h: i in [:fieldNames.size] do
+      let fieldName := fieldNames[i]
       let fieldNameLit := Syntax.mkStrLit (toString fieldName)
       let x := xs[numParams + i]!
       if i != 0 then
@@ -59,10 +59,10 @@ where
         let mut ctorArgs := #[]
         let mut rhs : Term := Syntax.mkStrLit (toString ctorInfo.name)
         rhs ← `(Format.text $rhs)
-        for i in [:xs.size] do
+        for h: i in [:xs.size] do
           -- Note: some inductive parameters are explicit if they were promoted from indices,
           -- so we process all constructor arguments in the same loop.
-          let x := xs[i]!
+          let x := xs[i]
           let a ← mkIdent <$> if i < indVal.numParams then pure header.argNames[i]! else mkFreshUserName `a
           if i < indVal.numParams then
             -- add `_` for inductive parameters, they are inaccessible
diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean
index 1fe81c39b4..051a79c3c0 100644
--- a/src/Lean/Elab/Inductive.lean
+++ b/src/Lean/Elab/Inductive.lean
@@ -168,8 +168,8 @@ private def checkHeader (r : ElabHeaderResult) (numParams : Nat) (firstType? : O
 
 -- Auxiliary function for checking whether the types in mutually inductive declaration are compatible.
 private partial def checkHeaders (rs : Array ElabHeaderResult) (numParams : Nat) (i : Nat) (firstType? : Option Expr) : TermElabM Unit := do
-  if i < rs.size then
-    let type ← checkHeader rs[i]! numParams firstType?
+  if h: i < rs.size then
+    let type ← checkHeader rs[i] numParams firstType?
     checkHeaders rs numParams (i+1) type
 
 private def elabHeader (views : Array InductiveView) : TermElabM (Array ElabHeaderResult) := do
@@ -222,11 +222,11 @@ private def replaceArrowBinderNames (type : Expr) (newNames : Array Name) : Expr
   go type 0
 where
   go (type : Expr) (i : Nat) : Expr :=
-    if i < newNames.size then
+    if h: i < newNames.size then
       match type with
       | .forallE n d b bi =>
         if n.hasMacroScopes then
-          mkForall newNames[i]! bi d (go b (i+1))
+          mkForall newNames[i] bi d (go b (i+1))
         else
           mkForall n bi d (go b (i+1))
       | _ => type
diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean
index 4b69e66d91..561cf745e3 100644
--- a/src/Lean/Elab/Match.lean
+++ b/src/Lean/Elab/Match.lean
@@ -330,8 +330,8 @@ private def elabPatterns (patternStxs : Array Syntax) (matchType : Expr) : Excep
   withReader (fun ctx => { ctx with implicitLambda := false }) do
     let mut patterns  := #[]
     let mut matchType := matchType
-    for idx in [:patternStxs.size] do
-      let patternStx := patternStxs[idx]!
+    for h: idx in [:patternStxs.size] do
+      let patternStx := patternStxs[idx]
       matchType ← whnf matchType
       match matchType with
       | Expr.forallE _ d b _ =>
diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index 43cd332792..4909847434 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -406,9 +406,9 @@ private def elabFunValues (headers : Array DefViewElabHeader) (vars : Array Expr
       (if header.kind.isTheorem && !deprecated.oldSectionVars.get (← getOptions) then withHeaderSecVars vars sc #[header] else fun x => x #[]) fun vars => do
       forallBoundedTelescope header.type header.numParams 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:header.binderIds.size] do
+        for h: i in [0:header.binderIds.size] do
           -- skip auto-bound prefix in `xs`
-          addLocalVarInfo header.binderIds[i]! xs[header.numParams - header.binderIds.size + i]!
+          addLocalVarInfo header.binderIds[i] xs[header.numParams - header.binderIds.size + i]!
         let val ← withReader ({ · with tacSnap? := header.tacSnap? }) do
           -- synthesize mvars here to force the top-level tactic block (if any) to run
           elabTermEnsuringType valStx type <* synthesizeSyntheticMVarsNoPostponing
diff --git a/src/Lean/Elab/PreDefinition/Nonrec/Eqns.lean b/src/Lean/Elab/PreDefinition/Nonrec/Eqns.lean
index 8121cf2f69..96abd18d00 100644
--- a/src/Lean/Elab/PreDefinition/Nonrec/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/Nonrec/Eqns.lean
@@ -77,9 +77,9 @@ def mkEqns (declName : Name) (info : DefinitionVal) : MetaM (Array Name) :=
     withReducible do
       mkEqnTypes #[] goal.mvarId!
   let mut thmNames := #[]
-  for i in [: eqnTypes.size] do
-    let type := eqnTypes[i]!
-    trace[Elab.definition.eqns] "eqnType[{i}]: {eqnTypes[i]!}"
+  for h: i in [: eqnTypes.size] do
+    let type := eqnTypes[i]
+    trace[Elab.definition.eqns] "eqnType[{i}]: {eqnTypes[i]}"
     let name := (Name.str baseName eqnThmSuffixBase).appendIndexAfter (i+1)
     thmNames := thmNames.push name
     let value ← mkProof declName type
diff --git a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean
index 1f0b71753b..84731211fd 100644
--- a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean
@@ -67,8 +67,8 @@ def mkEqns (info : EqnInfo) : MetaM (Array Name) :=
     mkEqnTypes info.declNames goal.mvarId!
   let baseName := info.declName
   let mut thmNames := #[]
-  for i in [: eqnTypes.size] do
-    let type := eqnTypes[i]!
+  for h: i in [: eqnTypes.size] do
+    let type := eqnTypes[i]
     trace[Elab.definition.structural.eqns] "eqnType {i}: {type}"
     let name := (Name.str baseName eqnThmSuffixBase).appendIndexAfter (i+1)
     thmNames := thmNames.push name
diff --git a/src/Lean/Elab/PreDefinition/WF/Eqns.lean b/src/Lean/Elab/PreDefinition/WF/Eqns.lean
index a8bea93c8b..6e6a90d72c 100644
--- a/src/Lean/Elab/PreDefinition/WF/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Eqns.lean
@@ -83,9 +83,9 @@ def mkEqns (declName : Name) (info : EqnInfo) : MetaM (Array Name) :=
     withReducible do
       mkEqnTypes info.declNames goal.mvarId!
   let mut thmNames := #[]
-  for i in [: eqnTypes.size] do
-    let type := eqnTypes[i]!
-    trace[Elab.definition.wf.eqns] "{eqnTypes[i]!}"
+  for h: i in [: eqnTypes.size] do
+    let type := eqnTypes[i]
+    trace[Elab.definition.wf.eqns] "{eqnTypes[i]}"
     let name := (Name.str baseName eqnThmSuffixBase).appendIndexAfter (i+1)
     thmNames := thmNames.push name
     let value ← mkProof declName type
diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean
index d67bfd8d14..ffedc36b36 100644
--- a/src/Lean/Elab/Quotation.lean
+++ b/src/Lean/Elab/Quotation.lean
@@ -655,9 +655,9 @@ The parameter `alts` provides position information for alternatives.
 -/
 private def checkUnusedAlts (stx : Syntax) (alts : Array Syntax) (altIdxMap : NameMap Nat) (ignoreIfUnused : IdxSet) : TermElabM Syntax := do
   let (stx, used) ← findUsedAlts stx altIdxMap
-  for i in [:alts.size] do
+  for h: i in [:alts.size] do
     unless used.contains i || ignoreIfUnused.contains i do
-      logErrorAt alts[i]! s!"redundant alternative #{i+1}"
+      logErrorAt alts[i] s!"redundant alternative #{i+1}"
   return stx
 
 def match_syntax.expand (stx : Syntax) : TermElabM Syntax := do
diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean
index 3e5e25223c..2c3c20190f 100644
--- a/src/Lean/Elab/SyntheticMVars.lean
+++ b/src/Lean/Elab/SyntheticMVars.lean
@@ -257,8 +257,8 @@ private def throwStuckAtUniverseCnstr : TermElabM Unit := do
     unless found.contains (lhs, rhs) do
       found := found.insert (lhs, rhs)
       uniqueEntries := uniqueEntries.push entry
-  for i in [1:uniqueEntries.size] do
-    logErrorAt uniqueEntries[i]!.ref (← mkLevelStuckErrorMessage uniqueEntries[i]!)
+  for h: i in [1:uniqueEntries.size] do
+    logErrorAt uniqueEntries[i].ref (← mkLevelStuckErrorMessage uniqueEntries[i]!)
   throwErrorAt uniqueEntries[0]!.ref (← mkLevelStuckErrorMessage uniqueEntries[0]!)
 
 /--
diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean
index 374180b490..da63d6431a 100644
--- a/src/Lean/Elab/Tactic/Induction.lean
+++ b/src/Lean/Elab/Tactic/Induction.lean
@@ -205,8 +205,8 @@ private def isWildcard (altStx : Syntax) : Bool :=
   getAltName altStx == `_
 
 private def checkAltNames (alts : Array Alt) (altsSyntax : Array Syntax) : TacticM Unit :=
-  for i in [:altsSyntax.size] do
-    let altStx := altsSyntax[i]!
+  for h: i in [:altsSyntax.size] do
+    let altStx := altsSyntax[i]
     if getAltName altStx == `_ && i != altsSyntax.size - 1 then
       withRef altStx <| throwError "invalid occurrence of wildcard alternative, it must be the last alternative"
     let altName := getAltName altStx
@@ -236,8 +236,8 @@ private def saveAltVarsInfo (altMVarId : MVarId) (altStx : Syntax) (fvarIds : Ar
     let altVars := getAltVars altStx
     for fvarId in fvarIds do
       if !useNamesForExplicitOnly || (← fvarId.getDecl).binderInfo.isExplicit then
-        if i < altVars.size then
-          Term.addLocalVarInfo altVars[i]! (mkFVar fvarId)
+        if h: i < altVars.size then
+          Term.addLocalVarInfo altVars[i] (mkFVar fvarId)
           i := i + 1
 
 open Language in
@@ -320,8 +320,8 @@ where
     2- The errors are produced in the same order the appear in the code above. This is not super
     important when using IDEs.
     -/
-    for altStxIdx in [0:altStxs.size] do
-      let altStx := altStxs[altStxIdx]!
+    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
         -- cover named alternative
diff --git a/src/Lean/Elab/Tactic/Omega/Core.lean b/src/Lean/Elab/Tactic/Omega/Core.lean
index ef6bb7abed..3912d785aa 100644
--- a/src/Lean/Elab/Tactic/Omega/Core.lean
+++ b/src/Lean/Elab/Tactic/Omega/Core.lean
@@ -513,13 +513,13 @@ def fourierMotzkinSelect (data : Array FourierMotzkinData) : MetaM FourierMotzki
   if bestSize = 0 then
     trace[omega] "Selected variable {data[0]!.var}."
     return data[0]!
-  for i in [1:data.size] do
-    let exact := data[i]!.exact
-    let size := data[i]!.size
+  for h: i in [1:data.size] do
+    let exact := data[i].exact
+    let size := data[i].size
     if size = 0 || !bestExact && exact || (bestExact == exact) && size < bestSize then
       if size = 0 then
-        trace[omega] "Selected variable {data[i]!.var}"
-        return data[i]!
+        trace[omega] "Selected variable {data[i].var}"
+        return data[i]
       bestIdx := i
       bestExact := exact
       bestSize := size
diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index 0b0c88f565..a07d6d0260 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -765,8 +765,8 @@ where
   loop (i : Nat) (env : Environment) : IO Environment := do
     -- Recall that the size of the array stored `persistentEnvExtensionRef` may increase when we import user-defined environment extensions.
     let pExtDescrs ← persistentEnvExtensionsRef.get
-    if i < pExtDescrs.size then
-      let extDescr := pExtDescrs[i]!
+    if h: i < pExtDescrs.size then
+      let extDescr := pExtDescrs[i]
       let s := extDescr.toEnvExtension.getState env
       let prevSize := (← persistentEnvExtensionsRef.get).size
       let prevAttrSize ← getNumBuiltinAttributes
diff --git a/src/Lean/LocalContext.lean b/src/Lean/LocalContext.lean
index ffdc746c2a..302ce45b1d 100644
--- a/src/Lean/LocalContext.lean
+++ b/src/Lean/LocalContext.lean
@@ -385,14 +385,14 @@ def size (lctx : LocalContext) : Nat :=
   Id.run <| lctx.findDeclRevM? f
 
 partial def isSubPrefixOfAux (a₁ a₂ : PArray (Option LocalDecl)) (exceptFVars : Array Expr) (i j : Nat) : Bool :=
-  if i < a₁.size then
-    match a₁[i]! with
+  if h: i < a₁.size then
+    match a₁[i] with
     | none       => isSubPrefixOfAux a₁ a₂ exceptFVars (i+1) j
     | some decl₁ =>
       if exceptFVars.any fun fvar => fvar.fvarId! == decl₁.fvarId then
         isSubPrefixOfAux a₁ a₂ exceptFVars (i+1) j
-      else if j < a₂.size then
-        match a₂[j]! with
+      else if h2: j < a₂.size then
+        match a₂[j] with
         | none       => isSubPrefixOfAux a₁ a₂ exceptFVars i (j+1)
         | some decl₂ => if decl₁.fvarId == decl₂.fvarId then isSubPrefixOfAux a₁ a₂ exceptFVars (i+1) (j+1) else isSubPrefixOfAux a₁ a₂ exceptFVars i (j+1)
       else false
diff --git a/src/Lean/Meta/ACLt.lean b/src/Lean/Meta/ACLt.lean
index 06fb73e21a..1cc4da2f6b 100644
--- a/src/Lean/Meta/ACLt.lean
+++ b/src/Lean/Meta/ACLt.lean
@@ -155,8 +155,8 @@ where
           if !infos[i]!.isInstImplicit then
             if !(← lt args[i]! b) then
               return false
-        for i in [infos.size:args.size] do
-          if !(← lt args[i]! b) then
+        for h: i in [infos.size:args.size] do
+          if !(← lt args[i] b) then
             return false
         return true
     | .lam _ d e ..     => lt d b <&&> lt e b
diff --git a/src/Lean/Meta/AppBuilder.lean b/src/Lean/Meta/AppBuilder.lean
index 898b59abee..f49dab0e27 100644
--- a/src/Lean/Meta/AppBuilder.lean
+++ b/src/Lean/Meta/AppBuilder.lean
@@ -277,7 +277,7 @@ private def mkAppMFinal (methodName : Name) (f : Expr) (args : Array Expr) (inst
 
 private partial def mkAppMArgs (f : Expr) (fType : Expr) (xs : Array Expr) : MetaM Expr :=
   let rec loop (type : Expr) (i : Nat) (j : Nat) (args : Array Expr) (instMVars : Array MVarId) : MetaM Expr := do
-    if i >= xs.size then
+    if h: i >= xs.size then
       mkAppMFinal `mkAppM f args instMVars
     else match type with
       | Expr.forallE n d b bi =>
@@ -293,7 +293,7 @@ private partial def mkAppMArgs (f : Expr) (fType : Expr) (xs : Array Expr) : Met
           let mvar ← mkFreshExprMVar d MetavarKind.synthetic n
           loop b i j (args.push mvar) (instMVars.push mvar.mvarId!)
         | _ =>
-          let x := xs[i]!
+          let x := xs[i]
           let xType ← inferType x
           if (← isDefEq d xType) then
             loop b (i+1) j (args.push x) instMVars
diff --git a/src/Lean/Meta/ArgsPacker.lean b/src/Lean/Meta/ArgsPacker.lean
index 8c1b8e7752..b590ac270a 100644
--- a/src/Lean/Meta/ArgsPacker.lean
+++ b/src/Lean/Meta/ArgsPacker.lean
@@ -69,8 +69,8 @@ The `type` should be the expected type of the packed argument, as created with `
 partial def pack (type : Expr) (args : Array Expr) : Expr := go 0 type
 where
   go (i : Nat) (type : Expr) : Expr :=
-    if i < args.size - 1 then
-      let arg := args[i]!
+    if h: i < args.size - 1 then
+      let arg := args[i]
       assert! type.isAppOfArity ``PSigma 2
       let us := type.getAppFn.constLevels!
       let α := type.appFn!.appArg!
diff --git a/src/Lean/Meta/CongrTheorems.lean b/src/Lean/Meta/CongrTheorems.lean
index f076c6a1ce..f66077aa99 100644
--- a/src/Lean/Meta/CongrTheorems.lean
+++ b/src/Lean/Meta/CongrTheorems.lean
@@ -77,7 +77,7 @@ partial def mkHCongrWithArity (f : Expr) (numArgs : Nat) : MetaM CongrTheorem :=
 where
   withNewEqs {α} (xs ys : Array Expr) (k : Array Expr → Array CongrArgKind → MetaM α) : MetaM α :=
     let rec loop (i : Nat) (eqs : Array Expr) (kinds : Array CongrArgKind) := do
-      if  i < xs.size then
+      if i < xs.size then
         let x := xs[i]!
         let y := ys[i]!
         let xType := (← inferType x).cleanupAnnotations
@@ -185,11 +185,11 @@ private def getClassSubobjectMask? (f : Expr) : MetaM (Option (Array Bool)) := d
   forallTelescopeReducing val.type (cleanupAnnotations := true) fun xs _ => do
     let env ← getEnv
     let mut mask := #[]
-    for i in [:xs.size] do
+    for h: i in [:xs.size] do
       if i < val.numParams then
         mask := mask.push false
       else
-        let localDecl ← xs[i]!.fvarId!.getDecl
+        let localDecl ← xs[i].fvarId!.getDecl
         mask := mask.push (isSubobjectField? env val.induct localDecl.userName).isSome
     return some mask
 
@@ -211,14 +211,14 @@ def getCongrSimpKinds (f : Expr) (info : FunInfo) : MetaM (Array CongrArgKind) :
   -/
   let mut result := #[]
   let mask? ← getClassSubobjectMask? f
-  for i in [:info.paramInfo.size] do
+  for h: i in [:info.paramInfo.size] do
     if info.resultDeps.contains i then
       result := result.push .fixed
-    else if info.paramInfo[i]!.isProp then
+    else if info.paramInfo[i].isProp then
       result := result.push .cast
-    else if info.paramInfo[i]!.isInstImplicit then
+    else if info.paramInfo[i].isInstImplicit then
       if let some mask := mask? then
-        if h : i < mask.size then
+        if h2 : i < mask.size then
           if mask[i] then
             -- Parameter is a subobect field of a class constructor. See comment above.
             result := result.push .eq
diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index cf5a576f14..9e8b38b78f 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -80,19 +80,19 @@ where
         checkpointDefEq do
           let args := b.getAppArgs
           let params := args[:ctorVal.numParams].toArray
-          for i in [ctorVal.numParams : args.size] do
+          for h: i in [ctorVal.numParams : args.size] do
             let j := i - ctorVal.numParams
             let proj ← mkProjFn ctorVal us params j a
             if ← isProof proj then
-              unless ← isAbstractedUnassignedMVar args[i]! do
+              unless ← isAbstractedUnassignedMVar args[i] do
                 -- Skip expensive unification problem that is likely solved
                 -- using proof irrelevance.  We already know that `proj` and
-                -- `args[i]!` have the same type, so they're defeq in any case.
+                -- `args[i]` have the same type, so they're defeq in any case.
                 -- See comment at `isAbstractedUnassignedMVar`.
                 continue
-            trace[Meta.isDefEq.eta.struct] "{a} =?= {b} @ [{j}], {proj} =?= {args[i]!}"
-            unless (← isDefEq proj args[i]!) do
-              trace[Meta.isDefEq.eta.struct] "failed, unexpected arg #{i}, projection{indentExpr proj}\nis not defeq to{indentExpr args[i]!}"
+            trace[Meta.isDefEq.eta.struct] "{a} =?= {b} @ [{j}], {proj} =?= {args[i]}"
+            unless (← isDefEq proj args[i]) do
+              trace[Meta.isDefEq.eta.struct] "failed, unexpected arg #{i}, projection{indentExpr proj}\nis not defeq to{indentExpr args[i]}"
               return false
           return true
       else
diff --git a/src/Lean/Meta/FunInfo.lean b/src/Lean/Meta/FunInfo.lean
index 34d6e318aa..310208e36e 100644
--- a/src/Lean/Meta/FunInfo.lean
+++ b/src/Lean/Meta/FunInfo.lean
@@ -59,8 +59,8 @@ private def getFunInfoAux (fn : Expr) (maxArgs? : Option Nat) : MetaM FunInfo :=
       forallBoundedTelescope fnType maxArgs? fun fvars type => do
         let mut paramInfo := #[]
         let mut higherOrderOutParams : FVarIdSet := {}
-        for i in [:fvars.size] do
-          let fvar := fvars[i]!
+        for h: i in [:fvars.size] do
+          let fvar := fvars[i]
           let decl ← getFVarLocalDecl fvar
           let backDeps := collectDeps fvars decl.type
           let dependsOnHigherOrderOutParam :=
@@ -79,9 +79,9 @@ private def getFunInfoAux (fn : Expr) (maxArgs? : Option Nat) : MetaM FunInfo :=
               if let some outParamPositions := getOutParamPositions? (← getEnv) className then
                 unless outParamPositions.isEmpty do
                   let args := decl.type.getAppArgs
-                  for i in [:args.size] do
+                  for h2: i in [:args.size] do
                     if outParamPositions.contains i then
-                      let arg := args[i]!
+                      let arg := args[i]
                       if let some idx := fvars.indexOf? arg then
                         if (← whnf (← inferType arg)).isForall then
                           paramInfo := paramInfo.modify idx fun info => { info with higherOrderOutParam := true }
diff --git a/src/Lean/Meta/IndPredBelow.lean b/src/Lean/Meta/IndPredBelow.lean
index be390c010e..9a266a7ca2 100644
--- a/src/Lean/Meta/IndPredBelow.lean
+++ b/src/Lean/Meta/IndPredBelow.lean
@@ -119,8 +119,8 @@ where
       modifyBinders { vars with target := vars.target ++ xs, motives := xs } 0
 
   modifyBinders (vars : Variables) (i : Nat) := do
-    if i < vars.args.size then
-      let binder := vars.args[i]!
+    if h: i < vars.args.size then
+      let binder := vars.args[i]
       let binderType ← inferType binder
       if (← checkCount binderType) then
         mkBelowBinder vars binder binderType fun indValIdx x =>
@@ -372,8 +372,8 @@ where
       (rest : Expr)
       (belowIndices : Array Nat)
       (xIdx yIdx : Nat) : MetaM $ Array Nat := do
-    if xIdx ≥ xs.size then return belowIndices else
-    let x := xs[xIdx]!
+    if h: xIdx ≥ xs.size then return belowIndices else
+    let x := xs[xIdx]
     let xTy ← inferType x
     let yTy := rest.bindingDomain!
     if (← isDefEq xTy yTy) then
diff --git a/src/Lean/Meta/PProdN.lean b/src/Lean/Meta/PProdN.lean
index 3c2b7f3556..d9685faa72 100644
--- a/src/Lean/Meta/PProdN.lean
+++ b/src/Lean/Meta/PProdN.lean
@@ -115,8 +115,8 @@ It returns a dummy motive `(xs : ) → PUnit` or `(xs : … ) → True` if no ex
 
 -/
 def packLambdas (type : Expr) (es : Array Expr) : MetaM Expr := do
-  if es.size = 1 then
-    return es[0]!
+  if h: es.size = 1 then
+    return es[0]
   forallTelescope type fun xs sort => do
     assert! sort.isSort
     -- NB: Use beta, not instantiateLambda; when constructing the belowDict below
@@ -131,8 +131,8 @@ The value analogue to `PProdN.packLambdas`.
 It is the identity if `es.size = 1`.
 -/
 def mkLambdas (type : Expr) (es : Array Expr) : MetaM Expr := do
-  if es.size = 1 then
-    return es[0]!
+  if h: es.size = 1 then
+    return es[0]
   forallTelescope type fun xs body => do
     let lvl ← getLevel body
     let es' := es.map (·.beta xs)
diff --git a/src/Lean/Meta/RecursorInfo.lean b/src/Lean/Meta/RecursorInfo.lean
index 342f93e4ac..bcb53f01d2 100644
--- a/src/Lean/Meta/RecursorInfo.lean
+++ b/src/Lean/Meta/RecursorInfo.lean
@@ -182,13 +182,13 @@ private def getUnivLevelPos (declName : Name) (lparams : List Name) (motiveLvl :
 private def getProduceMotiveAndRecursive (xs : Array Expr) (numParams numIndices majorPos : Nat) (motive : Expr) : MetaM (List Bool × Bool) := do
   let mut produceMotive := #[]
   let mut recursor      := false
-  for i in [:xs.size] do
+  for h: i in [:xs.size] do
     if i < numParams + 1 then
       continue --skip parameters and motive
     if majorPos - numIndices ≤ i && i ≤ majorPos then
       continue -- skip indices and major premise
     -- process minor premise
-    let x := xs[i]!
+    let x := xs[i]
     let xType ← inferType x
     (produceMotive, recursor) ← forallTelescopeReducing xType fun minorArgs minorResultType => minorResultType.withApp fun res _ => do
       let produceMotive := produceMotive.push (res == motive)
diff --git a/src/Lean/Meta/Reduce.lean b/src/Lean/Meta/Reduce.lean
index e5144d08a5..9ffb557b21 100644
--- a/src/Lean/Meta/Reduce.lean
+++ b/src/Lean/Meta/Reduce.lean
@@ -26,8 +26,8 @@ partial def reduce (e : Expr) (explicitOnly skipTypes skipProofs := true) : Meta
           let finfo ← getFunInfoNArgs f nargs
           let mut args  := e.getAppArgs
           for i in [:args.size] do
-            if i < finfo.paramInfo.size then
-              let info := finfo.paramInfo[i]!
+            if h: i < finfo.paramInfo.size then
+              let info := finfo.paramInfo[i]
               if !explicitOnly || info.isExplicit then
                 args ← args.modifyM i visit
             else
diff --git a/src/Lean/Meta/SizeOf.lean b/src/Lean/Meta/SizeOf.lean
index 0947ca2e3c..f829e4070c 100644
--- a/src/Lean/Meta/SizeOf.lean
+++ b/src/Lean/Meta/SizeOf.lean
@@ -16,8 +16,8 @@ private partial def mkLocalInstances (params : Array Expr) (k : Array Expr → M
   loop 0 #[]
 where
   loop (i : Nat) (insts : Array Expr) : MetaM α := do
-    if i < params.size then
-      let param := params[i]!
+    if h: i < params.size then
+      let param := params[i]
       let paramType ← inferType param
       let instType? ← forallTelescopeReducing paramType fun xs _ => do
         let type := mkAppN param xs
@@ -67,8 +67,8 @@ private partial def mkSizeOfMotives (motiveFVars : Array Expr) (k : Array Expr 
   loop 0 #[]
 where
   loop (i : Nat) (motives : Array Expr) : MetaM α := do
-    if i < motiveFVars.size then
-      let type ← inferType motiveFVars[i]!
+    if h: i < motiveFVars.size then
+      let type ← inferType motiveFVars[i]
       let motive ← forallTelescopeReducing type fun xs _ => do
         mkLambdaFVars xs <| mkConst ``Nat
       trace[Meta.sizeOf] "motive: {motive}"
diff --git a/src/Lean/Meta/Tactic/ElimInfo.lean b/src/Lean/Meta/Tactic/ElimInfo.lean
index 7e954798f6..34d9a6115b 100644
--- a/src/Lean/Meta/Tactic/ElimInfo.lean
+++ b/src/Lean/Meta/Tactic/ElimInfo.lean
@@ -68,8 +68,8 @@ def getElimExprInfo (elimExpr : Expr) (baseDeclName? : Option Name := none) : Me
       | some targetPos => pure targetPos.val
     let mut altsInfo := #[]
     let env ← getEnv
-    for i in [:xs.size] do
-      let x := xs[i]!
+    for h: i in [:xs.size] do
+      let x := xs[i]
       if x != motive && !targets.contains x then
         let xDecl ← x.fvarId!.getDecl
         if xDecl.binderInfo.isExplicit then
diff --git a/src/Lean/Meta/Tactic/Simp/Rewrite.lean b/src/Lean/Meta/Tactic/Simp/Rewrite.lean
index f7bcb53b3f..f71a9855bc 100644
--- a/src/Lean/Meta/Tactic/Simp/Rewrite.lean
+++ b/src/Lean/Meta/Tactic/Simp/Rewrite.lean
@@ -320,8 +320,8 @@ def simpMatchDiscrs? (info : MatcherInfo) (e : Expr) : SimpM (Option Result) :=
       r ← mkCongrFun r argNew
   unless modified do
     return none
-  for i in [info.numDiscrs : args.size] do
-    let arg := args[i]!
+  for h: i in [info.numDiscrs : args.size] do
+    let arg := args[i]
     r ← mkCongrFun r arg
   return some r
 
diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index 3b560a839c..b5873f71f9 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -207,8 +207,8 @@ def unexpandStructureInstance (stx : Syntax) : Delab := whenPPOption getPPStruct
       `(⟨$[$(stx[1].getArgs)],*⟩)
   let args := e.getAppArgs
   let fieldVals := args.extract s.numParams args.size
-  for idx in [:fieldNames.size] do
-    let fieldName := fieldNames[idx]!
+  for h: idx in [:fieldNames.size] do
+    let fieldName := fieldNames[idx]
     if (← getPPOption getPPStructureInstancesFlatten) && (Lean.isSubobjectField? env s.induct fieldName).isSome then
       match stx[1][idx] with
       | `({ $fields',* $[: $_]?}) =>
@@ -397,9 +397,9 @@ def delabAppImplicitCore (unexpand : Bool) (numArgs : Nat) (delabHead : Delab) (
 
   -- Field notation
   if let some (fieldIdx, field) := field? then
-    if fieldIdx < args.size then
+    if h: fieldIdx < args.size then
       let obj? : Option Term ← do
-        let arg := args[fieldIdx]!
+        let arg := args[fieldIdx]
         if let .regular s := arg then
           withNaryArg fieldIdx <| some <$> stripParentProjections s
         else
@@ -491,8 +491,8 @@ def useAppExplicit (numArgs : Nat) (paramKinds : Array ParamKind) : DelabM Bool
   -- If there was an error collecting ParamKinds, fall back to explicit mode.
   if paramKinds.size < numArgs then return true
 
-  if numArgs < paramKinds.size then
-    let nextParam := paramKinds[numArgs]!
+  if h: numArgs < paramKinds.size then
+    let nextParam := paramKinds[numArgs]
 
     -- If the next parameter is implicit or inst implicit, fall back to explicit mode.
     -- This is necessary for `@Eq` for example.
@@ -741,8 +741,8 @@ where
       m acc
 
   usingNames {α} (varNames : Array Name) (x : DelabM α) (i : Nat := 0) : DelabM α :=
-    if i < varNames.size then
-      withBindingBody varNames[i]! <| usingNames varNames x (i+1)
+    if h: i < varNames.size then
+      withBindingBody varNames[i] <| usingNames varNames x (i+1)
     else
       x
 
diff --git a/src/Lean/Server/References.lean b/src/Lean/Server/References.lean
index 23758ac02b..b30b3792f7 100644
--- a/src/Lean/Server/References.lean
+++ b/src/Lean/Server/References.lean
@@ -312,8 +312,8 @@ where
 
   findCanonicalRepresentative (idMap : Std.HashMap RefIdent RefIdent) (id : RefIdent) : RefIdent := Id.run do
     let mut canonicalRepresentative := id
-    while idMap.contains canonicalRepresentative do
-      canonicalRepresentative := idMap[canonicalRepresentative]!
+    while h: idMap.contains canonicalRepresentative do
+      canonicalRepresentative := idMap[canonicalRepresentative]
     return canonicalRepresentative
 
   buildIdMap posMap := Id.run <| StateT.run' (s := Std.HashMap.empty) do