diff --git a/README.md b/README.md
index 52794131..b9f98681 100644
--- a/README.md
+++ b/README.md
@@ -11,7 +11,7 @@ To build the book, change to the [`book`](book/) directory and run `lake exe fp-
 To read the book locally, serve that directory over HTTP and open the address that the server prints:
 
 ```
-python3 -m http.server --directory book/_out/html-multi
+lake exe verso-serve
 ```
 
 ## Publishing
diff --git a/book/.verso/verso-xref-manifest.json b/book/.verso/verso-xref-manifest.json
index e5909dc5..38ec5435 100644
--- a/book/.verso/verso-xref-manifest.json
+++ b/book/.verso/verso-xref-manifest.json
@@ -1,8 +1,7 @@
 {"version": 0,
  "sources":
  {"manual":
-  {"updated": "2026-08-04:14:48:20.312161000",
-   "updateFrequency": "manual",
+  {"updateFrequency": "manual",
    "shortName": "ref",
    "root": "https://lean-lang.org/doc/reference/4.26.0/",
    "longName": "Lean Language Reference"}},
diff --git a/book/FPLean/Monads/IO.lean b/book/FPLean/Monads/IO.lean
index 9404d171..e9747912 100644
--- a/book/FPLean/Monads/IO.lean
+++ b/book/FPLean/Monads/IO.lean
@@ -43,27 +43,27 @@ Nat.zero : Nat
 Nat.succ : Nat → Nat
 ```
 and
-```anchor printCharIsAlpha
-#print Char.isAlpha
+```anchor printStringToLower
+#print String.toLower
 ```
 results in
-```anchorInfo printCharIsAlpha
-def Char.isAlpha : Char → Bool :=
-fun c => c.isUpper || c.isLower
+```anchorInfo printStringToLower
+def String.toLower : String → String :=
+fun s => String.map Char.toLower s
 ```
 
 Sometimes, the output of {kw}`#print` includes Lean features that have not yet been presented in this book.
 For example,
-```anchor printListIsEmpty
-#print List.isEmpty
+```anchor printListHeadHuh
+#print List.head?
 ```
 produces
-```anchorInfo printListIsEmpty
-def List.isEmpty.{u} : {α : Type u} → List α → Bool :=
+```anchorInfo printListHeadHuh
+def List.head?.{u} : {α : Type u} → List α → Option α :=
 fun {α} x =>
   match x with
-  | [] => true
-  | head :: tail => false
+  | [] => none
+  | a :: tail => some a
 ```
 which includes a {lit}`.{u}` after the definition's name, and annotates types as {anchorTerm names}`Type u` rather than just {anchorTerm names}`Type`.
 This can be safely ignored for now.
diff --git a/book/FPLean/ProgramsProofs/InsertionSort.lean b/book/FPLean/ProgramsProofs/InsertionSort.lean
index 942ff0fd..b226e676 100644
--- a/book/FPLean/ProgramsProofs/InsertionSort.lean
+++ b/book/FPLean/ProgramsProofs/InsertionSort.lean
@@ -85,12 +85,10 @@ def insertSorted [Ord α] (arr : Array α) (i : Fin arr.size) : Array α :=
   match i with
   | ⟨0, _⟩ => arr
   | ⟨i' + 1, _⟩ =>
