diff --git a/src/Init/Data/Array/QSort.lean b/src/Init/Data/Array/QSort.lean
index cb4947e7a4..2d46546d68 100644
--- a/src/Init/Data/Array/QSort.lean
+++ b/src/Init/Data/Array/QSort.lean
@@ -8,9 +8,9 @@ import Init.Data.Array.Basic
 
 namespace Array
 -- TODO: remove the [Inhabited α] parameters as soon as we have the tactic framework for automating proof generation and using Array.fget
--- TODO: remove `partial` using well-founded recursion
 
-@[inline] def qpartition {α : Type} [Inhabited α] (as : Array α) (lt : α → α → Bool) (lo hi : Nat) : Nat × Array α :=
+def qpartition (as : Array α) (lt : α → α → Bool) (lo hi : Nat) : Nat × Array α :=
+  if h : as.size = 0 then (0, as) else have : Inhabited α := ⟨as[0]'(by revert h; cases as.size <;> simp [Nat.zero_lt_succ])⟩ -- TODO: remove
   let mid := (lo + hi) / 2
   let as  := if lt (as.get! mid) (as.get! lo) then as.swap! lo mid else as
   let as  := if lt (as.get! hi)  (as.get! lo) then as.swap! lo hi  else as
@@ -29,7 +29,7 @@ namespace Array
   loop as lo lo
 termination_by _ => hi - j
 
-@[inline] partial def qsort {α : Type} [Inhabited α] (as : Array α) (lt : α → α → Bool) (low := 0) (high := as.size - 1) : Array α :=
+@[inline] partial def qsort (as : Array α) (lt : α → α → Bool) (low := 0) (high := as.size - 1) : Array α :=
   let rec @[specialize] sort (as : Array α) (low high : Nat) :=
     if low < high then
       let p := qpartition as lt low high;
diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean
index 35c715cf1f..19974724a9 100644
--- a/src/Lean/CoreM.lean
+++ b/src/Lean/CoreM.lean
@@ -46,7 +46,6 @@ structure State where
   messages        : MessageLog     := {}
   /-- Info tree. We have the info tree here because we want to update it while adding attributes. -/
   infoState       : Elab.InfoState := {}
-  deriving Inhabited
 
 /-- Context for the CoreM monad. -/
 structure Context where
diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 3d93538354..d878e30ac8 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -1428,12 +1428,14 @@ private def mergeFailures (failures : Array (TermElabResult Expr)) : TermElabM 
 
 private def elabAppAux (f : Syntax) (namedArgs : Array NamedArg) (args : Array Arg) (ellipsis : Bool) (expectedType? : Option Expr) : TermElabM Expr := do
   let candidates ← elabAppFn f [] namedArgs args expectedType? (explicit := false) (ellipsis := ellipsis) (overloaded := false) #[]
-  if candidates.size == 1 then
-    applyResult candidates[0]!
+  if h : candidates.size = 1 then
+    have : 0 < candidates.size := by rw [h]; decide
+    applyResult candidates[0]
   else
     let successes ← getSuccesses candidates
-    if successes.size == 1 then
-      applyResult successes[0]!
+    if h : successes.size = 1 then
+      have : 0 < successes.size := by rw [h]; decide
+      applyResult successes[0]
     else if successes.size > 1 then
       let msgs : Array MessageData ← successes.mapM fun success => do
         match success with
diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 14754ed5a9..e6430a11b8 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -32,7 +32,6 @@ structure State where
   ngen           : NameGenerator := {}
   infoState      : InfoState := {}
   traceState     : TraceState := {}
-  deriving Inhabited
 
 structure Context where
   fileName       : String
diff --git a/src/Lean/Elab/InfoTree/Types.lean b/src/Lean/Elab/InfoTree/Types.lean
index 647e2624cd..afd685518c 100644
--- a/src/Lean/Elab/InfoTree/Types.lean
+++ b/src/Lean/Elab/InfoTree/Types.lean
@@ -23,7 +23,6 @@ structure ContextInfo where
   currNamespace : Name           := Name.anonymous
   openDecls     : List OpenDecl  := []
   ngen          : NameGenerator -- We must save the name generator to implement `ContextInfo.runMetaM` and making we not create `MVarId`s used in `mctx`.
-  deriving Inhabited
 
 /-- Base structure for `TermInfo`, `CommandInfo` and `TacticInfo`. -/
 structure ElabInfo where
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index a22063efd0..b5a0ee2ade 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -131,7 +131,6 @@ structure Snapshot where
   term   : Term.State
   tactic : Tactic.State
   stx    : Syntax
-  deriving Inhabited
 
 /--
   Key for the cache used to implement the `save` tactic.
@@ -242,7 +241,6 @@ instance : Inhabited (TermElabM α) where
 structure SavedState where
   meta   : Meta.SavedState
   «elab» : State
-  deriving Inhabited
 
 protected def saveState : TermElabM SavedState :=
   return { meta := (← Meta.saveState), «elab» := (← get) }
