diff --git a/examples/textbook/DemoTextbook.lean b/examples/textbook/DemoTextbook.lean
index 17f5eab3f..5fd0460b7 100644
--- a/examples/textbook/DemoTextbook.lean
+++ b/examples/textbook/DemoTextbook.lean
@@ -82,7 +82,7 @@ Expected error messages must be indicated explicitly:
 #eval y
 ```
 ```leanOutput yVal
-unknown identifier 'y'
+Unknown identifier `y`
 ```
 
 {include 1 DemoTextbook.Nat}
diff --git a/examples/website/DemoSite/Blog/Conditionals.lean b/examples/website/DemoSite/Blog/Conditionals.lean
index 3dbf396cf..81eaff40c 100644
--- a/examples/website/DemoSite/Blog/Conditionals.lean
+++ b/examples/website/DemoSite/Blog/Conditionals.lean
@@ -234,12 +234,12 @@ Here's some hoverable info:
 example : Nat := "Not a number"
 ```
 ```leanOutput typeErr
-type mismatch
+Type mismatch
   "Not a number"
 has type
-  String : Type
+  String
 but is expected to have type
-  Nat : Type
+  Nat
 ```
 
 
diff --git a/lake-manifest.json b/lake-manifest.json
index 33b0c823c..db92c5871 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "b16338c5c66f57ef5510d4334eb6fa4e2c6c8cd8",
+   "rev": "feac4e0c356b0928657bf3b54fa83ae952f53257",
    "name": "MD4Lean",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/lean-toolchain b/lean-toolchain
index 2c6e1c4ba..c7e310c44 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.22.0-rc4
+leanprover/lean4:v4.23.0-rc1
diff --git a/src/multi-verso/MultiVerso.lean b/src/multi-verso/MultiVerso.lean
index 021af12b3..4b5ea89ae 100644
--- a/src/multi-verso/MultiVerso.lean
+++ b/src/multi-verso/MultiVerso.lean
@@ -341,7 +341,7 @@ private def RemoteInfo.structBEq (x y : RemoteInfo) : Bool :=
   x1 == x2 &&
   y1 == y2 &&
   doms1.size == doms2.size &&
-  doms1.fold (init := true) fun soFar k v =>
+  doms1.foldl (init := true) fun soFar k v =>
     soFar && (doms2.find? k).isEqSome v
 
 private unsafe def RemoteInfo.fastBEq (x y : RemoteInfo) : Bool :=
diff --git a/src/multi-verso/MultiVerso/Slug.lean b/src/multi-verso/MultiVerso/Slug.lean
index 84e7ad60a..8c3af9646 100644
--- a/src/multi-verso/MultiVerso/Slug.lean
+++ b/src/multi-verso/MultiVerso/Slug.lean
@@ -13,28 +13,95 @@ open Verso.Method
 open Lean (ToJson FromJson)
 open Std (HashSet)
 
+private def validCharString := "abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789-_"
+
+
 /-- The characters allowed in slugs. -/
-def Slug.validChars := HashSet.ofList "abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789-_".toList
+def Slug.validChars := HashSet.ofList validCharString.toList
+
+/--
+A slug is well-formed if all its characters are valid.
+-/
+def Slug.WF (str : String) : Prop :=
+  str.toList.all (· ∈ validChars)
+
+open Lean Elab Command in
+#eval show CommandElabM Unit from do
+  let mut iter := validCharString.iter
+  while h : iter.hasNext do
+    let c := iter.curr' h
+    iter := iter.next' h
+    let n := mkIdent <| `Slug ++ (.str .anonymous s!"'{c}'_mem_validChars")
+    let cmd ←
+      `(@[simp, grind] protected theorem $n : ($(quote c) ∈ Slug.validChars) := by simp [Slug.validChars, validCharString])
+    elabCommand cmd
+
 
 private def mangle (c : Char) : String :=