-    have : i' < arr.size := by
-      grind
     match Ord.compare arr[i'] arr[i] with
     | .lt | .eq => arr
     | .gt =>
-      insertSorted (arr.swap i' i) ⟨i', by simp [*]⟩
+      insertSorted (arr.swap i' i) ⟨i', by grind⟩
 ```
 If the index {anchorName insertSorted}`i` is {anchorTerm insertSorted}`0`, then the element being inserted into the sorted region has reached the beginning of the region and is the smallest.
 If the index is {anchorTerm insertSorted}`i' + 1`, then the element at {anchorName insertSorted}`i'` should be compared to the element at {anchorName insertSorted}`i`.
@@ -103,19 +101,8 @@ If the element to the left is greater than the element being inserted, then the
 {anchorName names}`Array.swap` takes both of its indices as {anchorName names}`Nat`s, using the same tactics as array indexing behind the scenes to ensure that they are in bounds.
 
 Nonetheless, the {anchorName names}`Fin` used for the recursive call needs a proof that {anchorName insertSorted}`i'` is in bounds for the result of swapping two elements.
-The {anchorTerm insertSorted}`simp` tactic's database contains the fact that swapping two elements of an array doesn't change its size, and the {anchorTerm insertSorted}`[*]` argument instructs it to additionally use the assumption introduced by {kw}`have`.
-Omitting the {kw}`have`-expression with the proof that {anchorTerm insertSorted}`i' < arr.size` reveals the following goal:
-```anchorError insertSortedNoProof
-unsolved goals
-α : Type ?u.7
-inst✝ : Ord α
-arr : Array α
-i : Fin arr.size
-i' : Nat
-isLt✝ : i' + 1 < arr.size
-⊢ i' < arr.size
-```
-
+The {anchorTerm insertSorted}`grind` tactic's database contains the fact that swapping two elements of an array doesn't change its size.
+Combining this with the fact that {anchorTerm insertSorted}`i' + 1` is in bounds for the original array, {anchorTerm insertSorted}`grind` can conclude that {anchorName insertSorted}`i'` is in bounds after the swap.
 
 
 # The Outer Loop
@@ -385,10 +372,10 @@ theorem insert_sorted_size_eq [Ord α]
     (arr : Array α) (i : Fin arr.size) :
     (insertSorted arr i).size = arr.size := by
   fun_induction insertSorted with
-  | case1 arr isLt => skip
-  | case2 arr i isLt this isLt => skip
-  | case3 arr i isLt this isEq => skip
-  | case4 arr i isLt this isGt ih => skip
+  | case1 arr => skip
+  | case2 arr i this isLt => skip
+  | case3 arr i this isEq => skip
+  | case4 arr i this isGt ih => skip
 ```
 The first goal is the case for index {anchorTerm insertSorted}`0`.
 Here, the array is not modified, so proving that its size is unmodified will not require any complicated steps:
@@ -398,7 +385,7 @@ case case1
 α : Type u_1
 inst✝ : Ord α
 arr✝ arr : Array α
-isLt : 0 < arr.size
+isLt✝ : 0 < arr.size
 ⊢ arr.size = arr.size
 ```
 The next two goals are the same, and cover the {anchorName insertSorted}`.lt` and {anchorName insertSorted}`.eq` cases for the element comparison.
@@ -410,13 +397,12 @@ case case2
 inst✝ : Ord α
 arr✝ arr : Array α
 i : Nat
-isLt✝ : i + 1 < arr.size
-this : i < arr.size
-isLt : compare arr[i] arr[⟨i.succ, isLt✝⟩] = Ordering.lt
-⊢ (match compare arr[i] arr[⟨i.succ, isLt✝⟩] with
+this : i + 1 < arr.size
+isLt : compare arr[i] arr[⟨i.succ, this⟩] = Ordering.lt
+⊢ (match compare arr[i] arr[⟨i.succ, this⟩] with
     | Ordering.lt => arr
     | Ordering.eq => arr
-    | Ordering.gt => insertSorted (arr.swap i (↑⟨i.succ, isLt✝⟩) this ⋯) ⟨i, ⋯⟩).size =
+    | Ordering.gt => insertSorted (arr.swap i ↑⟨i.succ, this⟩ ⋯ ⋯) ⟨i, ⋯⟩).size =
   arr.size
 ```
 ```anchorError insert_sorted_size_eq_funInd1
@@ -426,13 +412,12 @@ case case3
 inst✝ : Ord α
 arr✝ arr : Array α
 i : Nat
-isLt : i + 1 < arr.size
-this : i < arr.size
-isEq : compare arr[i] arr[⟨i.succ, isLt⟩] = Ordering.eq
-⊢ (match compare arr[i] arr[⟨i.succ, isLt⟩] with
+this : i + 1 < arr.size
+isEq : compare arr[i] arr[⟨i.succ, this⟩] = Ordering.eq
+⊢ (match compare arr[i] arr[⟨i.succ, this⟩] with
     | Ordering.lt => arr
     | Ordering.eq => arr
-    | Ordering.gt => insertSorted (arr.swap i (↑⟨i.succ, isLt⟩) this ⋯) ⟨i, ⋯⟩).size =
+    | Ordering.gt => insertSorted (arr.swap i ↑⟨i.succ, this⟩ ⋯ ⋯) ⟨i, ⋯⟩).size =
   arr.size
 ```
 In the final case, once the {anchorTerm insertSorted}`match` is reduced, there will be some work left to do to prove that the next step of the insertion preserves the size of the array.
@@ -444,26 +429,24 @@ case case4
 inst✝ : Ord α
 arr✝ arr : Array α
 i : Nat
-isLt : i + 1 < arr.size
-this : i < arr.size
-isGt : compare arr[i] arr[⟨i.succ, isLt⟩] = Ordering.gt
-ih : (insertSorted (arr.swap i (↑⟨i.succ, isLt⟩) this ⋯) ⟨i, ⋯⟩).size = (arr.swap i (↑⟨i.succ, isLt⟩) this ⋯).size
-⊢ (match compare arr[i] arr[⟨i.succ, isLt⟩] with
+this : i + 1 < arr.size
+isGt : compare arr[i] arr[⟨i.succ, this⟩] = Ordering.gt
+ih : (insertSorted (arr.swap i ↑⟨i.succ, this⟩ ⋯ ⋯) ⟨i, ⋯⟩).size = (arr.swap i ↑⟨i.succ, this⟩ ⋯ ⋯).size
+⊢ (match compare arr[i] arr[⟨i.succ, this⟩] with
     | Ordering.lt => arr
     | Ordering.eq => arr
-    | Ordering.gt => insertSorted (arr.swap i (↑⟨i.succ, isLt⟩) this ⋯) ⟨i, ⋯⟩).size =
+    | Ordering.gt => insertSorted (arr.swap i ↑⟨i.succ, this⟩ ⋯ ⋯) ⟨i, ⋯⟩).size =
   arr.size
 ```
 :::
 
 :::paragraph
-The Lean library includes the theorem {anchorName insert_sorted_size_eq_funInd}`Array.size_swap`, which states that swapping two elements of an array doesn't change its size.
-By default, {tactic}`grind` doesn't use this fact, but once instructed to do so, it can take care of all four cases:
+The {tactic}`grind` tactic can take care of all four cases:
 ```anchor insert_sorted_size_eq_funInd
 theorem insert_sorted_size_eq [Ord α]
     (arr : Array α) (i : Fin arr.size) :
     (insertSorted arr i).size = arr.size := by
-  fun_induction insertSorted <;> grind [Array.size_swap]
+  fun_induction insertSorted <;> grind
 ```
 :::
 
@@ -533,7 +516,7 @@ Adding calls to {anchorName dbgTraceIfSharedSig}`dbgTraceIfShared` at each point
 Insertion sort has precisely one place that is at risk of copying rather than mutating: the call to {anchorName names}`Array.swap`.
 Replacing {anchorTerm insertSorted}`arr.swap i' i` with {anchorTerm InstrumentedInsertionSort (module := Examples.ProgramsProofs.InstrumentedInsertionSort)}`(dbgTraceIfShared "array to swap" arr).swap i' i` causes the program to emit {lit}`shared RC array to swap` whenever it is unable to mutate the array.
 However, this change to the program changes the proofs as well, because now there's a call to an additional function.
-Adding a local assumption that {anchorName dbgTraceIfSharedSig}`dbgTraceIfShared` preserves the length of its argument and adding it to some calls to {anchorTerm InstrumentedInsertionSort (module:=Examples.ProgramsProofs.InstrumentedInsertionSort)}`simp` is enough to fix the program and proofs.
+Adding a local assumption that {anchorName dbgTraceIfSharedSig}`dbgTraceIfShared` preserves the length of its argument and adding it to some calls to {anchorTerm InstrumentedInsertionSort (module:=Examples.ProgramsProofs.InstrumentedInsertionSort)}`grind` is enough to fix the program and proofs.
 
 The complete instrumented code for insertion sort is:
 ```anchor InstrumentedInsertionSort (module := Examples.ProgramsProofs.InstrumentedInsertionSort)
@@ -542,33 +525,25 @@ def insertSorted [Ord α] (arr : Array α) (i : Fin arr.size) : Array α :=
   | ⟨0, _⟩ => arr
   | ⟨i' + 1, _⟩ =>
     have : i' < arr.size := by
-      omega
+      grind
     match Ord.compare arr[i'] arr[i] with
     | .lt | .eq => arr
     | .gt =>
       have : (dbgTraceIfShared "array to swap" arr).size = arr.size := by
-        simp [dbgTraceIfShared]
+        grind [dbgTraceIfShared]
       insertSorted
         ((dbgTraceIfShared "array to swap" arr).swap i' i)
-        ⟨i', by simp [*]⟩
-
-theorem insert_sorted_size_eq [Ord α] (len : Nat) (i : Nat) :
-    (arr : Array α) → (isLt : i < arr.size) → (arr.size = len) →
-    (insertSorted arr ⟨i, isLt⟩).size = len := by
-  induction i with
-  | zero =>
-    intro arr isLt hLen
-    simp [insertSorted, *]
-  | succ i' ih =>
-    intro arr isLt hLen
-    simp [insertSorted, dbgTraceIfShared]
-    split <;> simp [*]
+        ⟨i', by grind [dbgTraceIfShared]⟩
+
+theorem insert_sorted_size_eq [Ord α]
+    (arr : Array α) (i : Fin arr.size) :
+    (insertSorted arr i).size = arr.size := by
+  fun_induction insertSorted <;> grind [dbgTraceIfShared]
 
 def insertionSortLoop [Ord α] (arr : Array α) (i : Nat) : Array α :=
   if h : i < arr.size then
     have : (insertSorted arr ⟨i, h⟩).size - (i + 1) < arr.size - i := by
-      rw [insert_sorted_size_eq arr.size i arr h rfl]
-      omega
+      grind [insert_sorted_size_eq]
     insertionSortLoop (insertSorted arr ⟨i, h⟩) (i + 1)
   else
     arr
@@ -631,7 +606,7 @@ def main (args : List String) : IO UInt32 := do
   | ["--shared"] => mainShared; pure 0
   | ["--unique"] => mainUnique; pure 0
   | _ =>
-    IO.println "Expected single argument, either \"--shared\" or \"--unique\""
+    IO.println "Expected either \"--shared\" or \"--unique\""
     pure 1
 ```
 
@@ -639,11 +614,11 @@ Running it with no arguments produces the expected usage information:
 ```interaction «sort-sharing» "sort-demo"
 { command := "sort",
   script := #[
-    .expect "Expected single argument, either \"--shared\" or \"--unique\"",
+    .expect "Expected either \"--shared\" or \"--unique\"",
     .exitCode 1] }
 ---
 $ sort
-< Expected single argument, either "--shared" or "--unique"
+< Expected either "--shared" or "--unique"
 ```
 
 The file {lit}`test-data` contains the following rocks:
diff --git a/book/lake-manifest.json b/book/lake-manifest.json
index f9cd4a1a..11994c1e 100644
--- a/book/lake-manifest.json
+++ b/book/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "655d4f6e89bbf4c3c946e54625dcbe1539ea1107",
+   "rev": "aa44714115e9973999dfdde63130f725c3265a82",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "56958b3901ca108830de34fbce6cecd4b5757c1f",
+   "rev": "76f052847294d189dc9924a33466b4b677f47e67",
    "name": "illuminate",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "b1c4a69a7e247ab7df20460212001673d74f08c0",
+   "rev": "38e9c3ce15cbb63c92e90bb9a92e4eb82131f669",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "859ab80c32c5851151919a7d757d7c0c0b6e39d2",
+   "rev": "847084e80500726e4331dded5f17007ddaf89c31",
    "name": "subverso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/book/lean-toolchain b/book/lean-toolchain
index fd85b262..e2a0e356 100644
--- a/book/lean-toolchain
+++ b/book/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.33.0-rc1
+leanprover/lean4:v4.34.0-rc1
\ No newline at end of file
diff --git a/book/verso-serve.toml b/book/verso-serve.toml
new file mode 100644
index 00000000..6a107047
--- /dev/null
+++ b/book/verso-serve.toml
@@ -0,0 +1,5 @@
+banner = "Functional Programming in Lean"
+
+[[mounts]]
+path = "/"
+dir = "_out/html-multi"
diff --git a/examples/Examples/Monads/Class.lean b/examples/Examples/Monads/Class.lean
index 3bceddb0..0fbd8d2d 100644
--- a/examples/Examples/Monads/Class.lean
+++ b/examples/Examples/Monads/Class.lean
@@ -891,20 +891,28 @@ instance : LawfulMonad (Reader ρ) where
   map_const := by
     simp [Functor.mapConst, Function.comp, Functor.map]
   id_map x := by
-    simp [Functor.map]
+    funext
+    simp [Functor.map, id, Function.comp]
   seqLeft_eq x _ := by
-    simp [SeqLeft.seqLeft, Seq.seq, Functor.map]
+    funext
+    simp [SeqLeft.seqLeft, Seq.seq, Functor.map, Function.comp]
   seqRight_eq _ y := by
-    simp [SeqRight.seqRight, Seq.seq, Functor.map]
+    funext
+    simp [SeqRight.seqRight, Seq.seq, Functor.map, Function.comp]
   pure_seq g x := by
-    simp [Seq.seq, Functor.map, pure]
+    funext
+    simp [Seq.seq, Functor.map, pure, Function.comp]
   bind_pure_comp f x := by
-    simp [Functor.map, bind, pure]
+    funext
+    simp [Functor.map, bind, pure, Function.comp]
   bind_map f x := by
-    simp [Seq.seq, bind, Functor.map]
+    funext
+    simp [Seq.seq, bind, Functor.map, Function.comp]
   pure_bind x f := by
+    funext
     simp [pure, bind]
   bind_assoc x f g := by
+    funext
     simp [bind]
 
 
diff --git a/examples/Examples/Monads/IO.lean b/examples/Examples/Monads/IO.lean
index de2213b8..33fda1e9 100644
--- a/examples/Examples/Monads/IO.lean
+++ b/examples/Examples/Monads/IO.lean
@@ -32,27 +32,27 @@ Nat.succ : Nat → Nat
 -- ANCHOR_END: printNat
 
 
-/-- info:
-def Char.isAlpha : Char → Bool :=
-fun c => c.isUpper || c.isLower
+/--
+info: def String.toLower : String → String :=
+fun s => String.map Char.toLower s
 -/
 #check_msgs in
--- ANCHOR: printCharIsAlpha
-#print Char.isAlpha
--- ANCHOR_END: printCharIsAlpha
+-- ANCHOR: printStringToLower
+#print String.toLower
+-- ANCHOR_END: printStringToLower
 
 
-/-- info:
-def List.isEmpty.{u} : {α : Type u} → List α → Bool :=
+/--
+info: def List.head?.{u} : {α : Type u} → List α → Option α :=
 fun {α} x =>
   match x with
-  | [] => true
-  | head :: tail => false
+  | [] => none
+  | a :: tail => some a
 -/
 #check_msgs in
--- ANCHOR: printListIsEmpty
-#print List.isEmpty
--- ANCHOR_END: printListIsEmpty
+-- ANCHOR: printListHeadHuh
+#print List.head?
+-- ANCHOR_END: printListHeadHuh
 
 
 
diff --git a/examples/Examples/ProgramsProofs/InsertionSort.lean b/examples/Examples/ProgramsProofs/InsertionSort.lean
index 4868a642..996dbbfe 100644
--- a/examples/Examples/ProgramsProofs/InsertionSort.lean
+++ b/examples/Examples/ProgramsProofs/InsertionSort.lean
@@ -50,12 +50,10 @@ def insertSorted [Ord α] (arr : Array α) (i : Fin arr.size) : Array α :=
   match i with
   | ⟨0, _⟩ => arr
   | ⟨i' + 1, _⟩ =>
-    have : i' < arr.size := by
-      grind
     match Ord.compare arr[i'] arr[i] with
     | .lt | .eq => arr
     | .gt =>
-      insertSorted (arr.swap i' i) ⟨i', by simp [*]⟩
+      insertSorted (arr.swap i' i) ⟨i', by grind⟩
 -- ANCHOR_END: insertSorted
 
 -- theorem insert_sorted_size_eq' [Ord α] (len : Nat) (i : Nat) :
@@ -220,7 +218,7 @@ case case1
 α : Type u_1
 inst✝ : Ord α
 arr✝ arr : Array α
-isLt : 0 < arr.size
+isLt✝ : 0 < arr.size
 ⊢ arr.size = arr.size
 ---
 error: unsolved goals
@@ -229,13 +227,12 @@ case case2
 inst✝ : Ord α
 arr✝ arr : Array α
 i : Nat
-isLt✝ : i + 1 < arr.size
-this : i < arr.size
-isLt : compare arr[i] arr[⟨i.succ, isLt✝⟩] = Ordering.lt
-⊢ (match compare arr[i] arr[⟨i.succ, isLt✝⟩] with
+this : i + 1 < arr.size
+isLt : compare arr[i] arr[⟨i.succ, this⟩] = Ordering.lt
+⊢ (match compare arr[i] arr[⟨i.succ, this⟩] with
       | Ordering.lt => arr
       | Ordering.eq => arr
-      | Ordering.gt => insertSorted (arr.swap i (↑⟨i.succ, isLt✝⟩) this ⋯) ⟨i, ⋯⟩).size =
+      | Ordering.gt => insertSorted (arr.swap i ↑⟨i.succ, this⟩ ⋯ ⋯) ⟨i, ⋯⟩).size =
     arr.size
 ---
 error: unsolved goals
@@ -244,13 +241,12 @@ case case3
 inst✝ : Ord α
 arr✝ arr : Array α
 i : Nat
-isLt : i + 1 < arr.size
-this : i < arr.size
-isEq : compare arr[i] arr[⟨i.succ, isLt⟩] = Ordering.eq
-⊢ (match compare arr[i] arr[⟨i.succ, isLt⟩] with
+this : i + 1 < arr.size
+isEq : compare arr[i] arr[⟨i.succ, this⟩] = Ordering.eq
+⊢ (match compare arr[i] arr[⟨i.succ, this⟩] with
       | Ordering.lt => arr
       | Ordering.eq => arr
-      | Ordering.gt => insertSorted (arr.swap i (↑⟨i.succ, isLt⟩) this ⋯) ⟨i, ⋯⟩).size =
+      | Ordering.gt => insertSorted (arr.swap i ↑⟨i.succ, this⟩ ⋯ ⋯) ⟨i, ⋯⟩).size =
     arr.size
 ---
 error: unsolved goals
@@ -259,14 +255,13 @@ case case4
 inst✝ : Ord α
 arr✝ arr : Array α
 i : Nat
-isLt : i + 1 < arr.size
-this : i < arr.size
-isGt : compare arr[i] arr[⟨i.succ, isLt⟩] = Ordering.gt
-ih : (insertSorted (arr.swap i (↑⟨i.succ, isLt⟩) this ⋯) ⟨i, ⋯⟩).size = (arr.swap i (↑⟨i.succ, isLt⟩) this ⋯).size
-⊢ (match compare arr[i] arr[⟨i.succ, isLt⟩] with
+this : i + 1 < arr.size
+isGt : compare arr[i] arr[⟨i.succ, this⟩] = Ordering.gt
+ih : (insertSorted (arr.swap i ↑⟨i.succ, this⟩ ⋯ ⋯) ⟨i, ⋯⟩).size = (arr.swap i ↑⟨i.succ, this⟩ ⋯ ⋯).size
+⊢ (match compare arr[i] arr[⟨i.succ, this⟩] with
       | Ordering.lt => arr
       | Ordering.eq => arr
-      | Ordering.gt => insertSorted (arr.swap i (↑⟨i.succ, isLt⟩) this ⋯) ⟨i, ⋯⟩).size =
+      | Ordering.gt => insertSorted (arr.swap i ↑⟨i.succ, this⟩ ⋯ ⋯) ⟨i, ⋯⟩).size =
     arr.size
 -/
 #check_msgs in
@@ -275,10 +270,10 @@ theorem insert_sorted_size_eq [Ord α]
     (arr : Array α) (i : Fin arr.size) :
     (insertSorted arr i).size = arr.size := by
   fun_induction insertSorted with
-  | case1 arr isLt => skip
-  | case2 arr i isLt this isLt => skip
-  | case3 arr i isLt this isEq => skip
-  | case4 arr i isLt this isGt ih => skip
+  | case1 arr => skip
+  | case2 arr i this isLt => skip
+  | case3 arr i this isEq => skip
+  | case4 arr i this isGt ih => skip
 -- ANCHOR_END: insert_sorted_size_eq_funInd1
 stop discarding
 
@@ -287,7 +282,7 @@ stop discarding
 theorem insert_sorted_size_eq [Ord α]
     (arr : Array α) (i : Fin arr.size) :
     (insertSorted arr i).size = arr.size := by
-  fun_induction insertSorted <;> grind [Array.size_swap]
+  fun_induction insertSorted <;> grind
 -- ANCHOR_END: insert_sorted_size_eq_funInd
 
 discarding
@@ -311,7 +306,7 @@ Could not find a decreasing measure.
 The basic measures relate at each recursive call as follows:
 (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
             arr i #1
-1) 324:4-55   ? ?  ?
+1) 319:4-55   ? ?  ?
 
 #1: arr.size - i
 
diff --git a/examples/Examples/ProgramsProofs/InstrumentedInsertionSort.lean b/examples/Examples/ProgramsProofs/InstrumentedInsertionSort.lean
index 82f9c57b..9c797a85 100644
--- a/examples/Examples/ProgramsProofs/InstrumentedInsertionSort.lean
+++ b/examples/Examples/ProgramsProofs/InstrumentedInsertionSort.lean
@@ -8,33 +8,25 @@ def insertSorted [Ord α] (arr : Array α) (i : Fin arr.size) : Array α :=
   | ⟨0, _⟩ => arr
   | ⟨i' + 1, _⟩ =>
     have : i' < arr.size := by
-      omega
+      grind
     match Ord.compare arr[i'] arr[i] with
     | .lt | .eq => arr
     | .gt =>
       have : (dbgTraceIfShared "array to swap" arr).size = arr.size := by
-        simp [dbgTraceIfShared]
+        grind [dbgTraceIfShared]
       insertSorted
         ((dbgTraceIfShared "array to swap" arr).swap i' i)
-        ⟨i', by simp [*]⟩
+        ⟨i', by grind [dbgTraceIfShared]⟩
 
-theorem insert_sorted_size_eq [Ord α] (len : Nat) (i : Nat) :
-    (arr : Array α) → (isLt : i < arr.size) → (arr.size = len) →
-    (insertSorted arr ⟨i, isLt⟩).size = len := by
-  induction i with
-  | zero =>
-    intro arr isLt hLen
-    simp [insertSorted, *]
-  | succ i' ih =>
-    intro arr isLt hLen
-    simp [insertSorted, dbgTraceIfShared]
-    split <;> simp [*]
+theorem insert_sorted_size_eq [Ord α]
+    (arr : Array α) (i : Fin arr.size) :
+    (insertSorted arr i).size = arr.size := by
+  fun_induction insertSorted <;> grind [dbgTraceIfShared]
 
 def insertionSortLoop [Ord α] (arr : Array α) (i : Nat) : Array α :=
   if h : i < arr.size then
     have : (insertSorted arr ⟨i, h⟩).size - (i + 1) < arr.size - i := by
-      rw [insert_sorted_size_eq arr.size i arr h rfl]
-      omega
+      grind [insert_sorted_size_eq]
     insertionSortLoop (insertSorted arr ⟨i, h⟩) (i + 1)
   else
     arr
@@ -80,6 +72,6 @@ def main (args : List String) : IO UInt32 := do
   | ["--shared"] => mainShared; pure 0
   | ["--unique"] => mainUnique; pure 0
   | _ =>
-    IO.println "Expected single argument, either \"--shared\" or \"--unique\""
+    IO.println "Expected either \"--shared\" or \"--unique\""
     pure 1
 -- ANCHOR_END: main
diff --git a/examples/lake-manifest.json b/examples/lake-manifest.json
index ce8f81e8..52664af4 100644
--- a/examples/lake-manifest.json
+++ b/examples/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "6b0b76cb79974cc1d43f988d26f7d3fa35e773cc",
+   "rev": "847084e80500726e4331dded5f17007ddaf89c31",
    "name": "subverso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/examples/lean-toolchain b/examples/lean-toolchain
index 87c20c6e..19fe76fa 100644
--- a/examples/lean-toolchain
+++ b/examples/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:4.32.0
+leanprover/lean4:4.33.0