@@ -262,9 +260,6 @@ instance : MonadBacktrack SavedState TermElabM where
 
 abbrev TermElabResult (α : Type) := EStateM.Result Exception SavedState α
 
-instance [Inhabited α] : Inhabited (TermElabResult α) where
-  default := EStateM.Result.ok default default
-
 /--
   Execute `x`, save resulting expression and new state.
   We remove any `Info` created by `x`.
diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index f7382565d9..78d914754d 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -24,7 +24,7 @@ def ModuleIdx := Nat
 
 abbrev ModuleIdx.toNat (midx : ModuleIdx) : Nat := midx
 
-instance : Inhabited ModuleIdx := inferInstanceAs (Inhabited Nat)
+instance : Inhabited ModuleIdx where default := (0 : Nat)
 
 abbrev ConstMap := SMap Name ConstantInfo
 
@@ -143,7 +143,9 @@ structure Environment where
   extraConstNames : NameSet
   /-- The header contains additional information that is not updated often. -/
   header       : EnvironmentHeader := {}
-  deriving Inhabited
+
+instance : Nonempty Environment :=
+  ⟨by refine' {..} <;> exact default⟩
 
 namespace Environment
 
@@ -299,6 +301,7 @@ unsafe def setState {σ} (ext : Ext σ) (env : Environment) (s : σ) : Environme
   if h : ext.idx < env.extensions.size then
     { env with extensions := env.extensions.set ⟨ext.idx, h⟩ (unsafeCast s) }
   else
+    have : Inhabited Environment := ⟨env⟩
     panic! invalidExtMsg
 
 @[inline] unsafe def modifyState {σ : Type} (ext : Ext σ) (env : Environment) (f : σ → σ) : Environment :=
@@ -309,6 +312,7 @@ unsafe def setState {σ} (ext : Ext σ) (env : Environment) (s : σ) : Environme
         let s : σ := f s
         unsafeCast s }
   else
+    have : Inhabited Environment := ⟨env⟩
     panic! invalidExtMsg
 
 unsafe def getState {σ} [Inhabited σ] (ext : Ext σ) (env : Environment) : σ :=
@@ -555,6 +559,7 @@ instance : Inhabited TagDeclarationExtension :=
   inferInstanceAs (Inhabited (SimplePersistentEnvExtension Name NameSet))
 
 def tag (ext : TagDeclarationExtension) (env : Environment) (declName : Name) : Environment :=
+  have : Inhabited Environment := ⟨env⟩
   assert! env.getModuleIdxFor? declName |>.isNone -- See comment at `TagDeclarationExtension`
   ext.addEntry env declName
 
@@ -584,6 +589,7 @@ instance : Inhabited (MapDeclarationExtension α) :=
   inferInstanceAs (Inhabited (SimplePersistentEnvExtension ..))
 
 def insert (ext : MapDeclarationExtension α) (env : Environment) (declName : Name) (val : α) : Environment :=
+  have : Inhabited Environment := ⟨env⟩
   assert! env.getModuleIdxFor? declName |>.isNone -- See comment at `MapDeclarationExtension`
   ext.addEntry env (declName, val)
 
diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index 9cd6660552..7455c1726a 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -261,7 +261,6 @@ structure State where
 structure SavedState where
   core        : Core.State
   meta        : State
-  deriving Inhabited
 
 /--
   Contextual information for the `MetaM` monad.
diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
index e19db48b0e..c0ffdd37e1 100644
--- a/src/Lean/Server/FileWorker.lean
+++ b/src/Lean/Server/FileWorker.lean
@@ -90,7 +90,7 @@ section Elab
       : AsyncElabM (Option Snapshot) := do
     cancelTk.check
     let s ← get
-    let lastSnap := s.snaps.back
+    let .some lastSnap := s.snaps.back? | panic! "empty snapshots"
     if lastSnap.isAtEnd then
       publishDiagnostics m lastSnap.diagnostics.toArray ctx.hOut
       publishProgressDone m ctx.hOut
@@ -123,7 +123,7 @@ section Elab
   def unfoldCmdSnaps (m : DocumentMeta) (snaps : Array Snapshot) (cancelTk : CancelToken) (startAfterMs : UInt32)
       : ReaderT WorkerContext IO (AsyncList ElabTaskError Snapshot) := do
     let ctx ← read
-    let headerSnap := snaps[0]!
+    let some headerSnap := snaps[0]? | panic! "empty snapshots"
     if headerSnap.msgLog.hasErrors then
       -- Treat header processing errors as fatal so users aren't swamped with
       -- followup errors
@@ -290,17 +290,16 @@ section Updates
         cancelTk.check
         IO.Process.exit 2
     else EIO.mapTask (ε := ElabTaskError) (t := headSnapTask) (prio := .dedicated) fun headSnap?? => do
-      let headSnap? ← MonadExcept.ofExcept headSnap??
       -- There is always at least one snapshot absent exceptions