-  match c with
-  | '<' => "_LT_"
-  | '>' => "_GT_"
-  | ';' => "_SEMI_"
-  | '‹' => "_FLQ_"
-  | '›' => "_FRQ_"
-  | '«' => "_FLQQ_"
-  | '»' => "_FLQQ_"
-  | '⟨' => "_LANGLE_"
-  | '⟩' => "_RANGLE_"
-  | '(' => "_LPAR_"
-  | ')' => "_RPAR_"
-  | '[' => "_LSQ_"
-  | ']' => "_RSQ_"
-  | '→' => "_ARR_"
-  | '↦' => "_MAPSTO_"
-  | '⊢' => "_VDASH_"
-  | _ => "___"
+  replacements.lookup c |>.getD "___"
+where
+  replacements : List (Char × String) := [
+    ('<', "_LT_"),
+    ('>', "_GT_"),
+    (';', "_SEMI_"),
+    ('‹', "_FLQ_"),
+    ('›', "_FRQ_"),
+    ('«', "_FLQQ_"),
+    ('»', "_FLQQ_"),
+    ('⟨', "_LANGLE_"),
+    ('⟩', "_RANGLE_"),
+    ('(', "_LPAR_"),
+    (')', "_RPAR_"),
+    ('[', "_LSQ_"),
+    (']', "_RSQ_"),
+    ('→', "_ARR_"),
+    ('↦', "_MAPSTO_"),
+    ('⊢', "_VDASH_")
+  ]
+
+
+@[simp, grind] theorem mangle.replacements_all_wf : (k, v) ∈ mangle.replacements → Slug.WF v := by
+  simp [Slug.WF, replacements]
+  intro
+  repeat (rename_i hk; cases hk; simp [*])
+
+@[simp, grind]
+private theorem mangle.replacements_wf (c : Char) : (c, s) ∈ mangle.replacements → Slug.WF (mangle c) := by
+  unfold mangle
+  generalize h : mangle.replacements = reps
+  have : ∀ k v, (k, v) ∈ reps → Slug.WF v := by
+    rw [← h]
+    grind only [=_ List.contains_iff_mem, mangle.replacements_all_wf]
+  clear h
+  fun_induction List.lookup <;> first | grind | simp
+
+@[simp, grind]
+private theorem mangle_wf (c : Char) : Slug.WF (mangle c) := by
+  unfold mangle
+  by_cases h : ∃ s, (c, s) ∈ mangle.replacements
+  . let ⟨w, p⟩ := h
+    apply mangle.replacements_wf _ p
+  . suffices List.lookup c mangle.replacements = none by
+      rw [this]
+      simp [Slug.WF]
+    generalize h' : mangle.replacements = xs
+    rw [h'] at h
+    clear h'
+    fun_induction List.lookup with try ((first | grind | simp); done)
+    | case2 _ _ _ _ beq =>
+      have := LawfulBEq.eq_of_beq beq
+      exfalso
+      apply h
+      simp [*]
+
+
+@[simp, grind]
+private theorem mangle_mem_valid (c : Char) : c ∈ (mangle c').data → c ∈ Slug.validChars := by
+  intro mem
+  have := mangle_wf c'
+  simp [Slug.WF] at this
+  apply this
+  assumption
 
 /--
 Converts a string to a valid slug, mangling as appropriate.
@@ -50,16 +117,13 @@ def asSlug (str : String) : String :=
         else acc ++ mangle c
   loop str.iter ""
 
-/--
-A slug is well-formed if all its characters are valid.
--/
-def Slug.WF (str : String) : Prop :=
-  str.toList.all (· ∈ validChars)
-
 instance : Decidable (c ∈ Slug.validChars) := inferInstance
 
 instance [DecidablePred p] : Decidable (String.all s (p ·)) :=
-  if h : String.all s (p ·) then isTrue h else isFalse h
+  if h : String.all s (p ·) then
+    isTrue h
+  else
+    isFalse h
 
 @[simp]
 theorem String.empty_all_eq_true : "".all p = true := by
@@ -68,59 +132,53 @@ theorem String.empty_all_eq_true : "".all p = true := by
 @[simp]
 theorem String.Pos.add_0_eq_size {c : Char} : (0 : String.Pos) + c = ⟨c.utf8Size⟩ := by
   simp only [HAdd.hAdd, String.Pos.byteIdx_zero, String.Pos.mk.injEq]
-  show 0 + c.utf8Size = c.utf8Size
-  simp
+  grind
 
 instance : DecidablePred Slug.WF := fun str =>
-  if h : str.toList.all (· ∈ Slug.validChars) then isTrue (by unfold Slug.WF; exact h) else isFalse h
-
-@[simp]
-theorem Slug.wf_mangle : WF (mangle c) := by
-  unfold mangle
-  split <;> dsimp [WF, validChars] <;> simp
+  if h : str.toList.all (· ∈ Slug.validChars) then
+    isTrue h
+  else
+    isFalse h
 
+@[grind]
 theorem Slug.wf_push (c str) : c ∈ validChars → WF str → WF (str.push c) := by
   unfold WF
   cases str
   intro mem wf
+  simp only [String.toList, List.all_eq_true, decide_eq_true_eq] at wf
   simp only [String.toList, String.data_push, List.all_append, List.all_cons, List.all_nil,
     Bool.and_true, Bool.and_eq_true, List.all_eq_true, decide_eq_true_eq]
-  and_intros <;> simp at wf <;> assumption
+  grind only
 
+@[grind]
 theorem Slug.wf_append (str1 str2) : WF str1 → WF str2 → WF (str1 ++ str2) := by
   unfold WF
   cases str1; cases str2
   intro wf1 wf2
   simp only [String.toList, String.data_append, List.all_append, Bool.and_eq_true, List.all_eq_true, decide_eq_true_eq]
   simp only [String.toList, List.all_eq_true, decide_eq_true_eq] at wf1 wf2
-  and_intros <;> assumption
+  grind only
+
+@[simp]
+theorem Slug.decide_WF_eq_wf (s : String) : (s.toList.all (fun x => decide (x ∈ validChars)) = true) = WF s := by
+  rfl
+
+@[grind, simp]
+theorem Slug.wf_forall : WF s → c ∈ s.data → c ∈ validChars := by
+  intro wf h
+  simp_all [WF]
 
 theorem Slug.asSlug_loop_valid : WF acc → WF (asSlug.loop iter acc) := by
   intro wfAcc
-  induction iter, acc using asSlug.loop.induct <;> unfold asSlug.loop <;> simp [*]
-  case case2 iter acc notEnd c ih =>
+  fun_induction asSlug.loop with try assumption
+  | case2 iter acc notEnd c ih =>
     apply ih
     unfold WF
-    simp only [WF, String.toList, List.all_eq_true, decide_eq_true_eq] at wfAcc
-    split
-    . simp only [String.toList, String.data_push, List.all_append, List.all_cons, List.all_nil,
-      Bool.and_true, Bool.and_eq_true, List.all_eq_true, decide_eq_true_eq]
-      and_intros <;> assumption
-    . split
-      . simp only [String.toList, ↓Char.isValue, String.data_push, List.all_append, List.all_cons,
-        List.all_nil, Bool.and_true, Bool.and_eq_true, List.all_eq_true, decide_eq_true_eq]
-        and_intros
-        . assumption
-        . simp [validChars]
-      . simp only [String.toList, String.data_append, List.all_append, Bool.and_eq_true,
-        List.all_eq_true, decide_eq_true_eq]
-        and_intros
-        . assumption
-        . intro c' mem
-          have : WF (mangle c) := wf_mangle
-          simp only [WF, String.toList, List.all_eq_true, decide_eq_true_eq] at this
-          simp [*]
+    (repeat' split) <;>
+      simp [*] <;>
+      grind only [=_ List.contains_iff_mem, List.contains_eq_mem, mangle_wf, wf_forall, mangle_mem_valid, wf_append, cases Or]
 
+@[grind]
 theorem Slug.asSlug_valid : WF (asSlug str) := by
   unfold asSlug
   apply asSlug_loop_valid
diff --git a/src/verso-blog/VersoBlog.lean b/src/verso-blog/VersoBlog.lean
index e68af6607..bb32018cd 100644
--- a/src/verso-blog/VersoBlog.lean
+++ b/src/verso-blog/VersoBlog.lean
@@ -21,7 +21,6 @@ import Verso.Doc.Suggestion
 import Verso.Hover
 import Verso.WithoutAsync
 open Verso.Output Html
-open Lean (RBMap)
 
 namespace Verso.Genre.Blog
 
diff --git a/src/verso-blog/VersoBlog/Basic.lean b/src/verso-blog/VersoBlog/Basic.lean
index 2f57e3720..19b8015ba 100644
--- a/src/verso-blog/VersoBlog/Basic.lean
+++ b/src/verso-blog/VersoBlog/Basic.lean
@@ -178,7 +178,7 @@ structure TraverseContext where
   components : Components
 
 structure TraverseState where
-  usedIds : Lean.RBMap (List String) (HashSet String) compare := {}
+  usedIds : Std.HashMap (List String) (HashSet String) := {}
   targets : Lean.NameMap Blog.Info.Target := {}
   blogs : Lean.NameMap Blog.Info.ArchivesMeta := {}
   refs : Lean.NameMap Blog.Info.Ref := {}
@@ -334,7 +334,7 @@ defmethod BlogPost.summary (post : BlogPost) : Array (Block Post) := Id.run do
 
 partial def TraverseState.freshId (state : Blog.TraverseState) (path : List String) (hint : Lean.Name) : String := Id.run do
   let mut idStr := mangle (toString hint)
-  match state.usedIds.find? path with
+  match state.usedIds[path]? with
   | none => return idStr
   | some used =>
     while used.contains idStr do
diff --git a/src/verso-blog/VersoBlog/Component.lean b/src/verso-blog/VersoBlog/Component.lean
index e3cc344a6..af52ef712 100644
--- a/src/verso-blog/VersoBlog/Component.lean
+++ b/src/verso-blog/VersoBlog/Component.lean
@@ -138,8 +138,8 @@ deriving TypeName
 
 open Lean in
 def Components.fromLists (blocks : List (Name × BlockComponent)) (inlines : List (Name × InlineComponent)) : Components where
-  blocks := .fromList (blocks.map fun (x, b) => (x, Dynamic.mk b)) _
-  inlines := .fromList (inlines.map fun (x, b) => (x, Dynamic.mk b)) _
+  blocks := .ofList (blocks.map fun (x, b) => (x, Dynamic.mk b)) _
+  inlines := .ofList (inlines.map fun (x, b) => (x, Dynamic.mk b)) _
 
 open Lean in
 private def nameAndDef [Monad m] [MonadRef m] [MonadQuotation m] (ext : Name × Name) : m Term := do
diff --git a/src/verso-blog/VersoBlog/Component/Ext.lean b/src/verso-blog/VersoBlog/Component/Ext.lean
index 2e2432164..719b4493a 100644
--- a/src/verso-blog/VersoBlog/Component/Ext.lean
+++ b/src/verso-blog/VersoBlog/Component/Ext.lean
@@ -15,7 +15,7 @@ initialize blockComponentExt :
     addImportedFn := fun _ => pure {},
     addEntryFn := fun as (src, tgt) => as.insert src tgt,
     exportEntriesFn := fun es =>
-      es.fold (fun a src tgt => a.push (src, tgt)) #[] |>.qsort (Name.quickLt ·.1 ·.1)
+      es.foldl (fun a src tgt => a.push (src, tgt)) #[] |>.qsort (Name.quickLt ·.1 ·.1)
   }
 
 initialize inlineComponentExt :
@@ -25,5 +25,5 @@ initialize inlineComponentExt :
     addImportedFn := fun _ => pure {},
     addEntryFn := fun as (src, tgt) => as.insert src tgt,
     exportEntriesFn := fun es =>
-      es.fold (fun a src tgt => a.push (src, tgt)) #[] |>.qsort (Name.quickLt ·.1 ·.1)
+      es.foldl (fun a src tgt => a.push (src, tgt)) #[] |>.qsort (Name.quickLt ·.1 ·.1)
   }
diff --git a/src/verso-blog/VersoBlog/Template.lean b/src/verso-blog/VersoBlog/Template.lean
index d14dbcc08..4bd510499 100644
--- a/src/verso-blog/VersoBlog/Template.lean
+++ b/src/verso-blog/VersoBlog/Template.lean
@@ -17,8 +17,7 @@ import Verso.Output.Html
 import Verso.Output.Html.CssVars
 import Verso.Code
 
-open Std (HashSet)
-open Lean (RBMap)
+open Std (HashSet TreeMap)
 
 open Verso Doc Output Html HtmlT
 open Verso.Genre Blog
@@ -52,9 +51,9 @@ instance : Coe Html Template.Params.Val where
    | other => ⟨.mk other, #[]⟩
 
 
-def Params := RBMap String Params.Val compare
+def Params := TreeMap String Params.Val
 
-instance : EmptyCollection Params := inferInstanceAs <| EmptyCollection (RBMap _ _ _)
+instance : EmptyCollection Params := inferInstanceAs <| EmptyCollection (TreeMap _ _ _)
 
 inductive Error where
   | missingParam (param : String)
@@ -258,16 +257,16 @@ namespace Verso.Genre.Blog.Template
 namespace Params
 
 def ofList (params : List (String × Val)) : Params :=
-  Lean.RBMap.ofList params
+  Std.TreeMap.ofList params _
 
 def toList (params : Params) : List (String × Val) :=
-  Lean.RBMap.toList params
+  Std.TreeMap.toList params
 
 def insert (params : Params) (key : String) (val : Val) : Params :=
-  Lean.RBMap.insert params key val
+  Std.TreeMap.insert params key val
 
 def erase (params : Params) (key : String) : Params :=
-  Lean.RBMap.erase params key
+  Std.TreeMap.erase params key
 
 
 end Params
@@ -287,7 +286,7 @@ namespace Template
 
 def param? [TypeName α] (key : String) : TemplateM (Option α) := do
   let ctx ← readThe Context
-  match ctx.params.find? key with
+  match ctx.params.get? key with
   | none => return none
   | some val =>
     if let some v := val.get? (α := α) then return (some v)
@@ -295,7 +294,7 @@ def param? [TypeName α] (key : String) : TemplateM (Option α) := do
 
 
 def param [TypeName α] (key : String) : TemplateM α := do
-  match (← read).params.find? key with
+  match (← read).params.get? key with
   | none => throw <| .missingParam key
   | some val =>
     if let some v := val.get? (α := α) then return v
diff --git a/src/verso-manual/VersoManual/Basic.lean b/src/verso-manual/VersoManual/Basic.lean
index 85317d7b5..03c68a4b7 100644
--- a/src/verso-manual/VersoManual/Basic.lean
+++ b/src/verso-manual/VersoManual/Basic.lean
@@ -222,7 +222,7 @@ instance : BEq Domains where
     x.all fun k v => y.find? k |>.isEqSome v
 
 instance : GetElem Domains Name Domain (fun ds d => ds.contents.contains d) where
-  getElem ds d _ok := ds.contents.find! d
+  getElem ds d _ok := ds.contents.get! d
 
 instance : GetElem? Domains Name Domain (fun ds d => ds.contents.contains d) where
   getElem? ds d := ds.contents.find? d
diff --git a/src/verso-manual/VersoManual/Bibliography.lean b/src/verso-manual/VersoManual/Bibliography.lean
index 400d8c081..51a194688 100644
--- a/src/verso-manual/VersoManual/Bibliography.lean
+++ b/src/verso-manual/VersoManual/Bibliography.lean
@@ -63,6 +63,9 @@ structure ArXiv where
   id : String
 deriving ToJson, FromJson, BEq, Hashable, Ord
 
+section
+attribute [local instance] lexOrd
+
 structure Article where
   title : Doc.Inline Manual
   authors : Array (Doc.Inline Manual)
@@ -74,6 +77,7 @@ structure Article where
   pages : Option (Nat × Nat) := none
   url : Option String := none
 deriving ToJson, FromJson, BEq, Hashable, Ord
+end
 
 inductive Citable where
   | inProceedings : InProceedings → Citable
diff --git a/src/verso-manual/VersoManual/Docstring.lean b/src/verso-manual/VersoManual/Docstring.lean
index 5ca72ff5d..5d7f0b3a8 100644
--- a/src/verso-manual/VersoManual/Docstring.lean
+++ b/src/verso-manual/VersoManual/Docstring.lean
@@ -37,7 +37,7 @@ open Lean Elab
 open Verso.Genre.Manual.Docstring
 open Verso.Doc.Suggestion
 
-variable {m} [Monad m] [MonadOptions m] [MonadEnv m] [MonadLiftT CoreM m] [MonadError m] [MonadLog m] [AddMessageContext m] [MonadInfoTree m]
+variable {m} [Monad m] [MonadOptions m] [MonadEnv m] [MonadLiftT CoreM m] [MonadError m] [MonadLog m] [AddMessageContext m] [MonadInfoTree m] [MonadLiftT MetaM m]
 
 def ValDesc.documentableName : ValDesc m (Ident × Name) where
   description := "a name with documentation"
@@ -1400,7 +1400,7 @@ structure DocstringConfig where
   label : Option String := none
 
 section
-variable [Monad m] [MonadOptions m] [MonadEnv m] [MonadLiftT CoreM m] [MonadError m]
+variable [Monad m] [MonadOptions m] [MonadEnv m] [MonadLiftT CoreM m] [MonadLiftT MetaM m] [MonadError m]
 variable [MonadLog m] [AddMessageContext m] [Elab.MonadInfoTree m]
 
 def DocstringConfig.parse : ArgParse m DocstringConfig :=
@@ -1497,7 +1497,7 @@ where
 
 section
 variable {m}
-variable [Monad m] [MonadError m] [MonadLiftT CoreM m] [MonadEnv m]
+variable [Monad m] [MonadError m] [MonadLiftT CoreM m] [MonadLiftT MetaM m] [MonadEnv m]
 variable [MonadLog m] [AddMessageContext m] [MonadOptions m] [MonadWithOptions m]
 variable [Lean.Elab.MonadInfoTree m]
 
diff --git a/src/verso-manual/VersoManual/Docstring/Progress.lean b/src/verso-manual/VersoManual/Docstring/Progress.lean
index ab6755f47..b8f93e0cb 100644
--- a/src/verso-manual/VersoManual/Docstring/Progress.lean
+++ b/src/verso-manual/VersoManual/Docstring/Progress.lean
@@ -114,7 +114,7 @@ def progress.descr : BlockDescr where
     let documented ← match ((← Doc.Html.HtmlT.state).get? `Verso.Genre.Manual.docstring).getD (pure <| .mkObj []) >>= Json.getObj? with
       | .error e =>
         Doc.Html.HtmlT.logError e
-        pure .leaf
+        pure {}
       | .ok v =>
         pure v
     let mut ok : NameSet := {}
@@ -142,7 +142,7 @@ def progress.descr : BlockDescr where
     return {{
       <dl>
         {{namespaces.map fun ns =>
-          let wanted := check.findD ns []
+          let wanted := check.getD ns []
           let notDocumented := wanted.filter (!ok.contains ·) |>.mergeSort (fun x y => x.toString < y.toString)
           let percentMissing :=
             if wanted.isEmpty then 0
diff --git a/src/verso-manual/VersoManual/Ext.lean b/src/verso-manual/VersoManual/Ext.lean
index 3f90beec7..790045b65 100644
--- a/src/verso-manual/VersoManual/Ext.lean
+++ b/src/verso-manual/VersoManual/Ext.lean
@@ -16,7 +16,7 @@ initialize inlineExtensionExt :
     addImportedFn := fun _ => pure {},
     addEntryFn := fun as (src, tgt) => as.insert src tgt,
     exportEntriesFn := fun es =>
-      es.fold (fun a src tgt => a.push (src, tgt)) #[] |>.qsort (Name.quickLt ·.1 ·.1)
+      es.foldl (fun a src tgt => a.push (src, tgt)) #[] |>.qsort (Name.quickLt ·.1 ·.1)
   }
 
 initialize blockExtensionExt :
@@ -26,5 +26,5 @@ initialize blockExtensionExt :
     addImportedFn := fun _ => pure {},
     addEntryFn := fun as (src, tgt) => as.insert src tgt,
     exportEntriesFn := fun es =>
-      es.fold (fun a src tgt => a.push (src, tgt)) #[] |>.qsort (Name.quickLt ·.1 ·.1)
+      es.foldl (fun a src tgt => a.push (src, tgt)) #[] |>.qsort (Name.quickLt ·.1 ·.1)
   }
diff --git a/src/verso-search/VersoSearch/PorterStemmer.lean b/src/verso-search/VersoSearch/PorterStemmer.lean
index d1fc8208a..bd00461fd 100644
--- a/src/verso-search/VersoSearch/PorterStemmer.lean
+++ b/src/verso-search/VersoSearch/PorterStemmer.lean
@@ -42,7 +42,11 @@ def isConsonant (str : String) (i : String.Pos) : Bool :=
   | _ => true
 termination_by i.byteIdx
 decreasing_by
-  simp [String.prev, *, String.utf8PrevAux_lt_of_pos]
+  simp [String.prev, *]
+  rename_i h
+  refine String.utf8PrevAux_lt_of_pos str.data 0 i ?_ h
+  let ⟨i⟩ := i
+  cases i <;> simp_all
 
 
 /--
diff --git a/src/verso/Verso/Code/External.lean b/src/verso/Verso/Code/External.lean
index a776a3edb..d946f9940 100644
--- a/src/verso/Verso/Code/External.lean
+++ b/src/verso/Verso/Code/External.lean
@@ -969,6 +969,7 @@ private def suggest : InlineExpander
     let region := region?.getD ""
 
     let (close, far) := defaultSuggestions.partition (fun (_, x) => hasSubstring region x)
+    have : Ord (String × String) := lexOrd
     let close := close.qsortOrd
     let far := far.qsortOrd
 
diff --git a/src/verso/Verso/Doc/Concrete.lean b/src/verso/Verso/Doc/Concrete.lean
index 5251b4de9..d591bcc06 100644
--- a/src/verso/Verso/Doc/Concrete.lean
+++ b/src/verso/Verso/Doc/Concrete.lean
@@ -259,6 +259,7 @@ def runVersoBlock (genre : Term) (block : TSyntax `block) : CommandElabM Unit :=
     let ((), docState', partState') ← runTermElabM fun _ => do
       let g ← Term.elabTerm genre (some (.const ``Doc.Genre [])) >>= instantiateMVars
       partCommand block |>.run genre g (docStateExt.getState env) partState
+    saveRefs docState' partState'
     modifyEnv fun env =>
       partStateExt.setState (docStateExt.setState env docState') (some partState')
   finally
diff --git a/src/verso/Verso/Doc/Elab.lean b/src/verso/Verso/Doc/Elab.lean
index 1bfdead38..c21673098 100644
--- a/src/verso/Verso/Doc/Elab.lean
+++ b/src/verso/Verso/Doc/Elab.lean
@@ -175,7 +175,7 @@ def _root_.Verso.Syntax.link.expand : InlineExpander
 @[inline_expander Verso.Syntax.footnote]
 def _root_.Verso.Syntax.link.footnote : InlineExpander
   | `(inline| footnote( $name:str )) => do
-    ``(Inline.footnote $name $(← addFootnoteRef name))
+    ``(Inline.footnote $(quote name.getString) $(← addFootnoteRef name))
   | _ => throwUnsupportedSyntax
 
 
diff --git a/src/verso/Verso/Doc/Elab/Monad.lean b/src/verso/Verso/Doc/Elab/Monad.lean
index b61075934..815485646 100644
--- a/src/verso/Verso/Doc/Elab/Monad.lean
+++ b/src/verso/Verso/Doc/Elab/Monad.lean
@@ -109,9 +109,11 @@ structure DocElabContext where
 structure DocDef (α : Type) where
   defSite : TSyntax `str
   val : α
+deriving Repr
 
 structure DocUses where
   useSites : Array Syntax := {}
+deriving Repr
 
 def DocUses.add (uses : DocUses) (loc : Syntax) : DocUses := {uses with useSites := uses.useSites.push loc}
 
@@ -133,7 +135,10 @@ def internalRefs (defs : HashMap String (DocDef α)) (refs : HashMap String DocU
   let keys : HashSet String := defs.fold (fun soFar k _ => HashSet.insert soFar k) <| refs.fold (fun soFar k _ => soFar.insert k) {}
   let mut refInfo := #[]
   for k in keys do
-    refInfo := refInfo.push ⟨defs[k]? |>.map (·.defSite), refs[k]? |>.map (·.useSites) |>.getD #[]⟩
+    refInfo := refInfo.push {
+      defSite := defs[k]? |>.map (·.defSite),
+      useSites := refs[k]? |>.map (·.useSites) |>.getD #[]
+    }
   refInfo
 
 
diff --git a/src/verso/Verso/Doc/Lsp.lean b/src/verso/Verso/Doc/Lsp.lean
index 3d5b6631f..3c8ff0f39 100644
--- a/src/verso/Verso/Doc/Lsp.lean
+++ b/src/verso/Verso/Doc/Lsp.lean
@@ -121,35 +121,6 @@ partial instance : FromJson Lean.Lsp.DocumentSymbolResult where
     let syms ← elts.mapM fromJson?
     pure ⟨syms⟩
 
-open Lean Server Lsp RequestM in
-def handleDef (params : TextDocumentPositionParams) (prev : RequestTask (Array LocationLink)) : RequestM (RequestTask (Array LocationLink)) := do
-  let doc ← readDoc
-  let text := doc.meta.text
-  let pos := text.lspPosToUtf8Pos params.position
-  bindWaitFindSnap doc (·.endPos + ' ' >= pos) (notFoundX := pure prev) fun snap => do
-    RequestM.mapTaskCostly prev fun prevLocs => do
-      let nodes := snap.infoTree.deepestNodes fun _ctxt info _arr =>
-        match info with
-        | .ofCustomInfo ⟨stx, data⟩ =>
-          if stx.containsPos pos then
-            data.get? DocRefInfo
-          else none
-        | _ => none
-      let mut locs : Array LocationLink := #[]
-      for node in nodes do
-        match node with
-        | ⟨some defSite, _⟩ =>
-          let mut origin : Option Range := none
-          for stx in node.syntax do
-            if let some ⟨head, tail⟩ := stx.getRange? then
-              if pos ≥ head && pos ≤ tail then
-                origin := stx.lspRange text
-                break
-          let some target := defSite.lspRange text
-            | continue
-          locs := locs.push {originSelectionRange? := origin, targetRange := target, targetUri := params.textDocument.uri, targetSelectionRange := target}
-        | _ => continue
-      pure (locs ++ prevLocs.toOption.getD #[])
 
 open Lean Server Lsp RequestM in
 def handleRefs (params : ReferenceParams) (prev : RequestTask (Array Location)) : RequestM (RequestTask (Array Location)) := do
@@ -622,6 +593,53 @@ where
       | .inr (.ok tl) => go timeoutTask tl
       | .inr (.error e) => return ⟨[], some e, true⟩
 
+open Lean Server Lsp RequestM in
+def handleDef (params : TextDocumentPositionParams) (prev : RequestTask (Array LeanLocationLink)) : RequestM (RequestTask (Array LeanLocationLink)) := do
+  let ctx ← read
+  let doc ← readDoc
+  let text := doc.meta.text
+  let pos := text.lspPosToUtf8Pos params.position
+  let locTask ← RequestM.asTask do
+    let (snaps, _, _) ← doc.cmdSnaps.getFinishedPrefixWithTimeout 300 (cancelTks := ctx.cancelTk.cancellationTasks)
+    let nodes := snaps.flatMap fun snap =>
+      snap.infoTree.collectNodesBottomUp fun _ctxt info _arr xs =>
+          match info with
+          | .ofCustomInfo ⟨stx, data⟩ =>
+            if stx.containsPos pos then
+              if let some i := data.get? DocRefInfo then i :: xs else xs
+            else xs
+          | _ => xs
+
+    let mut locs : Array LeanLocationLink := #[]
+    for node in nodes do
+      match node with
+      | ⟨some defSite, _⟩ =>
+        let mut origin : Option Range := none
+        for stx in node.syntax do
+          if let some ⟨head, tail⟩ := stx.getRange? then
+            if pos ≥ head && pos ≤ tail then
+              origin := stx.lspRange text
+              break
+        let some target := defSite.lspRange text
+          | continue
+        locs := locs.push {
+          originSelectionRange? := origin,
+          targetRange := target,
+          targetUri := params.textDocument.uri,
+          targetSelectionRange := target,
+          -- Because this is `none`, the watchdog will not keep this up to date as files are
+          -- edited. This seems to be OK, because this feature is currently only used for
+          -- references valid the current file. Adding the field would be useful in the future,
+          -- but it would require actually defining each footnote/link ref as its own name in the
+          -- environment and tracking this in Verso.
+          ident? := none,
+          isDefault := true
+        }
+      | _ => continue
+    pure locs
+  mergeResponses prev locTask fun xs ys =>
+    xs.getD #[] ++ ys.getD #[]
+
 open Lean Server Lsp RequestM in
 partial def handleTokens (prev : RequestTask SemanticTokens)
     (beginPos : String.Pos) (endPos? : Option String.Pos) :
@@ -922,7 +940,7 @@ open Lean.Server.FileWorker
 
 open Lean Server Lsp in
 initialize
-  chainLspRequestHandler "textDocument/definition" TextDocumentPositionParams (Array LocationLink) handleDef
+  chainLspRequestHandler "textDocument/definition" TextDocumentPositionParams (Array LeanLocationLink) handleDef
   -- chainLspRequestHandler "textDocument/references" ReferenceParams (Array Location) handleRefs -- TODO make this work - right now it goes through the watchdog so we can't chain it
   chainLspRequestHandler "textDocument/documentHighlight" DocumentHighlightParams DocumentHighlightResult handleHl
   chainLspRequestHandler "textDocument/documentSymbol" DocumentSymbolParams DocumentSymbolResult handleSyms
diff --git a/src/verso/Verso/Hint.lean b/src/verso/Verso/Hint.lean
index 5a6233d12..ad56023ab 100644
--- a/src/verso/Verso/Hint.lean
+++ b/src/verso/Verso/Hint.lean
@@ -21,7 +21,12 @@ The arguments are as follows:
 * `suggestions`: the suggestions to display.
 * `codeActionPrefix?`: if specified, text to display in place of "Try this: " in the code action
   label
+* `forceList`: if `true`, suggestions will be displayed as a bulleted list even if there is only
+  one.
 -/
-def hintAt (ref : Syntax) (hint : MessageData) (suggestions : Array Suggestion) (codeActionPrefix? : Option String := none) : CoreM MessageData :=
+def hintAt (ref : Syntax) (hint : MessageData) (suggestions : Array Suggestion)
+    (codeActionPrefix? : Option String := none)
+    (forceList : Bool := false) :
+    CoreM MessageData :=
   -- The @ guards against upstream signature changes going unnoticed
-  @MessageData.hint hint suggestions (ref? := some ref) (codeActionPrefix? := codeActionPrefix?)
+  @MessageData.hint hint suggestions (ref? := some ref) (codeActionPrefix? := codeActionPrefix?) (forceList := forceList)
diff --git a/src/verso/Verso/Instances.lean b/src/verso/Verso/Instances.lean
index 2e7221030..1c7630c3b 100644
--- a/src/verso/Verso/Instances.lean
+++ b/src/verso/Verso/Instances.lean
@@ -50,13 +50,13 @@ deriving instance ToJson for DefinitionSafety
 deriving instance FromJson for DefinitionSafety
 
 instance : Quote NameSet where
-  quote xs := mkCApp ``RBTree.fromList #[quote xs.toList, ⟨mkHole .missing⟩]
+  quote xs := mkCApp ``Std.TreeSet.ofList #[quote xs.toList, ⟨mkHole .missing⟩]
 instance : ToJson NameSet where
   toJson xs := toJson (xs.toArray : Array Name)
 instance : FromJson NameSet where
   fromJson? xs := do
     let arr ← fromJson? (α := Array Name) xs
-    pure <| RBTree.fromArray arr _
+    pure <| Std.TreeSet.ofArray arr _
 deriving instance Repr for NameSet
 
 section