diff --git a/src/Init/Data/BitVec/BasicAux.lean b/src/Init/Data/BitVec/BasicAux.lean
index d24139bf98..67453de38e 100644
--- a/src/Init/Data/BitVec/BasicAux.lean
+++ b/src/Init/Data/BitVec/BasicAux.lean
@@ -21,13 +21,6 @@ namespace BitVec
 
 section Nat
 
-/--
-The bitvector with value `i mod 2^n`.
--/
-@[expose, match_pattern]
-protected def ofNat (n : Nat) (i : Nat) : BitVec n where
-  toFin := Fin.ofNat (2^n) i
-
 instance instOfNat : OfNat (BitVec n) i where ofNat := .ofNat n i
 
 /-- Return the bound in terms of toNat. -/
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 1970e2d350..49d585467e 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -122,7 +122,7 @@ theorem getElem_of_getLsbD_eq_true {x : BitVec w} {i : Nat} (h : x.getLsbD i = t
 This normalized a bitvec using `ofFin` to `ofNat`.
 -/
 theorem ofFin_eq_ofNat : @BitVec.ofFin w (Fin.mk x lt) = BitVec.ofNat w x := by
-  simp only [BitVec.ofNat, Fin.ofNat, lt, Nat.mod_eq_of_lt]
+  simp only [BitVec.ofNat, Fin.Internal.ofNat_eq_ofNat, Fin.ofNat, lt, Nat.mod_eq_of_lt]
 
 /-- Prove nonequality of bitvectors in terms of nat operations. -/
 theorem toNat_ne_iff_ne {n} {x y : BitVec n} : x.toNat ≠ y.toNat ↔ x ≠ y := by
@@ -299,7 +299,7 @@ theorem length_pos_of_ne {x y : BitVec w} (h : x ≠ y) : 0 < w :=
 
 theorem ofFin_ofNat (n : Nat) :
     ofFin (no_index (OfNat.ofNat n : Fin (2^w))) = OfNat.ofNat n := by
-  simp only [OfNat.ofNat, Fin.ofNat, BitVec.ofNat]
+  simp only [OfNat.ofNat, Fin.Internal.ofNat_eq_ofNat, Fin.ofNat, BitVec.ofNat]
 
 -- We use a `grind_pattern` as `@[grind]` will not use the `no_index` term.
 grind_pattern ofFin_ofNat => ofFin (OfNat.ofNat n : Fin (2^w))
diff --git a/src/Init/Data/Fin/Basic.lean b/src/Init/Data/Fin/Basic.lean
index 3a6f48650b..743c0ab0a4 100644
--- a/src/Init/Data/Fin/Basic.lean
+++ b/src/Init/Data/Fin/Basic.lean
@@ -51,6 +51,11 @@ The assumption `NeZero n` ensures that `Fin n` is nonempty.
 @[expose] protected def ofNat (n : Nat) [NeZero n] (a : Nat) : Fin n :=
   ⟨a % n, Nat.mod_lt _ (pos_of_neZero n)⟩
 
+@[simp]
+theorem Internal.ofNat_eq_ofNat {n : Nat} {hn} {a : Nat} :
+  letI : NeZero n := ⟨Nat.pos_iff_ne_zero.1 hn⟩
+  Fin.Internal.ofNat n hn a = Fin.ofNat n a := rfl
+
 @[deprecated Fin.ofNat (since := "2025-05-28")]
 protected def ofNat' (n : Nat) [NeZero n] (a : Nat) : Fin n :=
   Fin.ofNat n a
diff --git a/src/Init/Data/Nat/Basic.lean b/src/Init/Data/Nat/Basic.lean
index 1313940efd..e09cc2a91b 100644
--- a/src/Init/Data/Nat/Basic.lean
+++ b/src/Init/Data/Nat/Basic.lean
@@ -257,8 +257,6 @@ attribute [simp] Nat.le_refl
 
 theorem succ_lt_succ {n m : Nat} : n < m → succ n < succ m := succ_le_succ
 
-theorem lt_succ_of_le {n m : Nat} : n ≤ m → n < succ m := succ_le_succ
-
 theorem le_of_lt_add_one {n m : Nat} : n < m + 1 → n ≤ m := le_of_succ_le_succ
 
 theorem lt_add_one_of_le {n m : Nat} : n ≤ m → n < m + 1 := succ_le_succ
@@ -271,37 +269,15 @@ theorem not_add_one_le_self : (n : Nat) → ¬ n + 1 ≤ n := Nat.not_succ_le_se
 
 theorem add_one_pos (n : Nat) : 0 < n + 1 := Nat.zero_lt_succ n
 
-theorem succ_sub_succ_eq_sub (n m : Nat) : succ n - succ m = n - m := by
-  induction m with
-  | zero      => exact rfl
-  | succ m ih => apply congrArg pred ih
-
-theorem pred_le : ∀ (n : Nat), pred n ≤ n
-  | zero   => Nat.le.refl
-  | succ _ => le_succ _
-
 theorem pred_lt : ∀ {n : Nat}, n ≠ 0 → pred n < n
   | zero,   h => absurd rfl h
   | succ _, _ => lt_succ_of_le (Nat.le_refl _)
 
 theorem sub_one_lt : ∀ {n : Nat}, n ≠ 0 → n - 1 < n := pred_lt
 
-@[simp] theorem sub_le (n m : Nat) : n - m ≤ n := by
-  induction m with
-  | zero      => exact Nat.le_refl (n - 0)
-  | succ m ih => apply Nat.le_trans (pred_le (n - m)) ih
-
 theorem sub_lt_of_lt {a b c : Nat} (h : a < c) : a - b < c :=
   Nat.lt_of_le_of_lt (Nat.sub_le _ _) h
 
-theorem sub_lt : ∀ {n m : Nat}, 0 < n → 0 < m → n - m < n
-  | 0,   _,   h1, _  => absurd h1 (Nat.lt_irrefl 0)
-  | _+1, 0,   _, h2  => absurd h2 (Nat.lt_irrefl 0)
-  | n+1, m+1, _,  _  =>
-    Eq.symm (succ_sub_succ_eq_sub n m) ▸
-      show n - m < succ n from
-      lt_succ_of_le (sub_le n m)
-
 theorem sub_succ (n m : Nat) : n - succ m = pred (n - m) := rfl
 
 theorem succ_sub_succ (n m : Nat) : succ n - succ m = n - m :=
@@ -316,9 +292,6 @@ theorem sub_add_eq (a b c : Nat) : a - (b + c) = a - b - c := by
   | zero => simp
   | succ c ih => simp only [Nat.add_succ, Nat.sub_succ, ih]
 
-protected theorem lt_of_lt_of_le {n m k : Nat} : n < m → m ≤ k → n < k :=
-  Nat.le_trans
-
 protected theorem lt_of_lt_of_eq {n m k : Nat} : n < m → m = k → n < k :=
   fun h₁ h₂ => h₂ ▸ h₁
 
@@ -356,12 +329,10 @@ protected theorem pos_of_ne_zero {n : Nat} : n ≠ 0 → 0 < n := (eq_zero_or_po
 
 theorem pos_of_neZero (n : Nat) [NeZero n] : 0 < n := Nat.pos_of_ne_zero (NeZero.ne _)
 
+attribute [simp] Nat.lt_add_one
+
 theorem lt.base (n : Nat) : n < succ n := Nat.le_refl (succ n)
 
-theorem lt_succ_self (n : Nat) : n < succ n := lt.base n
-
-@[simp] protected theorem lt_add_one (n : Nat) : n < n + 1 := lt.base n
-
 protected theorem le_total (m n : Nat) : m ≤ n ∨ n ≤ m :=
   match Nat.lt_or_ge m n with
   | Or.inl h => Or.inl (Nat.le_of_lt h)
@@ -457,7 +428,6 @@ protected theorem le_lt_asymm : ∀{a b : Nat}, a ≤ b → ¬(b < a) := flip Na
 
 theorem gt_of_not_le {n m : Nat} (h : ¬ n ≤ m) : n > m := (Nat.lt_or_ge m n).resolve_right h
 protected theorem lt_of_not_ge : ∀{a b : Nat}, ¬(b ≥ a) → b < a := Nat.gt_of_not_le
-protected theorem lt_of_not_le : ∀{a b : Nat}, ¬(a ≤ b) → b < a := Nat.gt_of_not_le
 
 theorem ge_of_not_lt {n m : Nat} (h : ¬ n < m) : n ≥ m := (Nat.lt_or_ge n m).resolve_left h
 protected theorem le_of_not_gt : ∀{a b : Nat}, ¬(b > a) → b ≤ a := Nat.ge_of_not_lt
@@ -770,10 +740,6 @@ protected theorem mul_lt_mul_of_pos_left {n m k : Nat} (h : n < m) (hk : k > 0)
 protected theorem mul_lt_mul_of_pos_right {n m k : Nat} (h : n < m) (hk : k > 0) : n * k < m * k :=
   Nat.mul_comm k m ▸ Nat.mul_comm k n ▸ Nat.mul_lt_mul_of_pos_left h hk
 
-protected theorem mul_pos {n m : Nat} (ha : n > 0) (hb : m > 0) : n * m > 0 :=
-  have h : 0 * m < n * m := Nat.mul_lt_mul_of_pos_right ha hb
-  Nat.zero_mul m ▸ h
-
 protected theorem le_of_mul_le_mul_left {a b c : Nat} (h : c * a ≤ c * b) (hc : 0 < c) : a ≤ b :=
   Nat.ge_of_not_lt fun hlt : b < a =>
     have h' : c * b < c * a := Nat.mul_lt_mul_of_pos_left hlt hc
@@ -833,11 +799,6 @@ set_option linter.missingDocs false in
 @[deprecated Nat.pow_le_pow_right (since := "2025-02-17")]
 abbrev pow_le_pow_of_le_right := @Nat.pow_le_pow_right
 
-protected theorem pow_pos (h : 0 < a) : 0 < a^n :=
-  match n with
-  | 0 => Nat.zero_lt_one
-  | _ + 1 => Nat.mul_pos (Nat.pow_pos h) h
-
 set_option linter.missingDocs false in
 @[deprecated Nat.pow_pos (since := "2025-02-17")]
 abbrev pos_pow_of_pos := @Nat.pow_pos
@@ -1199,6 +1160,8 @@ protected theorem sub_eq_iff_eq_add {c : Nat} (h : b ≤ a) : a - b = c ↔ a =
 protected theorem sub_eq_iff_eq_add' {c : Nat} (h : b ≤ a) : a - b = c ↔ a = b + c := by
   rw [Nat.add_comm, Nat.sub_eq_iff_eq_add h]
 
+attribute [simp] sub_le
+
 protected theorem sub_one_sub_lt_of_lt (h : a < b) : b - 1 - a < b := by
   rw [← Nat.sub_add_eq]
   exact sub_lt (zero_lt_of_lt h) (Nat.lt_add_right a Nat.one_pos)
diff --git a/src/Init/Data/Nat/Div/Basic.lean b/src/Init/Data/Nat/Div/Basic.lean
index ff836ae506..8ac397759b 100644
--- a/src/Init/Data/Nat/Div/Basic.lean
+++ b/src/Init/Data/Nat/Div/Basic.lean
@@ -24,47 +24,6 @@ there is some `c` such that `b = a * c`.
 instance : Dvd Nat where
   dvd a b := Exists (fun c => b = a * c)
 
-theorem div_rec_lemma {x y : Nat} : 0 < y ∧ y ≤ x → x - y < x :=
-  fun ⟨ypos, ylex⟩ => sub_lt (Nat.lt_of_lt_of_le ypos ylex) ypos
-
-theorem div_rec_fuel_lemma {x y fuel : Nat} (hy : 0 < y) (hle : y ≤ x) (hfuel : x < fuel + 1) :
-    x - y < fuel :=
-  Nat.lt_of_lt_of_le (div_rec_lemma ⟨hy, hle⟩) (Nat.le_of_lt_succ hfuel)
-
-/--
-Division of natural numbers, discarding the remainder. Division by `0` returns `0`. Usually accessed
-via the `/` operator.
-
-This operation is sometimes called “floor division.”
-
-This function is overridden at runtime with an efficient implementation. This definition is
-the logical model.
-
-Examples:
- * `21 / 3 = 7`
- * `21 / 5 = 4`
- * `0 / 22 = 0`
- * `5 / 0 = 0`
--/
-@[extern "lean_nat_div", irreducible]
-protected def div (x y : @& Nat) : Nat :=
-  if hy : 0 < y then
-    let rec
-      go (fuel : Nat) (x : Nat) (hfuel : x < fuel) : Nat :=
-      match fuel with
-      | 0 => by contradiction
-      | succ fuel =>
-        if h : y ≤ x then
-          go fuel (x - y) (div_rec_fuel_lemma hy h hfuel) + 1
-        else
-          0
-      termination_by structural fuel
-    go (x + 1) x (Nat.lt_succ_self _)
-  else
-    0
-
-instance instDiv : Div Nat := ⟨Nat.div⟩
-
 private theorem div.go.fuel_congr (x y fuel1 fuel2 : Nat) (hy : 0 < y) (h1 : x < fuel1) (h2 : x < fuel2) :
     Nat.div.go y hy fuel1 x h1 = Nat.div.go y hy fuel2 x h2 := by
   match fuel1, fuel2 with
@@ -154,36 +113,6 @@ protected def divExact (x y : @& Nat) (h : y ∣ x) : Nat :=
 @[simp]
 theorem divExact_eq_div {x y : Nat} (h : y ∣ x) : x.divExact y h = x / y := rfl
 
-/--
-The modulo operator, which computes the remainder when dividing one natural number by another.
-Usually accessed via the `%` operator. When the divisor is `0`, the result is the dividend rather
-than an error.
-
-This is the core implementation of `Nat.mod`. It computes the correct result for any two closed
-natural numbers, but it does not have some convenient [definitional
-reductions](lean-manual://section/type-system) when the `Nat`s contain free variables. The wrapper
-`Nat.mod` handles those cases specially and then calls `Nat.modCore`.
-
-This function is overridden at runtime with an efficient implementation. This definition is the
-logical model.
--/
-@[extern "lean_nat_mod", irreducible]
-protected noncomputable def modCore (x y : Nat) : Nat :=
-  if hy : 0 < y then
-    let rec
-      go (fuel : Nat) (x : Nat) (hfuel : x < fuel) : Nat :=
-      match fuel with
-      | 0 => by contradiction
-      | succ fuel =>
-        if h : y ≤ x then
-          go fuel (x - y) (div_rec_fuel_lemma hy h hfuel)
-        else
-          x
-      termination_by structural fuel
-    go (x + 1) x (Nat.lt_succ_self _)
-  else
-    x
-
 private theorem modCore.go.fuel_congr (x y fuel1 fuel2 : Nat) (hy : 0 < y) (h1 : x < fuel1) (h2 : x < fuel2) :
     Nat.modCore.go y hy fuel1 x h1 = Nat.modCore.go y hy fuel2 x h2 := by
   match fuel1, fuel2 with
@@ -214,51 +143,6 @@ protected theorem modCore_eq (x y : Nat) : Nat.modCore x y =
   next =>
     simp only [false_and, ↓reduceIte, *]
 
-
-/--
-The modulo operator, which computes the remainder when dividing one natural number by another.
-Usually accessed via the `%` operator. When the divisor is `0`, the result is the dividend rather
-than an error.
-
-`Nat.mod` is a wrapper around `Nat.modCore` that special-cases two situations, giving better
-definitional reductions:
- * `Nat.mod 0 m` should reduce to `m`, for all terms `m : Nat`.
- * `Nat.mod n (m + n + 1)` should reduce to `n` for concrete `Nat` literals `n`.
-
-These reductions help `Fin n` literals work well, because the `OfNat` instance for `Fin` uses
-`Nat.mod`. In particular, `(0 : Fin (n + 1)).val` should reduce definitionally to `0`. `Nat.modCore`
-can handle all numbers, but its definitional reductions are not as convenient.
-
-This function is overridden at runtime with an efficient implementation. This definition is the
-logical model.
-
-Examples:
- * `7 % 2 = 1`
- * `9 % 3 = 0`
- * `5 % 7 = 5`
- * `5 % 0 = 5`
- * `show ∀ (n : Nat), 0 % n = 0 from fun _ => rfl`
- * `show ∀ (m : Nat), 5 % (m + 6) = 5 from fun _ => rfl`
--/
-@[extern "lean_nat_mod"]
-protected def mod : @& Nat → @& Nat → Nat
-  /-
-  Nat.modCore is defined with fuel and thus does not reduce with open terms very well.
-  Nevertheless it is desirable for trivial `Nat.mod` calculations, namely
-  * `Nat.mod 0 m` for all `m`
-  * `Nat.mod n (m + n + 1)` for concrete literals `n`,
-  to reduce definitionally.
-  This property is desirable for `Fin n` literals, as it means `(ofNat 0 : Fin n).val = 0` by
-  definition.
-   -/
-  | 0, _ => 0
-  | n@(_ + 1), m =>
-    if m ≤ n -- NB: if n < m does not reduce as well as `m ≤ n`!
-    then Nat.modCore n m
-    else n
-
-instance instMod : Mod Nat := ⟨Nat.mod⟩
-
 protected theorem modCore_eq_mod (n m : Nat) : Nat.modCore n m = n % m := by
   change Nat.modCore n m = Nat.mod n m
   match n, m with
@@ -315,24 +199,6 @@ theorem mod_eq_sub_mod {a b : Nat} (h : a ≥ b) : a % b = (a - b) % b :=
   | Or.inl h₁ => h₁.symm ▸ (Nat.sub_zero a).symm ▸ rfl
   | Or.inr h₁ => (mod_eq a b).symm ▸ if_pos ⟨h₁, h⟩
 
-theorem mod_lt (x : Nat) {y : Nat} : y > 0 → x % y < y := by
-  induction x, y using mod.inductionOn with
-  | base x y h₁ =>
-    intro h₂
-    have h₁ : ¬ 0 < y ∨ ¬ y ≤ x := Decidable.not_and_iff_or_not.mp h₁
-    match h₁ with
-    | Or.inl h₁ => exact absurd h₂ h₁
-    | Or.inr h₁ =>
-      have hgt : y > x := gt_of_not_le h₁
-      have heq : x % y = x := mod_eq_of_lt hgt
-      rw [← heq] at hgt
-      exact hgt
-  | ind x y h h₂ =>
-    intro h₃
-    have ⟨_, h₁⟩ := h
-    rw [mod_eq_sub_mod h₁]
-    exact h₂ h₃
-
 @[simp] protected theorem sub_mod_add_mod_cancel (a b : Nat) [NeZero a] : a - b % a + b % a = a := by
   rw [Nat.sub_add_cancel]
   cases a with
diff --git a/src/Init/Data/Nat/Lemmas.lean b/src/Init/Data/Nat/Lemmas.lean
index 7185dc6c8b..a475956bd0 100644
--- a/src/Init/Data/Nat/Lemmas.lean
+++ b/src/Init/Data/Nat/Lemmas.lean
@@ -264,9 +264,6 @@ protected theorem pos_of_lt_add_left : n < k + n → 0 < k := by
 protected theorem add_pos_left (h : 0 < m) (n) : 0 < m + n :=
   Nat.lt_of_lt_of_le h (Nat.le_add_right ..)
 
-protected theorem add_pos_right (m) (h : 0 < n) : 0 < m + n :=
-  Nat.lt_of_lt_of_le h (Nat.le_add_left ..)
-
 protected theorem add_self_ne_one : ∀ n, n + n ≠ 1
   | n+1, h => by rw [Nat.succ_add, Nat.succ.injEq] at h; contradiction
 
diff --git a/src/Init/Data/String/Extra.lean b/src/Init/Data/String/Extra.lean
index 2322a2d283..15c06af6c0 100644
--- a/src/Init/Data/String/Extra.lean
+++ b/src/Init/Data/String/Extra.lean
@@ -11,6 +11,7 @@ import all Init.Data.ByteArray.Basic
 public import Init.Data.String.Basic
 import all Init.Data.String.Basic
 import Init.Data.UInt.Lemmas
+import Init.Data.UInt.Bitwise
 
 public section
 
@@ -135,7 +136,7 @@ the corresponding string, or panics if the array is not a valid UTF-8 encoding o
 /--
 Returns the sequence of bytes in a character's UTF-8 encoding.
 -/
-def utf8EncodeChar (c : Char) : List UInt8 :=
+def utf8EncodeCharFast (c : Char) : List UInt8 :=
   let v := c.val
   if v ≤ 0x7f then
     [v.toUInt8]
@@ -152,8 +153,58 @@ def utf8EncodeChar (c : Char) : List UInt8 :=
      (v >>>  6).toUInt8 &&& 0x3f ||| 0x80,
               v.toUInt8 &&& 0x3f ||| 0x80]
 
+private theorem Nat.add_two_pow_eq_or_of_lt {b : Nat} (i : Nat) (b_lt : b < 2 ^ i) (a : Nat) :
+    b + 2 ^ i * a = b ||| 2 ^ i * a := by
+  rw [Nat.add_comm, Nat.or_comm, Nat.two_pow_add_eq_or_of_lt b_lt]
+
+@[csimp]
+theorem utf8EncodeChar_eq_utf8EncodeCharFast : @utf8EncodeChar = @utf8EncodeCharFast := by
+  funext c
+  simp only [utf8EncodeChar, utf8EncodeCharFast, UInt8.ofNat_uInt32ToNat, UInt8.ofNat_add,
+    UInt8.reduceOfNat, UInt32.le_iff_toNat_le, UInt32.reduceToNat]
+  split
+  · rfl
+  · split
+    · simp only [List.cons.injEq, ← UInt8.toNat_inj, UInt8.toNat_add, UInt8.toNat_ofNat',
+        Nat.reducePow, UInt8.reduceToNat, Nat.mod_add_mod, UInt8.toNat_or, UInt8.toNat_and,
+        UInt32.toNat_toUInt8, UInt32.toNat_shiftRight, UInt32.reduceToNat, Nat.reduceMod, and_true]
+      refine ⟨?_, ?_⟩
+      · rw [Nat.mod_eq_of_lt (by omega), Nat.add_two_pow_eq_or_of_lt 5 (by omega) 6,
+          Nat.and_two_pow_sub_one_eq_mod _ 5, Nat.shiftRight_eq_div_pow,
+          Nat.mod_eq_of_lt (b := 256) (by omega)]
+      · rw [Nat.mod_eq_of_lt (by omega), Nat.add_two_pow_eq_or_of_lt 6 (by omega) 2,
+          Nat.and_two_pow_sub_one_eq_mod _ 6, Nat.mod_mod_of_dvd _ (by decide)]
+    · split
+      · simp only [List.cons.injEq, ← UInt8.toNat_inj, UInt8.toNat_add, UInt8.toNat_ofNat',
+          Nat.reducePow, UInt8.reduceToNat, Nat.mod_add_mod, UInt8.toNat_or, UInt8.toNat_and,
+          UInt32.toNat_toUInt8, UInt32.toNat_shiftRight, UInt32.reduceToNat, Nat.reduceMod, and_true]
+        refine ⟨?_, ?_, ?_⟩
+        · rw [Nat.mod_eq_of_lt (by omega), Nat.add_two_pow_eq_or_of_lt 4 (by omega) 14,
+            Nat.and_two_pow_sub_one_eq_mod _ 4, Nat.shiftRight_eq_div_pow,
+            Nat.mod_eq_of_lt (b := 256) (by omega)]
+        · rw [Nat.mod_eq_of_lt (by omega), Nat.add_two_pow_eq_or_of_lt 6 (by omega) 2,
+            Nat.and_two_pow_sub_one_eq_mod _ 6, Nat.shiftRight_eq_div_pow,
+            Nat.mod_mod_of_dvd (c.val.toNat / 2 ^ 6) (by decide)]
+        · rw [Nat.mod_eq_of_lt (by omega), Nat.add_two_pow_eq_or_of_lt 6 (by omega) 2,
+            Nat.and_two_pow_sub_one_eq_mod _ 6, Nat.mod_mod_of_dvd c.val.toNat (by decide)]
+      · simp only [List.cons.injEq, ← UInt8.toNat_inj, UInt8.toNat_add, UInt8.toNat_ofNat',
+          Nat.reducePow, UInt8.reduceToNat, Nat.mod_add_mod, UInt8.toNat_or, UInt8.toNat_and,
+          UInt32.toNat_toUInt8, UInt32.toNat_shiftRight, UInt32.reduceToNat, Nat.reduceMod, and_true]
+        refine ⟨?_, ?_, ?_, ?_⟩
+        · rw [Nat.mod_eq_of_lt (by omega), Nat.add_two_pow_eq_or_of_lt 3 (by omega) 30,
+            Nat.and_two_pow_sub_one_eq_mod _ 3, Nat.shiftRight_eq_div_pow,
+            Nat.mod_mod_of_dvd _ (by decide)]
+        · rw [Nat.mod_eq_of_lt (by omega), Nat.add_two_pow_eq_or_of_lt 6 (by omega) 2,
+            Nat.and_two_pow_sub_one_eq_mod _ 6, Nat.shiftRight_eq_div_pow,
+            Nat.mod_mod_of_dvd (c.val.toNat / 2 ^ 12) (by decide)]
+        · rw [Nat.mod_eq_of_lt (by omega), Nat.add_two_pow_eq_or_of_lt 6 (by omega) 2,
+            Nat.and_two_pow_sub_one_eq_mod _ 6, Nat.shiftRight_eq_div_pow,
+            Nat.mod_mod_of_dvd (c.val.toNat / 2 ^ 6) (by decide)]
+        · rw [Nat.mod_eq_of_lt (by omega), Nat.add_two_pow_eq_or_of_lt 6 (by omega) 2,
+            Nat.and_two_pow_sub_one_eq_mod _ 6, Nat.mod_mod_of_dvd c.val.toNat (by decide)]
+
 @[simp] theorem length_utf8EncodeChar (c : Char) : (utf8EncodeChar c).length = c.utf8Size := by
-  simp [Char.utf8Size, utf8EncodeChar]
+  simp [Char.utf8Size, utf8EncodeChar_eq_utf8EncodeCharFast, utf8EncodeCharFast]
   cases Decidable.em (c.val ≤ 0x7f) <;> simp [*]
   cases Decidable.em (c.val ≤ 0x7ff) <;> simp [*]
   cases Decidable.em (c.val ≤ 0xffff) <;> simp [*]
diff --git a/src/Init/Data/UInt/BasicAux.lean b/src/Init/Data/UInt/BasicAux.lean
index 89e555e253..2f7b00cbbc 100644
--- a/src/Init/Data/UInt/BasicAux.lean
+++ b/src/Init/Data/UInt/BasicAux.lean
@@ -29,21 +29,6 @@ def UInt8.toFin (x : UInt8) : Fin UInt8.size := x.toBitVec.toFin
 @[deprecated UInt8.toFin (since := "2025-02-12"), inherit_doc UInt8.toFin]
 def UInt8.val (x : UInt8) : Fin UInt8.size := x.toFin
 
-/--
-Converts a natural number to an 8-bit unsigned integer, wrapping on overflow.
-
-This function is overridden at runtime with an efficient implementation.
-
-Examples:
- * `UInt8.ofNat 5 = 5`
- * `UInt8.ofNat 255 = 255`
- * `UInt8.ofNat 256 = 0`
- * `UInt8.ofNat 259 = 3`
- * `UInt8.ofNat 32770 = 2`
--/
-@[extern "lean_uint8_of_nat"]
-def UInt8.ofNat (n : @& Nat) : UInt8 := ⟨BitVec.ofNat 8 n⟩
-
 /--
 Converts a natural number to an 8-bit unsigned integer, returning the largest representable value if
 the number is too large.
@@ -222,8 +207,8 @@ instance UInt32.instOfNat : OfNat UInt32 n := ⟨UInt32.ofNat n⟩
 
 theorem UInt32.ofNatLT_lt_of_lt {n m : Nat} (h1 : n < UInt32.size) (h2 : m < UInt32.size) :
      n < m → UInt32.ofNatLT n h1 < UInt32.ofNat m := by
-  simp only [(· < ·), BitVec.toNat, ofNatLT, BitVec.ofNatLT, ofNat, BitVec.ofNat, Fin.ofNat,
-    Nat.mod_eq_of_lt h2, imp_self]
+  simp only [(· < ·), BitVec.toNat, ofNatLT, BitVec.ofNatLT, ofNat, BitVec.ofNat,
+    Fin.Internal.ofNat_eq_ofNat, Fin.ofNat, Nat.mod_eq_of_lt h2, imp_self]
 
 @[deprecated UInt32.ofNatLT_lt_of_lt (since := "2025-02-13")]
 theorem UInt32.ofNat'_lt_of_lt {n m : Nat} (h1 : n < UInt32.size) (h2 : m < UInt32.size) :
@@ -231,8 +216,8 @@ theorem UInt32.ofNat'_lt_of_lt {n m : Nat} (h1 : n < UInt32.size) (h2 : m < UInt
 
 theorem UInt32.lt_ofNatLT_of_lt {n m : Nat} (h1 : n < UInt32.size) (h2 : m < UInt32.size) :
      m < n → UInt32.ofNat m < UInt32.ofNatLT n h1 := by
-  simp only [(· < ·), BitVec.toNat, ofNatLT, BitVec.ofNatLT, ofNat, BitVec.ofNat, Fin.ofNat,
-    Nat.mod_eq_of_lt h2, imp_self]
+  simp only [(· < ·), BitVec.toNat, ofNatLT, BitVec.ofNatLT, ofNat, BitVec.ofNat, Fin.Internal.ofNat_eq_ofNat,
+    Fin.ofNat, Nat.mod_eq_of_lt h2, imp_self]
 
 @[deprecated UInt32.lt_ofNatLT_of_lt (since := "2025-02-13")]
 theorem UInt32.lt_ofNat'_of_lt {n m : Nat} (h1 : n < UInt32.size) (h2 : m < UInt32.size) :
diff --git a/src/Init/GrindInstances/Ring/UInt.lean b/src/Init/GrindInstances/Ring/UInt.lean
index 718f42ec56..fdb62bb96d 100644
--- a/src/Init/GrindInstances/Ring/UInt.lean
+++ b/src/Init/GrindInstances/Ring/UInt.lean
@@ -40,7 +40,7 @@ theorem intCast_ofNat (x : Nat) : (OfNat.ofNat (α := Int) x : UInt8) = OfNat.of
     rw [Int.toNat_emod (Int.zero_le_ofNat x) (by decide)]
     erw [Int.toNat_natCast]
     rw [Int.toNat_pow_of_nonneg (by decide)]
-    simp only [ofNat, BitVec.ofNat, Fin.ofNat, Int.reduceToNat, Nat.dvd_refl,
+    simp only [ofNat, BitVec.ofNat, Fin.Internal.ofNat_eq_ofNat, Fin.ofNat, Int.reduceToNat, Nat.dvd_refl,
       Nat.mod_mod_of_dvd, instOfNat]
 
 end UInt8
@@ -70,7 +70,7 @@ theorem intCast_ofNat (x : Nat) : (OfNat.ofNat (α := Int) x : UInt16) = OfNat.o
     rw [Int.toNat_emod (Int.zero_le_ofNat x) (by decide)]
     erw [Int.toNat_natCast]
     rw [Int.toNat_pow_of_nonneg (by decide)]
-    simp only [ofNat, BitVec.ofNat, Fin.ofNat, Int.reduceToNat, Nat.dvd_refl,
+    simp only [ofNat, BitVec.ofNat, Fin.Internal.ofNat_eq_ofNat, Fin.ofNat, Int.reduceToNat, Nat.dvd_refl,
       Nat.mod_mod_of_dvd, instOfNat]
 
 end UInt16
@@ -100,7 +100,7 @@ theorem intCast_ofNat (x : Nat) : (OfNat.ofNat (α := Int) x : UInt32) = OfNat.o
     rw [Int.toNat_emod (Int.zero_le_ofNat x) (by decide)]
     erw [Int.toNat_natCast]
     rw [Int.toNat_pow_of_nonneg (by decide)]
-    simp only [ofNat, BitVec.ofNat, Fin.ofNat, Int.reduceToNat, Nat.dvd_refl,
+    simp only [ofNat, BitVec.ofNat, Fin.Internal.ofNat_eq_ofNat, Fin.ofNat, Int.reduceToNat, Nat.dvd_refl,
       Nat.mod_mod_of_dvd, instOfNat]
 
 end UInt32
@@ -130,7 +130,7 @@ theorem intCast_ofNat (x : Nat) : (OfNat.ofNat (α := Int) x : UInt64) = OfNat.o
     rw [Int.toNat_emod (Int.zero_le_ofNat x) (by decide)]
     erw [Int.toNat_natCast]
     rw [Int.toNat_pow_of_nonneg (by decide)]
-    simp only [ofNat, BitVec.ofNat, Fin.ofNat, Int.reduceToNat, Nat.dvd_refl,
+    simp only [ofNat, BitVec.ofNat, Fin.Internal.ofNat_eq_ofNat, Fin.ofNat, Int.reduceToNat, Nat.dvd_refl,
       Nat.mod_mod_of_dvd, instOfNat]
 
 end UInt64
@@ -157,7 +157,7 @@ theorem intCast_ofNat (x : Nat) : (OfNat.ofNat (α := Int) x : USize) = OfNat.of
     rw [Int.toNat_emod (Int.zero_le_ofNat x)]
     · erw [Int.toNat_natCast]
       rw [Int.toNat_pow_of_nonneg (by decide)]
-      simp only [ofNat, BitVec.ofNat, Fin.ofNat, Int.reduceToNat, Nat.dvd_refl,
+      simp only [ofNat, BitVec.ofNat, Fin.Internal.ofNat_eq_ofNat, Fin.ofNat, Int.reduceToNat, Nat.dvd_refl,
         Nat.mod_mod_of_dvd, instOfNat]
     · obtain _ | _ := System.Platform.numBits_eq <;> simp_all
 
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 5ea203ebe9..e97e013b01 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -1865,6 +1865,9 @@ protected theorem Nat.le_trans {n m k : Nat} : LE.le n m → LE.le m k → LE.le
   | h,  Nat.le.refl    => h
   | h₁, Nat.le.step h₂ => Nat.le.step (Nat.le_trans h₁ h₂)
 
+protected theorem Nat.lt_of_lt_of_le {n m k : Nat} : LT.lt n m → LE.le m k → LT.lt n k :=
+  Nat.le_trans
+
 protected theorem Nat.lt_trans {n m k : Nat} (h₁ : LT.lt n m) : LT.lt m k → LT.lt n k :=
   Nat.le_trans (le_step h₁)
 
@@ -1968,6 +1971,27 @@ theorem Nat.ble_eq_true_of_le (h : LE.le n m) : Eq (Nat.ble n m) true :=
 theorem Nat.not_le_of_not_ble_eq_true (h : Not (Eq (Nat.ble n m) true)) : Not (LE.le n m) :=
   fun h' => absurd (Nat.ble_eq_true_of_le h') h
 
+theorem Nat.lt_succ_of_le {n m : Nat} : LE.le n m → LT.lt n (succ m) := succ_le_succ
+
+protected theorem Nat.lt_add_one (n : Nat) : LT.lt n (HAdd.hAdd n 1) := Nat.le_refl (succ n)
+
+theorem Nat.lt_succ_self (n : Nat) : LT.lt n (succ n) := Nat.lt_add_one _
+
+protected theorem Nat.lt_of_not_le {a b : Nat} (h : Not (LE.le a b)) : LT.lt b a :=
+  (Nat.lt_or_ge b a).resolve_right h
+
+protected theorem Nat.add_pos_right :
+    {b : Nat} → (a : Nat) → (hb : LT.lt 0 b) → LT.lt 0 (HAdd.hAdd a b)
+  | succ _, _, _ => Nat.zero_lt_succ _
+
+protected theorem Nat.mul_pos :
+    {n m : Nat} → (hn : LT.lt 0 n) → (hm : LT.lt 0 m) → LT.lt 0 (HMul.hMul n m)
+  | _, succ _, ha, _ => Nat.add_pos_right _ ha
+
+protected theorem Nat.pow_pos {a : Nat} : {n : Nat} → (h : LT.lt 0 a) → LT.lt 0 (HPow.hPow a n)
+  | zero, _ => Nat.zero_lt_succ _
+  | succ _, h => Nat.mul_pos (Nat.pow_pos h) h
+
 /--
 A decision procedure for non-strict inequality of natural numbers, usually accessed via the
 `DecidableLE Nat` instance.
@@ -2021,6 +2045,160 @@ protected def Nat.sub : (@& Nat) → (@& Nat) → Nat
 instance instSubNat : Sub Nat where
   sub := Nat.sub
 
+theorem Nat.succ_sub_succ_eq_sub (n m : Nat) : Eq (HSub.hSub (succ n) (succ m)) (HSub.hSub n m) :=
+  m.rec rfl (fun _ ih => congrArg pred ih)
+
+theorem Nat.pred_le : ∀ (n : Nat), LE.le (Nat.pred n) n
+  | zero   => Nat.le.refl
+  | succ _ => le_succ _
+
+theorem Nat.sub_le (n m : Nat) : LE.le (HSub.hSub n m) n :=
+  m.rec (Nat.le_refl _) (fun _ ih => Nat.le_trans (pred_le _) ih)
+
+theorem Nat.sub_lt : ∀ {n m : Nat}, LT.lt 0 n → LT.lt 0 m → LT.lt (HSub.hSub n m) n
+  | 0,   _,   h1, _  => absurd h1 (Nat.lt_irrefl 0)
+  | Nat.succ _, 0,   _, h2  => absurd h2 (Nat.lt_irrefl 0)
+  | Nat.succ n, Nat.succ m, _,  _  =>
+    Eq.symm (succ_sub_succ_eq_sub n m) ▸
+      show LT.lt (HSub.hSub n m) (succ n) from
+      lt_succ_of_le (sub_le n m)
+
+theorem Nat.div_rec_lemma {x y : Nat} :
+    (And (LT.lt 0 y) (LE.le y x)) → LT.lt (HSub.hSub x y) x :=
+  fun ⟨ypos, ylex⟩ => sub_lt (Nat.lt_of_lt_of_le ypos ylex) ypos
+
+theorem Nat.div_rec_fuel_lemma {x y fuel : Nat} (hy : LT.lt 0 y) (hle : LE.le y x)
+    (hfuel : LT.lt x (HAdd.hAdd fuel 1)) : LT.lt (HSub.hSub x y) fuel :=
+  Nat.lt_of_lt_of_le (div_rec_lemma ⟨hy, hle⟩) (Nat.le_of_lt_succ hfuel)
+
+set_option bootstrap.genMatcherCode false in
+/--
+Division of natural numbers, discarding the remainder. Division by `0` returns `0`. Usually accessed
+via the `/` operator.
+
+This operation is sometimes called “floor division.”
+
+This function is overridden at runtime with an efficient implementation. This definition is
+the logical model.
+
+Examples:
+ * `21 / 3 = 7`
+ * `21 / 5 = 4`
+ * `0 / 22 = 0`
+ * `5 / 0 = 0`
+-/
+@[extern "lean_nat_div", irreducible]
+protected def Nat.div (x y : @& Nat) : Nat :=
+  dite (LT.lt 0 y) (fun hy =>
+    let rec
+      go (fuel : Nat) (x : Nat) (hfuel : LT.lt x fuel) : Nat :=
+      match fuel with
+      | succ fuel =>
+        dite (LE.le y x)
+          (fun h => HAdd.hAdd (go fuel (HSub.hSub x y) (div_rec_fuel_lemma hy h hfuel)) 1)
+          (fun _ => 0)
+      termination_by structural fuel
+    go (succ x) x (Nat.lt_succ_self _))
+    (fun _ => 0)
+
+instance Nat.instDiv : Div Nat := ⟨Nat.div⟩
+
+set_option bootstrap.genMatcherCode false in
+/--
+The modulo operator, which computes the remainder when dividing one natural number by another.
+Usually accessed via the `%` operator. When the divisor is `0`, the result is the dividend rather
+than an error.
+
+This is the core implementation of `Nat.mod`. It computes the correct result for any two closed
+natural numbers, but it does not have some convenient [definitional
+reductions](lean-manual://section/type-system) when the `Nat`s contain free variables. The wrapper
+`Nat.mod` handles those cases specially and then calls `Nat.modCore`.
+
+This function is overridden at runtime with an efficient implementation. This definition is the
+logical model.
+-/
+@[extern "lean_nat_mod"]
+protected noncomputable def Nat.modCore (x y : Nat) : Nat :=
+  dite (LT.lt 0 y)
+    (fun hy =>
+      let rec
+        go (fuel : Nat) (x : Nat) (hfuel : LT.lt x fuel) : Nat :=
+        match fuel with
+        | succ fuel =>
+          dite (LE.le y x)
+            (fun h => go fuel (HSub.hSub x y) (div_rec_fuel_lemma hy h hfuel))
+            (fun _ => x)
+        termination_by structural fuel
+      go (succ x) x (Nat.lt_succ_self _))
+    (fun _ => x)
+
+theorem Nat.modCoreGo_lt {fuel y : Nat} (hy : LT.lt 0 y) : (x : Nat) → (hfuel : LT.lt x fuel) →
+    LT.lt (Nat.modCore.go y hy fuel x hfuel) y :=
+  fuel.rec (fun _ h => absurd h (Nat.not_lt_zero _))
+    (fun _ ih x _ =>
+      show LT.lt (dite _ _ _) _ from
+        match Nat.decLe y x with
+        | .isTrue _ => ih _ _
+        | .isFalse h => Nat.lt_of_not_le h)
+
+theorem Nat.modCore_lt {x y : Nat} (hy : LT.lt 0 y) : LT.lt (Nat.modCore x y) y :=
+  show LT.lt (dite _ _ _) y from
+    match Nat.decLt 0 y with
+    | .isTrue _ => Nat.modCoreGo_lt hy x (Nat.lt_succ_self _)
+    | .isFalse h => absurd hy h
+
+attribute [irreducible] Nat.modCore
+
+set_option bootstrap.genMatcherCode false in
+/--
+The modulo operator, which computes the remainder when dividing one natural number by another.
+Usually accessed via the `%` operator. When the divisor is `0`, the result is the dividend rather
+than an error.
+
+`Nat.mod` is a wrapper around `Nat.modCore` that special-cases two situations, giving better
+definitional reductions:
+ * `Nat.mod 0 m` should reduce to `m`, for all terms `m : Nat`.
+ * `Nat.mod n (m + n + 1)` should reduce to `n` for concrete `Nat` literals `n`.
+
+These reductions help `Fin n` literals work well, because the `OfNat` instance for `Fin` uses
+`Nat.mod`. In particular, `(0 : Fin (n + 1)).val` should reduce definitionally to `0`. `Nat.modCore`
+can handle all numbers, but its definitional reductions are not as convenient.
+
+This function is overridden at runtime with an efficient implementation. This definition is the
+logical model.
+
+Examples:
+ * `7 % 2 = 1`
+ * `9 % 3 = 0`
+ * `5 % 7 = 5`
+ * `5 % 0 = 5`
+ * `show ∀ (n : Nat), 0 % n = 0 from fun _ => rfl`
+ * `show ∀ (m : Nat), 5 % (m + 6) = 5 from fun _ => rfl`
+-/
+@[extern "lean_nat_mod"]
+protected def Nat.mod : @& Nat → @& Nat → Nat
+  /-
+  Nat.modCore is defined with fuel and thus does not reduce with open terms very well.
+  Nevertheless it is desirable for trivial `Nat.mod` calculations, namely
+  * `Nat.mod 0 m` for all `m`
+  * `Nat.mod n (m + n + 1)` for concrete literals `n`,
+  to reduce definitionally.
+  This property is desirable for `Fin n` literals, as it means `(ofNat 0 : Fin n).val = 0` by
+  definition.
+   -/
+  | 0, _ => 0
+  | n@(succ _), m => ite (LE.le m n) (Nat.modCore n m) n
+
+instance Nat.instMod : Mod Nat := ⟨Nat.mod⟩
+
+theorem Nat.mod_lt : (x : Nat) →  {y : Nat} → (hy : LT.lt 0 y) → LT.lt (HMod.hMod x y) y
+  | 0, succ _, _ => Nat.zero_lt_succ _
+  | succ n, m, hm =>
+    show LT.lt (ite (LE.le m (succ n)) (Nat.modCore (succ n) m) (succ n)) _ from
+      match Nat.decLe m (succ n) with
+      | .isTrue _ => Nat.modCore_lt hm
+      | .isFalse h => Nat.lt_of_not_le h
+
 attribute [gen_constructor_elims] Nat
 
 /--
@@ -2090,6 +2268,14 @@ instance {n} : LE (Fin n) where
 instance Fin.decLt {n} (a b : Fin n) : Decidable (LT.lt a b) := Nat.decLt ..
 instance Fin.decLe {n} (a b : Fin n) : Decidable (LE.le a b) := Nat.decLe ..
 
+/--
+Returns `a` modulo `n` as a `Fin n`.
+
+This function exists for bootstrapping purposes. Use `Fin.ofNat` instead.
+-/
+@[expose] protected def Fin.Internal.ofNat (n : Nat) (hn : LT.lt 0 n) (a : Nat) : Fin n :=
+  ⟨HMod.hMod a n, Nat.mod_lt _ hn⟩
+
 /--
 A bitvector of the specified width.
 
@@ -2126,6 +2312,13 @@ instance : DecidableEq (BitVec w) := BitVec.decEq
 protected def BitVec.ofNatLT {w : Nat} (i : Nat) (p : LT.lt i (hPow 2 w)) : BitVec w where
   toFin := ⟨i, p⟩
 
+/--
+The bitvector with value `i mod 2^n`.
+-/
+@[expose, match_pattern]
+protected def BitVec.ofNat (n : Nat) (i : Nat) : BitVec n where
+  toFin := Fin.Internal.ofNat (HPow.hPow 2 n) (Nat.pow_pos (Nat.zero_lt_succ _)) i
+
 /--
 Return the underlying `Nat` that represents a bitvector.
 
@@ -2174,6 +2367,21 @@ This function is overridden at runtime with an efficient implementation.
 def UInt8.ofNatLT (n : @& Nat) (h : LT.lt n UInt8.size) : UInt8 where
   toBitVec := BitVec.ofNatLT n h
 
+/--
+Converts a natural number to an 8-bit unsigned integer, wrapping on overflow.
+
+This function is overridden at runtime with an efficient implementation.
+
+Examples:
+ * `UInt8.ofNat 5 = 5`
+ * `UInt8.ofNat 255 = 255`
+ * `UInt8.ofNat 256 = 0`
+ * `UInt8.ofNat 259 = 3`
+ * `UInt8.ofNat 32770 = 2`
+-/
+@[extern "lean_uint8_of_nat"]
+def UInt8.ofNat (n : @& Nat) : UInt8 := ⟨BitVec.ofNat 8 n⟩
+
 set_option bootstrap.genMatcherCode false in
 /--
 Decides whether two 8-bit unsigned integers are equal. Usually accessed via the `DecidableEq UInt8`
@@ -2784,6 +2992,37 @@ def List.concat {α : Type u} : List α → α → List α
   | nil,       b => cons b nil
   | cons a as, b => cons a (concat as b)
 
+/--
+Returns the sequence of bytes in a character's UTF-8 encoding.
+-/
+def String.utf8EncodeChar (c : Char) : List UInt8 :=
+  let v := c.val.toNat
+  ite (LE.le v 0x7f)
+    (List.cons (UInt8.ofNat v) List.nil)
+    (ite (LE.le v 0x7ff)
+      (List.cons
+        (UInt8.ofNat (HAdd.hAdd (HMod.hMod (HDiv.hDiv v 64) 0x20) 0xc0))
+        (List.cons
+          (UInt8.ofNat (HAdd.hAdd (HMod.hMod v 0x40) 0x80))
+          List.nil))
+      (ite (LE.le v 0xffff)
+        (List.cons
+          (UInt8.ofNat (HAdd.hAdd (HMod.hMod (HDiv.hDiv v 4096) 0x10) 0xe0))
+          (List.cons
+            (UInt8.ofNat (HAdd.hAdd (HMod.hMod (HDiv.hDiv v 64) 0x40) 0x80))
+            (List.cons
+              (UInt8.ofNat (HAdd.hAdd (HMod.hMod v 0x40) 0x80))
+              List.nil)))
+        (List.cons
+          (UInt8.ofNat (HAdd.hAdd (HMod.hMod (HDiv.hDiv v 262144) 0x08) 0xf0))
+          (List.cons
+            (UInt8.ofNat (HAdd.hAdd (HMod.hMod (HDiv.hDiv v 4096) 0x40) 0x80))
+            (List.cons
+              (UInt8.ofNat (HAdd.hAdd (HMod.hMod (HDiv.hDiv v 64) 0x40) 0x80))
+              (List.cons
+                (UInt8.ofNat (HAdd.hAdd (HMod.hMod v 0x40) 0x80))
+                List.nil))))))
+
 /--
 A string is a sequence of Unicode code points.
 
diff --git a/src/lake/Lake/Reservoir.lean b/src/lake/Lake/Reservoir.lean
index e33a60451f..f41e528ae6 100644
--- a/src/lake/Lake/Reservoir.lean
+++ b/src/lake/Lake/Reservoir.lean
@@ -151,7 +151,7 @@ public abbrev foldlUtf8 (c : Char) (f : σ → UInt8 → σ) (init : σ) : σ :=
   Id.run <| foldlUtf8M c (pure <| f · ·) init
 
 example : foldlUtf8 c (fun l b => b::l) List.nil = (String.utf8EncodeChar c).reverse := by
-  simp only [foldlUtf8, foldlUtf8M, String.utf8EncodeChar]
+  simp only [foldlUtf8, foldlUtf8M, String.utf8EncodeChar_eq_utf8EncodeCharFast, String.utf8EncodeCharFast]
   if h1 : c.val ≤ 0x7f then simp [h1]
   else if h2 : c.val ≤ 0x7ff then simp [h1, h2]
   else if h3 : c.val ≤ 0xffff then simp [h1, h2, h3]
diff --git a/tests/lean/librarySearch.lean b/tests/lean/librarySearch.lean
index c7054b8e8f..1bfd3b9e4d 100644
--- a/tests/lean/librarySearch.lean
+++ b/tests/lean/librarySearch.lean
@@ -134,28 +134,28 @@ example {α : Type} (x y : α) : x = y ↔ y = x := by apply?
 
 /--
 info: Try this:
-  exact Nat.add_pos_left ha b
+  exact Nat.add_pos_right a hb
 -/
 #guard_msgs in
-example (a b : Nat) (ha : 0 < a) (_hb : 0 < b) : 0 < a + b := by apply?
+example (a b : Nat) (_ha : 0 < a) (hb : 0 < b) : 0 < a + b := by apply?
 
 /--
 info: Try this:
-  exact Nat.add_pos_left ha b
+  exact Nat.add_pos_right a hb
 -/
 #guard_msgs in
 -- Verify that if maxHeartbeats is 0 we don't stop immediately.
 set_option maxHeartbeats 0 in
-example (a b : Nat) (ha : 0 < a) (_hb : 0 < b) : 0 < a + b := by apply?
+example (a b : Nat) (_ha : 0 < a) (hb : 0 < b) : 0 < a + b := by apply?
 
 section synonym
 
 /--
 info: Try this:
-  exact Nat.add_pos_left ha b
+  exact Nat.add_pos_right a hb
 -/
 #guard_msgs in
-example (a b : Nat) (ha : a > 0) (_hb : 0 < b) : 0 < a + b := by apply?
+example (a b : Nat) (_ha : a > 0) (hb : 0 < b) : 0 < a + b := by apply?
 
 /--
 info: Try this:
diff --git a/tests/lean/run/PPTopDownAnalyze.lean b/tests/lean/run/PPTopDownAnalyze.lean
index f4b964923f..975ce50b85 100644
--- a/tests/lean/run/PPTopDownAnalyze.lean
+++ b/tests/lean/run/PPTopDownAnalyze.lean
@@ -337,7 +337,7 @@ set_option pp.analyze.trustSubtypeMk true in
 
 #testDelabN Nat.brecOn
 #testDelabN Nat.below
-#testDelabN Nat.mod_lt
+#testDelabN Nat.mod_eq_of_lt
 #testDelabN List.partition
 #testDelabN List.partition.loop
 #testDelabN StateT.modifyGet
@@ -360,6 +360,9 @@ set_option pp.analyze.trustSubtypeMk true in
 #testDelabN Lean.Server.FileWorker.handlePlainTermGoal
 #testDelabN Lean.Server.FileWorker.handlePlainGoal
 
+-- TODO: this hangs
+-- #testDelabN Nat.mod_lt
+
 -- TODO: this error occurs because we use a term's type to determine `blockImplicit` (@),
 -- whereas we should actually use the expected type based on the function being applied.
 -- #testDelabN HEq.subst
diff --git a/tests/lean/run/grind_bitvec2.lean b/tests/lean/run/grind_bitvec2.lean
index 78aa65b7b4..8177ad7cc1 100644
--- a/tests/lean/run/grind_bitvec2.lean
+++ b/tests/lean/run/grind_bitvec2.lean
@@ -79,7 +79,7 @@ theorem getElem_of_getLsbD_eq_true {x : BitVec w} {i : Nat} (h : x.getLsbD i = t
 This normalized a bitvec using `ofFin` to `ofNat`.
 -/
 theorem ofFin_eq_ofNat : @BitVec.ofFin w (Fin.mk x lt) = BitVec.ofNat w x := by
-  simp only [BitVec.ofNat, Fin.ofNat, lt, Nat.mod_eq_of_lt]
+  simp only [BitVec.ofNat, Fin.Internal.ofNat_eq_ofNat, Fin.ofNat, lt, Nat.mod_eq_of_lt]
 
 /-- Prove nonequality of bitvectors in terms of nat operations. -/
 theorem toNat_ne_iff_ne {n} {x y : BitVec n} : x.toNat ≠ y.toNat ↔ x ≠ y := by
@@ -212,7 +212,7 @@ theorem length_pos_of_ne {x y : BitVec w} (h : x ≠ y) : 0 < w := by grind
 
 theorem ofFin_ofNat (n : Nat) :
     ofFin (no_index (OfNat.ofNat n : Fin (2^w))) = OfNat.ofNat n := by
-  simp only [OfNat.ofNat, Fin.ofNat, BitVec.ofNat]
+  simp only [OfNat.ofNat, Fin.Internal.ofNat_eq_ofNat, Fin.ofNat, BitVec.ofNat]
 
 -- We use a `grind_pattern` as `@[grind]` will not use the `no_index` term.
 grind_pattern ofFin_ofNat => ofFin (OfNat.ofNat n : Fin (2^w))