-      let headSnap := headSnap?.get!
+      let some headSnap ← MonadExcept.ofExcept headSnap?? | panic! "empty snapshots"
       let newHeaderSnap := { headSnap with stx := newHeaderStx, mpState := newMpState }
       let changePos := oldDoc.meta.text.source.firstDiffPos newMeta.text.source
       -- Ignore exceptions, we are only interested in the successful snapshots
       let (cmdSnaps, _) ← oldDoc.cmdSnaps.getFinishedPrefix
       -- NOTE(WN): we invalidate eagerly as `endPos` consumes input greedily. To re-elaborate only
       -- when really necessary, we could do a whitespace-aware `Syntax` comparison instead.
-      let mut validSnaps := cmdSnaps.takeWhile (fun s => s.endPos < changePos)
-      if validSnaps.length ≤ 1 then
+      let mut validSnaps ← pure (cmdSnaps.takeWhile (fun s => s.endPos < changePos))
+      if h : validSnaps.length ≤ 1 then
         validSnaps := [newHeaderSnap]
       else
         /- When at least one valid non-header snap exists, it may happen that a change does not fall
@@ -308,10 +307,12 @@ section Updates
            We check for this here. We do not currently handle crazy grammars in which an appended
            token can merge two or more previous commands into one. To do so would require reparsing
            the entire file. -/
-        let mut lastSnap := validSnaps.getLast!
-        let preLastSnap := if validSnaps.length ≥ 2
-          then validSnaps.get! (validSnaps.length - 2)
-          else newHeaderSnap
+        have : validSnaps.length ≥ 2 := Nat.gt_of_not_le h
+        let mut lastSnap := validSnaps.getLast (by subst ·; simp at h)
+        let preLastSnap :=
+          have : 0 < validSnaps.length := Nat.lt_of_lt_of_le (by decide) this
+          have : validSnaps.length - 2 < validSnaps.length := Nat.sub_lt this (by decide)
+          validSnaps[validSnaps.length - 2]
         let newLastStx ← parseNextCmd newMeta.mkInputContext preLastSnap
         if newLastStx != lastSnap.stx then
           validSnaps := validSnaps.dropLast
diff --git a/src/Lean/Server/References.lean b/src/Lean/Server/References.lean
index 020ac7856f..44fb928f3c 100644
--- a/src/Lean/Server/References.lean
+++ b/src/Lean/Server/References.lean
@@ -21,7 +21,6 @@ structure Reference where
   ci : ContextInfo
   info : Info
   isBinder : Bool
-  deriving Inhabited
 
 structure RefInfo where
   definition : Option Reference
diff --git a/src/Lean/Server/Snapshots.lean b/src/Lean/Server/Snapshots.lean
index 474692c36d..f4e2b76bf6 100644
--- a/src/Lean/Server/Snapshots.lean
+++ b/src/Lean/Server/Snapshots.lean
@@ -39,16 +39,6 @@ structure Snapshot where
   interactiveDiags : PersistentArray Widget.InteractiveDiagnostic
   tacticCache : IO.Ref Tactic.Cache
 
-instance : Inhabited Snapshot where
-  default := {
-    beginPos         := default
-    stx              := default
-    mpState          := default
-    cmdState         := default
-    interactiveDiags := default
-    tacticCache      := dummyTacticCache
-  }
-
 namespace Snapshot
 
 def endPos (s : Snapshot) : String.Pos :=
diff --git a/src/Lean/Widget/Basic.lean b/src/Lean/Widget/Basic.lean
index 4fe67fa7ea..65ff340185 100644
--- a/src/Lean/Widget/Basic.lean
+++ b/src/Lean/Widget/Basic.lean
@@ -18,7 +18,7 @@ functionality is purpose-specific to showing the contents of infoview popups.
 structure InfoWithCtx where
   ctx  : Elab.ContextInfo
   info : Elab.Info
-  deriving Inhabited, TypeName
+  deriving TypeName
 
 deriving instance TypeName for MessageData
 
diff --git a/src/Lean/Widget/InteractiveCode.lean b/src/Lean/Widget/InteractiveCode.lean
index fa3ee0da3b..f7a6162320 100644
--- a/src/Lean/Widget/InteractiveCode.lean
+++ b/src/Lean/Widget/InteractiveCode.lean
@@ -36,7 +36,7 @@ structure SubexprInfo where
   -- kind : Lsp.SymbolKind
   /-- Ask the renderer to highlight this node in the given color. -/
   diffStatus? : Option DiffTag := none
-  deriving Inhabited, RpcEncodable
+  deriving RpcEncodable
 
 /-- Pretty-printed syntax (usually but not necessarily an `Expr`) with embedded `Info`s. -/
 abbrev CodeWithInfos := TaggedText SubexprInfo
diff --git a/src/lake b/src/lake
index 5a54cfe427..d0b530530f 160000
--- a/src/lake
+++ b/src/lake
@@ -1 +1 @@
-Subproject commit 5a54cfe4272046ef770c1a00eb26d60e772f4e89
+Subproject commit d0b530530f14dde97a547b03abf87eee06360d60