fixes

While there appears to be an underlying issue of blocking tasks that
this specific PR is not resolving, it should alleviate the problems
described in
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/reliable.20file.20desync.20on.20Linux.20Mint
as it effectively reverts the relevant change introduced in 4.13.0-rc1
when the trace option is not set.

src/Init/Core.lean

@@ -1385,6 +1385,7 @@ gen_injective_theorems% Except
 gen_injective_theorems% EStateM.Result
 gen_injective_theorems% Lean.Name
 gen_injective_theorems% Lean.Syntax
+gen_injective_theorems% BitVec
 
 theorem Nat.succ.inj {m n : Nat} : m.succ = n.succ → m = n :=
   fun x => Nat.noConfusion x id
@@ -1864,7 +1865,8 @@ section
 variable {α : Type u}
 variable (r : α → α → Prop)
 
-instance {α : Sort u} {s : Setoid α} [d : ∀ (a b : α), Decidable (a ≈ b)] : DecidableEq (Quotient s) :=
+instance Quotient.decidableEq {α : Sort u} {s : Setoid α} [d : ∀ (a b : α), Decidable (a ≈ b)]
+    : DecidableEq (Quotient s) :=
   fun (q₁ q₂ : Quotient s) =>
     Quotient.recOnSubsingleton₂ q₁ q₂
       fun a₁ a₂ =>

src/Init/Data/Array/Basic.lean

@@ -7,7 +7,7 @@ prelude
 import Init.WFTactics
 import Init.Data.Nat.Basic
 import Init.Data.Fin.Basic
-import Init.Data.UInt.Basic
+import Init.Data.UInt.BasicAux
 import Init.Data.Repr
 import Init.Data.ToString.Basic
 import Init.GetElem
@@ -607,13 +607,17 @@ protected def appendList (as : Array α) (bs : List α) : Array α :=
 instance : HAppend (Array α) (List α) (Array α) := ⟨Array.appendList⟩
 
 @[inline]
-def concatMapM [Monad m] (f : α → m (Array β)) (as : Array α) : m (Array β) :=
+def flatMapM [Monad m] (f : α → m (Array β)) (as : Array α) : m (Array β) :=
   as.foldlM (init := empty) fun bs a => do return bs ++ (← f a)
 
+@[deprecated concatMapM (since := "2024-10-16")] abbrev concatMapM := @flatMapM
+
 @[inline]
-def concatMap (f : α → Array β) (as : Array α) : Array β :=
+def flatMap (f : α → Array β) (as : Array α) : Array β :=
   as.foldl (init := empty) fun bs a => bs ++ f a
 
+@[deprecated flatMap (since := "2024-10-16")] abbrev concatMap := @flatMap
+
 /-- Joins array of array into a single array.
 
 `flatten #[#[a₁, a₂, ⋯], #[b₁, b₂, ⋯], ⋯]` = `#[a₁, a₂, ⋯, b₁, b₂, ⋯]`

src/Init/Data/Array/Lemmas.lean

@@ -45,16 +45,6 @@ theorem getElem?_eq_getElem?_toList (a : Array α) (i : Nat) : a[i]? = a.toList[
   rw [getElem?_eq]
   split <;> simp_all
 
-@[deprecated getElem_eq_getElem_toList (since := "2024-09-25")]
-abbrev getElem_eq_toList_getElem := @getElem_eq_getElem_toList
-
-@[deprecated getElem_eq_toList_getElem (since := "2024-09-09")]
-abbrev getElem_eq_data_getElem := @getElem_eq_getElem_toList
-
-@[deprecated getElem_eq_toList_getElem (since := "2024-06-12")]
-theorem getElem_eq_toList_get (a : Array α) (h : i < a.size) : a[i] = a.toList.get ⟨i, h⟩ := by
-  simp
-
 theorem get_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
     have : i < (a.push x).size := by simp [*, Nat.lt_succ_of_le, Nat.le_of_lt]
     (a.push x)[i] = a[i] := by
@@ -77,7 +67,10 @@ namespace List
 
 open Array
 
-/-! ### Lemmas about `List.toArray`. -/
+/-! ### Lemmas about `List.toArray`.
+
+We prefer to pull `List.toArray` outwards.
+-/
 
 @[simp] theorem size_toArrayAux {a : List α} {b : Array α} :
     (a.toArrayAux b).size = b.size + a.length := by
@@ -85,20 +78,11 @@ open Array
 
 @[simp] theorem toArray_toList (a : Array α) : a.toList.toArray = a := rfl
 
-@[deprecated toArray_toList (since := "2024-09-09")]
-abbrev toArray_data := @toArray_toList
-
 @[simp] theorem getElem_toArray {a : List α} {i : Nat} (h : i < a.toArray.size) :
     a.toArray[i] = a[i]'(by simpa using h) := rfl
 
 @[simp] theorem getElem?_toArray {a : List α} {i : Nat} : a.toArray[i]? = a[i]? := rfl
 
-@[deprecated "Use the reverse direction of `List.push_toArray`." (since := "2024-09-27")]
-theorem toArray_concat {as : List α} {x : α} :
-    (as ++ [x]).toArray = as.toArray.push x := by
-  apply ext'
-  simp
-
 @[simp] theorem push_toArray (l : List α) (a : α) : l.toArray.push a = (l ++ [a]).toArray := by
   apply ext'
   simp
@@ -163,20 +147,12 @@ end List
 
 namespace Array
 
-attribute [simp] uset
-
 @[simp] theorem singleton_def (v : α) : singleton v = #[v] := rfl
 
 @[simp] theorem toArray_toList (a : Array α) : a.toList.toArray = a := rfl
 
-@[deprecated toArray_toList (since := "2024-09-09")]
-abbrev toArray_data := @toArray_toList
-
 @[simp] theorem length_toList {l : Array α} : l.toList.length = l.size := rfl
 
-@[deprecated length_toList (since := "2024-09-09")]
-abbrev data_length := @length_toList
-
 @[simp] theorem mkEmpty_eq (α n) : @mkEmpty α n = #[] := rfl
 
 @[simp] theorem size_mk (as : List α) : (Array.mk as).size = as.length := by simp [size]
@@ -225,9 +201,6 @@ where
     induction l generalizing arr <;> simp [*]
   simp [H]
 
-@[deprecated toList_map (since := "2024-09-09")]
-abbrev map_data := @toList_map
-
 @[simp] theorem size_map (f : α → β) (arr : Array α) : (arr.map f).size = arr.size := by
   simp only [← length_toList]
   simp
@@ -242,24 +215,16 @@ abbrev map_data := @toList_map
   cases arr
   simp
 
-theorem foldl_toList_eq_bind (l : List α) (acc : Array β)
+theorem foldl_toList_eq_flatMap (l : List α) (acc : Array β)
     (F : Array β → α → Array β) (G : α → List β)
     (H : ∀ acc a, (F acc a).toList = acc.toList ++ G a) :
-    (l.foldl F acc).toList = acc.toList ++ l.bind G := by
-  induction l generalizing acc <;> simp [*, List.bind]
-
-@[deprecated foldl_toList_eq_bind (since := "2024-09-09")]
-abbrev foldl_data_eq_bind := @foldl_toList_eq_bind
+    (l.foldl F acc).toList = acc.toList ++ l.flatMap G := by
+  induction l generalizing acc <;> simp [*, List.flatMap]
 
 theorem foldl_toList_eq_map (l : List α) (acc : Array β) (G : α → β) :
     (l.foldl (fun acc a => acc.push (G a)) acc).toList = acc.toList ++ l.map G := by
   induction l generalizing acc <;> simp [*]
 
-@[deprecated foldl_toList_eq_map (since := "2024-09-09")]
-abbrev foldl_data_eq_map := @foldl_toList_eq_map
-
-theorem size_uset (a : Array α) (v i h) : (uset a i v h).size = a.size := by simp
-
 theorem anyM_eq_anyM_loop [Monad m] (p : α → m Bool) (as : Array α) (start stop) :
     anyM p as start stop = anyM.loop p as (min stop as.size) (Nat.min_le_right ..) start := by
   simp only [anyM, Nat.min_def]; split <;> rfl
@@ -274,6 +239,12 @@ theorem mem_def {a : α} {as : Array α} : a ∈ as ↔ a ∈ as.toList :=
 @[simp] theorem not_mem_empty (a : α) : ¬(a ∈ #[]) := by
   simp [mem_def]
 
+/-! # uset -/
+
+attribute [simp] uset
+
+theorem size_uset (a : Array α) (v i h) : (uset a i v h).size = a.size := by simp
+
 /-! # get -/
 
 @[simp] theorem get_eq_getElem (a : Array α) (i : Fin _) : a.get i = a[i.1] := rfl
@@ -393,6 +364,10 @@ termination_by n - i
     (ofFn f)[i] = f ⟨i, size_ofFn f ▸ h⟩ :=
   getElem_ofFn_go _ _ _ (by simp) (by simp) nofun
 
+theorem getElem?_ofFn (f : Fin n → α) (i : Nat) :
+    (ofFn f)[i]? = if h : i < n then some (f ⟨i, h⟩) else none := by
+  simp [getElem?_def]
+
 /-- # mkArray -/
 
 @[simp] theorem size_mkArray (n : Nat) (v : α) : (mkArray n v).size = n :=
@@ -400,19 +375,17 @@ termination_by n - i
 
 @[simp] theorem toList_mkArray (n : Nat) (v : α) : (mkArray n v).toList = List.replicate n v := rfl
 
-@[deprecated toList_mkArray (since := "2024-09-09")]
-abbrev mkArray_data := @toList_mkArray
-
 @[simp] theorem getElem_mkArray (n : Nat) (v : α) (h : i < (mkArray n v).size) :
     (mkArray n v)[i] = v := by simp [Array.getElem_eq_getElem_toList]
 
+theorem getElem?_mkArray (n : Nat) (v : α) (i : Nat) :
+    (mkArray n v)[i]? = if i < n then some v else none := by
+  simp [getElem?_def]
+
 /-- # mem -/
 
 theorem mem_toList {a : α} {l : Array α} : a ∈ l.toList ↔ a ∈ l := mem_def.symm
 
-@[deprecated mem_toList (since := "2024-09-09")]
-abbrev mem_data := @mem_toList
-
 theorem not_mem_nil (a : α) : ¬ a ∈ #[] := nofun
 
 theorem getElem_of_mem {a : α} {as : Array α} :
@@ -422,6 +395,12 @@ theorem getElem_of_mem {a : α} {as : Array α} :
   exists i
   exists hbound
 
+theorem getElem?_of_mem {a : α} {as : Array α} :
+    a ∈ as → ∃ (n : Nat), as[n]? = some a := by
+  intro ha
+  rcases List.getElem?_of_mem ha.val with ⟨i, hi⟩
+  exists i
+
 @[simp] theorem mem_dite_empty_left {x : α} [Decidable p] {l : ¬ p → Array α} :
     (x ∈ if h : p then #[] else l h) ↔ ∃ h : ¬ p, x ∈ l h := by
   split <;> simp_all [mem_def]
@@ -444,14 +423,11 @@ theorem lt_of_getElem {x : α} {a : Array α} {idx : Nat} {hidx : idx < a.size}
     idx < a.size :=
   hidx
 
-theorem getElem?_mem {l : Array α} {i : Fin l.size} : l[i] ∈ l := by
+theorem getElem_mem {l : Array α} {i : Nat} (h : i < l.size) : l[i] ∈ l := by
   erw [Array.mem_def, getElem_eq_getElem_toList]
   apply List.get_mem
 
-theorem getElem_fin_eq_toList_get (a : Array α) (i : Fin _) : a[i] = a.toList.get i := rfl
-
-@[deprecated getElem_fin_eq_toList_get (since := "2024-09-09")]
-abbrev getElem_fin_eq_data_get := @getElem_fin_eq_toList_get
+theorem getElem_fin_eq_getElem_toList (a : Array α) (i : Fin a.size) : a[i] = a.toList[i] := rfl
 
 @[simp] theorem ugetElem_eq_getElem (a : Array α) {i : USize} (h : i.toNat < a.size) :
   a[i] = a[i.toNat] := rfl
@@ -462,26 +438,8 @@ theorem get?_len_le (a : Array α) (i : Nat) (h : a.size ≤ i) : a[i]? = none :
 theorem getElem_mem_toList (a : Array α) (h : i < a.size) : a[i] ∈ a.toList := by
   simp only [getElem_eq_getElem_toList, List.getElem_mem]
 
-@[deprecated getElem_mem_toList (since := "2024-09-09")]
-abbrev getElem_mem_data := @getElem_mem_toList
-
-theorem getElem?_eq_toList_getElem? (a : Array α) (i : Nat) : a[i]? = a.toList[i]? := by
-  by_cases i < a.size <;> simp_all [getElem?_pos, getElem?_neg]
-
-@[deprecated getElem?_eq_toList_getElem? (since := "2024-09-30")]
-theorem getElem?_eq_toList_get? (a : Array α) (i : Nat) : a[i]? = a.toList.get? i := by
-  by_cases i < a.size <;> simp_all [getElem?_pos, getElem?_neg, List.get?_eq_get, eq_comm]
-
-set_option linter.deprecated false in
-@[deprecated getElem?_eq_toList_getElem? (since := "2024-09-09")]
-abbrev getElem?_eq_data_get? := @getElem?_eq_toList_get?
-
-set_option linter.deprecated false in
-theorem get?_eq_toList_get? (a : Array α) (i : Nat) : a.get? i = a.toList.get? i :=
-  getElem?_eq_toList_get? ..
-
-@[deprecated get?_eq_toList_get? (since := "2024-09-09")]
-abbrev get?_eq_data_get? := @get?_eq_toList_get?
+theorem get?_eq_get?_toList (a : Array α) (i : Nat) : a.get? i = a.toList.get? i := by
+  simp [getElem?_eq_getElem?_toList]
 
 theorem get!_eq_get? [Inhabited α] (a : Array α) : a.get! n = (a.get? n).getD default := by
   simp [get!_eq_getD]
@@ -494,7 +452,7 @@ theorem getElem?_eq_some_iff {as : Array α} : as[n]? = some a ↔ ∃ h : n < a
   simp [back, back?]
 
 @[simp] theorem back?_push (a : Array α) : (a.push x).back? = some x := by
-  simp [back?, getElem?_eq_toList_getElem?]
+  simp [back?, getElem?_eq_getElem?_toList]
 
 theorem back_push [Inhabited α] (a : Array α) : (a.push x).back = x := by simp
 
@@ -525,9 +483,6 @@ theorem get?_push {a : Array α} : (a.push x)[i]? = if i = a.size then some x el
 
 @[simp] theorem toList_set (a : Array α) (i v) : (a.set i v).toList = a.toList.set i.1 v := rfl
 
-@[deprecated toList_set (since := "2024-09-09")]
-abbrev data_set := @toList_set
-
 theorem get_set_eq (a : Array α) (i : Fin a.size) (v : α) :
     (a.set i v)[i.1] = v := by
   simp only [set, getElem_eq_getElem_toList, List.getElem_set_self]
@@ -568,12 +523,9 @@ theorem swap_def (a : Array α) (i j : Fin a.size) :
 @[simp] theorem toList_swap (a : Array α) (i j : Fin a.size) :
     (a.swap i j).toList = (a.toList.set i (a.get j)).set j (a.get i) := by simp [swap_def]
 
-@[deprecated toList_swap (since := "2024-09-09")]
-abbrev data_swap := @toList_swap
-
-theorem get?_swap (a : Array α) (i j : Fin a.size) (k : Nat) : (a.swap i j)[k]? =
+theorem getElem?_swap (a : Array α) (i j : Fin a.size) (k : Nat) : (a.swap i j)[k]? =
     if j = k then some a[i.1] else if i = k then some a[j.1] else a[k]? := by
-  simp [swap_def, get?_set, ← getElem_fin_eq_toList_get]
+  simp [swap_def, get?_set, ← getElem_fin_eq_getElem_toList]
 
 @[simp] theorem swapAt_def (a : Array α) (i : Fin a.size) (v : α) :
     a.swapAt i v = (a[i.1], a.set i v) := rfl
@@ -591,9 +543,6 @@ theorem swapAt!_def (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
 
 @[simp] theorem toList_pop (a : Array α) : a.pop.toList = a.toList.dropLast := by simp [pop]
 
-@[deprecated toList_pop (since := "2024-09-09")]
-abbrev data_pop := @toList_pop
-
 @[simp] theorem pop_empty : (#[] : Array α).pop = #[] := rfl
 
 @[simp] theorem pop_push (a : Array α) : (a.push x).pop = a := by simp [pop]
@@ -626,9 +575,6 @@ theorem eq_push_of_size_ne_zero {as : Array α} (h : as.size ≠ 0) :
 
 theorem size_eq_length_toList (as : Array α) : as.size = as.toList.length := rfl
 
-@[deprecated size_eq_length_toList (since := "2024-09-09")]
-abbrev size_eq_length_data := @size_eq_length_toList
-
 @[simp] theorem size_swap! (a : Array α) (i j) :
     (a.swap! i j).size = a.size := by unfold swap!; split <;> (try split) <;> simp [size_swap]
 
@@ -653,14 +599,10 @@ abbrev size_eq_length_data := @size_eq_length_toList
 @[simp] theorem toList_range (n : Nat) : (range n).toList = List.range n := by
   induction n <;> simp_all [range, Nat.fold, flip, List.range_succ]
 
-@[deprecated toList_range (since := "2024-09-09")]
-abbrev data_range := @toList_range
-
 @[simp]
 theorem getElem_range {n : Nat} {x : Nat} (h : x < (Array.range n).size) : (Array.range n)[x] = x := by
   simp [getElem_eq_getElem_toList]
 
-set_option linter.deprecated false in
 @[simp] theorem toList_reverse (a : Array α) : a.reverse.toList = a.toList.reverse := by
   let rec go (as : Array α) (i j hj)
       (h : i + j + 1 = a.size) (h₂ : as.size = a.size)
@@ -673,9 +615,9 @@ set_option linter.deprecated false in
       · rwa [Nat.add_right_comm i]
       · simp [size_swap, h₂]
       · intro k
-        rw [← getElem?_eq_toList_getElem?, get?_swap]
+        rw [← getElem?_eq_getElem?_toList, getElem?_swap]
         simp only [H, getElem_eq_getElem_toList, ← List.getElem?_eq_getElem, Nat.le_of_lt h₁,
-          getElem?_eq_toList_getElem?]
+          getElem?_eq_getElem?_toList]
         split <;> rename_i h₂
         · simp only [← h₂, Nat.not_le.2 (Nat.lt_succ_self _), Nat.le_refl, and_false]
           exact (List.getElem?_reverse' (j+1) i (Eq.trans (by simp_arith) h)).symm
@@ -702,9 +644,6 @@ set_option linter.deprecated false in
         true_and, Nat.not_lt] at h
       rw [List.getElem?_eq_none_iff.2 ‹_›, List.getElem?_eq_none_iff.2 (a.toList.length_reverse ▸ ‹_›)]
 
-@[deprecated toList_reverse (since := "2024-09-30")]
-abbrev reverse_toList := @toList_reverse
-
 /-! ### foldl / foldr -/
 
 @[simp] theorem foldlM_loop_empty [Monad m] (f : β → α → m β) (init : β) (i j : Nat) :
@@ -733,7 +672,7 @@ abbrev reverse_toList := @toList_reverse
     foldrM f init #[] start stop = return init := by
   simp [foldrM]
 
--- This proof is the pure version of `Array.SatisfiesM_foldlM`,
+-- This proof is the pure version of `Array.SatisfiesM_foldlM` in Batteries,
 -- reproduced to avoid a dependency on `SatisfiesM`.
 theorem foldl_induction
     {as : Array α} (motive : Nat → β → Prop) {init : β} (h0 : motive 0 init) {f : β → α → β}
@@ -749,7 +688,7 @@ theorem foldl_induction
     · next hj => exact Nat.le_antisymm h₁ (Nat.ge_of_not_lt hj) ▸ H
   simpa [foldl, foldlM] using go (Nat.zero_le _) (Nat.le_refl _) h0
 
--- This proof is the pure version of `Array.SatisfiesM_foldrM`,
+-- This proof is the pure version of `Array.SatisfiesM_foldrM` in Batteries,
 -- reproduced to avoid a dependency on `SatisfiesM`.
 theorem foldr_induction
     {as : Array α} (motive : Nat → β → Prop) {init : β} (h0 : motive as.size init) {f : α → β → β}
@@ -795,9 +734,6 @@ theorem mapM_eq_mapM_toList [Monad m] [LawfulMonad m] (f : α → m β) (arr : A
     toList <$> arr.mapM f = arr.toList.mapM f := by
   simp [mapM_eq_mapM_toList]
 
-@[deprecated mapM_eq_mapM_toList (since := "2024-09-09")]
-abbrev mapM_eq_mapM_data := @mapM_eq_mapM_toList
-
 theorem mapM_map_eq_foldl (as : Array α) (f : α → β) (i) :
     mapM.map (m := Id) f as i b = as.foldl (start := i) (fun r a => r.push (f a)) b := by
   unfold mapM.map
@@ -869,6 +805,12 @@ theorem map_spec (as : Array α) (f : α → β) (p : Fin as.size → β → Pro
   · simp only [getElem_map, get_push, size_map]
     split <;> rfl
 
+@[simp] theorem map_pop {f : α → β} {as : Array α} :
+    as.pop.map f = (as.map f).pop := by
+  ext
+  · simp
+  · simp only [getElem_map, getElem_pop, size_map]
+
 /-! ### mapIdx -/
 
 -- This could also be proved from `SatisfiesM_mapIdxM` in Batteries.
@@ -942,12 +884,6 @@ theorem getElem_modify_of_ne {as : Array α} {i : Nat} (h : i ≠ j)
     (as.modify i f)[j] = as[j]'(by simpa using hj) := by
   simp [getElem_modify hj, h]
 
-@[deprecated getElem_modify (since := "2024-08-08")]
-theorem get_modify {arr : Array α} {x i} (h : i < (arr.modify x f).size) :
-    (arr.modify x f).get ⟨i, h⟩ =
-    if x = i then f (arr.get ⟨i, by simpa using h⟩) else arr.get ⟨i, by simpa using h⟩ := by
-  simp [getElem_modify h]
-
 /-! ### filter -/
 
 @[simp] theorem toList_filter (p : α → Bool) (l : Array α) :
@@ -961,9 +897,6 @@ theorem get_modify {arr : Array α} {x i} (h : i < (arr.modify x f).size) :
   induction l with simp
   | cons => split <;> simp [*]
 
-@[deprecated toList_filter (since := "2024-09-09")]
-abbrev filter_data := @toList_filter
-
 @[simp] theorem filter_filter (q) (l : Array α) :
     filter p (filter q l) = filter (fun a => p a && q a) l := by
   apply ext'
@@ -997,9 +930,6 @@ theorem filter_congr {as bs : Array α} (h : as = bs)
   · simp_all [Id.run, List.filterMap_cons]
     split <;> simp_all
 
-@[deprecated toList_filterMap (since := "2024-09-09")]
-abbrev filterMap_data := @toList_filterMap
-
 @[simp] theorem mem_filterMap {f : α → Option β} {l : Array α} {b : β} :
     b ∈ filterMap f l ↔ ∃ a, a ∈ l ∧ f a = some b := by
   simp only [mem_def, toList_filterMap, List.mem_filterMap]
@@ -1017,9 +947,6 @@ theorem size_empty : (#[] : Array α).size = 0 := rfl
 
 theorem toList_empty : (#[] : Array α).toList = [] := rfl
 
-@[deprecated toList_empty (since := "2024-09-09")]
-abbrev empty_data := @toList_empty
-
 /-! ### append -/
 
 theorem push_eq_append_singleton (as : Array α) (x) : as.push x = as ++ #[x] := rfl
@@ -1042,9 +969,6 @@ theorem getElem_append_left {as bs : Array α} {h : i < (as ++ bs).size} (hlt :
   conv => rhs; rw [← List.getElem_append_left (bs := bs.toList) (h' := h')]
   apply List.get_of_eq; rw [toList_append]
 
-@[deprecated getElem_append_left (since := "2024-09-30")]
-abbrev get_append_left := @getElem_append_left
-
 theorem getElem_append_right {as bs : Array α} {h : i < (as ++ bs).size} (hle : as.size ≤ i)
     (hlt : i - as.size < bs.size := Nat.sub_lt_left_of_lt_add hle (size_append .. ▸ h)) :
     (as ++ bs)[i] = bs[i - as.size] := by
@@ -1053,9 +977,6 @@ theorem getElem_append_right {as bs : Array α} {h : i < (as ++ bs).size} (hle :
   conv => rhs; rw [← List.getElem_append_right (h₁ := hle) (h₂ := h')]
   apply List.get_of_eq; rw [toList_append]
 
-@[deprecated getElem_append_right (since := "2024-09-30")]
-abbrev get_append_right := @getElem_append_right
-
 @[simp] theorem append_nil (as : Array α) : as ++ #[] = as := by
   apply ext'; simp only [toList_append, toList_empty, List.append_nil]
 
@@ -1298,9 +1219,6 @@ theorem any_toList {p : α → Bool} (as : Array α) : as.toList.any p = as.any
   rw [Bool.eq_iff_iff, any_eq_true, List.any_eq_true]; simp only [List.mem_iff_get]
   exact ⟨fun ⟨_, ⟨i, rfl⟩, h⟩ => ⟨i, h⟩, fun ⟨i, h⟩ => ⟨_, ⟨i, rfl⟩, h⟩⟩
 
-@[deprecated "Use the reverse direction of `Array.any_toList`" (since := "2024-09-30")]
-abbrev any_def := @any_toList
-
 /-! ### all -/
 
 theorem allM_eq_not_anyM_not [Monad m] [LawfulMonad m] (p : α → m Bool) (as : Array α) :
@@ -1340,9 +1258,6 @@ theorem all_toList {p : α → Bool} (as : Array α) : as.toList.all p = as.all
     rw [← getElem_eq_getElem_toList]
     exact w ⟨r, h⟩
 
-@[deprecated "Use the reverse direction of `Array.all_toList`" (since := "2024-09-30")]
-abbrev all_def := @all_toList
-
 theorem all_eq_true_iff_forall_mem {l : Array α} : l.all p ↔ ∀ x, x ∈ l → p x := by
   simp only [← all_toList, List.all_eq_true, mem_def]
 
@@ -1412,33 +1327,8 @@ theorem swap_comm (a : Array α) {i j : Fin a.size} : a.swap i j = a.swap j i :=
     · split <;> simp_all
     · split <;> simp_all
 
-@[deprecated getElem_extract_loop_lt_aux (since := "2024-09-30")]
-abbrev get_extract_loop_lt_aux := @getElem_extract_loop_lt_aux
-@[deprecated getElem_extract_loop_lt (since := "2024-09-30")]
-abbrev get_extract_loop_lt := @getElem_extract_loop_lt
-@[deprecated getElem_extract_loop_ge_aux (since := "2024-09-30")]
-abbrev get_extract_loop_ge_aux := @getElem_extract_loop_ge_aux
-@[deprecated getElem_extract_loop_ge (since := "2024-09-30")]
-abbrev get_extract_loop_ge := @getElem_extract_loop_ge
-@[deprecated getElem_extract_aux (since := "2024-09-30")]
-abbrev get_extract_aux := @getElem_extract_aux
-@[deprecated getElem_extract (since := "2024-09-30")]
-abbrev get_extract := @getElem_extract
-
-@[deprecated getElem_swap_right (since := "2024-09-30")]
-abbrev get_swap_right := @getElem_swap_right
-@[deprecated getElem_swap_left (since := "2024-09-30")]
-abbrev get_swap_left := @getElem_swap_left
-@[deprecated getElem_swap_of_ne (since := "2024-09-30")]
-abbrev get_swap_of_ne := @getElem_swap_of_ne
-@[deprecated getElem_swap (since := "2024-09-30")]
-abbrev get_swap := @getElem_swap
-@[deprecated getElem_swap' (since := "2024-09-30")]
-abbrev get_swap' := @getElem_swap'
-
 end Array
 
-
 open Array
 
 namespace List
@@ -1583,3 +1473,158 @@ theorem filterMap_toArray (f : α → Option β) (l : List α) :
   simp
 
 end List
+
+/-! ### Deprecations -/
+
+namespace List
+
+@[deprecated toArray_toList (since := "2024-09-09")]
+abbrev toArray_data := @toArray_toList
+
+@[deprecated "Use the reverse direction of `List.push_toArray`." (since := "2024-09-27")]
+theorem toArray_concat {as : List α} {x : α} :
+    (as ++ [x]).toArray = as.toArray.push x := by
+  apply ext'
+  simp
+
+end List
+
+namespace Array
+
+@[deprecated getElem_eq_getElem_toList (since := "2024-09-25")]
+abbrev getElem_eq_toList_getElem := @getElem_eq_getElem_toList
+
+@[deprecated getElem_eq_toList_getElem (since := "2024-09-09")]
+abbrev getElem_eq_data_getElem := @getElem_eq_getElem_toList
+
+@[deprecated getElem_eq_toList_getElem (since := "2024-06-12")]
+theorem getElem_eq_toList_get (a : Array α) (h : i < a.size) : a[i] = a.toList.get ⟨i, h⟩ := by
+  simp
+
+@[deprecated toArray_toList (since := "2024-09-09")]
+abbrev toArray_data := @toArray_toList
+
+@[deprecated length_toList (since := "2024-09-09")]
+abbrev data_length := @length_toList
+
+@[deprecated toList_map (since := "2024-09-09")]
+abbrev map_data := @toList_map
+
+@[deprecated foldl_toList_eq_flatMap (since := "2024-10-16")]
+abbrev foldl_toList_eq_bind := @foldl_toList_eq_flatMap
+
+@[deprecated foldl_toList_eq_flatMap (since := "2024-10-16")]
+abbrev foldl_data_eq_bind := @foldl_toList_eq_flatMap
+
+@[deprecated foldl_toList_eq_map (since := "2024-09-09")]
+abbrev foldl_data_eq_map := @foldl_toList_eq_map
+
+@[deprecated toList_mkArray (since := "2024-09-09")]
+abbrev mkArray_data := @toList_mkArray
+
+@[deprecated mem_toList (since := "2024-09-09")]
+abbrev mem_data := @mem_toList
+
+@[deprecated getElem_mem (since := "2024-10-17")]
+abbrev getElem?_mem := @getElem_mem
+
+@[deprecated getElem_fin_eq_getElem_toList (since := "2024-10-17")]
+abbrev getElem_fin_eq_toList_get := @getElem_fin_eq_getElem_toList
+
+@[deprecated getElem_fin_eq_getElem_toList (since := "2024-09-09")]
+abbrev getElem_fin_eq_data_get := @getElem_fin_eq_getElem_toList
+
+@[deprecated getElem_mem_toList (since := "2024-09-09")]
+abbrev getElem_mem_data := @getElem_mem_toList
+
+@[deprecated getElem?_eq_getElem?_toList (since := "2024-10-17")]
+abbrev getElem?_eq_toList_getElem? := @getElem?_eq_getElem?_toList
+
+@[deprecated getElem?_eq_toList_getElem? (since := "2024-09-30")]
+theorem getElem?_eq_toList_get? (a : Array α) (i : Nat) : a[i]? = a.toList.get? i := by
+  by_cases i < a.size <;> simp_all [getElem?_pos, getElem?_neg, List.get?_eq_get, eq_comm]
+
+set_option linter.deprecated false in
+@[deprecated getElem?_eq_toList_getElem? (since := "2024-09-09")]
+abbrev getElem?_eq_data_get? := @getElem?_eq_toList_get?
+
+@[deprecated get?_eq_get?_toList (since := "2024-10-17")]
+abbrev get?_eq_toList_get? := @get?_eq_get?_toList
+
+@[deprecated get?_eq_toList_get? (since := "2024-09-09")]
+abbrev get?_eq_data_get? := @get?_eq_get?_toList
+
+@[deprecated toList_set (since := "2024-09-09")]
+abbrev data_set := @toList_set
+
+@[deprecated toList_swap (since := "2024-09-09")]
+abbrev data_swap := @toList_swap
+
+@[deprecated getElem?_swap (since := "2024-10-17")] abbrev get?_swap := @getElem?_swap
+
+@[deprecated toList_pop (since := "2024-09-09")] abbrev data_pop := @toList_pop
+
+@[deprecated size_eq_length_toList (since := "2024-09-09")]
+abbrev size_eq_length_data := @size_eq_length_toList
+
+@[deprecated toList_range (since := "2024-09-09")]
+abbrev data_range := @toList_range
+
+@[deprecated toList_reverse (since := "2024-09-30")]
+abbrev reverse_toList := @toList_reverse
+
+@[deprecated mapM_eq_mapM_toList (since := "2024-09-09")]
+abbrev mapM_eq_mapM_data := @mapM_eq_mapM_toList
+
+@[deprecated getElem_modify (since := "2024-08-08")]
+theorem get_modify {arr : Array α} {x i} (h : i < (arr.modify x f).size) :
+    (arr.modify x f).get ⟨i, h⟩ =
+    if x = i then f (arr.get ⟨i, by simpa using h⟩) else arr.get ⟨i, by simpa using h⟩ := by
+  simp [getElem_modify h]
+
+@[deprecated toList_filter (since := "2024-09-09")]
+abbrev filter_data := @toList_filter
+
+@[deprecated toList_filterMap (since := "2024-09-09")]
+abbrev filterMap_data := @toList_filterMap
+
+@[deprecated toList_empty (since := "2024-09-09")]
+abbrev empty_data := @toList_empty
+
+@[deprecated getElem_append_left (since := "2024-09-30")]
+abbrev get_append_left := @getElem_append_left
+
+@[deprecated getElem_append_right (since := "2024-09-30")]
+abbrev get_append_right := @getElem_append_right
+
+@[deprecated "Use the reverse direction of `Array.any_toList`" (since := "2024-09-30")]
+abbrev any_def := @any_toList
+
+@[deprecated "Use the reverse direction of `Array.all_toList`" (since := "2024-09-30")]
+abbrev all_def := @all_toList
+
+@[deprecated getElem_extract_loop_lt_aux (since := "2024-09-30")]
+abbrev get_extract_loop_lt_aux := @getElem_extract_loop_lt_aux
+@[deprecated getElem_extract_loop_lt (since := "2024-09-30")]
+abbrev get_extract_loop_lt := @getElem_extract_loop_lt
+@[deprecated getElem_extract_loop_ge_aux (since := "2024-09-30")]
+abbrev get_extract_loop_ge_aux := @getElem_extract_loop_ge_aux
+@[deprecated getElem_extract_loop_ge (since := "2024-09-30")]
+abbrev get_extract_loop_ge := @getElem_extract_loop_ge
+@[deprecated getElem_extract_aux (since := "2024-09-30")]
+abbrev get_extract_aux := @getElem_extract_aux
+@[deprecated getElem_extract (since := "2024-09-30")]
+abbrev get_extract := @getElem_extract
+
+@[deprecated getElem_swap_right (since := "2024-09-30")]
+abbrev get_swap_right := @getElem_swap_right
+@[deprecated getElem_swap_left (since := "2024-09-30")]
+abbrev get_swap_left := @getElem_swap_left
+@[deprecated getElem_swap_of_ne (since := "2024-09-30")]
+abbrev get_swap_of_ne := @getElem_swap_of_ne
+@[deprecated getElem_swap (since := "2024-09-30")]
+abbrev get_swap := @getElem_swap
+@[deprecated getElem_swap' (since := "2024-09-30")]
+abbrev get_swap' := @getElem_swap'
+
+end Array

src/Init/Data/BitVec/Basic.lean

@@ -8,12 +8,13 @@ import Init.Data.Fin.Basic
 import Init.Data.Nat.Bitwise.Lemmas
 import Init.Data.Nat.Power2
 import Init.Data.Int.Bitwise
+import Init.Data.BitVec.BasicAux
 
 /-!
-We define bitvectors. We choose the `Fin` representation over others for its relative efficiency
-(Lean has special support for `Nat`), alignment with `UIntXY` types which are also represented
-with `Fin`, and the fact that bitwise operations on `Fin` are already defined. Some other possible
-representations are `List Bool`, `{ l : List Bool // l.length = w }`, `Fin w → Bool`.
+We define the basic algebraic structure of bitvectors. We choose the `Fin` representation over
+others for its relative efficiency (Lean has special support for `Nat`),  and the fact that bitwise
+operations on `Fin` are already defined. Some other possible representations are `List Bool`,
+`{ l : List Bool // l.length = w }`, `Fin w → Bool`.
 
 We define many of the bitvector operations from the
 [`QF_BV` logic](https://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV).
@@ -22,60 +23,12 @@ of SMT-LIBv2.
 
 set_option linter.missingDocs true
 
-/--
-A bitvector of the specified width.
-
-This is represented as the underlying `Nat` number in both the runtime
-and the kernel, inheriting all the special support for `Nat`.
--/
-structure BitVec (w : Nat) where
-  /-- Construct a `BitVec w` from a number less than `2^w`.
-  O(1), because we use `Fin` as the internal representation of a bitvector. -/
-  ofFin ::
-  /-- Interpret a bitvector as a number less than `2^w`.
-  O(1), because we use `Fin` as the internal representation of a bitvector. -/
-  toFin : Fin (2^w)
-
-/--
-Bitvectors have decidable equality. This should be used via the instance `DecidableEq (BitVec n)`.
--/
--- We manually derive the `DecidableEq` instances for `BitVec` because
--- we want to have builtin support for bit-vector literals, and we
--- need a name for this function to implement `canUnfoldAtMatcher` at `WHNF.lean`.
-def BitVec.decEq (x y : BitVec n) : Decidable (x = y) :=
-  match x, y with
-  | ⟨n⟩, ⟨m⟩ =>
-    if h : n = m then
-      isTrue (h ▸ rfl)
-    else
-      isFalse (fun h' => BitVec.noConfusion h' (fun h' => absurd h' h))
-
-instance : DecidableEq (BitVec n) := BitVec.decEq
-
 namespace BitVec
 
 section Nat
 
-/-- The `BitVec` with value `i`, given a proof that `i < 2^n`. -/
-@[match_pattern]
-protected def ofNatLt {n : Nat} (i : Nat) (p : i < 2^n) : BitVec n where
-  toFin := ⟨i, p⟩
-
-/-- The `BitVec` with value `i mod 2^n`. -/
-@[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
 instance natCastInst : NatCast (BitVec w) := ⟨BitVec.ofNat w⟩
 
-/-- Given a bitvector `x`, return the underlying `Nat`. This is O(1) because `BitVec` is a
-(zero-cost) wrapper around a `Nat`. -/
-protected def toNat (x : BitVec n) : Nat := x.toFin.val
-
-/-- Return the bound in terms of toNat. -/
-theorem isLt (x : BitVec w) : x.toNat < 2^w := x.toFin.isLt
-
 @[deprecated isLt (since := "2024-03-12")]
 theorem toNat_lt (x : BitVec n) : x.toNat < 2^n := x.isLt
 
@@ -238,22 +191,6 @@ end repr_toString
 
 section arithmetic
 
-/--
-Addition for bit vectors. This can be interpreted as either signed or unsigned addition
-modulo `2^n`.
-
-SMT-Lib name: `bvadd`.
--/
-protected def add (x y : BitVec n) : BitVec n := .ofNat n (x.toNat + y.toNat)
-instance : Add (BitVec n) := ⟨BitVec.add⟩
-
-/--
-Subtraction for bit vectors. This can be interpreted as either signed or unsigned subtraction
-modulo `2^n`.
--/
-protected def sub (x y : BitVec n) : BitVec n := .ofNat n ((2^n - y.toNat) + x.toNat)
-instance : Sub (BitVec n) := ⟨BitVec.sub⟩
-
 /--
 Negation for bit vectors. This can be interpreted as either signed or unsigned negation
 modulo `2^n`.
@@ -387,10 +324,6 @@ SMT-Lib name: `bvult`.
 -/
 protected def ult (x y : BitVec n) : Bool := x.toNat < y.toNat
 
-instance : LT (BitVec n) where lt := (·.toNat < ·.toNat)
-instance (x y : BitVec n) : Decidable (x < y) :=
-  inferInstanceAs (Decidable (x.toNat < y.toNat))
-
 /--
 Unsigned less-than-or-equal-to for bit vectors.
 
@@ -398,10 +331,6 @@ SMT-Lib name: `bvule`.
 -/
 protected def ule (x y : BitVec n) : Bool := x.toNat ≤ y.toNat
 
-instance : LE (BitVec n) where le := (·.toNat ≤ ·.toNat)
-instance (x y : BitVec n) : Decidable (x ≤ y) :=
-  inferInstanceAs (Decidable (x.toNat ≤ y.toNat))
-
 /--
 Signed less-than for bit vectors.
 

src/Init/Data/BitVec/BasicAux.lean

@@ -0,0 +1,52 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joe Hendrix, Wojciech Nawrocki, Leonardo de Moura, Mario Carneiro, Alex Keizer, Harun Khan, Abdalrhman M Mohamed
+-/
+prelude
+import Init.Data.Fin.Basic
+
+set_option linter.missingDocs true
+
+/-!
+This module exists to provide the very basic `BitVec` definitions required for
+`Init.Data.UInt.BasicAux`.
+-/
+
+namespace BitVec
+
+section Nat
+
+/-- The `BitVec` with value `i mod 2^n`. -/
+@[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. -/
+theorem isLt (x : BitVec w) : x.toNat < 2^w := x.toFin.isLt
+
+end Nat
+
+section arithmetic
+
+/--
+Addition for bit vectors. This can be interpreted as either signed or unsigned addition
+modulo `2^n`.
+
+SMT-Lib name: `bvadd`.
+-/
+protected def add (x y : BitVec n) : BitVec n := .ofNat n (x.toNat + y.toNat)
+instance : Add (BitVec n) := ⟨BitVec.add⟩
+
+/--
+Subtraction for bit vectors. This can be interpreted as either signed or unsigned subtraction
+modulo `2^n`.
+-/
+protected def sub (x y : BitVec n) : BitVec n := .ofNat n ((2^n - y.toNat) + x.toNat)
+instance : Sub (BitVec n) := ⟨BitVec.sub⟩
+
+end arithmetic
+
+end BitVec

src/Init/Data/BitVec/Bitblast.lean

@@ -267,6 +267,21 @@ theorem add_eq_adc (w : Nat) (x y : BitVec w) : x + y = (adc x y false).snd := b
 
 /-! ### add -/
 
+theorem getMsbD_add {i : Nat} {i_lt : i < w} {x y : BitVec w} :
+    getMsbD (x + y) i =
+      Bool.xor (getMsbD x i) (Bool.xor (getMsbD y i) (carry (w - 1 - i) x y false)) := by
+  simp [getMsbD, getLsbD_add, i_lt, show w - 1 - i < w by omega]
+
+theorem msb_add {w : Nat} {x y: BitVec w} :
+    (x + y).msb =
+      Bool.xor x.msb (Bool.xor y.msb (carry (w - 1) x y false)) := by
+  simp only [BitVec.msb, BitVec.getMsbD]
+  by_cases h : w ≤ 0
+  · simp [h, show w = 0 by omega]
+  · rw [getLsbD_add (x := x)]
+    simp [show w > 0 by omega]
+    omega
+
 /-- Adding a bitvector to its own complement yields the all ones bitpattern -/
 @[simp] theorem add_not_self (x : BitVec w) : x + ~~~x = allOnes w := by
   rw [add_eq_adc, adc, iunfoldr_replace (fun _ => false) (allOnes w)]
@@ -292,6 +307,26 @@ theorem add_eq_or_of_and_eq_zero {w : Nat} (x y : BitVec w)
       simp_all [hx]
     · by_cases hx : x.getLsbD i <;> simp_all [hx]
 
+/-! ### Sub-/
+
+theorem getLsbD_sub {i : Nat} {i_lt : i < w} {x y : BitVec w} :
+    (x - y).getLsbD i
+      = (x.getLsbD i ^^ ((~~~y + 1#w).getLsbD i ^^ carry i x (~~~y + 1#w) false)) := by
+  rw [sub_toAdd, BitVec.neg_eq_not_add, getLsbD_add]
+  omega
+
+theorem getMsbD_sub {i : Nat} {i_lt : i < w} {x y : BitVec w} :
+    (x - y).getMsbD i =
+      (x.getMsbD i ^^ ((~~~y + 1).getMsbD i ^^ carry (w - 1 - i) x (~~~y + 1) false)) := by
+  rw [sub_toAdd, neg_eq_not_add, getMsbD_add]
+  · rfl
+  · omega
+
+theorem msb_sub {x y: BitVec w} :
+    (x - y).msb
+      = (x.msb ^^ ((~~~y + 1#w).msb ^^ carry (w - 1 - 0) x (~~~y + 1#w) false)) := by
+  simp [sub_toAdd, BitVec.neg_eq_not_add, msb_add]
+
 /-! ### Negation -/
 
 theorem bit_not_testBit (x : BitVec w) (i : Fin w) :

src/Init/Data/BitVec/Lemmas.lean

@@ -286,6 +286,19 @@ theorem getLsbD_ofNat (n : Nat) (x : Nat) (i : Nat) :
 
 @[simp] theorem getMsbD_zero : (0#w).getMsbD i = false := by simp [getMsbD]
 
+@[simp] theorem getLsbD_one : (1#w).getLsbD i = (decide (0 < w) && decide (i = 0)) := by
+  simp only [getLsbD, toNat_ofNat, Nat.testBit_mod_two_pow]
+  by_cases h : i = 0
+    <;> simp [h, Nat.testBit_to_div_mod, Nat.div_eq_of_lt]
+
+@[simp] theorem getElem_one (h : i < w) : (1#w)[i] = decide (i = 0) := by
+  simp [← getLsbD_eq_getElem, getLsbD_one, h, show 0 < w by omega]
+
+/-- The msb at index `w-1` is the least significant bit, and is true when the width is nonzero. -/
+@[simp] theorem getMsbD_one : (1#w).getMsbD i = (decide (i = w - 1) && decide (0 < w)) := by
+  simp only [getMsbD]
+  by_cases h : 0 < w <;> by_cases h' : i = w - 1 <;> simp [h, h'] <;> omega
+
 @[simp] theorem toNat_mod_cancel (x : BitVec n) : x.toNat % (2^n) = x.toNat :=
   Nat.mod_eq_of_lt x.isLt
 
@@ -347,6 +360,10 @@ theorem getElem_ofBool {b : Bool} {i : Nat} : (ofBool b)[0] = b := by
 
 @[simp] theorem msb_zero : (0#w).msb = false := by simp [BitVec.msb, getMsbD]
 
+@[simp] theorem msb_one : (1#w).msb = decide (w = 1) := by
+  simp [BitVec.msb, getMsbD_one, ← Bool.decide_and]
+  omega
+
 theorem msb_eq_getLsbD_last (x : BitVec w) :
     x.msb = x.getLsbD (w - 1) := by
   simp only [BitVec.msb, getMsbD]
@@ -2073,6 +2090,11 @@ theorem sub_eq_xor {a b : BitVec 1} : a - b = a ^^^ b := by
   have hb : b = 0 ∨ b = 1 := eq_zero_or_eq_one _
   rcases ha with h | h <;> (rcases hb with h' | h' <;> (simp [h, h']))
 
+@[simp]
+theorem sub_eq_self {x : BitVec 1} : -x = x := by
+  have ha : x = 0 ∨ x = 1 := eq_zero_or_eq_one _
+  rcases ha with h | h <;> simp [h]
+
 theorem not_neg (x : BitVec w) : ~~~(-x) = x + -1#w := by
   rcases w with _ | w
   · apply Subsingleton.elim
@@ -2341,6 +2363,24 @@ theorem toNat_sdiv {x y : BitVec w} : (x.sdiv y).toNat =
   simp only [sdiv_eq, toNat_udiv]
   by_cases h : x.msb <;> by_cases h' : y.msb <;> simp [h, h']
 
+@[simp]
+theorem zero_sdiv {x : BitVec w} : (0#w).sdiv x = 0#w := by
+  simp only [sdiv_eq]
+  rcases x.msb with msb | msb <;> simp
+
+@[simp]
+theorem sdiv_zero {x : BitVec n} : x.sdiv 0#n = 0#n := by
+  simp only [sdiv_eq, msb_zero]
+  rcases x.msb with msb | msb <;> apply eq_of_toNat_eq <;> simp
+
+@[simp]
+theorem sdiv_one {x : BitVec w} : x.sdiv 1#w = x := by
+  simp only [sdiv_eq]
+  · by_cases h : w = 1
+    · subst h
+      rcases x.msb with msb | msb <;> simp
+    · rcases x.msb with msb | msb <;> simp [h]
+
 theorem sdiv_eq_and (x y : BitVec 1) : x.sdiv y = x &&& y := by
   have hx : x = 0#1 ∨ x = 1#1 := by bv_omega
   have hy : y = 0#1 ∨ y = 1#1 := by bv_omega
@@ -2349,9 +2389,13 @@ theorem sdiv_eq_and (x y : BitVec 1) : x.sdiv y = x &&& y := by
       rfl
 
 @[simp]
-theorem sdiv_zero {x : BitVec n} : x.sdiv 0#n = 0#n := by
-  simp only [sdiv_eq, msb_zero]
-  rcases x.msb with msb | msb <;> apply eq_of_toNat_eq <;> simp
+theorem sdiv_self {x : BitVec w} :
+    x.sdiv x = if x == 0#w then 0#w else 1#w := by
+  simp [sdiv_eq]
+  · by_cases h : w = 1
+    · subst h
+      rcases x.msb with msb | msb <;> simp
+    · rcases x.msb with msb | msb <;> simp [h]
 
 /-! ### smod -/
 
@@ -2653,14 +2697,6 @@ theorem twoPow_zero {w : Nat} : twoPow w 0 = 1#w := by
   apply eq_of_toNat_eq
   simp
 
-@[simp]
-theorem getLsbD_one {w i : Nat} : (1#w).getLsbD i = (decide (0 < w) && decide (0 = i)) := by
-  rw [← twoPow_zero, getLsbD_twoPow]
-
-@[simp]
-theorem getElem_one {w i : Nat} (h : i < w) : (1#w)[i] = decide (i = 0) := by
-  rw [← twoPow_zero, getElem_twoPow]
-
 theorem shiftLeft_eq_mul_twoPow (x : BitVec w) (n : Nat) :
     x <<< n = x * (BitVec.twoPow w n) := by
   ext i
@@ -2680,7 +2716,6 @@ theorem shiftLeft_eq_mul_twoPow (x : BitVec w) (n : Nat) :
 @[simp] theorem zero_concat_true : concat 0#w true = 1#(w + 1) := by
   ext
   simp [getLsbD_concat]
-  omega
 
 /- ### setWidth, setWidth, and bitwise operations -/
 
@@ -2721,7 +2756,7 @@ theorem and_one_eq_setWidth_ofBool_getLsbD {x : BitVec w} :
   ext i
   simp only [getLsbD_and, getLsbD_one, getLsbD_setWidth, Fin.is_lt, decide_True, getLsbD_ofBool,
     Bool.true_and]
-  by_cases h : (0 = (i : Nat)) <;> simp [h] <;> omega
+  by_cases h : ((i : Nat) = 0) <;> simp [h] <;> omega
 
 @[simp]
 theorem replicate_zero_eq {x : BitVec w} : x.replicate 0 = 0#0 := by

src/Init/Data/Char/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 prelude
-import Init.Data.UInt.Basic
+import Init.Data.UInt.BasicAux
 
 /-- Determines if the given integer is a valid [Unicode scalar value](https://www.unicode.org/glossary/#unicode_scalar_value).
 
@@ -42,8 +42,10 @@ theorem isValidUInt32 (n : Nat) (h : isValidCharNat n) : n < UInt32.size := by
 
 theorem isValidChar_of_isValidCharNat (n : Nat) (h : isValidCharNat n) : isValidChar (UInt32.ofNat' n (isValidUInt32 n h)) :=
   match h with
-  | Or.inl h        => Or.inl h
-  | Or.inr ⟨h₁, h₂⟩ => Or.inr ⟨h₁, h₂⟩
+  | Or.inl h =>
+    Or.inl (UInt32.ofNat'_lt_of_lt _ (by decide) h)
+  | Or.inr ⟨h₁, h₂⟩ =>
+    Or.inr ⟨UInt32.lt_ofNat'_of_lt _ (by decide) h₁, UInt32.ofNat'_lt_of_lt _ (by decide) h₂⟩
 
 theorem isValidChar_zero : isValidChar 0 :=
   Or.inl (by decide)
@@ -57,7 +59,7 @@ theorem isValidChar_zero : isValidChar 0 :=
   c.val.toUInt8
 
 /-- The numbers from 0 to 256 are all valid UTF-8 characters, so we can embed one in the other. -/
-def ofUInt8 (n : UInt8) : Char := ⟨n.toUInt32, .inl (Nat.lt_trans n.1.2 (by decide))⟩
+def ofUInt8 (n : UInt8) : Char := ⟨n.toUInt32, .inl (Nat.lt_trans n.toBitVec.isLt (by decide))⟩
 
 instance : Inhabited Char where
   default := 'A'

src/Init/Data/List/Attach.lean

@@ -639,14 +639,16 @@ and simplifies these to the function directly taking the value.
   | nil => simp
   | cons a l ih => simp [ih, hf, filterMap_cons]
 
-@[simp] theorem bind_subtype {p : α → Prop} {l : List { x // p x }}
+@[simp] theorem flatMap_subtype {p : α → Prop} {l : List { x // p x }}
     {f : { x // p x } → List β} {g : α → List β} {hf : ∀ x h, f ⟨x, h⟩ = g x} :
-    (l.bind f) = l.unattach.bind g := by
+    (l.flatMap f) = l.unattach.flatMap g := by
   unfold unattach
   induction l with
   | nil => simp
   | cons a l ih => simp [ih, hf]
 
+@[deprecated flatMap_subtype (since := "2024-10-16")] abbrev bind_subtype := @flatMap_subtype
+
 @[simp] theorem unattach_filter {p : α → Prop} {l : List { x // p x }}
     {f : { x // p x } → Bool} {g : α → Bool} {hf : ∀ x h, f ⟨x, h⟩ = g x} :
     (l.filter f).unattach = l.unattach.filter g := by

src/Init/Data/List/Basic.lean

@@ -558,28 +558,38 @@ def flatten : List (List α) → List α
 
 @[deprecated flatten (since := "2024-10-14"), inherit_doc flatten] abbrev join := @flatten
 
-/-! ### pure -/
+/-! ### singleton -/
 
-/-- `pure x = [x]` is the `pure` operation of the list monad. -/
-@[inline] protected def pure {α : Type u} (a : α) : List α := [a]
+/-- `singleton x = [x]`. -/
+@[inline] protected def singleton {α : Type u} (a : α) : List α := [a]
 
-/-! ### bind -/
+set_option linter.missingDocs false in
+@[deprecated singleton (since := "2024-10-16")] protected abbrev pure := @singleton
+
+/-! ### flatMap -/
 
 /--
-`bind xs f` is the bind operation of the list monad. It applies `f` to each element of `xs`
+`flatMap xs f` applies `f` to each element of `xs`
 to get a list of lists, and then concatenates them all together.
 * `[2, 3, 2].bind range = [0, 1, 0, 1, 2, 0, 1]`
 -/
-@[inline] protected def bind {α : Type u} {β : Type v} (a : List α) (b : α → List β) : List β := flatten (map b a)
+@[inline] def flatMap {α : Type u} {β : Type v} (a : List α) (b : α → List β) : List β := flatten (map b a)
 
-@[simp] theorem bind_nil (f : α → List β) : List.bind [] f = [] := by simp [flatten, List.bind]
-@[simp] theorem bind_cons x xs (f : α → List β) :
-  List.bind (x :: xs) f = f x ++ List.bind xs f := by simp [flatten, List.bind]
+@[simp] theorem flatMap_nil (f : α → List β) : List.flatMap [] f = [] := by simp [flatten, List.flatMap]
+@[simp] theorem flatMap_cons x xs (f : α → List β) :
+  List.flatMap (x :: xs) f = f x ++ List.flatMap xs f := by simp [flatten, List.flatMap]
 
 set_option linter.missingDocs false in
-@[deprecated bind_nil (since := "2024-06-15")] abbrev nil_bind := @bind_nil
+@[deprecated flatMap (since := "2024-10-16")] abbrev bind := @flatMap
 set_option linter.missingDocs false in
-@[deprecated bind_cons (since := "2024-06-15")] abbrev cons_bind := @bind_cons
+@[deprecated flatMap_nil (since := "2024-10-16")] abbrev nil_flatMap := @flatMap_nil
+set_option linter.missingDocs false in
+@[deprecated flatMap_cons (since := "2024-10-16")] abbrev cons_flatMap := @flatMap_cons
+
+set_option linter.missingDocs false in
+@[deprecated flatMap_nil (since := "2024-06-15")] abbrev nil_bind := @flatMap_nil
+set_option linter.missingDocs false in
+@[deprecated flatMap_cons (since := "2024-06-15")] abbrev cons_bind := @flatMap_cons
 
 /-! ### replicate -/
 
@@ -1398,8 +1408,17 @@ def unzip : List (α × β) → List α × List β
 
 /-! ## Ranges and enumeration -/
 
+/-- Sum of a list.
+
+`List.sum [a, b, c] = a + (b + (c + 0))` -/
+def sum {α} [Add α] [Zero α] : List α → α :=
+  foldr (· + ·) 0
+
+@[simp] theorem sum_nil [Add α] [Zero α] : ([] : List α).sum = 0 := rfl
+@[simp] theorem sum_cons [Add α] [Zero α] {a : α} {l : List α} : (a::l).sum = a + l.sum := rfl
+
 /-- Sum of a list of natural numbers. -/
--- This is not in the `List` namespace as later `List.sum` will be defined polymorphically.
+-- We intend to subsequently deprecate this in favor of `List.sum`.
 protected def _root_.Nat.sum (l : List Nat) : Nat := l.foldr (·+·) 0
 
 @[simp] theorem _root_.Nat.sum_nil : Nat.sum ([] : List Nat) = 0 := rfl

src/Init/Data/List/Count.lean

@@ -156,7 +156,7 @@ theorem countP_filterMap (p : β → Bool) (f : α → Option β) (l : List α)
   simp (config := { contextual := true }) [Option.getD_eq_iff, Option.isSome_eq_isSome]
 
 @[simp] theorem countP_flatten (l : List (List α)) :
-    countP p l.flatten = Nat.sum (l.map (countP p)) := by
+    countP p l.flatten = (l.map (countP p)).sum := by
   simp only [countP_eq_length_filter, filter_flatten]
   simp [countP_eq_length_filter']
 
@@ -232,7 +232,7 @@ theorem count_singleton (a b : α) : count a [b] = if b == a then 1 else 0 := by
 @[simp] theorem count_append (a : α) : ∀ l₁ l₂, count a (l₁ ++ l₂) = count a l₁ + count a l₂ :=
   countP_append _
 
-theorem count_flatten (a : α) (l : List (List α)) : count a l.flatten = Nat.sum (l.map (count a)) := by
+theorem count_flatten (a : α) (l : List (List α)) : count a l.flatten = (l.map (count a)).sum := by
   simp only [count_eq_countP, countP_flatten, count_eq_countP']
 
 @[deprecated count_flatten (since := "2024-10-14")] abbrev count_join := @count_flatten

src/Init/Data/List/Find.lean

@@ -378,14 +378,18 @@ theorem find?_flatten_eq_some {xs : List (List α)} {p : α → Bool} {a : α} :
     · exact h₁ l ml a m
     · exact h₂ a m
 
-@[simp] theorem find?_bind (xs : List α) (f : α → List β) (p : β → Bool) :
-    (xs.bind f).find? p = xs.findSome? (fun x => (f x).find? p) := by
-  simp [bind_def, findSome?_map]; rfl
+@[simp] theorem find?_flatMap (xs : List α) (f : α → List β) (p : β → Bool) :
+    (xs.flatMap f).find? p = xs.findSome? (fun x => (f x).find? p) := by
+  simp [flatMap_def, findSome?_map]; rfl
 
-theorem find?_bind_eq_none {xs : List α} {f : α → List β} {p : β → Bool} :
-    (xs.bind f).find? p = none ↔ ∀ x ∈ xs, ∀ y ∈ f x, !p y := by
+@[deprecated find?_flatMap (since := "2024-10-16")] abbrev find?_bind := @find?_flatMap
+
+theorem find?_flatMap_eq_none {xs : List α} {f : α → List β} {p : β → Bool} :
+    (xs.flatMap f).find? p = none ↔ ∀ x ∈ xs, ∀ y ∈ f x, !p y := by
   simp
 
+@[deprecated find?_flatMap_eq_none (since := "2024-10-16")] abbrev find?_bind_eq_none := @find?_flatMap_eq_none
+
 theorem find?_replicate : find? p (replicate n a) = if n = 0 then none else if p a then some a else none := by
   cases n
   · simp
@@ -789,7 +793,7 @@ theorem findIdx?_of_eq_none {xs : List α} {p : α → Bool} (w : xs.findIdx? p
 theorem findIdx?_flatten {l : List (List α)} {p : α → Bool} :
     l.flatten.findIdx? p =
       (l.findIdx? (·.any p)).map
-        fun i => Nat.sum ((l.take i).map List.length) +
+        fun i => ((l.take i).map List.length).sum +
           (l[i]?.map fun xs => xs.findIdx p).getD 0 := by
   induction l with
   | nil => simp

src/Init/Data/List/Impl.lean

@@ -93,29 +93,29 @@ The following operations are given `@[csimp]` replacements below:
 @[csimp] theorem foldr_eq_foldrTR : @foldr = @foldrTR := by
   funext α β f init l; simp [foldrTR, Array.foldr_eq_foldr_toList, -Array.size_toArray]
 
-/-! ### bind  -/
+/-! ### flatMap  -/
 
-/-- Tail recursive version of `List.bind`. -/
-@[inline] def bindTR (as : List α) (f : α → List β) : List β := go as #[] where
-  /-- Auxiliary for `bind`: `bind.go f as = acc.toList ++ bind f as` -/
+/-- Tail recursive version of `List.flatMap`. -/
+@[inline] def flatMapTR (as : List α) (f : α → List β) : List β := go as #[] where
+  /-- Auxiliary for `flatMap`: `flatMap.go f as = acc.toList ++ bind f as` -/
   @[specialize] go : List α → Array β → List β
   | [], acc => acc.toList
   | x::xs, acc => go xs (acc ++ f x)
 
-@[csimp] theorem bind_eq_bindTR : @List.bind = @bindTR := by
+@[csimp] theorem flatMap_eq_flatMapTR : @List.flatMap = @flatMapTR := by
   funext α β as f
-  let rec go : ∀ as acc, bindTR.go f as acc = acc.toList ++ as.bind f
-    | [], acc => by simp [bindTR.go, bind]
-    | x::xs, acc => by simp [bindTR.go, bind, go xs]
+  let rec go : ∀ as acc, flatMapTR.go f as acc = acc.toList ++ as.flatMap f
+    | [], acc => by simp [flatMapTR.go, flatMap]
+    | x::xs, acc => by simp [flatMapTR.go, flatMap, go xs]
   exact (go as #[]).symm
 
 /-! ### flatten -/
 
 /-- Tail recursive version of `List.flatten`. -/
-@[inline] def flattenTR (l : List (List α)) : List α := bindTR l id
+@[inline] def flattenTR (l : List (List α)) : List α := flatMapTR l id
 
 @[csimp] theorem flatten_eq_flattenTR : @flatten = @flattenTR := by
-  funext α l; rw [← List.bind_id, List.bind_eq_bindTR]; rfl
+  funext α l; rw [← List.flatMap_id, List.flatMap_eq_flatMapTR]; rfl
 
 /-! ## Sublists -/
 

src/Init/Data/List/Lemmas.lean

@@ -2070,8 +2070,7 @@ theorem eq_nil_or_concat : ∀ l : List α, l = [] ∨ ∃ L b, l = concat L b
 
 /-! ### flatten -/
 
-
-@[simp] theorem length_flatten (L : List (List α)) : (flatten L).length = Nat.sum (L.map length) := by
+@[simp] theorem length_flatten (L : List (List α)) : (flatten L).length = (L.map length).sum := by
   induction L with
   | nil => rfl
   | cons =>
@@ -2098,8 +2097,8 @@ theorem forall_mem_flatten {p : α → Prop} {L : List (List α)} :
   simp only [mem_flatten, forall_exists_index, and_imp]
   constructor <;> (intros; solve_by_elim)
 
-theorem flatten_eq_bind {L : List (List α)} : flatten L = L.bind id := by
-  induction L <;> simp [List.bind]
+theorem flatten_eq_flatMap {L : List (List α)} : flatten L = L.flatMap id := by
+  induction L <;> simp [List.flatMap]
 
 theorem head?_flatten {L : List (List α)} : (flatten L).head? = L.findSome? fun l => l.head? := by
   induction L with
@@ -2216,86 +2215,86 @@ theorem eq_iff_flatten_eq : ∀ {L L' : List (List α)},
       obtain ⟨rfl, h⟩ := append_inj h₁ h₂
       exact ⟨rfl, h, h₃⟩
 
-/-! ### bind -/
+/-! ### flatMap -/
 
-theorem bind_def (l : List α) (f : α → List β) : l.bind f = flatten (map f l) := by rfl
+theorem flatMap_def (l : List α) (f : α → List β) : l.flatMap f = flatten (map f l) := by rfl
 
-@[simp] theorem bind_id (l : List (List α)) : List.bind l id = l.flatten := by simp [bind_def]
+@[simp] theorem flatMap_id (l : List (List α)) : List.flatMap l id = l.flatten := by simp [flatMap_def]
 
-@[simp] theorem mem_bind {f : α → List β} {b} {l : List α} : b ∈ l.bind f ↔ ∃ a, a ∈ l ∧ b ∈ f a := by
-  simp [bind_def, mem_flatten]
+@[simp] theorem mem_flatMap {f : α → List β} {b} {l : List α} : b ∈ l.flatMap f ↔ ∃ a, a ∈ l ∧ b ∈ f a := by
+  simp [flatMap_def, mem_flatten]
   exact ⟨fun ⟨_, ⟨a, h₁, rfl⟩, h₂⟩ => ⟨a, h₁, h₂⟩, fun ⟨a, h₁, h₂⟩ => ⟨_, ⟨a, h₁, rfl⟩, h₂⟩⟩
 
-theorem exists_of_mem_bind {b : β} {l : List α} {f : α → List β} :
-    b ∈ l.bind f → ∃ a, a ∈ l ∧ b ∈ f a := mem_bind.1
+theorem exists_of_mem_flatMap {b : β} {l : List α} {f : α → List β} :
+    b ∈ l.flatMap f → ∃ a, a ∈ l ∧ b ∈ f a := mem_flatMap.1
 
-theorem mem_bind_of_mem {b : β} {l : List α} {f : α → List β} {a} (al : a ∈ l) (h : b ∈ f a) :
-    b ∈ l.bind f := mem_bind.2 ⟨a, al, h⟩
+theorem mem_flatMap_of_mem {b : β} {l : List α} {f : α → List β} {a} (al : a ∈ l) (h : b ∈ f a) :
+    b ∈ l.flatMap f := mem_flatMap.2 ⟨a, al, h⟩
 
 @[simp]
-theorem bind_eq_nil_iff {l : List α} {f : α → List β} : List.bind l f = [] ↔ ∀ x ∈ l, f x = [] :=
+theorem flatMap_eq_nil_iff {l : List α} {f : α → List β} : List.flatMap l f = [] ↔ ∀ x ∈ l, f x = [] :=
   flatten_eq_nil_iff.trans <| by
     simp only [mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
 
-@[deprecated bind_eq_nil_iff (since := "2024-09-05")] abbrev bind_eq_nil := @bind_eq_nil_iff
+@[deprecated flatMap_eq_nil_iff (since := "2024-09-05")] abbrev bind_eq_nil := @flatMap_eq_nil_iff
 
-theorem forall_mem_bind {p : β → Prop} {l : List α} {f : α → List β} :
-    (∀ (x) (_ : x ∈ l.bind f), p x) ↔ ∀ (a) (_ : a ∈ l) (b) (_ : b ∈ f a), p b := by
-  simp only [mem_bind, forall_exists_index, and_imp]
+theorem forall_mem_flatMap {p : β → Prop} {l : List α} {f : α → List β} :
+    (∀ (x) (_ : x ∈ l.flatMap f), p x) ↔ ∀ (a) (_ : a ∈ l) (b) (_ : b ∈ f a), p b := by
+  simp only [mem_flatMap, forall_exists_index, and_imp]
   constructor <;> (intros; solve_by_elim)
 
-theorem bind_singleton (f : α → List β) (x : α) : [x].bind f = f x :=
+theorem flatMap_singleton (f : α → List β) (x : α) : [x].flatMap f = f x :=
   append_nil (f x)
 
-@[simp] theorem bind_singleton' (l : List α) : (l.bind fun x => [x]) = l := by
+@[simp] theorem flatMap_singleton' (l : List α) : (l.flatMap fun x => [x]) = l := by
   induction l <;> simp [*]
 
-theorem head?_bind {l : List α} {f : α → List β} :
-    (l.bind f).head? = l.findSome? fun a => (f a).head? := by
+theorem head?_flatMap {l : List α} {f : α → List β} :
+    (l.flatMap f).head? = l.findSome? fun a => (f a).head? := by
   induction l with
   | nil => rfl
   | cons =>
     simp only [findSome?_cons]
     split <;> simp_all
 
-@[simp] theorem bind_append (xs ys : List α) (f : α → List β) :
-    (xs ++ ys).bind f = xs.bind f ++ ys.bind f := by
-  induction xs; {rfl}; simp_all [bind_cons, append_assoc]
+@[simp] theorem flatMap_append (xs ys : List α) (f : α → List β) :
+    (xs ++ ys).flatMap f = xs.flatMap f ++ ys.flatMap f := by
+  induction xs; {rfl}; simp_all [flatMap_cons, append_assoc]
 
-@[deprecated bind_append (since := "2024-07-24")] abbrev append_bind := @bind_append
+@[deprecated flatMap_append (since := "2024-07-24")] abbrev append_bind := @flatMap_append
 
-theorem bind_assoc {α β} (l : List α) (f : α → List β) (g : β → List γ) :
-    (l.bind f).bind g = l.bind fun x => (f x).bind g := by
+theorem flatMap_assoc {α β} (l : List α) (f : α → List β) (g : β → List γ) :
+    (l.flatMap f).flatMap g = l.flatMap fun x => (f x).flatMap g := by
   induction l <;> simp [*]
 
-theorem map_bind (f : β → γ) (g : α → List β) :
-    ∀ l : List α, (l.bind g).map f = l.bind fun a => (g a).map f
+theorem map_flatMap (f : β → γ) (g : α → List β) :
+    ∀ l : List α, (l.flatMap g).map f = l.flatMap fun a => (g a).map f
   | [] => rfl
-  | a::l => by simp only [bind_cons, map_append, map_bind _ _ l]
+  | a::l => by simp only [flatMap_cons, map_append, map_flatMap _ _ l]
 
-theorem bind_map (f : α → β) (g : β → List γ) (l : List α) :
-    (map f l).bind g = l.bind (fun a => g (f a)) := by
-  induction l <;> simp [bind_cons, *]
+theorem flatMap_map (f : α → β) (g : β → List γ) (l : List α) :
+    (map f l).flatMap g = l.flatMap (fun a => g (f a)) := by
+  induction l <;> simp [flatMap_cons, *]
 
-theorem map_eq_bind {α β} (f : α → β) (l : List α) : map f l = l.bind fun x => [f x] := by
+theorem map_eq_flatMap {α β} (f : α → β) (l : List α) : map f l = l.flatMap fun x => [f x] := by
   simp only [← map_singleton]
-  rw [← bind_singleton' l, map_bind, bind_singleton']
+  rw [← flatMap_singleton' l, map_flatMap, flatMap_singleton']
 
-theorem filterMap_bind {β γ} (l : List α) (g : α → List β) (f : β → Option γ) :
-    (l.bind g).filterMap f = l.bind fun a => (g a).filterMap f := by
+theorem filterMap_flatMap {β γ} (l : List α) (g : α → List β) (f : β → Option γ) :
+    (l.flatMap g).filterMap f = l.flatMap fun a => (g a).filterMap f := by
   induction l <;> simp [*]
 
-theorem filter_bind (l : List α) (g : α → List β) (f : β → Bool) :
-    (l.bind g).filter f = l.bind fun a => (g a).filter f := by
+theorem filter_flatMap (l : List α) (g : α → List β) (f : β → Bool) :
+    (l.flatMap g).filter f = l.flatMap fun a => (g a).filter f := by
   induction l <;> simp [*]
 
-theorem bind_eq_foldl (f : α → List β) (l : List α) :
-    l.bind f = l.foldl (fun acc a => acc ++ f a) [] := by
-  suffices ∀ l', l' ++ l.bind f = l.foldl (fun acc a => acc ++ f a) l' by simpa using this []
+theorem flatMap_eq_foldl (f : α → List β) (l : List α) :
+    l.flatMap f = l.foldl (fun acc a => acc ++ f a) [] := by
+  suffices ∀ l', l' ++ l.flatMap f = l.foldl (fun acc a => acc ++ f a) l' by simpa using this []
   intro l'
   induction l generalizing l'
   · simp
-  · next ih => rw [bind_cons, ← append_assoc, ih, foldl_cons]
+  · next ih => rw [flatMap_cons, ← append_assoc, ih, foldl_cons]
 
 /-! ### replicate -/
 
@@ -2485,10 +2484,10 @@ theorem filterMap_replicate_of_some {f : α → Option β} (h : f a = some b) :
     simp only [replicate_succ, flatten_cons, ih, append_replicate_replicate, replicate_inj, or_true,
       and_true, add_one_mul, Nat.add_comm]
 
-theorem bind_replicate {β} (f : α → List β) : (replicate n a).bind f = (replicate n (f a)).flatten := by
+theorem flatMap_replicate {β} (f : α → List β) : (replicate n a).flatMap f = (replicate n (f a)).flatten := by
   induction n with
   | zero => simp
-  | succ n ih => simp only [replicate_succ, bind_cons, ih, flatten_cons]
+  | succ n ih => simp only [replicate_succ, flatMap_cons, ih, flatten_cons]
 
 @[simp] theorem isEmpty_replicate : (replicate n a).isEmpty = decide (n = 0) := by
   cases n <;> simp [replicate_succ]
@@ -2673,10 +2672,10 @@ theorem flatten_reverse (L : List (List α)) :
     L.reverse.flatten = (L.map reverse).flatten.reverse := by
   induction L <;> simp_all
 
-theorem reverse_bind {β} (l : List α) (f : α → List β) : (l.bind f).reverse = l.reverse.bind (reverse ∘ f) := by
+theorem reverse_flatMap {β} (l : List α) (f : α → List β) : (l.flatMap f).reverse = l.reverse.flatMap (reverse ∘ f) := by
   induction l <;> simp_all
 
-theorem bind_reverse {β} (l : List α) (f : α → List β) : (l.reverse.bind f) = (l.bind (reverse ∘ f)).reverse := by
+theorem flatMap_reverse {β} (l : List α) (f : α → List β) : (l.reverse.flatMap f) = (l.flatMap (reverse ∘ f)).reverse := by
   induction l <;> simp_all
 
 @[simp] theorem reverseAux_eq (as bs : List α) : reverseAux as bs = reverse as ++ bs :=
@@ -2784,15 +2783,15 @@ theorem getLast_filterMap_of_eq_some {f : α → Option β} {l : List α} {w : l
   rw [head_filterMap_of_eq_some (by simp_all)]
   simp_all
 
-theorem getLast?_bind {L : List α} {f : α → List β} :
-    (L.bind f).getLast? = L.reverse.findSome? fun a => (f a).getLast? := by
-  simp only [← head?_reverse, reverse_bind]
-  rw [head?_bind]
+theorem getLast?_flatMap {L : List α} {f : α → List β} :
+    (L.flatMap f).getLast? = L.reverse.findSome? fun a => (f a).getLast? := by
+  simp only [← head?_reverse, reverse_flatMap]
+  rw [head?_flatMap]
   rfl
 
 theorem getLast?_flatten {L : List (List α)} :
     (flatten L).getLast? = L.reverse.findSome? fun l => l.getLast? := by
-  simp [← bind_id, getLast?_bind]
+  simp [← flatMap_id, getLast?_flatMap]
 
 theorem getLast?_replicate (a : α) (n : Nat) : (replicate n a).getLast? = if n = 0 then none else some a := by
   simp only [← head?_reverse, reverse_replicate, head?_replicate]
@@ -3301,12 +3300,12 @@ theorem all_eq_not_any_not (l : List α) (p : α → Bool) : l.all p = !l.any (!
 
 @[deprecated all_flatten (since := "2024-10-14")] abbrev all_join := @all_flatten
 
-@[simp] theorem any_bind {l : List α} {f : α → List β} :
-    (l.bind f).any p = l.any fun a => (f a).any p := by
+@[simp] theorem any_flatMap {l : List α} {f : α → List β} :
+    (l.flatMap f).any p = l.any fun a => (f a).any p := by
   induction l <;> simp_all
 
-@[simp] theorem all_bind {l : List α} {f : α → List β} :
-    (l.bind f).all p = l.all fun a => (f a).all p := by
+@[simp] theorem all_flatMap {l : List α} {f : α → List β} :
+    (l.flatMap f).all p = l.all fun a => (f a).all p := by
   induction l <;> simp_all
 
 @[simp] theorem any_reverse {l : List α} : l.reverse.any f = l.any f := by
@@ -3346,7 +3345,7 @@ theorem all_eq_not_any_not (l : List α) (p : α → Bool) : l.all p = !l.any (!
 @[deprecated exists_of_mem_flatten (since := "2024-10-14")] abbrev exists_of_mem_join := @exists_of_mem_flatten
 @[deprecated mem_flatten_of_mem (since := "2024-10-14")] abbrev mem_join_of_mem := @mem_flatten_of_mem
 @[deprecated forall_mem_flatten (since := "2024-10-14")] abbrev forall_mem_join := @forall_mem_flatten
-@[deprecated flatten_eq_bind (since := "2024-10-14")] abbrev join_eq_bind := @flatten_eq_bind
+@[deprecated flatten_eq_flatMap (since := "2024-10-14")] abbrev join_eq_bind := @flatten_eq_flatMap
 @[deprecated head?_flatten (since := "2024-10-14")] abbrev head?_join := @head?_flatten
 @[deprecated foldl_flatten (since := "2024-10-14")] abbrev foldl_join := @foldl_flatten
 @[deprecated foldr_flatten (since := "2024-10-14")] abbrev foldr_join := @foldr_flatten
@@ -3373,5 +3372,30 @@ theorem join_map_filter (p : α → Bool) (l : List (List α)) :
 @[deprecated reverse_flatten (since := "2024-10-14")] abbrev reverse_join := @reverse_flatten
 @[deprecated flatten_reverse (since := "2024-10-14")] abbrev join_reverse := @flatten_reverse
 @[deprecated getLast?_flatten (since := "2024-10-14")] abbrev getLast?_join := @getLast?_flatten
+@[deprecated flatten_eq_flatMap (since := "2024-10-16")] abbrev flatten_eq_bind := @flatten_eq_flatMap
+@[deprecated flatMap_def (since := "2024-10-16")] abbrev bind_def := @flatMap_def
+@[deprecated flatMap_id (since := "2024-10-16")] abbrev bind_id := @flatMap_id
+@[deprecated mem_flatMap (since := "2024-10-16")] abbrev mem_bind := @mem_flatMap
+@[deprecated exists_of_mem_flatMap (since := "2024-10-16")] abbrev exists_of_mem_bind := @exists_of_mem_flatMap
+@[deprecated mem_flatMap_of_mem (since := "2024-10-16")] abbrev mem_bind_of_mem := @mem_flatMap_of_mem
+@[deprecated flatMap_eq_nil_iff (since := "2024-10-16")] abbrev bind_eq_nil_iff := @flatMap_eq_nil_iff
+@[deprecated forall_mem_flatMap (since := "2024-10-16")] abbrev forall_mem_bind := @forall_mem_flatMap
+@[deprecated flatMap_singleton (since := "2024-10-16")] abbrev bind_singleton := @flatMap_singleton
+@[deprecated flatMap_singleton' (since := "2024-10-16")] abbrev bind_singleton' := @flatMap_singleton'
+@[deprecated head?_flatMap (since := "2024-10-16")] abbrev head_bind := @head?_flatMap
+@[deprecated flatMap_append (since := "2024-10-16")] abbrev bind_append := @flatMap_append
+@[deprecated flatMap_assoc (since := "2024-10-16")] abbrev bind_assoc := @flatMap_assoc
+@[deprecated map_flatMap (since := "2024-10-16")] abbrev map_bind := @map_flatMap
+@[deprecated flatMap_map (since := "2024-10-16")] abbrev bind_map := @flatMap_map
+@[deprecated map_eq_flatMap (since := "2024-10-16")] abbrev map_eq_bind := @map_eq_flatMap
+@[deprecated filterMap_flatMap (since := "2024-10-16")] abbrev filterMap_bind := @filterMap_flatMap
+@[deprecated filter_flatMap (since := "2024-10-16")] abbrev filter_bind := @filter_flatMap
+@[deprecated flatMap_eq_foldl (since := "2024-10-16")] abbrev bind_eq_foldl := @flatMap_eq_foldl
+@[deprecated flatMap_replicate (since := "2024-10-16")] abbrev bind_replicate := @flatMap_replicate
+@[deprecated reverse_flatMap (since := "2024-10-16")] abbrev reverse_bind := @reverse_flatMap
+@[deprecated flatMap_reverse (since := "2024-10-16")] abbrev bind_reverse := @flatMap_reverse
+@[deprecated getLast?_flatMap (since := "2024-10-16")] abbrev getLast?_bind := @getLast?_flatMap
+@[deprecated any_flatMap (since := "2024-10-16")] abbrev any_bind := @any_flatMap
+@[deprecated all_flatMap (since := "2024-10-16")] abbrev all_bind := @all_flatMap
 
 end List

src/Init/Data/List/Pairwise.lean

@@ -173,10 +173,12 @@ theorem pairwise_flatten {L : List (List α)} :
 
 @[deprecated pairwise_flatten (since := "2024-10-14")] abbrev pairwise_join := @pairwise_flatten
 
-theorem pairwise_bind {R : β → β → Prop} {l : List α} {f : α → List β} :
-    List.Pairwise R (l.bind f) ↔
+theorem pairwise_flatMap {R : β → β → Prop} {l : List α} {f : α → List β} :
+    List.Pairwise R (l.flatMap f) ↔
       (∀ a ∈ l, Pairwise R (f a)) ∧ Pairwise (fun a₁ a₂ => ∀ x ∈ f a₁, ∀ y ∈ f a₂, R x y) l := by
-  simp [List.bind, pairwise_flatten, pairwise_map]
+  simp [List.flatMap, pairwise_flatten, pairwise_map]
+
+@[deprecated pairwise_flatMap (since := "2024-10-14")] abbrev pairwise_bind := @pairwise_flatMap
 
 theorem pairwise_reverse {l : List α} :
     l.reverse.Pairwise R ↔ l.Pairwise (fun a b => R b a) := by

src/Init/Data/List/Perm.lean

@@ -470,9 +470,11 @@ theorem Perm.flatten {l₁ l₂ : List (List α)} (h : l₁ ~ l₂) : l₁.flatt
 
 @[deprecated Perm.flatten (since := "2024-10-14")] abbrev Perm.join := @Perm.flatten
 
-theorem Perm.bind_right {l₁ l₂ : List α} (f : α → List β) (p : l₁ ~ l₂) : l₁.bind f ~ l₂.bind f :=
+theorem Perm.flatMap_right {l₁ l₂ : List α} (f : α → List β) (p : l₁ ~ l₂) : l₁.flatMap f ~ l₂.flatMap f :=
   (p.map _).flatten
 
+@[deprecated Perm.flatMap_right (since := "2024-10-16")] abbrev Perm.bind_right := @Perm.flatMap_right
+
 theorem Perm.eraseP (f : α → Bool) {l₁ l₂ : List α}
     (H : Pairwise (fun a b => f a → f b → False) l₁) (p : l₁ ~ l₂) : eraseP f l₁ ~ eraseP f l₂ := by
   induction p with

src/Init/Data/List/Range.lean

@@ -20,7 +20,6 @@ open Nat
 
 /-! ## Ranges and enumeration -/
 
-
 /-! ### range' -/
 
 theorem range'_succ (s n step) : range' s (n + 1) step = s :: range' (s + step) n step := by

src/Init/Data/List/Sublist.lean

@@ -976,7 +976,7 @@ theorem mem_of_mem_drop {n} {l : List α} (h : a ∈ l.drop n) : a ∈ l :=
   drop_subset _ _ h
 
 theorem drop_suffix_drop_left (l : List α) {m n : Nat} (h : m ≤ n) : drop n l <:+ drop m l := by
-  rw [← Nat.sub_add_cancel h, ← drop_drop]
+  rw [← Nat.sub_add_cancel h, Nat.add_comm, ← drop_drop]
   apply drop_suffix
 
 -- See `Init.Data.List.Nat.TakeDrop` for `take_prefix_take_left`.

src/Init/Data/List/TakeDrop.lean

@@ -97,14 +97,14 @@ theorem get?_take {l : List α} {n m : Nat} (h : m < n) : (l.take n).get? m = l.
 
 theorem getElem?_take_of_succ {l : List α} {n : Nat} : (l.take (n + 1))[n]? = l[n]? := by simp
 
-@[simp] theorem drop_drop (n : Nat) : ∀ (m) (l : List α), drop n (drop m l) = drop (n + m) l
+@[simp] theorem drop_drop (n : Nat) : ∀ (m) (l : List α), drop n (drop m l) = drop (m + n) l
   | m, [] => by simp
   | 0, l => by simp
   | m + 1, a :: l =>
     calc
       drop n (drop (m + 1) (a :: l)) = drop n (drop m l) := rfl
-      _ = drop (n + m) l := drop_drop n m l
-      _ = drop (n + (m + 1)) (a :: l) := rfl
+      _ = drop (m + n) l := drop_drop n m l
+      _ = drop ((m + 1) + n) (a :: l) := by rw [Nat.add_right_comm]; rfl
 
 theorem take_drop : ∀ (m n : Nat) (l : List α), take n (drop m l) = drop m (take (m + n) l)
   | 0, _, _ => by simp
@@ -112,7 +112,7 @@ theorem take_drop : ∀ (m n : Nat) (l : List α), take n (drop m l) = drop m (t
   | _+1, _, _ :: _ => by simpa [Nat.succ_add, take_succ_cons, drop_succ_cons] using take_drop ..
 
 @[deprecated drop_drop (since := "2024-06-15")]
-theorem drop_add (m n) (l : List α) : drop (m + n) l = drop m (drop n l) := by
+theorem drop_add (m n) (l : List α) : drop (m + n) l = drop n (drop m l) := by
   simp [drop_drop]
 
 @[simp]
@@ -126,7 +126,7 @@ theorem tail_drop (l : List α) (n : Nat) : (l.drop n).tail = l.drop (n + 1) :=
 
 @[simp]
 theorem drop_tail (l : List α) (n : Nat) : l.tail.drop n = l.drop (n + 1) := by
-  rw [← drop_drop, drop_one]
+  rw [Nat.add_comm, ← drop_drop, drop_one]
 
 @[simp]
 theorem drop_eq_nil_iff {l : List α} {k : Nat} : l.drop k = [] ↔ l.length ≤ k := by

src/Init/Data/Nat/Basic.lean

@@ -131,7 +131,7 @@ theorem or_exists_add_one : p 0 ∨ (Exists fun n => p (n + 1)) ↔ Exists p :=
 @[simp] theorem blt_eq : (Nat.blt x y = true) = (x < y) := propext <| Iff.intro Nat.le_of_ble_eq_true Nat.ble_eq_true_of_le
 
 instance : LawfulBEq Nat where
-  eq_of_beq h := Nat.eq_of_beq_eq_true h
+  eq_of_beq h := by simpa using h
   rfl := by simp [BEq.beq]
 
 theorem beq_eq_true_eq (a b : Nat) : ((a == b) = true) = (a = b) := by simp
@@ -796,6 +796,8 @@ theorem pos_pow_of_pos {n : Nat} (m : Nat) (h : 0 < n) : 0 < n^m :=
   | zero => cases h
   | succ n => simp [Nat.pow_succ]
 
+protected theorem two_pow_pos (w : Nat) : 0 < 2^w := Nat.pos_pow_of_pos _ (by decide)
+
 instance {n m : Nat} [NeZero n] : NeZero (n^m) :=
   ⟨Nat.ne_zero_iff_zero_lt.mpr (Nat.pos_pow_of_pos m (pos_of_neZero _))⟩
 

src/Init/Data/Nat/Power2.lean

@@ -8,8 +8,6 @@ import Init.Data.Nat.Linear
 
 namespace Nat
 
-protected theorem two_pow_pos (w : Nat) : 0 < 2^w := Nat.pos_pow_of_pos _ (by decide)
-
 theorem nextPowerOfTwo_dec {n power : Nat} (h₁ : power > 0) (h₂ : power < n) : n - power * 2 < n - power := by
   have : power * 2 = power + power := by simp_arith
   rw [this, Nat.sub_add_eq]

src/Init/Data/Prod.lean

@@ -7,6 +7,8 @@ prelude
 import Init.SimpLemmas
 import Init.NotationExtra
 
+namespace Prod
+
 instance [BEq α] [BEq β] [LawfulBEq α] [LawfulBEq β] : LawfulBEq (α × β) where
   eq_of_beq {a b} (h : a.1 == b.1 && a.2 == b.2) := by
     cases a; cases b
@@ -14,9 +16,65 @@ instance [BEq α] [BEq β] [LawfulBEq α] [LawfulBEq β] : LawfulBEq (α × β)
   rfl {a} := by cases a; simp [BEq.beq, LawfulBEq.rfl]
 
 @[simp]
-protected theorem Prod.forall {p : α × β → Prop} : (∀ x, p x) ↔ ∀ a b, p (a, b) :=
+protected theorem «forall» {p : α × β → Prop} : (∀ x, p x) ↔ ∀ a b, p (a, b) :=
   ⟨fun h a b ↦ h (a, b), fun h ⟨a, b⟩ ↦ h a b⟩
 
 @[simp]
-protected theorem Prod.exists {p : α × β → Prop} : (∃ x, p x) ↔ ∃ a b, p (a, b) :=
+protected theorem «exists» {p : α × β → Prop} : (∃ x, p x) ↔ ∃ a b, p (a, b) :=
   ⟨fun ⟨⟨a, b⟩, h⟩ ↦ ⟨a, b, h⟩, fun ⟨a, b, h⟩ ↦ ⟨⟨a, b⟩, h⟩⟩
+
+@[simp] theorem map_id : Prod.map (@id α) (@id β) = id := rfl
+
+@[simp] theorem map_id' : Prod.map (fun a : α => a) (fun b : β => b) = fun x ↦ x := rfl
+
+/--
+Composing a `Prod.map` with another `Prod.map` is equal to
+a single `Prod.map` of composed functions.
+-/
+theorem map_comp_map (f : α → β) (f' : γ → δ) (g : β → ε) (g' : δ → ζ) :
+    Prod.map g g' ∘ Prod.map f f' = Prod.map (g ∘ f) (g' ∘ f') :=
+  rfl
+
+/--
+Composing a `Prod.map` with another `Prod.map` is equal to
+a single `Prod.map` of composed functions, fully applied.
+-/
+theorem map_map (f : α → β) (f' : γ → δ) (g : β → ε) (g' : δ → ζ) (x : α × γ) :
+    Prod.map g g' (Prod.map f f' x) = Prod.map (g ∘ f) (g' ∘ f') x :=
+  rfl
+
+/-- Swap the factors of a product. `swap (a, b) = (b, a)` -/
+def swap : α × β → β × α := fun p => (p.2, p.1)
+
+@[simp]
+theorem swap_swap : ∀ x : α × β, swap (swap x) = x
+  | ⟨_, _⟩ => rfl
+
+@[simp]
+theorem fst_swap {p : α × β} : (swap p).1 = p.2 :=
+  rfl
+
+@[simp]
+theorem snd_swap {p : α × β} : (swap p).2 = p.1 :=
+  rfl
+
+@[simp]
+theorem swap_prod_mk {a : α} {b : β} : swap (a, b) = (b, a) :=
+  rfl
+
+@[simp]
+theorem swap_swap_eq : swap ∘ swap = @id (α × β) :=
+  funext swap_swap
+
+@[simp]
+theorem swap_inj {p q : α × β} : swap p = swap q ↔ p = q := by
+  cases p; cases q; simp [and_comm]
+
+/--
+For two functions `f` and `g`, the composition of `Prod.map f g` with `Prod.swap`
+is equal to the composition of `Prod.swap` with `Prod.map g f`.
+-/
+theorem map_comp_swap (f : α → β) (g : γ → δ) :
+    Prod.map f g ∘ Prod.swap = Prod.swap ∘ Prod.map g f := rfl
+
+end Prod

src/Init/Data/Repr.lean

@@ -7,7 +7,7 @@ prelude
 import Init.Data.Format.Basic
 import Init.Data.Int.Basic
 import Init.Data.Nat.Div
-import Init.Data.UInt.Basic
+import Init.Data.UInt.BasicAux
 import Init.Control.Id
 open Sum Subtype Nat
 

src/Init/Data/String/Basic.lean

@@ -317,6 +317,9 @@ theorem _root_.Char.utf8Size_le_four (c : Char) : c.utf8Size ≤ 4 := by
 
 @[simp] theorem pos_add_char (p : Pos) (c : Char) : (p + c).byteIdx = p.byteIdx + c.utf8Size := rfl
 
+protected theorem Pos.ne_zero_of_lt : {a b : Pos} → a < b → b ≠ 0
+  | _, _, hlt, rfl => Nat.not_lt_zero _ hlt
+
 theorem lt_next (s : String) (i : Pos) : i.1 < (s.next i).1 :=
   Nat.add_lt_add_left (Char.utf8Size_pos _) _
 
@@ -1021,6 +1024,66 @@ instance hasBeq : BEq Substring := ⟨beq⟩
 def sameAs (ss1 ss2 : Substring) : Bool :=
   ss1.startPos == ss2.startPos && ss1 == ss2
 
+/--
+Returns the longest common prefix of two substrings.
+The returned substring will use the same underlying string as `s`.
+-/
+def commonPrefix (s t : Substring) : Substring :=
+  { s with stopPos := loop s.startPos t.startPos }
+where
+  /-- Returns the ending position of the common prefix, working up from `spos, tpos`. -/
+  loop spos tpos :=
+    if h : spos < s.stopPos ∧ tpos < t.stopPos then
+      if s.str.get spos == t.str.get tpos then
+        have := Nat.sub_lt_sub_left h.1 (s.str.lt_next spos)
+        loop (s.str.next spos) (t.str.next tpos)
+      else
+        spos
+    else
+      spos
+  termination_by s.stopPos.byteIdx - spos.byteIdx
+
+/--
+Returns the longest common suffix of two substrings.
+The returned substring will use the same underlying string as `s`.
+-/
+def commonSuffix (s t : Substring) : Substring :=
+  { s with startPos := loop s.stopPos t.stopPos }
+where
+  /-- Returns the starting position of the common prefix, working down from `spos, tpos`. -/
+  loop spos tpos :=
+    if h : s.startPos < spos ∧ t.startPos < tpos then
+      let spos' := s.str.prev spos
+      let tpos' := t.str.prev tpos
+      if s.str.get spos' == t.str.get tpos' then
+        have : spos' < spos := s.str.prev_lt_of_pos spos (String.Pos.ne_zero_of_lt h.1)
+        loop spos' tpos'
+      else
+        spos
+    else
+      spos
+  termination_by spos.byteIdx
+
+/--
+If `pre` is a prefix of `s`, i.e. `s = pre ++ t`, returns the remainder `t`.
+-/
+def dropPrefix? (s : Substring) (pre : Substring) : Option Substring :=
+  let t := s.commonPrefix pre
+  if t.bsize = pre.bsize then
+    some { s with startPos := t.stopPos }
+  else
+    none
+
+/--
+If `suff` is a suffix of `s`, i.e. `s = t ++ suff`, returns the remainder `t`.
+-/
+def dropSuffix? (s : Substring) (suff : Substring) : Option Substring :=
+  let t := s.commonSuffix suff
+  if t.bsize = suff.bsize then
+    some { s with stopPos := t.startPos }
+  else
+    none
+
 end Substring
 
 namespace String
@@ -1082,6 +1145,28 @@ namespace String
 @[inline] def decapitalize (s : String) :=
   s.set 0 <| s.get 0 |>.toLower
 
+/--
+If `pre` is a prefix of `s`, i.e. `s = pre ++ t`, returns the remainder `t`.
+-/
+def dropPrefix? (s : String) (pre : Substring) : Option Substring :=
+  s.toSubstring.dropPrefix? pre
+
+/--
+If `suff` is a suffix of `s`, i.e. `s = t ++ suff`, returns the remainder `t`.
+-/
+def dropSuffix? (s : String) (suff : Substring) : Option Substring :=
+  s.toSubstring.dropSuffix? suff
+
+/-- `s.stripPrefix pre` will remove `pre` from the beginning of `s` if it occurs there,
+or otherwise return `s`. -/
+def stripPrefix (s : String) (pre : Substring) : String :=
+  s.dropPrefix? pre |>.map Substring.toString |>.getD s
+
+/-- `s.stripSuffix suff` will remove `suff` from the end of `s` if it occurs there,
+or otherwise return `s`. -/
+def stripSuffix (s : String) (suff : Substring) : String :=
+  s.dropSuffix? suff |>.map Substring.toString |>.getD s
+
 end String
 
 namespace Char

src/Init/Data/String/Extra.lean

@@ -5,6 +5,7 @@ Author: Leonardo de Moura
 -/
 prelude
 import Init.Data.ByteArray
+import Init.Data.UInt.Lemmas
 
 namespace String
 
@@ -20,14 +21,14 @@ def toNat! (s : String) : Nat :=
 def utf8DecodeChar? (a : ByteArray) (i : Nat) : Option Char := do
   let c ← a[i]?
   if c &&& 0x80 == 0 then
-    some ⟨c.toUInt32, .inl (Nat.lt_trans c.1.2 (by decide))⟩
+    some ⟨c.toUInt32, .inl (Nat.lt_trans c.toBitVec.isLt (by decide))⟩
   else if c &&& 0xe0 == 0xc0 then
     let c1 ← a[i+1]?
     guard (c1 &&& 0xc0 == 0x80)
     let r := ((c &&& 0x1f).toUInt32 <<< 6) ||| (c1 &&& 0x3f).toUInt32
     guard (0x80 ≤ r)
     -- TODO: Prove h from the definition of r once we have the necessary lemmas
-    if h : r < 0xd800 then some ⟨r, .inl h⟩ else none
+    if h : r < 0xd800 then some ⟨r, .inl (UInt32.toNat_lt_of_lt (by decide) h)⟩ else none
   else if c &&& 0xf0 == 0xe0 then
     let c1 ← a[i+1]?
     let c2 ← a[i+2]?
@@ -38,7 +39,14 @@ def utf8DecodeChar? (a : ByteArray) (i : Nat) : Option Char := do
       (c2 &&& 0x3f).toUInt32
     guard (0x800 ≤ r)
     -- TODO: Prove `r < 0x110000` from the definition of r once we have the necessary lemmas
-    if h : r < 0xd800 ∨ 0xdfff < r ∧ r < 0x110000 then some ⟨r, h⟩ else none
+    if h : r < 0xd800 ∨ 0xdfff < r ∧ r < 0x110000 then
+      have :=
+        match h with
+        | .inl h => Or.inl (UInt32.toNat_lt_of_lt (by decide) h)
+        | .inr h => Or.inr ⟨UInt32.lt_toNat_of_lt (by decide) h.left, UInt32.toNat_lt_of_lt (by decide) h.right⟩
+      some ⟨r, this⟩
+    else
+      none
   else if c &&& 0xf8 == 0xf0 then
     let c1 ← a[i+1]?
     let c2 ← a[i+2]?
@@ -50,7 +58,7 @@ def utf8DecodeChar? (a : ByteArray) (i : Nat) : Option Char := do
       ((c2 &&& 0x3f).toUInt32 <<< 6) |||
       (c3 &&& 0x3f).toUInt32
     if h : 0x10000 ≤ r ∧ r < 0x110000 then
-      some ⟨r, .inr ⟨Nat.lt_of_lt_of_le (by decide) h.1, h.2⟩⟩
+      some ⟨r, .inr ⟨Nat.lt_of_lt_of_le (by decide) (UInt32.le_toNat_of_le (by decide) h.left), UInt32.toNat_lt_of_lt (by decide) h.right⟩⟩
     else none
   else
     none
@@ -117,10 +125,10 @@ def utf8EncodeChar (c : Char) : List UInt8 :=
 /-- Converts the given `String` to a [UTF-8](https://en.wikipedia.org/wiki/UTF-8) encoded byte array. -/
 @[extern "lean_string_to_utf8"]
 def toUTF8 (a : @& String) : ByteArray :=
-  ⟨⟨a.data.bind utf8EncodeChar⟩⟩
+  ⟨⟨a.data.flatMap utf8EncodeChar⟩⟩
 
 @[simp] theorem size_toUTF8 (s : String) : s.toUTF8.size = s.utf8ByteSize := by
-  simp [toUTF8, ByteArray.size, Array.size, utf8ByteSize, List.bind]
+  simp [toUTF8, ByteArray.size, Array.size, utf8ByteSize, List.flatMap]
   induction s.data <;> simp [List.map, List.flatten, utf8ByteSize.go, Nat.add_comm, *]
 
 /-- Accesses a byte in the UTF-8 encoding of the `String`. O(1) -/

src/Init/Data/ToString/Basic.lean

@@ -5,7 +5,7 @@ Author: Leonardo de Moura
 -/
 prelude
 import Init.Data.String.Basic
-import Init.Data.UInt.Basic
+import Init.Data.UInt.BasicAux
 import Init.Data.Nat.Div
 import Init.Data.Repr
 import Init.Data.Int.Basic

src/Init/Data/UInt.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
 prelude
+import Init.Data.UInt.BasicAux
 import Init.Data.UInt.Basic
 import Init.Data.UInt.Log2
 import Init.Data.UInt.Lemmas

src/Init/Data/UInt/Basic.lean

@@ -4,52 +4,50 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Init.Data.Fin.Basic
+import Init.Data.UInt.BasicAux
+import Init.Data.BitVec.Basic
 
 open Nat
 
-@[extern "lean_uint8_of_nat"]
-def UInt8.ofNat (n : @& Nat) : UInt8 := ⟨Fin.ofNat n⟩
-abbrev Nat.toUInt8 := UInt8.ofNat
-@[extern "lean_uint8_to_nat"]
-def UInt8.toNat (n : UInt8) : Nat := n.val.val
 @[extern "lean_uint8_add"]
-def UInt8.add (a b : UInt8) : UInt8 := ⟨a.val + b.val⟩
+def UInt8.add (a b : UInt8) : UInt8 := ⟨a.toBitVec + b.toBitVec⟩
 @[extern "lean_uint8_sub"]
-def UInt8.sub (a b : UInt8) : UInt8 := ⟨a.val - b.val⟩
+def UInt8.sub (a b : UInt8) : UInt8 := ⟨a.toBitVec - b.toBitVec⟩
 @[extern "lean_uint8_mul"]
-def UInt8.mul (a b : UInt8) : UInt8 := ⟨a.val * b.val⟩
+def UInt8.mul (a b : UInt8) : UInt8 := ⟨a.toBitVec * b.toBitVec⟩
 @[extern "lean_uint8_div"]
-def UInt8.div (a b : UInt8) : UInt8 := ⟨a.val / b.val⟩
+def UInt8.div (a b : UInt8) : UInt8 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩
 @[extern "lean_uint8_mod"]
-def UInt8.mod (a b : UInt8) : UInt8 := ⟨a.val % b.val⟩
-@[extern "lean_uint8_modn"]
+def UInt8.mod (a b : UInt8) : UInt8 := ⟨BitVec.umod a.toBitVec b.toBitVec⟩
+@[extern "lean_uint8_modn", deprecated UInt8.mod (since := "2024-09-23")]
 def UInt8.modn (a : UInt8) (n : @& Nat) : UInt8 := ⟨Fin.modn a.val n⟩
 @[extern "lean_uint8_land"]
-def UInt8.land (a b : UInt8) : UInt8 := ⟨Fin.land a.val b.val⟩
+def UInt8.land (a b : UInt8) : UInt8 := ⟨a.toBitVec &&& b.toBitVec⟩
 @[extern "lean_uint8_lor"]
-def UInt8.lor (a b : UInt8) : UInt8 := ⟨Fin.lor a.val b.val⟩
+def UInt8.lor (a b : UInt8) : UInt8 := ⟨a.toBitVec ||| b.toBitVec⟩
 @[extern "lean_uint8_xor"]
-def UInt8.xor (a b : UInt8) : UInt8 := ⟨Fin.xor a.val b.val⟩
+def UInt8.xor (a b : UInt8) : UInt8 := ⟨a.toBitVec ^^^ b.toBitVec⟩
 @[extern "lean_uint8_shift_left"]
-def UInt8.shiftLeft (a b : UInt8) : UInt8 := ⟨a.val <<< (modn b 8).val⟩
+def UInt8.shiftLeft (a b : UInt8) : UInt8 := ⟨a.toBitVec <<< (mod b 8).toBitVec⟩
 @[extern "lean_uint8_shift_right"]
-def UInt8.shiftRight (a b : UInt8) : UInt8 := ⟨a.val >>> (modn b 8).val⟩
-def UInt8.lt (a b : UInt8) : Prop := a.val < b.val
-def UInt8.le (a b : UInt8) : Prop := a.val ≤ b.val
+def UInt8.shiftRight (a b : UInt8) : UInt8 := ⟨a.toBitVec >>> (mod b 8).toBitVec⟩
+def UInt8.lt (a b : UInt8) : Prop := a.toBitVec < b.toBitVec
+def UInt8.le (a b : UInt8) : Prop := a.toBitVec ≤ b.toBitVec
 
-instance UInt8.instOfNat : OfNat UInt8 n := ⟨UInt8.ofNat n⟩
 instance : Add UInt8       := ⟨UInt8.add⟩
 instance : Sub UInt8       := ⟨UInt8.sub⟩
 instance : Mul UInt8       := ⟨UInt8.mul⟩
 instance : Mod UInt8       := ⟨UInt8.mod⟩
+
+set_option linter.deprecated false in
 instance : HMod UInt8 Nat UInt8 := ⟨UInt8.modn⟩
+
 instance : Div UInt8       := ⟨UInt8.div⟩
 instance : LT UInt8        := ⟨UInt8.lt⟩
 instance : LE UInt8        := ⟨UInt8.le⟩
 
 @[extern "lean_uint8_complement"]
-def UInt8.complement (a:UInt8) : UInt8 := 0-(a+1)
+def UInt8.complement (a : UInt8) : UInt8 := ⟨~~~a.toBitVec⟩
 
 instance : Complement UInt8 := ⟨UInt8.complement⟩
 instance : AndOp UInt8     := ⟨UInt8.land⟩
@@ -58,69 +56,58 @@ instance : Xor UInt8       := ⟨UInt8.xor⟩
 instance : ShiftLeft UInt8  := ⟨UInt8.shiftLeft⟩
 instance : ShiftRight UInt8 := ⟨UInt8.shiftRight⟩
 
-set_option bootstrap.genMatcherCode false in
 @[extern "lean_uint8_dec_lt"]
 def UInt8.decLt (a b : UInt8) : Decidable (a < b) :=
-  match a, b with
-  | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n < m))
+  inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))
 
-set_option bootstrap.genMatcherCode false in
 @[extern "lean_uint8_dec_le"]
 def UInt8.decLe (a b : UInt8) : Decidable (a ≤ b) :=
-  match a, b with
-  | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n <= m))
+  inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))
 
 instance (a b : UInt8) : Decidable (a < b) := UInt8.decLt a b
 instance (a b : UInt8) : Decidable (a ≤ b) := UInt8.decLe a b
 instance : Max UInt8 := maxOfLe
 instance : Min UInt8 := minOfLe
 
-@[extern "lean_uint16_of_nat"]
-def UInt16.ofNat (n : @& Nat) : UInt16 := ⟨Fin.ofNat n⟩
-abbrev Nat.toUInt16 := UInt16.ofNat
-@[extern "lean_uint16_to_nat"]
-def UInt16.toNat (n : UInt16) : Nat := n.val.val
 @[extern "lean_uint16_add"]
-def UInt16.add (a b : UInt16) : UInt16 := ⟨a.val + b.val⟩
+def UInt16.add (a b : UInt16) : UInt16 := ⟨a.toBitVec + b.toBitVec⟩
 @[extern "lean_uint16_sub"]
-def UInt16.sub (a b : UInt16) : UInt16 := ⟨a.val - b.val⟩
+def UInt16.sub (a b : UInt16) : UInt16 := ⟨a.toBitVec - b.toBitVec⟩
 @[extern "lean_uint16_mul"]
-def UInt16.mul (a b : UInt16) : UInt16 := ⟨a.val * b.val⟩
+def UInt16.mul (a b : UInt16) : UInt16 := ⟨a.toBitVec * b.toBitVec⟩
 @[extern "lean_uint16_div"]
-def UInt16.div (a b : UInt16) : UInt16 := ⟨a.val / b.val⟩
+def UInt16.div (a b : UInt16) : UInt16 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩
 @[extern "lean_uint16_mod"]
-def UInt16.mod (a b : UInt16) : UInt16 := ⟨a.val % b.val⟩
-@[extern "lean_uint16_modn"]
+def UInt16.mod (a b : UInt16) : UInt16 := ⟨BitVec.umod a.toBitVec b.toBitVec⟩
+@[extern "lean_uint16_modn", deprecated UInt16.mod (since := "2024-09-23")]
 def UInt16.modn (a : UInt16) (n : @& Nat) : UInt16 := ⟨Fin.modn a.val n⟩
 @[extern "lean_uint16_land"]
-def UInt16.land (a b : UInt16) : UInt16 := ⟨Fin.land a.val b.val⟩
+def UInt16.land (a b : UInt16) : UInt16 := ⟨a.toBitVec &&& b.toBitVec⟩
 @[extern "lean_uint16_lor"]
-def UInt16.lor (a b : UInt16) : UInt16 := ⟨Fin.lor a.val b.val⟩
+def UInt16.lor (a b : UInt16) : UInt16 := ⟨a.toBitVec ||| b.toBitVec⟩
 @[extern "lean_uint16_xor"]
-def UInt16.xor (a b : UInt16) : UInt16 := ⟨Fin.xor a.val b.val⟩
+def UInt16.xor (a b : UInt16) : UInt16 := ⟨a.toBitVec ^^^ b.toBitVec⟩
 @[extern "lean_uint16_shift_left"]
-def UInt16.shiftLeft (a b : UInt16) : UInt16 := ⟨a.val <<< (modn b 16).val⟩
-@[extern "lean_uint16_to_uint8"]
-def UInt16.toUInt8 (a : UInt16) : UInt8 := a.toNat.toUInt8
-@[extern "lean_uint8_to_uint16"]
-def UInt8.toUInt16 (a : UInt8) : UInt16 := ⟨a.val, Nat.lt_trans a.1.2 (by decide)⟩
+def UInt16.shiftLeft (a b : UInt16) : UInt16 := ⟨a.toBitVec <<< (mod b 16).toBitVec⟩
 @[extern "lean_uint16_shift_right"]
-def UInt16.shiftRight (a b : UInt16) : UInt16 := ⟨a.val >>> (modn b 16).val⟩
-def UInt16.lt (a b : UInt16) : Prop := a.val < b.val
-def UInt16.le (a b : UInt16) : Prop := a.val ≤ b.val
+def UInt16.shiftRight (a b : UInt16) : UInt16 := ⟨a.toBitVec >>> (mod b 16).toBitVec⟩
+def UInt16.lt (a b : UInt16) : Prop := a.toBitVec < b.toBitVec
+def UInt16.le (a b : UInt16) : Prop := a.toBitVec ≤ b.toBitVec
 
-instance UInt16.instOfNat : OfNat UInt16 n := ⟨UInt16.ofNat n⟩
 instance : Add UInt16       := ⟨UInt16.add⟩
 instance : Sub UInt16       := ⟨UInt16.sub⟩
 instance : Mul UInt16       := ⟨UInt16.mul⟩
 instance : Mod UInt16       := ⟨UInt16.mod⟩
+
+set_option linter.deprecated false in
 instance : HMod UInt16 Nat UInt16 := ⟨UInt16.modn⟩
+
 instance : Div UInt16       := ⟨UInt16.div⟩
 instance : LT UInt16        := ⟨UInt16.lt⟩
 instance : LE UInt16        := ⟨UInt16.le⟩
 
 @[extern "lean_uint16_complement"]
-def UInt16.complement (a:UInt16) : UInt16 := 0-(a+1)
+def UInt16.complement (a : UInt16) : UInt16 := ⟨~~~a.toBitVec⟩
 
 instance : Complement UInt16 := ⟨UInt16.complement⟩
 instance : AndOp UInt16     := ⟨UInt16.land⟩
@@ -132,74 +119,53 @@ instance : ShiftRight UInt16 := ⟨UInt16.shiftRight⟩
 set_option bootstrap.genMatcherCode false in
 @[extern "lean_uint16_dec_lt"]
 def UInt16.decLt (a b : UInt16) : Decidable (a < b) :=
-  match a, b with
-  | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n < m))
+  inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))
 
 set_option bootstrap.genMatcherCode false in
 @[extern "lean_uint16_dec_le"]
 def UInt16.decLe (a b : UInt16) : Decidable (a ≤ b) :=
-  match a, b with
-  | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n <= m))
+  inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))
 
 instance (a b : UInt16) : Decidable (a < b) := UInt16.decLt a b
 instance (a b : UInt16) : Decidable (a ≤ b) := UInt16.decLe a b
 instance : Max UInt16 := maxOfLe
 instance : Min UInt16 := minOfLe
 
-@[extern "lean_uint32_of_nat"]
-def UInt32.ofNat (n : @& Nat) : UInt32 := ⟨Fin.ofNat n⟩
-@[extern "lean_uint32_of_nat"]
-def UInt32.ofNat' (n : Nat) (h : n < UInt32.size) : UInt32 := ⟨⟨n, h⟩⟩
-/--
-Converts the given natural number to `UInt32`, but returns `2^32 - 1` for natural numbers `>= 2^32`.
--/
-def UInt32.ofNatTruncate (n : Nat) : UInt32 :=
-  if h : n < UInt32.size then
-    UInt32.ofNat' n h
-  else
-    UInt32.ofNat' (UInt32.size - 1) (by decide)
-abbrev Nat.toUInt32 := UInt32.ofNat
 @[extern "lean_uint32_add"]
-def UInt32.add (a b : UInt32) : UInt32 := ⟨a.val + b.val⟩
+def UInt32.add (a b : UInt32) : UInt32 := ⟨a.toBitVec + b.toBitVec⟩
 @[extern "lean_uint32_sub"]
-def UInt32.sub (a b : UInt32) : UInt32 := ⟨a.val - b.val⟩
+def UInt32.sub (a b : UInt32) : UInt32 := ⟨a.toBitVec - b.toBitVec⟩
 @[extern "lean_uint32_mul"]
-def UInt32.mul (a b : UInt32) : UInt32 := ⟨a.val * b.val⟩
+def UInt32.mul (a b : UInt32) : UInt32 := ⟨a.toBitVec * b.toBitVec⟩
 @[extern "lean_uint32_div"]
-def UInt32.div (a b : UInt32) : UInt32 := ⟨a.val / b.val⟩
+def UInt32.div (a b : UInt32) : UInt32 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩
 @[extern "lean_uint32_mod"]
-def UInt32.mod (a b : UInt32) : UInt32 := ⟨a.val % b.val⟩
-@[extern "lean_uint32_modn"]
+def UInt32.mod (a b : UInt32) : UInt32 := ⟨BitVec.umod a.toBitVec b.toBitVec⟩
+@[extern "lean_uint32_modn", deprecated UInt32.mod (since := "2024-09-23")]
 def UInt32.modn (a : UInt32) (n : @& Nat) : UInt32 := ⟨Fin.modn a.val n⟩
 @[extern "lean_uint32_land"]
-def UInt32.land (a b : UInt32) : UInt32 := ⟨Fin.land a.val b.val⟩
+def UInt32.land (a b : UInt32) : UInt32 := ⟨a.toBitVec &&& b.toBitVec⟩
 @[extern "lean_uint32_lor"]
-def UInt32.lor (a b : UInt32) : UInt32 := ⟨Fin.lor a.val b.val⟩
+def UInt32.lor (a b : UInt32) : UInt32 := ⟨a.toBitVec ||| b.toBitVec⟩
 @[extern "lean_uint32_xor"]
-def UInt32.xor (a b : UInt32) : UInt32 := ⟨Fin.xor a.val b.val⟩
+def UInt32.xor (a b : UInt32) : UInt32 := ⟨a.toBitVec ^^^ b.toBitVec⟩
 @[extern "lean_uint32_shift_left"]
-def UInt32.shiftLeft (a b : UInt32) : UInt32 := ⟨a.val <<< (modn b 32).val⟩
+def UInt32.shiftLeft (a b : UInt32) : UInt32 := ⟨a.toBitVec <<< (mod b 32).toBitVec⟩
 @[extern "lean_uint32_shift_right"]
-def UInt32.shiftRight (a b : UInt32) : UInt32 := ⟨a.val >>> (modn b 32).val⟩
-@[extern "lean_uint32_to_uint8"]
-def UInt32.toUInt8 (a : UInt32) : UInt8 := a.toNat.toUInt8
-@[extern "lean_uint32_to_uint16"]
-def UInt32.toUInt16 (a : UInt32) : UInt16 := a.toNat.toUInt16
-@[extern "lean_uint8_to_uint32"]
-def UInt8.toUInt32 (a : UInt8) : UInt32 := ⟨a.val, Nat.lt_trans a.1.2 (by decide)⟩
-@[extern "lean_uint16_to_uint32"]
-def UInt16.toUInt32 (a : UInt16) : UInt32 := ⟨a.val, Nat.lt_trans a.1.2 (by decide)⟩
+def UInt32.shiftRight (a b : UInt32) : UInt32 := ⟨a.toBitVec >>> (mod b 32).toBitVec⟩
 
-instance UInt32.instOfNat : OfNat UInt32 n := ⟨UInt32.ofNat n⟩
 instance : Add UInt32       := ⟨UInt32.add⟩
 instance : Sub UInt32       := ⟨UInt32.sub⟩
 instance : Mul UInt32       := ⟨UInt32.mul⟩
 instance : Mod UInt32       := ⟨UInt32.mod⟩
+
+set_option linter.deprecated false in
 instance : HMod UInt32 Nat UInt32 := ⟨UInt32.modn⟩
+
 instance : Div UInt32       := ⟨UInt32.div⟩
 
 @[extern "lean_uint32_complement"]
-def UInt32.complement (a:UInt32) : UInt32 := 0-(a+1)
+def UInt32.complement (a : UInt32) : UInt32 := ⟨~~~a.toBitVec⟩
 
 instance : Complement UInt32 := ⟨UInt32.complement⟩
 instance : AndOp UInt32     := ⟨UInt32.land⟩
@@ -208,60 +174,45 @@ instance : Xor UInt32       := ⟨UInt32.xor⟩
 instance : ShiftLeft UInt32  := ⟨UInt32.shiftLeft⟩
 instance : ShiftRight UInt32 := ⟨UInt32.shiftRight⟩
 
-@[extern "lean_uint64_of_nat"]
-def UInt64.ofNat (n : @& Nat) : UInt64 := ⟨Fin.ofNat n⟩
-abbrev Nat.toUInt64 := UInt64.ofNat
-@[extern "lean_uint64_to_nat"]
-def UInt64.toNat (n : UInt64) : Nat := n.val.val
 @[extern "lean_uint64_add"]
-def UInt64.add (a b : UInt64) : UInt64 := ⟨a.val + b.val⟩
+def UInt64.add (a b : UInt64) : UInt64 := ⟨a.toBitVec + b.toBitVec⟩
 @[extern "lean_uint64_sub"]
-def UInt64.sub (a b : UInt64) : UInt64 := ⟨a.val - b.val⟩
+def UInt64.sub (a b : UInt64) : UInt64 := ⟨a.toBitVec - b.toBitVec⟩
 @[extern "lean_uint64_mul"]
-def UInt64.mul (a b : UInt64) : UInt64 := ⟨a.val * b.val⟩
+def UInt64.mul (a b : UInt64) : UInt64 := ⟨a.toBitVec * b.toBitVec⟩
 @[extern "lean_uint64_div"]
-def UInt64.div (a b : UInt64) : UInt64 := ⟨a.val / b.val⟩
+def UInt64.div (a b : UInt64) : UInt64 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩
 @[extern "lean_uint64_mod"]
-def UInt64.mod (a b : UInt64) : UInt64 := ⟨a.val % b.val⟩
-@[extern "lean_uint64_modn"]
+def UInt64.mod (a b : UInt64) : UInt64 := ⟨BitVec.umod a.toBitVec b.toBitVec⟩
+@[extern "lean_uint64_modn", deprecated UInt64.mod (since := "2024-09-23")]
 def UInt64.modn (a : UInt64) (n : @& Nat) : UInt64 := ⟨Fin.modn a.val n⟩
 @[extern "lean_uint64_land"]
-def UInt64.land (a b : UInt64) : UInt64 := ⟨Fin.land a.val b.val⟩
+def UInt64.land (a b : UInt64) : UInt64 := ⟨a.toBitVec &&& b.toBitVec⟩
 @[extern "lean_uint64_lor"]
-def UInt64.lor (a b : UInt64) : UInt64 := ⟨Fin.lor a.val b.val⟩
+def UInt64.lor (a b : UInt64) : UInt64 := ⟨a.toBitVec ||| b.toBitVec⟩
 @[extern "lean_uint64_xor"]
-def UInt64.xor (a b : UInt64) : UInt64 := ⟨Fin.xor a.val b.val⟩
+def UInt64.xor (a b : UInt64) : UInt64 := ⟨a.toBitVec ^^^ b.toBitVec⟩
 @[extern "lean_uint64_shift_left"]
-def UInt64.shiftLeft (a b : UInt64) : UInt64 := ⟨a.val <<< (modn b 64).val⟩
+def UInt64.shiftLeft (a b : UInt64) : UInt64 := ⟨a.toBitVec <<< (mod b 64).toBitVec⟩
 @[extern "lean_uint64_shift_right"]
-def UInt64.shiftRight (a b : UInt64) : UInt64 := ⟨a.val >>> (modn b 64).val⟩
-def UInt64.lt (a b : UInt64) : Prop := a.val < b.val
-def UInt64.le (a b : UInt64) : Prop := a.val ≤ b.val
-@[extern "lean_uint64_to_uint8"]
-def UInt64.toUInt8 (a : UInt64) : UInt8 := a.toNat.toUInt8
-@[extern "lean_uint64_to_uint16"]
-def UInt64.toUInt16 (a : UInt64) : UInt16 := a.toNat.toUInt16
-@[extern "lean_uint64_to_uint32"]
-def UInt64.toUInt32 (a : UInt64) : UInt32 := a.toNat.toUInt32
-@[extern "lean_uint8_to_uint64"]
-def UInt8.toUInt64 (a : UInt8) : UInt64 := ⟨a.val, Nat.lt_trans a.1.2 (by decide)⟩
-@[extern "lean_uint16_to_uint64"]
-def UInt16.toUInt64 (a : UInt16) : UInt64 := ⟨a.val, Nat.lt_trans a.1.2 (by decide)⟩
-@[extern "lean_uint32_to_uint64"]
-def UInt32.toUInt64 (a : UInt32) : UInt64 := ⟨a.val, Nat.lt_trans a.1.2 (by decide)⟩
+def UInt64.shiftRight (a b : UInt64) : UInt64 := ⟨a.toBitVec >>> (mod b 64).toBitVec⟩
+def UInt64.lt (a b : UInt64) : Prop := a.toBitVec < b.toBitVec
+def UInt64.le (a b : UInt64) : Prop := a.toBitVec ≤ b.toBitVec
 
-instance UInt64.instOfNat : OfNat UInt64 n := ⟨UInt64.ofNat n⟩
 instance : Add UInt64       := ⟨UInt64.add⟩
 instance : Sub UInt64       := ⟨UInt64.sub⟩
 instance : Mul UInt64       := ⟨UInt64.mul⟩
 instance : Mod UInt64       := ⟨UInt64.mod⟩
+
+set_option linter.deprecated false in
 instance : HMod UInt64 Nat UInt64 := ⟨UInt64.modn⟩
+
 instance : Div UInt64       := ⟨UInt64.div⟩
 instance : LT UInt64        := ⟨UInt64.lt⟩
 instance : LE UInt64        := ⟨UInt64.le⟩
 
 @[extern "lean_uint64_complement"]
-def UInt64.complement (a:UInt64) : UInt64 := 0-(a+1)
+def UInt64.complement (a : UInt64) : UInt64 := ⟨~~~a.toBitVec⟩
 
 instance : Complement UInt64 := ⟨UInt64.complement⟩
 instance : AndOp UInt64     := ⟨UInt64.land⟩
@@ -273,79 +224,52 @@ instance : ShiftRight UInt64 := ⟨UInt64.shiftRight⟩
 @[extern "lean_bool_to_uint64"]
 def Bool.toUInt64 (b : Bool) : UInt64 := if b then 1 else 0
 
-set_option bootstrap.genMatcherCode false in
 @[extern "lean_uint64_dec_lt"]
 def UInt64.decLt (a b : UInt64) : Decidable (a < b) :=
-  match a, b with
-  | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n < m))
+  inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))
 
-set_option bootstrap.genMatcherCode false in
 @[extern "lean_uint64_dec_le"]
 def UInt64.decLe (a b : UInt64) : Decidable (a ≤ b) :=
-  match a, b with
-  | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n <= m))
+  inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))
 
 instance (a b : UInt64) : Decidable (a < b) := UInt64.decLt a b
 instance (a b : UInt64) : Decidable (a ≤ b) := UInt64.decLe a b
 instance : Max UInt64 := maxOfLe
 instance : Min UInt64 := minOfLe
 
--- This instance would interfere with the global instance `NeZero (n + 1)`,
--- so we only enable it locally.
-@[local instance]
-private def instNeZeroUSizeSize : NeZero USize.size := ⟨add_one_ne_zero _⟩
-
-@[deprecated (since := "2024-09-16")]
-theorem usize_size_gt_zero : USize.size > 0 :=
-  Nat.zero_lt_succ ..
-
-@[extern "lean_usize_of_nat"]
-def USize.ofNat (n : @& Nat) : USize := ⟨Fin.ofNat'  _ n⟩
-abbrev Nat.toUSize := USize.ofNat
-@[extern "lean_usize_to_nat"]
-def USize.toNat (n : USize) : Nat := n.val.val
-@[extern "lean_usize_add"]
-def USize.add (a b : USize) : USize := ⟨a.val + b.val⟩
-@[extern "lean_usize_sub"]
-def USize.sub (a b : USize) : USize := ⟨a.val - b.val⟩
 @[extern "lean_usize_mul"]
-def USize.mul (a b : USize) : USize := ⟨a.val * b.val⟩
+def USize.mul (a b : USize) : USize := ⟨a.toBitVec * b.toBitVec⟩
 @[extern "lean_usize_div"]
-def USize.div (a b : USize) : USize := ⟨a.val / b.val⟩
+def USize.div (a b : USize) : USize := ⟨a.toBitVec / b.toBitVec⟩
 @[extern "lean_usize_mod"]
-def USize.mod (a b : USize) : USize := ⟨a.val % b.val⟩
-@[extern "lean_usize_modn"]
+def USize.mod (a b : USize) : USize := ⟨a.toBitVec % b.toBitVec⟩
+@[extern "lean_usize_modn", deprecated USize.mod (since := "2024-09-23")]
 def USize.modn (a : USize) (n : @& Nat) : USize := ⟨Fin.modn a.val n⟩
 @[extern "lean_usize_land"]
-def USize.land (a b : USize) : USize := ⟨Fin.land a.val b.val⟩
+def USize.land (a b : USize) : USize := ⟨a.toBitVec &&& b.toBitVec⟩
 @[extern "lean_usize_lor"]
-def USize.lor (a b : USize) : USize := ⟨Fin.lor a.val b.val⟩
+def USize.lor (a b : USize) : USize := ⟨a.toBitVec ||| b.toBitVec⟩
 @[extern "lean_usize_xor"]
-def USize.xor (a b : USize) : USize := ⟨Fin.xor a.val b.val⟩
+def USize.xor (a b : USize) : USize := ⟨a.toBitVec ^^^ b.toBitVec⟩
 @[extern "lean_usize_shift_left"]
-def USize.shiftLeft (a b : USize) : USize := ⟨a.val <<< (modn b System.Platform.numBits).val⟩
+def USize.shiftLeft (a b : USize) : USize := ⟨a.toBitVec <<< (mod b (USize.ofNat System.Platform.numBits)).toBitVec⟩
 @[extern "lean_usize_shift_right"]
-def USize.shiftRight (a b : USize) : USize := ⟨a.val >>> (modn b System.Platform.numBits).val⟩
+def USize.shiftRight (a b : USize) : USize := ⟨a.toBitVec >>> (mod b (USize.ofNat System.Platform.numBits)).toBitVec⟩
 @[extern "lean_uint32_to_usize"]
-def UInt32.toUSize (a : UInt32) : USize := USize.ofNat32 a.val a.1.2
+def UInt32.toUSize (a : UInt32) : USize := USize.ofNat32 a.toBitVec.toNat a.toBitVec.isLt
 @[extern "lean_usize_to_uint32"]
 def USize.toUInt32 (a : USize) : UInt32 := a.toNat.toUInt32
 
-def USize.lt (a b : USize) : Prop := a.val < b.val
-def USize.le (a b : USize) : Prop := a.val ≤ b.val
-
-instance USize.instOfNat : OfNat USize n := ⟨USize.ofNat n⟩
-instance : Add USize       := ⟨USize.add⟩
-instance : Sub USize       := ⟨USize.sub⟩
 instance : Mul USize       := ⟨USize.mul⟩
 instance : Mod USize       := ⟨USize.mod⟩
+
+set_option linter.deprecated false in
 instance : HMod USize Nat USize := ⟨USize.modn⟩
+
 instance : Div USize       := ⟨USize.div⟩
-instance : LT USize        := ⟨USize.lt⟩
-instance : LE USize        := ⟨USize.le⟩
 
 @[extern "lean_usize_complement"]
-def USize.complement (a:USize) : USize := 0-(a+1)
+def USize.complement (a : USize) : USize := ⟨~~~a.toBitVec⟩
 
 instance : Complement USize := ⟨USize.complement⟩
 instance : AndOp USize      := ⟨USize.land⟩
@@ -354,19 +278,5 @@ instance : Xor USize        := ⟨USize.xor⟩
 instance : ShiftLeft USize  := ⟨USize.shiftLeft⟩
 instance : ShiftRight USize := ⟨USize.shiftRight⟩
 
-set_option bootstrap.genMatcherCode false in
-@[extern "lean_usize_dec_lt"]
-def USize.decLt (a b : USize) : Decidable (a < b) :=
-  match a, b with
-  | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n < m))
-
-set_option bootstrap.genMatcherCode false in
-@[extern "lean_usize_dec_le"]
-def USize.decLe (a b : USize) : Decidable (a ≤ b) :=
-  match a, b with
-  | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n <= m))
-
-instance (a b : USize) : Decidable (a < b) := USize.decLt a b
-instance (a b : USize) : Decidable (a ≤ b) := USize.decLe a b
 instance : Max USize := maxOfLe
 instance : Min USize := minOfLe

src/Init/Data/UInt/BasicAux.lean

@@ -0,0 +1,132 @@
+/-
+Copyright (c) 2018 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Data.Fin.Basic
+import Init.Data.BitVec.BasicAux
+
+/-!
+This module exists to provide the very basic `UInt8` etc. definitions required for
+`Init.Data.Char.Basic` and `Init.Data.Array.Basic`. These are very important as they are used in
+meta code that is then (transitively) used in `Init.Data.UInt.Basic` and `Init.Data.BitVec.Basic`.
+This file thus breaks the import cycle that would be created by this dependency.
+-/
+
+open Nat
+
+def UInt8.val (x : UInt8) : Fin UInt8.size := x.toBitVec.toFin
+@[extern "lean_uint8_of_nat"]
+def UInt8.ofNat (n : @& Nat) : UInt8 := ⟨BitVec.ofNat 8 n⟩
+abbrev Nat.toUInt8 := UInt8.ofNat
+@[extern "lean_uint8_to_nat"]
+def UInt8.toNat (n : UInt8) : Nat := n.toBitVec.toNat
+
+instance UInt8.instOfNat : OfNat UInt8 n := ⟨UInt8.ofNat n⟩
+
+def UInt16.val (x : UInt16) : Fin UInt16.size := x.toBitVec.toFin
+@[extern "lean_uint16_of_nat"]
+def UInt16.ofNat (n : @& Nat) : UInt16 := ⟨BitVec.ofNat 16 n⟩
+abbrev Nat.toUInt16 := UInt16.ofNat
+@[extern "lean_uint16_to_nat"]
+def UInt16.toNat (n : UInt16) : Nat := n.toBitVec.toNat
+@[extern "lean_uint16_to_uint8"]
+def UInt16.toUInt8 (a : UInt16) : UInt8 := a.toNat.toUInt8
+@[extern "lean_uint8_to_uint16"]
+def UInt8.toUInt16 (a : UInt8) : UInt16 := ⟨⟨a.toNat, Nat.lt_trans a.toBitVec.isLt (by decide)⟩⟩
+
+instance UInt16.instOfNat : OfNat UInt16 n := ⟨UInt16.ofNat n⟩
+
+def UInt32.val (x : UInt32) : Fin UInt32.size := x.toBitVec.toFin
+@[extern "lean_uint32_of_nat"]
+def UInt32.ofNat (n : @& Nat) : UInt32 := ⟨BitVec.ofNat 32 n⟩
+@[extern "lean_uint32_of_nat"]
+def UInt32.ofNat' (n : Nat) (h : n < UInt32.size) : UInt32 := ⟨BitVec.ofNatLt n h⟩
+/--
+Converts the given natural number to `UInt32`, but returns `2^32 - 1` for natural numbers `>= 2^32`.
+-/
+def UInt32.ofNatTruncate (n : Nat) : UInt32 :=
+  if h : n < UInt32.size then
+    UInt32.ofNat' n h
+  else
+    UInt32.ofNat' (UInt32.size - 1) (by decide)
+abbrev Nat.toUInt32 := UInt32.ofNat
+@[extern "lean_uint32_to_uint8"]
+def UInt32.toUInt8 (a : UInt32) : UInt8 := a.toNat.toUInt8
+@[extern "lean_uint32_to_uint16"]
+def UInt32.toUInt16 (a : UInt32) : UInt16 := a.toNat.toUInt16
+@[extern "lean_uint8_to_uint32"]
+def UInt8.toUInt32 (a : UInt8) : UInt32 := ⟨⟨a.toNat, Nat.lt_trans a.toBitVec.isLt (by decide)⟩⟩
+@[extern "lean_uint16_to_uint32"]
+def UInt16.toUInt32 (a : UInt16) : UInt32 := ⟨⟨a.toNat, Nat.lt_trans a.toBitVec.isLt (by decide)⟩⟩
+
+instance UInt32.instOfNat : OfNat UInt32 n := ⟨UInt32.ofNat n⟩
+
+theorem UInt32.ofNat'_lt_of_lt {n m : Nat} (h1 : n < UInt32.size) (h2 : m < UInt32.size) :
+     n < m → UInt32.ofNat' n h1 < UInt32.ofNat m := by
+  simp only [(· < ·), BitVec.toNat, ofNat', BitVec.ofNatLt, ofNat, BitVec.ofNat, Fin.ofNat',
+    Nat.mod_eq_of_lt h2, imp_self]
+
+theorem UInt32.lt_ofNat'_of_lt {n m : Nat} (h1 : n < UInt32.size) (h2 : m < UInt32.size) :
+     m < n → UInt32.ofNat m < UInt32.ofNat' n h1  := by
+  simp only [(· < ·), BitVec.toNat, ofNat', BitVec.ofNatLt, ofNat, BitVec.ofNat, Fin.ofNat',
+    Nat.mod_eq_of_lt h2, imp_self]
+
+def UInt64.val (x : UInt64) : Fin UInt64.size := x.toBitVec.toFin
+@[extern "lean_uint64_of_nat"]
+def UInt64.ofNat (n : @& Nat) : UInt64 := ⟨BitVec.ofNat 64 n⟩
+abbrev Nat.toUInt64 := UInt64.ofNat
+@[extern "lean_uint64_to_nat"]
+def UInt64.toNat (n : UInt64) : Nat := n.toBitVec.toNat
+@[extern "lean_uint64_to_uint8"]
+def UInt64.toUInt8 (a : UInt64) : UInt8 := a.toNat.toUInt8
+@[extern "lean_uint64_to_uint16"]
+def UInt64.toUInt16 (a : UInt64) : UInt16 := a.toNat.toUInt16
+@[extern "lean_uint64_to_uint32"]
+def UInt64.toUInt32 (a : UInt64) : UInt32 := a.toNat.toUInt32
+@[extern "lean_uint8_to_uint64"]
+def UInt8.toUInt64 (a : UInt8) : UInt64 := ⟨⟨a.toNat, Nat.lt_trans a.toBitVec.isLt (by decide)⟩⟩
+@[extern "lean_uint16_to_uint64"]
+def UInt16.toUInt64 (a : UInt16) : UInt64 := ⟨⟨a.toNat, Nat.lt_trans a.toBitVec.isLt (by decide)⟩⟩
+@[extern "lean_uint32_to_uint64"]
+def UInt32.toUInt64 (a : UInt32) : UInt64 := ⟨⟨a.toNat, Nat.lt_trans a.toBitVec.isLt (by decide)⟩⟩
+
+instance UInt64.instOfNat : OfNat UInt64 n := ⟨UInt64.ofNat n⟩
+
+theorem usize_size_gt_zero : USize.size > 0 := by
+  cases usize_size_eq with
+  | inl h => rw [h]; decide
+  | inr h => rw [h]; decide
+
+def USize.val (x : USize) : Fin USize.size := x.toBitVec.toFin
+@[extern "lean_usize_of_nat"]
+def USize.ofNat (n : @& Nat) : USize := ⟨BitVec.ofNat _ n⟩
+abbrev Nat.toUSize := USize.ofNat
+@[extern "lean_usize_to_nat"]
+def USize.toNat (n : USize) : Nat := n.toBitVec.toNat
+@[extern "lean_usize_add"]
+def USize.add (a b : USize) : USize := ⟨a.toBitVec + b.toBitVec⟩
+@[extern "lean_usize_sub"]
+def USize.sub (a b : USize) : USize := ⟨a.toBitVec - b.toBitVec⟩
+
+def USize.lt (a b : USize) : Prop := a.toBitVec < b.toBitVec
+def USize.le (a b : USize) : Prop := a.toBitVec ≤ b.toBitVec
+
+instance USize.instOfNat : OfNat USize n := ⟨USize.ofNat n⟩
+
+instance : Add USize       := ⟨USize.add⟩
+instance : Sub USize       := ⟨USize.sub⟩
+instance : LT USize        := ⟨USize.lt⟩
+instance : LE USize        := ⟨USize.le⟩
+
+@[extern "lean_usize_dec_lt"]
+def USize.decLt (a b : USize) : Decidable (a < b) :=
+  inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))
+
+@[extern "lean_usize_dec_le"]
+def USize.decLe (a b : USize) : Decidable (a ≤ b) :=
+  inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))
+
+instance (a b : USize) : Decidable (a < b) := USize.decLt a b
+instance (a b : USize) : Decidable (a ≤ b) := USize.decLe a b

src/Init/Data/UInt/Bitwise.lean

@@ -6,13 +6,14 @@ Authors: Markus Himmel
 prelude
 import Init.Data.UInt.Basic
 import Init.Data.Fin.Bitwise
+import Init.Data.BitVec.Lemmas
 
 set_option hygiene false in
 macro "declare_bitwise_uint_theorems" typeName:ident : command =>
 `(
 namespace $typeName
 
-@[simp] protected theorem and_toNat (a b : $typeName) : (a &&& b).toNat = a.toNat &&& b.toNat := Fin.and_val ..
+@[simp] protected theorem and_toNat (a b : $typeName) : (a &&& b).toNat = a.toNat &&& b.toNat := BitVec.toNat_and ..
 
 end $typeName
 )

src/Init/Data/UInt/Lemmas.lean

@@ -6,6 +6,8 @@ Authors: Leonardo de Moura
 prelude
 import Init.Data.UInt.Basic
 import Init.Data.Fin.Lemmas
+import Init.Data.BitVec.Lemmas
+import Init.Data.BitVec.Bitblast
 
 set_option hygiene false in
 macro "declare_uint_theorems" typeName:ident : command =>
@@ -17,50 +19,111 @@ instance : Inhabited $typeName where
 
 theorem zero_def : (0 : $typeName) = ⟨0⟩ := rfl
 theorem one_def : (1 : $typeName) = ⟨1⟩ := rfl
-theorem sub_def (a b : $typeName) : a - b = ⟨a.val - b.val⟩ := rfl
-theorem mul_def (a b : $typeName) : a * b = ⟨a.val * b.val⟩ := rfl
-theorem mod_def (a b : $typeName) : a % b = ⟨a.val % b.val⟩ := rfl
-theorem add_def (a b : $typeName) : a + b = ⟨a.val + b.val⟩ := rfl
+theorem sub_def (a b : $typeName) : a - b = ⟨a.toBitVec - b.toBitVec⟩ := rfl
+theorem mul_def (a b : $typeName) : a * b = ⟨a.toBitVec * b.toBitVec⟩ := rfl
+theorem mod_def (a b : $typeName) : a % b = ⟨a.toBitVec % b.toBitVec⟩ := rfl
+theorem add_def (a b : $typeName) : a + b = ⟨a.toBitVec + b.toBitVec⟩ := rfl
 
-@[simp] theorem mk_val_eq : ∀ (a : $typeName), mk a.val = a
+@[simp] theorem mk_toBitVec_eq : ∀ (a : $typeName), mk a.toBitVec = a
   | ⟨_, _⟩ => rfl
-theorem val_eq_of_lt {a : Nat} : a < size → ((ofNat a).val : Nat) = a :=
-  Nat.mod_eq_of_lt
-theorem toNat_ofNat_of_lt {n : Nat} (h : n < size) : (ofNat n).toNat = n := by
-  rw [toNat, val_eq_of_lt h]
 
-theorem le_def {a b : $typeName} : a ≤ b ↔ a.1 ≤ b.1 := .rfl
-theorem lt_def {a b : $typeName} : a < b ↔ a.1 < b.1 := .rfl
-theorem lt_iff_val_lt_val {a b : $typeName} : a < b ↔ a.val < b.val := .rfl
-@[simp] protected theorem not_le {a b : $typeName} : ¬ a ≤ b ↔ b < a := Fin.not_le
-@[simp] protected theorem not_lt {a b : $typeName} : ¬ a < b ↔ b ≤ a := Fin.not_lt
+theorem toBitVec_eq_of_lt {a : Nat} : a < size → (ofNat a).toBitVec.toNat = a :=
+  Nat.mod_eq_of_lt
+
+theorem toNat_ofNat_of_lt {n : Nat} (h : n < size) : (ofNat n).toNat = n := by
+  rw [toNat, toBitVec_eq_of_lt h]
+
+theorem le_def {a b : $typeName} : a ≤ b ↔ a.toBitVec ≤ b.toBitVec := .rfl
+
+theorem lt_def {a b : $typeName} : a < b ↔ a.toBitVec < b.toBitVec := .rfl
+
+@[simp] protected theorem not_le {a b : $typeName} : ¬ a ≤ b ↔ b < a := by simp [le_def, lt_def]
+
+@[simp] protected theorem not_lt {a b : $typeName} : ¬ a < b ↔ b ≤ a := by simp [le_def, lt_def]
+
 @[simp] protected theorem le_refl (a : $typeName) : a ≤ a := by simp [le_def]
+
 @[simp] protected theorem lt_irrefl (a : $typeName) : ¬ a < a := by simp
-protected theorem le_trans {a b c : $typeName} : a ≤ b → b ≤ c → a ≤ c := Fin.le_trans
-protected theorem lt_trans {a b c : $typeName} : a < b → b < c → a < c := Fin.lt_trans
-protected theorem le_total (a b : $typeName) : a ≤ b ∨ b ≤ a := Fin.le_total a.1 b.1
-protected theorem lt_asymm {a b : $typeName} (h : a < b) : ¬ b < a := Fin.lt_asymm h
-protected theorem val_eq_of_eq {a b : $typeName} (h : a = b) : a.val = b.val := h ▸ rfl
-protected theorem eq_of_val_eq {a b : $typeName} (h : a.val = b.val) : a = b := by cases a; cases b; simp at h; simp [h]
-open $typeName (val_eq_of_eq) in
-protected theorem ne_of_val_ne {a b : $typeName} (h : a.val ≠ b.val) : a ≠ b := fun h' => absurd (val_eq_of_eq h') h
-open $typeName (ne_of_val_ne) in
-protected theorem ne_of_lt {a b : $typeName} (h : a < b) : a ≠ b := ne_of_val_ne (Fin.ne_of_lt h)
+
+protected theorem le_trans {a b c : $typeName} : a ≤ b → b ≤ c → a ≤ c := BitVec.le_trans
+
+protected theorem lt_trans {a b c : $typeName} : a < b → b < c → a < c := BitVec.lt_trans
+
+protected theorem le_total (a b : $typeName) : a ≤ b ∨ b ≤ a := BitVec.le_total ..
+
+protected theorem lt_asymm {a b : $typeName} : a < b → ¬ b < a := BitVec.lt_asymm
+
+protected theorem toBitVec_eq_of_eq {a b : $typeName} (h : a = b) : a.toBitVec = b.toBitVec := h ▸ rfl
+
+protected theorem eq_of_toBitVec_eq {a b : $typeName} (h : a.toBitVec = b.toBitVec) : a = b := by
+  cases a; cases b; simp_all
+
+open $typeName (eq_of_toBitVec_eq) in
+protected theorem eq_of_val_eq {a b : $typeName} (h : a.val = b.val) : a = b := by
+  rcases a with ⟨⟨_⟩⟩; rcases b with ⟨⟨_⟩⟩; simp_all [val]
+
+open $typeName (toBitVec_eq_of_eq) in
+protected theorem ne_of_toBitVec_ne {a b : $typeName} (h : a.toBitVec ≠ b.toBitVec) : a ≠ b :=
+  fun h' => absurd (toBitVec_eq_of_eq h') h
+
+open $typeName (ne_of_toBitVec_ne) in
+protected theorem ne_of_lt {a b : $typeName} (h : a < b) : a ≠ b := by
+  apply ne_of_toBitVec_ne
+  apply BitVec.ne_of_lt
+  simpa [lt_def] using h
 
 @[simp] protected theorem toNat_zero : (0 : $typeName).toNat = 0 := Nat.zero_mod _
-@[simp] protected theorem toNat_mod (a b : $typeName) : (a % b).toNat = a.toNat % b.toNat := Fin.mod_val ..
-@[simp] protected theorem toNat_div (a b : $typeName) : (a / b).toNat = a.toNat / b.toNat := Fin.div_val ..
-@[simp] protected theorem toNat_sub_of_le (a b : $typeName) : b ≤ a → (a - b).toNat = a.toNat - b.toNat := Fin.sub_val_of_le
-@[simp] protected theorem toNat_modn (a : $typeName) (b : Nat) : (a.modn b).toNat = a.toNat % b := Fin.modn_val ..
-protected theorem modn_lt {m : Nat} : ∀ (u : $typeName), m > 0 → toNat (u % m) < m
-  | ⟨u⟩, h => Fin.modn_lt u h
-open $typeName (modn_lt) in
-protected theorem mod_lt (a b : $typeName) (h : 0 < b) : a % b < b := modn_lt _ (by simp [lt_def] at h; exact h)
+
+@[simp] protected theorem toNat_mod (a b : $typeName) : (a % b).toNat = a.toNat % b.toNat := BitVec.toNat_umod ..
+
+@[simp] protected theorem toNat_div (a b : $typeName) : (a / b).toNat = a.toNat / b.toNat := BitVec.toNat_udiv  ..
+
+@[simp] protected theorem toNat_sub_of_le (a b : $typeName) : b ≤ a → (a - b).toNat = a.toNat - b.toNat := BitVec.toNat_sub_of_le
+
+protected theorem toNat_lt_size (a : $typeName) : a.toNat < size := a.toBitVec.isLt
+
+open $typeName (toNat_mod toNat_lt_size) in
+protected theorem toNat_mod_lt {m : Nat} : ∀ (u : $typeName), m > 0 → toNat (u % ofNat m) < m := by
+  intro u h1
+  by_cases h2 : m < size
+  · rw [toNat_mod, toNat_ofNat_of_lt h2]
+    apply Nat.mod_lt _ h1
+  · apply Nat.lt_of_lt_of_le
+    · apply toNat_lt_size
+    · simpa using h2
+
+open $typeName (toNat_mod_lt) in
+set_option linter.deprecated false in
+@[deprecated toNat_mod_lt (since := "2024-09-24")]
+protected theorem modn_lt {m : Nat} : ∀ (u : $typeName), m > 0 → toNat (u % m) < m := by
+  intro u
+  simp only [(· % ·)]
+  simp only [gt_iff_lt, toNat, modn, Fin.modn_val, BitVec.natCast_eq_ofNat, BitVec.toNat_ofNat,
+    Nat.reducePow]
+  rw [Nat.mod_eq_of_lt]
+  · apply Nat.mod_lt
+  · apply Nat.lt_of_le_of_lt
+    · apply Nat.mod_le
+    · apply Fin.is_lt
+
+protected theorem mod_lt (a : $typeName) {b : $typeName} : 0 < b → a % b < b := by
+  simp only [lt_def, mod_def]
+  apply BitVec.umod_lt
+
 protected theorem toNat.inj : ∀ {a b : $typeName}, a.toNat = b.toNat → a = b
   | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
-protected theorem toNat_lt_size (a : $typeName) : a.toNat < size := a.1.2
+
 @[simp] protected theorem ofNat_one : ofNat 1 = 1 := rfl
 
+@[simp]
+theorem val_ofNat (n : Nat) : val (no_index (OfNat.ofNat n)) = OfNat.ofNat n := rfl
+
+@[simp]
+theorem toBitVec_ofNat (n : Nat) : toBitVec (no_index (OfNat.ofNat n)) = BitVec.ofNat _ n := rfl
+
+@[simp]
+theorem mk_ofNat (n : Nat) : mk (BitVec.ofNat _ n) = OfNat.ofNat n := rfl
+
 end $typeName
 )
 
@@ -70,27 +133,34 @@ declare_uint_theorems UInt32
 declare_uint_theorems UInt64
 declare_uint_theorems USize
 
+theorem UInt32.toNat_lt_of_lt {n : UInt32} {m : Nat} (h : m < size) : n < ofNat m → n.toNat < m := by
+  simp [lt_def, BitVec.lt_def, UInt32.toNat, toBitVec_eq_of_lt h]
+
+theorem UInt32.lt_toNat_of_lt {n : UInt32} {m : Nat} (h : m < size) : ofNat m < n → m < n.toNat := by
+  simp [lt_def, BitVec.lt_def, UInt32.toNat, toBitVec_eq_of_lt h]
+
+theorem UInt32.toNat_le_of_le {n : UInt32} {m : Nat} (h : m < size) : n ≤ ofNat m → n.toNat ≤ m := by
+  simp [le_def, BitVec.le_def, UInt32.toNat, toBitVec_eq_of_lt h]
+
+theorem UInt32.le_toNat_of_le {n : UInt32} {m : Nat} (h : m < size) : ofNat m ≤ n → m ≤ n.toNat := by
+  simp [le_def, BitVec.le_def, UInt32.toNat, toBitVec_eq_of_lt h]
+
 @[deprecated (since := "2024-06-23")] protected abbrev UInt8.zero_toNat := @UInt8.toNat_zero
 @[deprecated (since := "2024-06-23")] protected abbrev UInt8.div_toNat := @UInt8.toNat_div
 @[deprecated (since := "2024-06-23")] protected abbrev UInt8.mod_toNat := @UInt8.toNat_mod
-@[deprecated (since := "2024-06-23")] protected abbrev UInt8.modn_toNat := @UInt8.toNat_modn
 
 @[deprecated (since := "2024-06-23")] protected abbrev UInt16.zero_toNat := @UInt16.toNat_zero
 @[deprecated (since := "2024-06-23")] protected abbrev UInt16.div_toNat := @UInt16.toNat_div
 @[deprecated (since := "2024-06-23")] protected abbrev UInt16.mod_toNat := @UInt16.toNat_mod
-@[deprecated (since := "2024-06-23")] protected abbrev UInt16.modn_toNat := @UInt16.toNat_modn
 
 @[deprecated (since := "2024-06-23")] protected abbrev UInt32.zero_toNat := @UInt32.toNat_zero
 @[deprecated (since := "2024-06-23")] protected abbrev UInt32.div_toNat := @UInt32.toNat_div
 @[deprecated (since := "2024-06-23")] protected abbrev UInt32.mod_toNat := @UInt32.toNat_mod
-@[deprecated (since := "2024-06-23")] protected abbrev UInt32.modn_toNat := @UInt32.toNat_modn
 
 @[deprecated (since := "2024-06-23")] protected abbrev UInt64.zero_toNat := @UInt64.toNat_zero
 @[deprecated (since := "2024-06-23")] protected abbrev UInt64.div_toNat := @UInt64.toNat_div
 @[deprecated (since := "2024-06-23")] protected abbrev UInt64.mod_toNat := @UInt64.toNat_mod
-@[deprecated (since := "2024-06-23")] protected abbrev UInt64.modn_toNat := @UInt64.toNat_modn
 
 @[deprecated (since := "2024-06-23")] protected abbrev USize.zero_toNat := @USize.toNat_zero
 @[deprecated (since := "2024-06-23")] protected abbrev USize.div_toNat := @USize.toNat_div
 @[deprecated (since := "2024-06-23")] protected abbrev USize.mod_toNat := @USize.toNat_mod
-@[deprecated (since := "2024-06-23")] protected abbrev USize.modn_toNat := @USize.toNat_modn

src/Init/Data/UInt/Log2.lean

@@ -7,16 +7,16 @@ prelude
 import Init.Data.Fin.Log2
 
 @[extern "lean_uint8_log2"]
-def UInt8.log2 (a : UInt8) : UInt8 := ⟨Fin.log2 a.val⟩
+def UInt8.log2 (a : UInt8) : UInt8 := ⟨⟨Fin.log2 a.val⟩⟩
 
 @[extern "lean_uint16_log2"]
-def UInt16.log2 (a : UInt16) : UInt16 := ⟨Fin.log2 a.val⟩
+def UInt16.log2 (a : UInt16) : UInt16 := ⟨⟨Fin.log2 a.val⟩⟩
 
 @[extern "lean_uint32_log2"]
-def UInt32.log2 (a : UInt32) : UInt32 := ⟨Fin.log2 a.val⟩
+def UInt32.log2 (a : UInt32) : UInt32 := ⟨⟨Fin.log2 a.val⟩⟩
 
 @[extern "lean_uint64_log2"]
-def UInt64.log2 (a : UInt64) : UInt64 := ⟨Fin.log2 a.val⟩
+def UInt64.log2 (a : UInt64) : UInt64 := ⟨⟨Fin.log2 a.val⟩⟩
 
 @[extern "lean_usize_log2"]
-def USize.log2 (a : USize) : USize := ⟨Fin.log2 a.val⟩
+def USize.log2 (a : USize) : USize := ⟨⟨Fin.log2 a.val⟩⟩

src/Init/Prelude.lean

@@ -1592,9 +1592,6 @@ def Nat.beq : (@& Nat) → (@& Nat) → Bool
   | succ _, zero   => false
   | succ n, succ m => beq n m
 
-instance : BEq Nat where
-  beq := Nat.beq
-
 theorem Nat.eq_of_beq_eq_true : {n m : Nat} → Eq (beq n m) true → Eq n m
   | zero,   zero,   _ => rfl
   | zero,   succ _, h => Bool.noConfusion h
@@ -1869,6 +1866,52 @@ 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 ..
 
+/--
+A bitvector of the specified width.
+
+This is represented as the underlying `Nat` number in both the runtime
+and the kernel, inheriting all the special support for `Nat`.
+-/
+structure BitVec (w : Nat) where
+  /-- Construct a `BitVec w` from a number less than `2^w`.
+  O(1), because we use `Fin` as the internal representation of a bitvector. -/
+  ofFin ::
+  /-- Interpret a bitvector as a number less than `2^w`.
+  O(1), because we use `Fin` as the internal representation of a bitvector. -/
+  toFin : Fin (hPow 2 w)
+
+/--
+Bitvectors have decidable equality. This should be used via the instance `DecidableEq (BitVec n)`.
+-/
+-- We manually derive the `DecidableEq` instances for `BitVec` because
+-- we want to have builtin support for bit-vector literals, and we
+-- need a name for this function to implement `canUnfoldAtMatcher` at `WHNF.lean`.
+def BitVec.decEq (x y : BitVec n) : Decidable (Eq x y) :=
+  match x, y with
+  | ⟨n⟩, ⟨m⟩ =>
+    dite (Eq n m)
+      (fun h => isTrue (h ▸ rfl))
+      (fun h => isFalse (fun h' => BitVec.noConfusion h' (fun h' => absurd h' h)))
+
+instance : DecidableEq (BitVec n) := BitVec.decEq
+
+/-- The `BitVec` with value `i`, given a proof that `i < 2^n`. -/
+@[match_pattern]
+protected def BitVec.ofNatLt {n : Nat} (i : Nat) (p : LT.lt i (hPow 2 n)) : BitVec n where
+  toFin := ⟨i, p⟩
+
+/-- Given a bitvector `x`, return the underlying `Nat`. This is O(1) because `BitVec` is a
+(zero-cost) wrapper around a `Nat`. -/
+protected def BitVec.toNat (x : BitVec n) : Nat := x.toFin.val
+
+instance : LT (BitVec n) where lt := (LT.lt ·.toNat ·.toNat)
+instance (x y : BitVec n) : Decidable (LT.lt x y) :=
+  inferInstanceAs (Decidable (LT.lt x.toNat y.toNat))
+
+instance : LE (BitVec n) where le := (LE.le ·.toNat ·.toNat)
+instance (x y : BitVec n) : Decidable (LE.le x y) :=
+  inferInstanceAs (Decidable (LE.le x.toNat y.toNat))
+
 /-- The size of type `UInt8`, that is, `2^8 = 256`. -/
 abbrev UInt8.size : Nat := 256
 
@@ -1877,12 +1920,12 @@ The type of unsigned 8-bit integers. This type has special support in the
 compiler to make it actually 8 bits rather than wrapping a `Nat`.
 -/
 structure UInt8 where
-  /-- Unpack a `UInt8` as a `Nat` less than `2^8`.
+  /-- Unpack a `UInt8` as a `BitVec 8`.
   This function is overridden with a native implementation. -/
-  val : Fin UInt8.size
+  toBitVec : BitVec 8
 
 attribute [extern "lean_uint8_of_nat_mk"] UInt8.mk
-attribute [extern "lean_uint8_to_nat"] UInt8.val
+attribute [extern "lean_uint8_to_nat"] UInt8.toBitVec
 
 /--
 Pack a `Nat` less than `2^8` into a `UInt8`.
@@ -1890,7 +1933,7 @@ This function is overridden with a native implementation.
 -/
 @[extern "lean_uint8_of_nat"]
 def UInt8.ofNatCore (n : @& Nat) (h : LT.lt n UInt8.size) : UInt8 where
-  val := { val := n, isLt := h }
+  toBitVec := BitVec.ofNatLt n h
 
 set_option bootstrap.genMatcherCode false in
 /--
@@ -1901,7 +1944,9 @@ This function is overridden with a native implementation.
 def UInt8.decEq (a b : UInt8) : Decidable (Eq a b) :=
   match a, b with
   | ⟨n⟩, ⟨m⟩ =>
-    dite (Eq n m) (fun h => isTrue (h ▸ rfl)) (fun h => isFalse (fun h' => UInt8.noConfusion h' (fun h' => absurd h' h)))
+    dite (Eq n m)
+      (fun h => isTrue (h ▸ rfl))
+      (fun h => isFalse (fun h' => UInt8.noConfusion h' (fun h' => absurd h' h)))
 
 instance : DecidableEq UInt8 := UInt8.decEq
 
@@ -1916,12 +1961,12 @@ The type of unsigned 16-bit integers. This type has special support in the
 compiler to make it actually 16 bits rather than wrapping a `Nat`.
 -/
 structure UInt16 where
-  /-- Unpack a `UInt16` as a `Nat` less than `2^16`.
+  /-- Unpack a `UInt16` as a `BitVec 16`.
   This function is overridden with a native implementation. -/
-  val : Fin UInt16.size
+  toBitVec : BitVec 16
 
 attribute [extern "lean_uint16_of_nat_mk"] UInt16.mk
-attribute [extern "lean_uint16_to_nat"] UInt16.val
+attribute [extern "lean_uint16_to_nat"] UInt16.toBitVec
 
 /--
 Pack a `Nat` less than `2^16` into a `UInt16`.
@@ -1929,7 +1974,7 @@ This function is overridden with a native implementation.
 -/
 @[extern "lean_uint16_of_nat"]
 def UInt16.ofNatCore (n : @& Nat) (h : LT.lt n UInt16.size) : UInt16 where
-  val := { val := n, isLt := h }
+  toBitVec := BitVec.ofNatLt n h
 
 set_option bootstrap.genMatcherCode false in
 /--
@@ -1940,7 +1985,9 @@ This function is overridden with a native implementation.
 def UInt16.decEq (a b : UInt16) : Decidable (Eq a b) :=
   match a, b with
   | ⟨n⟩, ⟨m⟩ =>
-    dite (Eq n m) (fun h => isTrue (h ▸ rfl)) (fun h => isFalse (fun h' => UInt16.noConfusion h' (fun h' => absurd h' h)))
+    dite (Eq n m)
+      (fun h => isTrue (h ▸ rfl))
+      (fun h => isFalse (fun h' => UInt16.noConfusion h' (fun h' => absurd h' h)))
 
 instance : DecidableEq UInt16 := UInt16.decEq
 
@@ -1955,12 +2002,12 @@ The type of unsigned 32-bit integers. This type has special support in the
 compiler to make it actually 32 bits rather than wrapping a `Nat`.
 -/
 structure UInt32 where
-  /-- Unpack a `UInt32` as a `Nat` less than `2^32`.
+  /-- Unpack a `UInt32` as a `BitVec 32.
   This function is overridden with a native implementation. -/
-  val : Fin UInt32.size
+  toBitVec : BitVec 32
 
 attribute [extern "lean_uint32_of_nat_mk"] UInt32.mk
-attribute [extern "lean_uint32_to_nat"] UInt32.val
+attribute [extern "lean_uint32_to_nat"] UInt32.toBitVec
 
 /--
 Pack a `Nat` less than `2^32` into a `UInt32`.
@@ -1968,14 +2015,14 @@ This function is overridden with a native implementation.
 -/
 @[extern "lean_uint32_of_nat"]
 def UInt32.ofNatCore (n : @& Nat) (h : LT.lt n UInt32.size) : UInt32 where
-  val := { val := n, isLt := h }
+  toBitVec := BitVec.ofNatLt n h
 
 /--
 Unpack a `UInt32` as a `Nat`.
 This function is overridden with a native implementation.
 -/
 @[extern "lean_uint32_to_nat"]
-def UInt32.toNat (n : UInt32) : Nat := n.val.val
+def UInt32.toNat (n : UInt32) : Nat := n.toBitVec.toNat
 
 set_option bootstrap.genMatcherCode false in
 /--
@@ -1994,30 +2041,26 @@ instance : Inhabited UInt32 where
   default := UInt32.ofNatCore 0 (by decide)
 
 instance : LT UInt32 where
-  lt a b := LT.lt a.val b.val
+  lt a b := LT.lt a.toBitVec b.toBitVec
 
 instance : LE UInt32 where
-  le a b := LE.le a.val b.val
+  le a b := LE.le a.toBitVec b.toBitVec
 
-set_option bootstrap.genMatcherCode false in
 /--
 Decides less-equal on `UInt32`.
 This function is overridden with a native implementation.
 -/
 @[extern "lean_uint32_dec_lt"]
 def UInt32.decLt (a b : UInt32) : Decidable (LT.lt a b) :=
-  match a, b with
-  | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (LT.lt n m))
+  inferInstanceAs (Decidable (LT.lt a.toBitVec b.toBitVec))
 
-set_option bootstrap.genMatcherCode false in
 /--
 Decides less-than on `UInt32`.
 This function is overridden with a native implementation.
 -/
 @[extern "lean_uint32_dec_le"]
 def UInt32.decLe (a b : UInt32) : Decidable (LE.le a b) :=
-  match a, b with
-  | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (LE.le n m))
+  inferInstanceAs (Decidable (LE.le a.toBitVec b.toBitVec))
 
 instance (a b : UInt32) : Decidable (LT.lt a b) := UInt32.decLt a b
 instance (a b : UInt32) : Decidable (LE.le a b) := UInt32.decLe a b
@@ -2031,12 +2074,12 @@ The type of unsigned 64-bit integers. This type has special support in the
 compiler to make it actually 64 bits rather than wrapping a `Nat`.
 -/
 structure UInt64 where
-  /-- Unpack a `UInt64` as a `Nat` less than `2^64`.
+  /-- Unpack a `UInt64` as a `BitVec 64`.
   This function is overridden with a native implementation. -/
-  val : Fin UInt64.size
+  toBitVec: BitVec 64
 
 attribute [extern "lean_uint64_of_nat_mk"] UInt64.mk
-attribute [extern "lean_uint64_to_nat"] UInt64.val
+attribute [extern "lean_uint64_to_nat"] UInt64.toBitVec
 
 /--
 Pack a `Nat` less than `2^64` into a `UInt64`.
@@ -2044,7 +2087,7 @@ This function is overridden with a native implementation.
 -/
 @[extern "lean_uint64_of_nat"]
 def UInt64.ofNatCore (n : @& Nat) (h : LT.lt n UInt64.size) : UInt64 where
-  val := { val := n, isLt := h }
+  toBitVec := BitVec.ofNatLt n h
 
 set_option bootstrap.genMatcherCode false in
 /--
@@ -2055,36 +2098,20 @@ This function is overridden with a native implementation.
 def UInt64.decEq (a b : UInt64) : Decidable (Eq a b) :=
   match a, b with
   | ⟨n⟩, ⟨m⟩ =>
-    dite (Eq n m) (fun h => isTrue (h ▸ rfl)) (fun h => isFalse (fun h' => UInt64.noConfusion h' (fun h' => absurd h' h)))
+    dite (Eq n m)
+      (fun h => isTrue (h ▸ rfl))
+      (fun h => isFalse (fun h' => UInt64.noConfusion h' (fun h' => absurd h' h)))
 
 instance : DecidableEq UInt64 := UInt64.decEq
 
 instance : Inhabited UInt64 where
   default := UInt64.ofNatCore 0 (by decide)
 
-/--
-The size of type `USize`, that is, `2^System.Platform.numBits`, which may
-be either `2^32` or `2^64` depending on the platform's architecture.
-
-Remark: we define `USize.size` using `(2^numBits - 1) + 1` to ensure the
-Lean unifier can solve constraints such as `?m + 1 = USize.size`. Recall that
-`numBits` does not reduce to a numeral in the Lean kernel since it is platform
-specific. Without this trick, the following definition would be rejected by the
-Lean type checker.
-```
-def one: Fin USize.size := 1
-```
-Because Lean would fail to synthesize instance `OfNat (Fin USize.size) 1`.
-Recall that the `OfNat` instance for `Fin` is
-```
-instance : OfNat (Fin (n+1)) i where
-  ofNat := Fin.ofNat i
-```
--/
-abbrev USize.size : Nat := hAdd (hSub (hPow 2 System.Platform.numBits) 1) 1
+/-- The size of type `USize`, that is, `2^System.Platform.numBits`. -/
+abbrev USize.size : Nat := (hPow 2 System.Platform.numBits)
 
 theorem usize_size_eq : Or (Eq USize.size 4294967296) (Eq USize.size 18446744073709551616) :=
-  show Or (Eq (Nat.succ (Nat.sub (hPow 2 System.Platform.numBits) 1)) 4294967296) (Eq (Nat.succ (Nat.sub (hPow 2 System.Platform.numBits) 1)) 18446744073709551616) from
+  show Or (Eq (hPow 2 System.Platform.numBits) 4294967296) (Eq (hPow 2 System.Platform.numBits) 18446744073709551616) from
   match System.Platform.numBits, System.Platform.numBits_eq with
   | _, Or.inl rfl => Or.inl (by decide)
   | _, Or.inr rfl => Or.inr (by decide)
@@ -2097,21 +2124,20 @@ For example, if running on a 32-bit machine, USize is equivalent to UInt32.
 Or on a 64-bit machine, UInt64.
 -/
 structure USize where
-  /-- Unpack a `USize` as a `Nat` less than `USize.size`.
+  /-- Unpack a `USize` as a `BitVec System.Platform.numBits`.
   This function is overridden with a native implementation. -/
-  val : Fin USize.size
+  toBitVec : BitVec System.Platform.numBits
 
 attribute [extern "lean_usize_of_nat_mk"] USize.mk
-attribute [extern "lean_usize_to_nat"] USize.val
+attribute [extern "lean_usize_to_nat"] USize.toBitVec
 
 /--
 Pack a `Nat` less than `USize.size` into a `USize`.
 This function is overridden with a native implementation.
 -/
 @[extern "lean_usize_of_nat"]
-def USize.ofNatCore (n : @& Nat) (h : LT.lt n USize.size) : USize := {
-  val := { val := n, isLt := h }
-}
+def USize.ofNatCore (n : @& Nat) (h : LT.lt n USize.size) : USize where
+  toBitVec := BitVec.ofNatLt n h
 
 set_option bootstrap.genMatcherCode false in
 /--
@@ -2122,7 +2148,9 @@ This function is overridden with a native implementation.
 def USize.decEq (a b : USize) : Decidable (Eq a b) :=
   match a, b with
   | ⟨n⟩, ⟨m⟩ =>
-    dite (Eq n m) (fun h =>isTrue (h ▸ rfl)) (fun h => isFalse (fun h' => USize.noConfusion h' (fun h' => absurd h' h)))
+    dite (Eq n m)
+      (fun h => isTrue (h ▸ rfl))
+      (fun h => isFalse (fun h' => USize.noConfusion h' (fun h' => absurd h' h)))
 
 instance : DecidableEq USize := USize.decEq
 
@@ -2138,12 +2166,12 @@ This function is overridden with a native implementation.
 -/
 @[extern "lean_usize_of_nat"]
 def USize.ofNat32 (n : @& Nat) (h : LT.lt n 4294967296) : USize where
-  val := {
-    val  := n
-    isLt := match USize.size, usize_size_eq with
+  toBitVec :=
+    BitVec.ofNatLt n (
+      match System.Platform.numBits, System.Platform.numBits_eq with
       | _, Or.inl rfl => h
       | _, Or.inr rfl => Nat.lt_trans h (by decide)
-  }
+    )
 
 /--
 A `Nat` denotes a valid unicode codepoint if it is less than `0x110000`, and
@@ -2178,7 +2206,7 @@ This function is overridden with a native implementation.
 -/
 @[extern "lean_uint32_of_nat"]
 def Char.ofNatAux (n : @& Nat) (h : n.isValidChar) : Char :=
-  { val := ⟨{ val := n, isLt := isValidChar_UInt32 h }⟩, valid := h }
+  { val := ⟨BitVec.ofNatLt n (isValidChar_UInt32 h)⟩, valid := h }
 
 /--
 Convert a `Nat` into a `Char`. If the `Nat` does not encode a valid unicode scalar value,
@@ -2188,7 +2216,7 @@ Convert a `Nat` into a `Char`. If the `Nat` does not encode a valid unicode scal
 def Char.ofNat (n : Nat) : Char :=
   dite (n.isValidChar)
     (fun h => Char.ofNatAux n h)
-    (fun _ => { val := ⟨{ val := 0, isLt := by decide }⟩, valid := Or.inl (by decide) })
+    (fun _ => { val := ⟨BitVec.ofNatLt 0 (by decide)⟩, valid := Or.inl (by decide) })
 
 theorem Char.eq_of_val_eq : ∀ {c d : Char}, Eq c.val d.val → Eq c d
   | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
@@ -3448,15 +3476,13 @@ This function is overridden with a native implementation.
 -/
 @[extern "lean_usize_to_uint64"]
 def USize.toUInt64 (u : USize) : UInt64 where
-  val := {
-    val  := u.val.val
-    isLt :=
-      let ⟨n, h⟩ := u
-      show LT.lt n _ from
-      match USize.size, usize_size_eq, h with
-      | _, Or.inl rfl, h => Nat.lt_trans h (by decide)
-      | _, Or.inr rfl, h => h
-  }
+  toBitVec := BitVec.ofNatLt u.toBitVec.toNat (
+        let ⟨⟨n, h⟩⟩ := u
+        show LT.lt n _ from
+        match System.Platform.numBits, System.Platform.numBits_eq, h with
+        | _, Or.inl rfl, h => Nat.lt_trans h (by decide)
+        | _, Or.inr rfl, h => h
+      )
 
 /-- An opaque hash mixing operation, used to implement hashing for tuples. -/
 @[extern "lean_uint64_mix_hash"]

src/Init/SizeOf.lean

@@ -67,6 +67,7 @@ deriving instance SizeOf for PLift
 deriving instance SizeOf for ULift
 deriving instance SizeOf for Decidable
 deriving instance SizeOf for Fin
+deriving instance SizeOf for BitVec
 deriving instance SizeOf for UInt8
 deriving instance SizeOf for UInt16
 deriving instance SizeOf for UInt32

src/Init/SizeOfLemmas.lean

@@ -11,22 +11,25 @@ import Init.Data.Nat.Linear
 @[simp] protected theorem Fin.sizeOf (a : Fin n) : sizeOf a = a.val + 1 := by
   cases a; simp_arith
 
-@[simp] protected theorem UInt8.sizeOf (a : UInt8) : sizeOf a = a.toNat + 2 := by
-  cases a; simp_arith [UInt8.toNat]
+@[simp] protected theorem BitVec.sizeOf (a : BitVec w) : sizeOf a = sizeOf a.toFin + 1 := by
+  cases a; simp_arith
 
-@[simp] protected theorem UInt16.sizeOf (a : UInt16) : sizeOf a = a.toNat + 2 := by
-  cases a; simp_arith [UInt16.toNat]
+@[simp] protected theorem UInt8.sizeOf (a : UInt8) : sizeOf a = a.toNat + 3 := by
+  cases a; simp_arith [UInt8.toNat, BitVec.toNat]
 
-@[simp] protected theorem UInt32.sizeOf (a : UInt32) : sizeOf a = a.toNat + 2 := by
-  cases a; simp_arith [UInt32.toNat]
+@[simp] protected theorem UInt16.sizeOf (a : UInt16) : sizeOf a = a.toNat + 3 := by
+  cases a; simp_arith [UInt16.toNat, BitVec.toNat]
 
-@[simp] protected theorem UInt64.sizeOf (a : UInt64) : sizeOf a = a.toNat + 2 := by
-  cases a; simp_arith [UInt64.toNat]
+@[simp] protected theorem UInt32.sizeOf (a : UInt32) : sizeOf a = a.toNat + 3 := by
+  cases a; simp_arith [UInt32.toNat, BitVec.toNat]
 
-@[simp] protected theorem USize.sizeOf (a : USize) : sizeOf a = a.toNat + 2 := by
-  cases a; simp_arith [USize.toNat]
+@[simp] protected theorem UInt64.sizeOf (a : UInt64) : sizeOf a = a.toNat + 3 := by
+  cases a; simp_arith [UInt64.toNat, BitVec.toNat]
 
-@[simp] protected theorem Char.sizeOf (a : Char) : sizeOf a = a.toNat + 3 := by
+@[simp] protected theorem USize.sizeOf (a : USize) : sizeOf a = a.toNat + 3 := by
+  cases a; simp_arith [USize.toNat, BitVec.toNat]
+
+@[simp] protected theorem Char.sizeOf (a : Char) : sizeOf a = a.toNat + 4 := by
   cases a; simp_arith [Char.toNat]
 
 @[simp] protected theorem Subtype.sizeOf {α : Sort u_1} {p : α → Prop} (s : Subtype p) : sizeOf s = sizeOf s.val + 1 := by

src/Init/Tactics.lean

@@ -910,6 +910,15 @@ macro_rules | `(tactic| trivial) => `(tactic| simp)
 -/
 syntax "trivial" : tactic
 
+/--
+`classical tacs` runs `tacs` in a scope where `Classical.propDecidable` is a low priority
+local instance.
+
+Note that `classical` is a scoping tactic: it adds the instance only within the
+scope of the tactic.
+-/
+syntax (name := classical) "classical" ppDedent(tacticSeq) : tactic
+
 /--
 The `split` tactic is useful for breaking nested if-then-else and `match` expressions into separate cases.
 For a `match` expression with `n` cases, the `split` tactic generates at most `n` subgoals.

src/Lean/Data/HashMap.lean

@@ -46,7 +46,7 @@ private def mkIdx {sz : Nat} (hash : UInt64) (h : sz.isPowerOfTwo) : { u : USize
   if h' : u.toNat < sz then
     ⟨u, h'⟩
   else
-    ⟨0, by simp [USize.toNat, OfNat.ofNat, USize.ofNat]; apply Nat.pos_of_isPowerOfTwo h⟩
+    ⟨0, by simp; apply Nat.pos_of_isPowerOfTwo h⟩
 
 @[inline] def reinsertAux (hashFn : α → UInt64) (data : HashMapBucket α β) (a : α) (b : β) : HashMapBucket α β :=
   let ⟨i, h⟩ := mkIdx (hashFn a) data.property

src/Lean/Data/HashSet.lean

@@ -42,7 +42,7 @@ private def mkIdx {sz : Nat} (hash : UInt64) (h : sz.isPowerOfTwo) : { u : USize
   if h' : u.toNat < sz then
     ⟨u, h'⟩
   else
-    ⟨0, by simp [USize.toNat, OfNat.ofNat, USize.ofNat]; apply Nat.pos_of_isPowerOfTwo h⟩
+    ⟨0, by simp; apply Nat.pos_of_isPowerOfTwo h⟩
 
 @[inline] def reinsertAux (hashFn : α → UInt64) (data : HashSetBucket α) (a : α) : HashSetBucket α :=
   let ⟨i, h⟩ := mkIdx (hashFn a) data.property

src/Lean/Data/Lsp/Capabilities.lean

@@ -54,7 +54,7 @@ structure WorkspaceEditClientCapabilities where
   deriving ToJson, FromJson
 
 structure WorkspaceClientCapabilities where
-  applyEdit: Bool
+  applyEdit? : Option Bool := none
   workspaceEdit? : Option WorkspaceEditClientCapabilities := none
   deriving ToJson, FromJson
 

src/Lean/Data/PersistentArray.lean

@@ -7,6 +7,7 @@ prelude
 import Init.Data.Array.Basic
 import Init.NotationExtra
 import Init.Data.ToString.Macro
+import Init.Data.UInt.Basic
 
 universe u v w
 

src/Lean/Data/PersistentHashMap.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Init.Data.Array.BasicAux
 import Init.Data.ToString.Macro
+import Init.Data.UInt.Basic
 
 namespace Lean
 universe u v w w'

src/Lean/Data/Xml/Parser.lean

@@ -459,7 +459,7 @@ mutual
 
       let z ← optional (Content.Character <$> CharData)
       pure #[y, z]
-    let xs := #[x] ++ xs.concatMap id |>.filterMap id
+    let xs := #[x] ++ xs.flatMap id |>.filterMap id
     let mut res := #[]
     for x in xs do
       if res.size > 0 then

src/Lean/Elab/BuiltinCommand.lean

@@ -229,7 +229,7 @@ private def replaceBinderAnnotation (binder : TSyntax ``Parser.Term.bracketedBin
 
 @[builtin_command_elab «variable»] def elabVariable : CommandElab
   | `(variable $binders*) => do
-    let binders ← binders.concatMapM replaceBinderAnnotation
+    let binders ← binders.flatMapM replaceBinderAnnotation
     -- Try to elaborate `binders` for sanity checking
     runTermElabM fun _ => Term.withSynthesize <| Term.withAutoBoundImplicit <|
       Term.elabBinders binders fun _ => pure ()
@@ -348,7 +348,7 @@ def failIfSucceeds (x : CommandElabM Unit) : CommandElabM Unit := do
 @[builtin_command_elab Lean.Parser.Command.include] def elabInclude : CommandElab
   | `(Lean.Parser.Command.include| include $ids*) => do
     let sc ← getScope
-    let vars ← sc.varDecls.concatMapM getBracketedBinderIds
+    let vars ← sc.varDecls.flatMapM getBracketedBinderIds
     let mut uids := #[]
     for id in ids do
       if let some idx := vars.findIdx? (· == id.getId) then

src/Lean/Elab/Command.lean

@@ -532,11 +532,12 @@ def elabCommandTopLevel (stx : Syntax) : CommandElabM Unit := withRef stx do pro
     let mut msgs := (← get).messages
     for tree in (← getInfoTrees) do
       trace[Elab.info] (← tree.format)
-    if let some snap := (← read).snap? then
-      -- We can assume that the root command snapshot is not involved in parallelism yet, so this
-      -- should be true iff the command supports incrementality
-      if (← IO.hasFinished snap.new.result) then
-        liftCoreM <| Language.ToSnapshotTree.toSnapshotTree snap.new.result.get |>.trace
+    if (← isTracingEnabledFor `Elab.snapshotTree) then
+      if let some snap := (← read).snap? then
+        -- We can assume that the root command snapshot is not involved in parallelism yet, so this
+        -- should be true iff the command supports incrementality
+        if (← IO.hasFinished snap.new.result) then
+          liftCoreM <| Language.ToSnapshotTree.toSnapshotTree snap.new.result.get |>.trace
     modify fun st => { st with
       messages := initMsgs ++ msgs
       infoState := { st.infoState with trees := initInfoTrees ++ st.infoState.trees }
@@ -571,7 +572,7 @@ def getBracketedBinderIds : Syntax → CommandElabM (Array Name)
 private def mkTermContext (ctx : Context) (s : State) : CommandElabM Term.Context := do
   let scope      := s.scopes.head!
   let mut sectionVars := {}
-  for id in (← scope.varDecls.concatMapM getBracketedBinderIds), uid in scope.varUIds do
+  for id in (← scope.varDecls.flatMapM getBracketedBinderIds), uid in scope.varUIds do
     sectionVars := sectionVars.insert id uid
   return {
     macroStack             := ctx.macroStack
@@ -714,7 +715,7 @@ def expandDeclId (declId : Syntax) (modifiers : Modifiers) : CommandElabM Expand
   let currNamespace ← getCurrNamespace
   let currLevelNames ← getLevelNames
   let r ← Elab.expandDeclId currNamespace currLevelNames declId modifiers
-  for id in (← (← getScope).varDecls.concatMapM getBracketedBinderIds) do
+  for id in (← (← getScope).varDecls.flatMapM getBracketedBinderIds) do
     if id == r.shortName then
       throwError "invalid declaration name '{r.shortName}', there is a section variable with the same name"
   return r

src/Lean/Elab/Frontend.lean

@@ -151,7 +151,7 @@ def runFrontend
   snaps.runAndReport opts jsonOutput
 
   if let some ileanFileName := ileanFileName? then
-    let trees := snaps.getAll.concatMap (match ·.infoTree? with | some t => #[t] | _ => #[])
+    let trees := snaps.getAll.flatMap (match ·.infoTree? with | some t => #[t] | _ => #[])
     let references := Lean.Server.findModuleRefs inputCtx.fileMap trees (localVars := false)
     let ilean := { module := mainModuleName, references := ← references.toLspModuleRefs : Lean.Server.Ilean }
     IO.FS.writeFile ileanFileName $ Json.compress $ toJson ilean

src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean

@@ -226,7 +226,7 @@ def allCombinations (xss : Array (Array α)) : Option (Array (Array α)) :=
   else
     let rec go i acc : Array (Array α):=
       if h : i < xss.size then
-        xss[i].concatMap fun x => go (i + 1) (acc.push x)
+        xss[i].flatMap fun x => go (i + 1) (acc.push x)
       else
         #[acc]
     some (go 0 #[])

src/Lean/Elab/Tactic.lean

@@ -43,3 +43,4 @@ import Lean.Elab.Tactic.Rewrites
 import Lean.Elab.Tactic.DiscrTreeKey
 import Lean.Elab.Tactic.BVDecide
 import Lean.Elab.Tactic.BoolToPropSimps
+import Lean.Elab.Tactic.Classical

src/Lean/Elab/Tactic/Basic.lean

@@ -52,6 +52,7 @@ instance : Monad TacticM :=
 instance : Inhabited (TacticM α) where
   default := fun _ _ => default
 
+/-- Returns the list of goals. Goals may or may not already be assigned. -/
 def getGoals : TacticM (List MVarId) :=
   return (← get).goals
 
@@ -300,13 +301,22 @@ instance : MonadBacktrack SavedState TacticM where
   saveState := Tactic.saveState
   restoreState b := b.restore
 
+/--
+Non-backtracking `try`/`catch`.
+-/
 @[inline] protected def tryCatch {α} (x : TacticM α) (h : Exception → TacticM α) : TacticM α := do
+  try x catch ex => h ex
+
+/--
+Backtracking `try`/`catch`. This is used for the `MonadExcept` instance for `TacticM`.
+-/
+@[inline] protected def tryCatchRestore {α} (x : TacticM α) (h : Exception → TacticM α) : TacticM α := do
   let b ← saveState
   try x catch ex => b.restore; h ex
 
 instance : MonadExcept Exception TacticM where
   throw    := throw
-  tryCatch := Tactic.tryCatch
+  tryCatch := Tactic.tryCatchRestore
 
 /-- Execute `x` with error recovery disabled -/
 def withoutRecover (x : TacticM α) : TacticM α :=
@@ -342,12 +352,26 @@ def adaptExpander (exp : Syntax → TacticM Syntax) : Tactic := fun stx => do
   let stx' ← exp stx
   withMacroExpansion stx stx' $ evalTactic stx'
 
-/-- Add the given goals at the end of the current goals collection. -/
+/-- Add the given goal to the front of the current list of goals. -/
+def pushGoal (mvarId : MVarId) : TacticM Unit :=
+  modify fun s => { s with goals := mvarId :: s.goals }
+
+/-- Add the given goals to the front of the current list of goals. -/
+def pushGoals (mvarIds : List MVarId) : TacticM Unit :=
+  modify fun s => { s with goals := mvarIds ++ s.goals }
+
+/-- Add the given goals at the end of the current list of goals. -/
 def appendGoals (mvarIds : List MVarId) : TacticM Unit :=
   modify fun s => { s with goals := s.goals ++ mvarIds }
 
-/-- Discard the first goal and replace it by the given list of goals,
-keeping the other goals. -/
+/--
+Discard the first goal and replace it by the given list of goals,
+keeping the other goals. This is used in conjunction with `getMainGoal`.
+
+Contract: between `getMainGoal` and `replaceMainGoal`, nothing manipulates the goal list.
+
+See also `Lean.Elab.Tactic.popMainGoal` and `Lean.Elab.Tactic.pushGoal`/`Lean.Elab.Tactic.pushGoal` for another interface.
+-/
 def replaceMainGoal (mvarIds : List MVarId) : TacticM Unit := do
   let (_ :: mvarIds') ← getGoals | throwNoGoalsToBeSolved
   modify fun _ => { goals := mvarIds ++ mvarIds' }
@@ -365,6 +389,16 @@ where
         setGoals (mvarId :: mvarIds)
         return mvarId
 
+/--
+Return the first goal, and remove it from the goal list.
+
+See also: `Lean.Elab.Tactic.pushGoal` and `Lean.Elab.Tactic.pushGoals`.
+-/
+def popMainGoal : TacticM MVarId := do
+  let mvarId ← getMainGoal
+  replaceMainGoal []
+  return mvarId
+
 /-- Return the main goal metavariable declaration. -/
 def getMainDecl : TacticM MetavarDecl := do
   (← getMainGoal).getDecl

src/Lean/Elab/Tactic/Calc.lean

@@ -14,9 +14,9 @@ open Meta
 @[builtin_tactic Lean.calcTactic]
 def evalCalc : Tactic := fun stx => withMainContext do
   let steps : TSyntax ``calcSteps := ⟨stx[1]⟩
-  let (val, mvarIds) ← withCollectingNewGoalsFrom (tagSuffix := `calc) do
-    let target := (← getMainTarget).consumeMData
-    let tag ← getMainTag
+  let target := (← getMainTarget).consumeMData
+  let tag ← getMainTag
+  let (val, mvarIds) ← withCollectingNewGoalsFrom (parentTag := tag) (tagSuffix := `calc) do
     runTermElab do
     let mut val ← Term.elabCalcSteps steps
     let mut valType ← instantiateMVars (← inferType val)

src/Lean/Elab/Tactic/Classical.lean

@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2021 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro, Kim Morrison
+-/
+prelude
+import Lean.Elab.Tactic.Basic
+
+/-! # `classical` tactic -/
+
+namespace Lean.Elab.Tactic
+open Lean Meta Elab.Tactic
+
+/--
+`classical t` runs `t` in a scope where `Classical.propDecidable` is a low priority
+local instance.
+-/
+def classical [Monad m] [MonadEnv m] [MonadFinally m] [MonadLiftT MetaM m] (t : m α) :
+    m α := do
+  modifyEnv Meta.instanceExtension.pushScope
+  Meta.addInstance ``Classical.propDecidable .local 10
+  try
+    t
+  finally
+    modifyEnv Meta.instanceExtension.popScope
+
+@[builtin_tactic Lean.Parser.Tactic.classical]
+def evalClassical : Tactic := fun stx => do
+  match stx with
+  | `(tactic| classical $tacs:tacticSeq) =>
+     classical <| Elab.Tactic.evalTactic tacs
+  | _ => throwUnsupportedSyntax
+
+end Lean.Elab.Tactic

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -56,11 +56,6 @@ def elabTermEnsuringType (stx : Syntax) (expectedType? : Option Expr) (mayPostpo
       Term.throwTypeMismatchError none expectedType eType e
     return e
 
-/-- Try to close main goal using `x target`, where `target` is the type of the main goal.  -/
-def closeMainGoalUsing (tacName : Name) (x : Expr → TacticM Expr) (checkUnassigned := true) : TacticM Unit :=
-  withMainContext do
-    closeMainGoal (tacName := tacName) (checkUnassigned := checkUnassigned) (← x (← getMainTarget))
-
 def logUnassignedAndAbort (mvarIds : Array MVarId) : TacticM Unit := do
    if (← Term.logUnassignedUsingErrorInfos mvarIds) then
      throwAbortTactic
@@ -69,14 +64,37 @@ def filterOldMVars (mvarIds : Array MVarId) (mvarCounterSaved : Nat) : MetaM (Ar
   let mctx ← getMCtx
   return mvarIds.filter fun mvarId => (mctx.getDecl mvarId |>.index) >= mvarCounterSaved
 
+/--
+Try to close main goal using `x target tag`, where `target` is the type of the main goal and `tag` is its user name.
+
+If `checkNewUnassigned` is true, then throws an error if the resulting value has metavariables that were created during the execution of `x`.
+If it is false, then it is the responsibility of `x` to add such metavariables to the goal list.
+
+During the execution of `x`:
+* The local context is that of the main goal.
+* The goal list has the main goal removed.
+* It is allowable to modify the goal list, for example with `Lean.Elab.Tactic.pushGoals`.
+
+On failure, the main goal remains at the front of the goal list.
+-/
+def closeMainGoalUsing (tacName : Name) (x : Expr → Name → TacticM Expr) (checkNewUnassigned := true) : TacticM Unit := do
+  let mvarCounterSaved := (← getMCtx).mvarCounter
+  let mvarId ← popMainGoal
+  Tactic.tryCatch
+    (mvarId.withContext do
+      let val ← x (← mvarId.getType) (← mvarId.getTag)
+      if checkNewUnassigned then
+        let mvars ← filterOldMVars (← getMVars val) mvarCounterSaved
+        logUnassignedAndAbort mvars
+      unless (← mvarId.checkedAssign val) do
+        throwTacticEx tacName mvarId m!"attempting to close the goal using{indentExpr val}\nthis is often due occurs-check failure")
+    (fun ex => do
+      pushGoal mvarId
+      throw ex)
+
 @[builtin_tactic «exact»] def evalExact : Tactic := fun stx => do
   match stx with
-  | `(tactic| exact $e) =>
-    closeMainGoalUsing `exact (checkUnassigned := false) fun type => do
-      let mvarCounterSaved := (← getMCtx).mvarCounter
-      let r ← elabTermEnsuringType e type
-      logUnassignedAndAbort (← filterOldMVars (← getMVars r) mvarCounterSaved)
-      return r
+  | `(tactic| exact $e) => closeMainGoalUsing `exact fun type _ => elabTermEnsuringType e type
   | _ => throwUnsupportedSyntax
 
 def sortMVarIdArrayByIndex [MonadMCtx m] [Monad m] (mvarIds : Array MVarId) : m (Array MVarId) := do
@@ -93,9 +111,12 @@ def sortMVarIdsByIndex [MonadMCtx m] [Monad m] (mvarIds : List MVarId) : m (List
   return (← sortMVarIdArrayByIndex mvarIds.toArray).toList
 
 /--
-  Execute `k`, and collect new "holes" in the resulting expression.
+Execute `k`, and collect new "holes" in the resulting expression.
+
+* `parentTag` and `tagSuffix` are used to tag untagged goals with `Lean.Elab.Tactic.tagUntaggedGoals`.
+* If `allowNaturalHoles` is true, then `_`'s are allowed and create new goals.
 -/
-def withCollectingNewGoalsFrom (k : TacticM Expr) (tagSuffix : Name) (allowNaturalHoles := false) : TacticM (Expr × List MVarId) :=
+def withCollectingNewGoalsFrom (k : TacticM Expr) (parentTag : Name) (tagSuffix : Name) (allowNaturalHoles := false) : TacticM (Expr × List MVarId) :=
   /-
   When `allowNaturalHoles = true`, unassigned holes should become new metavariables, including `_`s.
   Thus, we set `holesAsSyntheticOpaque` to true if it is not already set to `true`.
@@ -144,7 +165,7 @@ where
     appear in the `.lean` file. We should tell users to prefer tagged goals.
     -/
     let newMVarIds ← sortMVarIdsByIndex newMVarIds.toList
-    tagUntaggedGoals (← getMainTag) tagSuffix newMVarIds
+    tagUntaggedGoals parentTag tagSuffix newMVarIds
     return (val, newMVarIds)
 
 /-- Elaborates `stx` and collects the `MVarId`s of any holes that were created during elaboration.
@@ -153,8 +174,8 @@ With `allowNaturalHoles := false` (the default), any new natural holes (`_`) whi
 be synthesized during elaboration cause `elabTermWithHoles` to fail. (Natural goals appearing in
 `stx` which were created prior to elaboration are permitted.)
 
-Unnamed `MVarId`s are renamed to share the main goal's tag. If multiple unnamed goals are
-encountered, `tagSuffix` is appended to the main goal's tag along with a numerical index.
+Unnamed `MVarId`s are renamed to share the tag `parentTag?` (or the main goal's tag if `parentTag?` is `none`).
+If multiple unnamed goals are encountered, `tagSuffix` is appended to this tag along with a numerical index.
 
 Note:
 * Previously-created `MVarId`s which appear in `stx` are not returned.
@@ -163,8 +184,8 @@ metavariables.
 * When `allowNaturalHoles := true`, `stx` is elaborated under `withAssignableSyntheticOpaque`,
 meaning that `.syntheticOpaque` metavariables might be assigned during elaboration. This is a
 consequence of the implementation. -/
-def elabTermWithHoles (stx : Syntax) (expectedType? : Option Expr) (tagSuffix : Name) (allowNaturalHoles := false) : TacticM (Expr × List MVarId) := do
-  withCollectingNewGoalsFrom (elabTermEnsuringType stx expectedType?) tagSuffix allowNaturalHoles
+def elabTermWithHoles (stx : Syntax) (expectedType? : Option Expr) (tagSuffix : Name) (allowNaturalHoles := false) (parentTag? : Option Name := none) : TacticM (Expr × List MVarId) := do
+  withCollectingNewGoalsFrom (elabTermEnsuringType stx expectedType?) (← parentTag?.getDM getMainTag) tagSuffix allowNaturalHoles
 
 /-- If `allowNaturalHoles == true`, then we allow the resultant expression to contain unassigned "natural" metavariables.
    Recall that "natutal" metavariables are created for explicit holes `_` and implicit arguments. They are meant to be
@@ -395,7 +416,7 @@ private partial def blameDecideReductionFailure (inst : Expr) : MetaM Expr := wi
   return inst
 
 def evalDecideCore (tacticName : Name) (kernelOnly : Bool) : TacticM Unit :=
-  closeMainGoalUsing tacticName fun expectedType => do
+  closeMainGoalUsing tacticName fun expectedType _ => do
     let expectedType ← preprocessPropToDecide expectedType
     let pf ← mkDecideProof expectedType
     -- Get instance from `pf`
@@ -501,7 +522,7 @@ private def mkNativeAuxDecl (baseName : Name) (type value : Expr) : TermElabM Na
   pure auxName
 
 @[builtin_tactic Lean.Parser.Tactic.nativeDecide] def evalNativeDecide : Tactic := fun _ =>
-  closeMainGoalUsing `nativeDecide fun expectedType => do
+  closeMainGoalUsing `nativeDecide fun expectedType _ => do
     let expectedType ← preprocessPropToDecide expectedType
     let d ← mkDecide expectedType
     let auxDeclName ← mkNativeAuxDecl `_nativeDecide (Lean.mkConst `Bool) d

src/Lean/Expr.lean

@@ -1038,6 +1038,14 @@ def getForallBinderNames : Expr → List Name
   | forallE n _ b _ => n :: getForallBinderNames b
   | _ => []
 
+/--
+Returns the number of leading `∀` binders of an expression. Ignores metadata.
+-/
+def getNumHeadForalls : Expr → Nat
+  | mdata _ b => getNumHeadForalls b
+  | forallE _ _ body _ => getNumHeadForalls body + 1
+  | _ => 0
+
 /--
 If the given expression is a sequence of
 function applications `f a₁ .. aₙ`, return `f`.
@@ -1085,6 +1093,16 @@ private def getAppNumArgsAux : Expr → Nat → Nat
 def getAppNumArgs (e : Expr) : Nat :=
   getAppNumArgsAux e 0
 
+/-- Like `getAppNumArgs` but ignores metadata. -/
+def getAppNumArgs' (e : Expr) : Nat :=
+  go e 0
+where
+  /-- Auxiliary definition for `getAppNumArgs'`. -/
+  go : Expr → Nat → Nat
+    | mdata _ b, n => go b n
+    | app f _  , n => go f (n + 1)
+    | _        , n => n
+
 /--
 Like `Lean.Expr.getAppFn` but assumes the application has up to `maxArgs` arguments.
 If there are any more arguments than this, then they are returned by `getAppFn` as part of the function.

src/Lean/Meta/DiscrTree.lean

@@ -76,7 +76,7 @@ def Key.format : Key → Format
   | .const k _       => Std.format k
   | .proj s i _      => Std.format s ++ "." ++ Std.format i
   | .fvar k _        => Std.format k.name
-  | .arrow           => "→"
+  | .arrow           => "∀"
 
 instance : ToFormat Key := ⟨Key.format⟩
 
@@ -113,7 +113,8 @@ where
       mkApp m!"{mkFVar fvarId}" (← goN nargs) parenIfNonAtomic
     | .proj _ i nargs =>
       mkApp m!"{← go}.{i+1}" (← goN nargs) parenIfNonAtomic
-    | .arrow => return "<arrow>"
+    | .arrow =>
+      mkApp m!"∀ " (← goN 1) parenIfNonAtomic
     | .star => return "_"
     | .other => return "<other>"
     | .lit (.natVal v) => return m!"{v}"
@@ -129,21 +130,15 @@ def Key.arity : Key → Nat
   | .const _ a  => a
   | .fvar _ a   => a
   /-
-  Remark: `.arrow` used to have arity 2, and was used to encode non-dependent arrows.
-  However, this feature was a recurrent source of bugs. For example, a theorem about
-  a dependent arrow can be applied to a non-dependent one. The reverse direction may
-  also happen. See issue #2835.
-  ```
-  -- A theorem about the non-dependent arrow `a → a`
-  theorem imp_self' {a : Prop} : (a → a) ↔ True := ⟨fun _ => trivial, fun _ => id⟩
-
-  -- can be applied to the dependent one `(h : P a) → P (f h)`.
-  example {α : Prop} {P : α → Prop} {f : ∀ {a}, P a → α} {a : α} : (h : P a) → P (f h) := by
-    simp only [imp_self']
-  ```
-  Thus, we now index dependent and non-dependent arrows using the key `.arrow` with arity 0.
+  Remark: `.arrow` used to have arity 2, and was used to encode only **non**-dependent
+  arrows. However, this feature was a recurrent source of bugs. For example, a
+  theorem about a dependent arrow can be applied to a non-dependent one. The
+  reverse direction may also happen. See issue #2835. Therefore, `.arrow` was made
+  to have arity 0. But this throws away easy to use information, and makes it so
+  that ∀ and ∃ behave quite differently. So now `.arrow` at least indexes the
+  domain of the forall (whether dependent or non-dependent).
   -/
-  | .arrow      => 0
+  | .arrow      => 1
   | .proj _ _ a => 1 + a
   | _           => 0
 
@@ -422,7 +417,8 @@ private def pushArgs (root : Bool) (todo : Array Expr) (e : Expr) (config : Whnf
         return (.other, todo)
       else
         return (.star, todo)
-    | .forallE .. => return (.arrow, todo)
+    | .forallE _n d _ _ =>
+      return (.arrow, todo.push d)
     | _ => return (.other, todo)
 
 @[inherit_doc pushArgs]
@@ -581,7 +577,7 @@ private def getKeyArgs (e : Expr) (isMatch root : Bool) (config : WhnfCoreConfig
   | .proj s i a .. =>
     let nargs := e.getAppNumArgs
     return (.proj s i nargs, #[a] ++ e.getAppRevArgs)
-  | .forallE .. => return (.arrow, #[])
+  | .forallE _ d _ _ => return (.arrow, #[d])
   | _ => return (.other, #[])
 
 private abbrev getMatchKeyArgs (e : Expr) (root : Bool) (config : WhnfCoreConfig) : MetaM (Key × Array Expr) :=

src/Lean/Meta/RecursorInfo.lean

@@ -67,29 +67,6 @@ instance : ToString RecursorInfo := ⟨fun info =>
 
 end RecursorInfo
 
-private def mkRecursorInfoForKernelRec (declName : Name) (val : RecursorVal) : MetaM RecursorInfo := do
-  let ival ← getConstInfoInduct val.getInduct
-  let numLParams    := ival.levelParams.length
-  let univLevelPos  := (List.range numLParams).map RecursorUnivLevelPos.majorType
-  let univLevelPos  := if val.levelParams.length == numLParams then univLevelPos else RecursorUnivLevelPos.motive :: univLevelPos
-  let produceMotive := List.replicate val.numMinors true
-  let paramsPos     := (List.range val.numParams).map some
-  let indicesPos    := (List.range val.numIndices).map fun pos => val.numParams + pos
-  let numArgs       := val.numIndices + val.numParams + val.numMinors + val.numMotives + 1
-  pure {
-    recursorName  := declName,
-    typeName      := val.getInduct,
-    univLevelPos  := univLevelPos,
-    majorPos      := val.getMajorIdx,
-    depElim       := true,
-    recursive     := ival.isRec,
-    produceMotive := produceMotive,
-    paramsPos     := paramsPos,
-    indicesPos    := indicesPos,
-    numArgs       := numArgs
-  }
-
-
 private def getMajorPosIfAuxRecursor? (declName : Name) (majorPos? : Option Nat) : MetaM (Option Nat) :=
   if majorPos?.isSome then pure majorPos?
   else do
@@ -202,8 +179,8 @@ private def checkMotiveResultType (declName : Name) (motiveArgs : Array Expr) (m
   if !motiveResultType.isSort || motiveArgs.size != motiveTypeParams.size then
     throwError "invalid user defined recursor '{declName}', motive must have a type of the form (C : Pi (i : B A), I A i -> Type), where A is (possibly empty) sequence of variables (aka parameters), (i : B A) is a (possibly empty) telescope (aka indices), and I is a constant"
 
-private def mkRecursorInfoAux (cinfo : ConstantInfo) (majorPos? : Option Nat) : MetaM RecursorInfo := do
-  let declName := cinfo.name
+private def mkRecursorInfoCore (declName : Name) (majorPos? : Option Nat) : MetaM RecursorInfo := do
+  let cinfo ← getConstInfo declName
   let majorPos? ← getMajorPosIfAuxRecursor? declName majorPos?
   forallTelescopeReducing cinfo.type fun xs type => type.withApp fun motive motiveArgs => do
     checkMotive declName motive motiveArgs
@@ -250,12 +227,6 @@ def Attribute.Recursor.getMajorPos (stx : Syntax) : AttrM Nat := do
   else
     throwErrorAt stx "unexpected attribute argument, numeral expected"
 
-private def mkRecursorInfoCore (declName : Name) (majorPos? : Option Nat := none) : MetaM RecursorInfo := do
-  let cinfo ← getConstInfo declName
-  match cinfo with
-  | ConstantInfo.recInfo val => mkRecursorInfoForKernelRec declName val
-  | _                        => mkRecursorInfoAux cinfo majorPos?
-
 builtin_initialize recursorAttribute : ParametricAttribute Nat ←
   registerParametricAttribute {
     name := `recursor,
@@ -269,11 +240,7 @@ def getMajorPos? (env : Environment) (declName : Name) : Option Nat :=
   recursorAttribute.getParam? env declName
 
 def mkRecursorInfo (declName : Name) (majorPos? : Option Nat := none) : MetaM RecursorInfo := do
-  let cinfo ← getConstInfo declName
-  match cinfo with
-  | ConstantInfo.recInfo val => mkRecursorInfoForKernelRec declName val
-  | _                        => match majorPos? with
-    | none => do mkRecursorInfoAux cinfo (getMajorPos? (← getEnv) declName)
-    | _    => mkRecursorInfoAux cinfo majorPos?
+  let majorPos? := majorPos? <|> getMajorPos? (← getEnv) declName
+  mkRecursorInfoCore declName majorPos?
 
 end Lean.Meta

src/Lean/Meta/Tactic/AC/Main.lean

@@ -86,35 +86,63 @@ def toACExpr (op l r : Expr) : MetaM (Array Expr × ACExpr) := do
     | PreExpr.op l r => Data.AC.Expr.op (toACExpr varMap l) (toACExpr varMap r)
     | PreExpr.var x => Data.AC.Expr.var (varMap x)
 
-def buildNormProof (preContext : PreContext) (l r : Expr) : MetaM (Lean.Expr × Lean.Expr) := do
-  let (vars, acExpr) ← toACExpr preContext.op l r
-
-  let α ← inferType vars[0]!
+/--
+In order to prevent the kernel trying to reduce the atoms of the expression, we abstract the proof
+over them. But `ac_rfl` proofs are not completely abstract in the value of the atoms – it recognizes
+neutral elements. So we have to abstract over these proofs as well.
+-/
+def abstractAtoms (preContext : PreContext) (atoms : Array Expr)
+    (k : Array (Expr × Option Expr) → MetaM Expr) : MetaM Expr := do
+  let α ← inferType atoms[0]!
   let u ← getLevel α
-  let (isNeutrals, context) ← mkContext α u vars
-  let acExprNormed := Data.AC.evalList ACExpr preContext $ Data.AC.norm (preContext, isNeutrals) acExpr
-  let tgt := convertTarget vars acExprNormed
-  let lhs := convert acExpr
-  let rhs := convert acExprNormed
-  let proof := mkAppN (mkConst ``Context.eq_of_norm [u]) #[α, context, lhs, rhs, ←mkEqRefl (mkConst ``Bool.true)]
+  let rec go i (acc : Array (Expr × Option Expr)) (vars : Array Expr) (args : Array Expr) := do
+    if h : i < atoms.size then
+      withLocalDeclD `x α fun v => do
+        match (← getInstance ``LawfulIdentity #[preContext.op, atoms[i]]) with
+        | none =>
+          go (i+1) (acc.push (v, .none)) (vars.push v) (args.push atoms[i])
+        | some inst =>
+          withLocalDeclD `inst (mkApp3 (mkConst ``LawfulIdentity [u]) α preContext.op v) fun iv =>
+            go (i+1) (acc.push (v, .some iv)) (vars ++ #[v,iv]) (args ++ #[atoms[i], inst])
+    else
+      let proof ← k acc
+      let proof ← mkLambdaFVars vars proof
+      let proof := mkAppN proof args
+      return proof
+  go 0 #[] #[] #[]
+
+def buildNormProof (preContext : PreContext) (l r : Expr) : MetaM (Lean.Expr × Lean.Expr) := do
+  let (atoms, acExpr) ← toACExpr preContext.op l r
+  let proof ← abstractAtoms preContext atoms fun varsData => do
+    let α ← inferType atoms[0]!
+    let u ← getLevel α
+    let context ← mkContext α u varsData
+    let isNeutrals := varsData.map (·.2.isSome)
+    let vars := varsData.map (·.1)
+    let acExprNormed := Data.AC.evalList ACExpr preContext $ Data.AC.norm (preContext, isNeutrals) acExpr
+    let lhs := convert acExpr
+    let rhs := convert acExprNormed
+    let proof := mkAppN (mkConst ``Context.eq_of_norm [u]) #[α, context, lhs, rhs, ←mkEqRefl (mkConst ``Bool.true)]
+    let proofType ← mkEq (convertTarget vars acExpr) (convertTarget vars acExprNormed)
+    let proof ← mkExpectedTypeHint proof proofType
+    return proof
+  let some (_, _, tgt) := (← inferType proof).eq? | panic! "unexpected proof type"
   return (proof, tgt)
 where
-  mkContext (α : Expr) (u : Level) (vars : Array Expr) : MetaM (Array Bool × Expr) := do
-    let arbitrary := vars[0]!
+  mkContext (α : Expr) (u : Level) (vars : Array (Expr × Option Expr)) : MetaM Expr := do
+    let arbitrary := vars[0]!.1
     let plift := mkApp (mkConst ``PLift [.zero])
     let pliftUp := mkApp2 (mkConst ``PLift.up [.zero])
     let noneE tp   := mkApp  (mkConst ``Option.none [.zero]) (plift tp)
     let someE tp v := mkApp2 (mkConst ``Option.some [.zero]) (plift tp) (pliftUp tp v)
-    let vars ← vars.mapM fun x => do
+    let vars ← vars.mapM fun ⟨x, inst?⟩ =>
       let isNeutral :=
         let isNeutralClass := mkApp3 (mkConst ``LawfulIdentity [u]) α preContext.op x
-        match ←getInstance ``LawfulIdentity #[preContext.op, x] with
-        | none => (false, noneE isNeutralClass)
-        | some isNeutral => (true, someE isNeutralClass isNeutral)
+        match inst? with
+        | none => noneE isNeutralClass
+        | some isNeutral => someE isNeutralClass isNeutral
+      return mkApp4 (mkConst ``Variable.mk [u]) α preContext.op x isNeutral
 
-      return (isNeutral.1, mkApp4 (mkConst ``Variable.mk [u]) α preContext.op x isNeutral.2)
-
-    let (isNeutrals, vars) := vars.unzip
     let vars := vars.toList
     let vars ← mkListLit (mkApp2 (mkConst ``Variable [u]) α preContext.op) vars
 
@@ -130,7 +158,7 @@ where
       | none => noneE idemClass
       | some idem => someE idemClass idem
 
-    return (isNeutrals, mkApp7 (mkConst ``Lean.Data.AC.Context.mk [u]) α preContext.op preContext.assoc comm idem vars arbitrary)
+    return mkApp7 (mkConst ``Lean.Data.AC.Context.mk [u]) α preContext.op preContext.assoc comm idem vars arbitrary
 
   convert : ACExpr → Expr
     | .op l r => mkApp2 (mkConst ``Data.AC.Expr.op) (convert l) (convert r)

src/Lean/Meta/Tactic/Intro.lean

@@ -164,7 +164,11 @@ does not start with a forall, lambda or let. -/
 abbrev _root_.Lean.MVarId.intro1P (mvarId : MVarId) : MetaM (FVarId × MVarId) :=
   intro1Core mvarId true
 
-private partial def getIntrosSize : Expr → Nat
+/--
+Calculate the number of new hypotheses that would be created by `intros`,
+i.e. the number of binders which can be introduced without unfolding definitions.
+-/
+partial def getIntrosSize : Expr → Nat
   | .forallE _ _ b _ => getIntrosSize b + 1
   | .letE _ _ _ b _  => getIntrosSize b + 1
   | .mdata _ b       => getIntrosSize b

src/Lean/Meta/Tactic/LinearArith/Nat/Simp.lean

@@ -8,24 +8,43 @@ import Lean.Meta.Tactic.LinearArith.Nat.Basic
 
 namespace Lean.Meta.Linear.Nat
 
+/-
+To prevent the kernel from accidentially reducing the atoms in the equation while typechecking,
+we abstract over them.
+-/
+def withAbstractAtoms (atoms : Array Expr) (k : Array Expr → MetaM (Option (Expr × Expr))) :
+    MetaM (Option (Expr × Expr)) := do
+  let atoms := atoms
+  let decls : Array (Name × (Array Expr → MetaM Expr)) ← atoms.mapM fun _ => do
+    return ((← mkFreshUserName `x), fun _ => pure (mkConst ``Nat))
+  withLocalDeclsD decls fun ctxt => do
+    let some (r, p) ← k ctxt | return none
+    let r := (← mkLambdaFVars ctxt r).beta atoms
+    let p := mkAppN (← mkLambdaFVars ctxt p) atoms
+    return some (r, p)
+
 def simpCnstrPos? (e : Expr) : MetaM (Option (Expr × Expr)) := do
-  let (some c, ctx) ← ToLinear.run (ToLinear.toLinearCnstr? e) | return none
-  let c₁ := c.toPoly
-  let c₂ := c₁.norm
-  if c₂.isUnsat then
-    let p := mkApp3 (mkConst ``Nat.Linear.ExprCnstr.eq_false_of_isUnsat) (← toContextExpr ctx) (toExpr c) reflTrue
-    return some (mkConst ``False, p)
-  else if c₂.isValid then
-    let p := mkApp3 (mkConst ``Nat.Linear.ExprCnstr.eq_true_of_isValid) (← toContextExpr ctx) (toExpr c) reflTrue
-    return some (mkConst ``True, p)
-  else
-    let c₂ : LinearCnstr := c₂.toExpr
-    let r ← c₂.toArith ctx
-    if r != e then
-      let p := mkApp4 (mkConst ``Nat.Linear.ExprCnstr.eq_of_toNormPoly_eq) (← toContextExpr ctx) (toExpr c) (toExpr c₂) reflTrue
-      return some (r, ← mkExpectedTypeHint p (← mkEq e r))
+  let (some c, atoms) ← ToLinear.run (ToLinear.toLinearCnstr? e) | return none
+  withAbstractAtoms atoms fun ctx => do
+    let lhs ← c.toArith ctx
+    let c₁ := c.toPoly
+    let c₂ := c₁.norm
+    if c₂.isUnsat then
+      let r := mkConst ``False
+      let p := mkApp3 (mkConst ``Nat.Linear.ExprCnstr.eq_false_of_isUnsat) (← toContextExpr ctx) (toExpr c) reflTrue
+      return some (r, ← mkExpectedTypeHint p (← mkEq lhs r))
+    else if c₂.isValid then
+      let r := mkConst ``True
+      let p := mkApp3 (mkConst ``Nat.Linear.ExprCnstr.eq_true_of_isValid) (← toContextExpr ctx) (toExpr c) reflTrue
+      return some (r, ← mkExpectedTypeHint p (← mkEq lhs r))
     else
-      return none
+      let c₂ : LinearCnstr := c₂.toExpr
+      let r ← c₂.toArith ctx
+      if r != lhs then
+        let p := mkApp4 (mkConst ``Nat.Linear.ExprCnstr.eq_of_toNormPoly_eq) (← toContextExpr ctx) (toExpr c) (toExpr c₂) reflTrue
+        return some (r, ← mkExpectedTypeHint p (← mkEq lhs r))
+      else
+        return none
 
 def simpCnstr? (e : Expr) : MetaM (Option (Expr × Expr)) := do
   if let some arg := e.not? then

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean

@@ -62,12 +62,12 @@ builtin_simproc [simp, seval] reduceNe  (( _ : Fin _) ≠ _)  := reduceBinPred `
 builtin_dsimproc [simp, seval] reduceBEq  (( _ : Fin _) == _)  := reduceBoolPred ``BEq.beq 4 (. == .)
 builtin_dsimproc [simp, seval] reduceBNe  (( _ : Fin _) != _)  := reduceBoolPred ``bne 4 (. != .)
 
-/-- Simplification procedure for ensuring `Fin` literals are normalized. -/
+/-- Simplification procedure for ensuring `Fin n` literals are normalized. -/
 builtin_dsimproc [simp, seval] isValue ((OfNat.ofNat _ : Fin _)) := fun e => do
   let_expr OfNat.ofNat _ m _ ← e | return .continue
   let some ⟨n, v⟩ ← getFinValue? e | return .continue
   let some m ← getNatValue? m | return .continue
-  if n == m then
+  if m < n then
     -- Design decision: should we return `.continue` instead of `.done` when simplifying.
     -- In the symbolic evaluator, we must return `.done`, otherwise it will unfold the `OfNat.ofNat`
     return .done e

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean

@@ -149,11 +149,14 @@ private def mkSubNat (x y : Expr) : Expr :=
 private def mkEqNat (x y : Expr) : Expr :=
   mkAppN (mkConst ``Eq [levelOne]) #[mkConst ``Nat, x, y]
 
-private def mkBeqNat (x y : Expr) : Expr :=
-  mkAppN (mkConst ``BEq.beq [levelZero]) #[mkConst ``Nat, mkConst ``instBEqNat, x, y]
+private def mkBEqNatInstance : Expr :=
+  mkAppN (mkConst ``instBEqOfDecidableEq [levelZero]) #[mkConst ``Nat, mkConst ``instDecidableEqNat []]
+
+private def mkBEqNat (x y : Expr) : Expr :=
+  mkAppN (mkConst ``BEq.beq [levelZero]) #[mkConst ``Nat, mkBEqNatInstance, x, y]
 
 private def mkBneNat (x y : Expr) : Expr :=
-  mkAppN (mkConst ``bne [levelZero]) #[mkConst ``Nat, mkConst ``instBEqNat, x, y]
+  mkAppN (mkConst ``bne [levelZero]) #[mkConst ``Nat, mkBEqNatInstance, x, y]
 
 private def mkLENat (x y : Expr) : Expr :=
   mkAppN (.const ``LE.le [levelZero]) #[mkConst ``Nat, mkConst ``instLENat, x, y]
@@ -250,7 +253,7 @@ builtin_simproc [simp, seval] reduceBeqDiff ((_ : Nat) == _) := fun e => do
     return .done  { expr := mkConst ``false, proof? := some q, cache := true }
   | some (.eq u v p) =>
     let q := mkAppN (mkConst ``Nat.Simproc.beqEqOfEqEq) #[x, y, u, v, p]
-    return .visit { expr := mkBeqNat u v, proof? := some q, cache := true }
+    return .visit { expr := mkBEqNat u v, proof? := some q, cache := true }
 
 builtin_simproc [simp, seval] reduceBneDiff ((_ : Nat) != _) := fun e => do
   unless e.isAppOfArity ``bne 4 do

src/Lean/Server/CodeActions/Basic.lean

@@ -124,7 +124,7 @@ def handleCodeAction (params : CodeActionParams) : RequestM (RequestTask (Array
         let names := codeActionProviderExt.getState env |>.toArray
         let caps ← names.mapM evalCodeActionProvider
         return (← builtinCodeActionProviders.get).toList.toArray ++ Array.zip names caps
-      caps.concatMapM fun (providerName, cap) => do
+      caps.flatMapM fun (providerName, cap) => do
         let cas ← cap params snap
         cas.mapIdxM fun i lca => do
           if lca.lazy?.isNone then return lca.eager

src/Lean/Server/CodeActions/Provider.lean

@@ -38,7 +38,7 @@ A code action which calls all `@[hole_code_action]` code actions on each hole
     unless head ≤ endPos && startPos ≤ tail do return result
     result.push (ctx, info)
   let #[(ctx, info)] := holes | return #[]
-  (holeCodeActionExt.getState snap.env).2.concatMapM (· params snap ctx info)
+  (holeCodeActionExt.getState snap.env).2.flatMapM (· params snap ctx info)
 
 /--
 The return value of `findTactic?`.

src/Lean/Server/InfoUtils.lean

@@ -197,7 +197,7 @@ def InfoTree.smallestInfo? (p : Info → Bool) (t : InfoTree) : Option (ContextI
 /-- Find an info node, if any, which should be shown on hover/cursor at position `hoverPos`. -/
 partial def InfoTree.hoverableInfoAt? (t : InfoTree) (hoverPos : String.Pos) (includeStop := false) (omitAppFns := false) (omitIdentApps := false) : Option InfoWithCtx := Id.run do
   let results := t.visitM (m := Id) (postNode := fun ctx info children results => do
-    let mut results := results.bind (·.getD [])
+    let mut results := results.flatMap (·.getD [])
     if omitAppFns && info.stx.isOfKind ``Parser.Term.app && info.stx[0].isIdent then
         results := results.filter (·.2.info.stx != info.stx[0])
     if omitIdentApps && info.stx.isIdent then

src/Lean/Server/Watchdog.lean

@@ -669,7 +669,7 @@ where
     let grouped := incomingCalls.groupByKey (·.«from»)
     let collapsed := grouped.toArray.map fun ⟨_, group⟩ => {
       «from» := group[0]!.«from»
-      fromRanges := group.concatMap (·.fromRanges)
+      fromRanges := group.flatMap (·.fromRanges)
     }
     collapsed
 
@@ -716,7 +716,7 @@ where
     let grouped := outgoingCalls.groupByKey (·.to)
     let collapsed := grouped.toArray.map fun ⟨_, group⟩ => {
       to := group[0]!.to
-      fromRanges := group.concatMap (·.fromRanges)
+      fromRanges := group.flatMap (·.fromRanges)
     }
     collapsed
 

src/Lean/ToExpr.lean

@@ -59,35 +59,35 @@ instance : ToExpr (BitVec n) where
 instance : ToExpr UInt8 where
   toTypeExpr := mkConst ``UInt8
   toExpr a :=
-    let r := mkRawNatLit a.val
+    let r := mkRawNatLit a.toNat
     mkApp3 (.const ``OfNat.ofNat [0]) (mkConst ``UInt8) r
       (.app (.const ``UInt8.instOfNat []) r)
 
 instance : ToExpr UInt16 where
   toTypeExpr := mkConst ``UInt16
   toExpr a :=
-    let r := mkRawNatLit a.val
+    let r := mkRawNatLit a.toNat
     mkApp3 (.const ``OfNat.ofNat [0]) (mkConst ``UInt16) r
       (.app (.const ``UInt16.instOfNat []) r)
 
 instance : ToExpr UInt32 where
   toTypeExpr := mkConst ``UInt32
   toExpr a :=
-    let r := mkRawNatLit a.val
+    let r := mkRawNatLit a.toNat
     mkApp3 (.const ``OfNat.ofNat [0]) (mkConst ``UInt32) r
       (.app (.const ``UInt32.instOfNat []) r)
 
 instance : ToExpr UInt64 where
   toTypeExpr := mkConst ``UInt64
   toExpr a :=
-    let r := mkRawNatLit a.val
+    let r := mkRawNatLit a.toNat
     mkApp3 (.const ``OfNat.ofNat [0]) (mkConst ``UInt64) r
       (.app (.const ``UInt64.instOfNat []) r)
 
 instance : ToExpr USize where
   toTypeExpr := mkConst ``USize
   toExpr a :=
-    let r := mkRawNatLit a.val
+    let r := mkRawNatLit a.toNat
     mkApp3 (.const ``OfNat.ofNat [0]) (mkConst ``USize) r
       (.app (.const ``USize.instOfNat []) r)
 

src/Std/Data/DHashMap/Internal/Defs.lean

@@ -156,7 +156,7 @@ namespace DHashMap.Internal
 
 /-- Internal implementation detail of the hash map -/
 def toListModel (buckets : Array (AssocList α β)) : List ((a : α) × β a) :=
-  buckets.toList.bind AssocList.toList
+  buckets.toList.flatMap AssocList.toList
 
 /-- Internal implementation detail of the hash map -/
 @[inline] def computeSize (buckets : Array (AssocList α β)) : Nat :=

src/Std/Data/DHashMap/Internal/Index.lean

@@ -54,9 +54,9 @@ cf. https://github.com/leanprover/lean4/issues/4157
         · exact Nat.one_pos
         · exact Nat.lt_of_le_of_lt h h'
       · exact h'
-      · rw [USize.le_def, Fin.le_def]
+      · rw [USize.le_def, BitVec.le_def]
         change _ ≤ (_ % _)
-        rw [Nat.mod_eq_of_lt h', USize.ofNat, Fin.val_ofNat', Nat.mod_eq_of_lt]
+        rw [Nat.mod_eq_of_lt h', USize.ofNat, BitVec.toNat_ofNat, Nat.mod_eq_of_lt]
         · exact h
         · exact Nat.lt_of_le_of_lt h h'
     · exact Nat.lt_of_lt_of_le (USize.toNat_lt_size _) (Nat.le_of_not_lt h')⟩

src/Std/Data/DHashMap/Internal/List/Associative.lean

@@ -1720,13 +1720,13 @@ theorem containsKey_append [BEq α] {l l' : List ((a : α) × β a)} {a : α} :
     containsKey a (l ++ l') = (containsKey a l || containsKey a l') := by
   simp [containsKey_eq_isSome_getEntry?]
 
-theorem containsKey_bind_eq_false [BEq α] {γ : Type w} {l : List γ} {f : γ → List ((a : α) × β a)}
+theorem containsKey_flatMap_eq_false [BEq α] {γ : Type w} {l : List γ} {f : γ → List ((a : α) × β a)}
     {a : α} (h : ∀ (i : Nat) (h : i < l.length), containsKey a (f l[i]) = false) :
-    containsKey a (l.bind f) = false := by
+    containsKey a (l.flatMap f) = false := by
   induction l
   · simp
   · next g t ih =>
-    simp only [List.bind_cons, containsKey_append, Bool.or_eq_false_iff]
+    simp only [List.flatMap_cons, containsKey_append, Bool.or_eq_false_iff]
     refine ⟨?_, ?_⟩
     · simpa using h 0 (by simp)
     · refine ih ?_

src/Std/Data/DHashMap/Internal/Model.lean

@@ -88,7 +88,7 @@ theorem exists_bucket_of_uset [BEq α] [Hashable α]
           containsKey k l = false) := by
   have h₀ : 0 < self.size := by omega
   obtain ⟨l₁, l₂, h₁, h₂, h₃⟩ := Array.exists_of_uset self i d hi
-  refine ⟨l₁.bind AssocList.toList ++ l₂.bind AssocList.toList, ?_, ?_, ?_⟩
+  refine ⟨l₁.flatMap AssocList.toList ++ l₂.flatMap AssocList.toList, ?_, ?_, ?_⟩
   · rw [toListModel, h₁]
     simpa using perm_append_comm_assoc _ _ _
   · rw [toListModel, h₃]
@@ -96,12 +96,12 @@ theorem exists_bucket_of_uset [BEq α] [Hashable α]
   · intro _ h k hki
     simp only [containsKey_append, Bool.or_eq_false_iff]
     refine ⟨?_, ?_⟩
-    · apply List.containsKey_bind_eq_false
+    · apply List.containsKey_flatMap_eq_false
       intro j hj
       rw [List.getElem_append_left' (l₂ := self[i] :: l₂), getElem_congr_coll h₁.symm]
       apply (h.hashes_to j _).containsKey_eq_false h₀ k
       omega
-    · apply List.containsKey_bind_eq_false
+    · apply List.containsKey_flatMap_eq_false
       intro j hj
       rw [← List.getElem_cons_succ self[i] _ _
         (by simp only [Array.ugetElem_eq_getElem, List.length_cons]; omega)]
@@ -121,7 +121,7 @@ theorem exists_bucket_of_update [BEq α] [Hashable α] (m : Array (AssocList α
 
 theorem exists_bucket' [BEq α] [Hashable α]
     (self : Array (AssocList α β)) (i : USize) (hi : i.toNat < self.size) :
-      ∃ l, Perm (self.toList.bind AssocList.toList) (self[i.toNat].toList ++ l) ∧
+      ∃ l, Perm (self.toList.flatMap AssocList.toList) (self[i.toNat].toList ++ l) ∧
         (∀ [LawfulHashable α], IsHashSelf self → ∀ k,
           (mkIdx self.size (by omega) (hash k)).1.toNat = i.toNat → containsKey k l = false) := by
   obtain ⟨l, h₁, -, h₂⟩ := exists_bucket_of_uset self i hi .nil
@@ -186,8 +186,8 @@ theorem toListModel_updateAllBuckets {m : Raw₀ α β} {f : AssocList α β →
     have := (hg (l := []) (l' := [])).length_eq
     rw [List.length_append, List.append_nil] at this
     omega
-  rw [updateAllBuckets, toListModel, Array.toList_map, List.bind_eq_foldl, List.foldl_map,
-    toListModel, List.bind_eq_foldl]
+  rw [updateAllBuckets, toListModel, Array.toList_map, List.flatMap_eq_foldl, List.foldl_map,
+    toListModel, List.flatMap_eq_foldl]
   suffices ∀ (l : List (AssocList α β)) (l' : List ((a: α) × δ a)) (l'' : List ((a : α) × β a)),
       Perm (g l'') l' →
       Perm (l.foldl (fun acc a => acc ++ (f a).toList) l')

src/Std/Data/DHashMap/Internal/WF.lean

@@ -31,14 +31,14 @@ namespace Std.DHashMap.Internal
 @[simp]
 theorem toListModel_mkArray_nil {c} :
     toListModel (mkArray c (AssocList.nil : AssocList α β)) = [] := by
-  suffices ∀ d, (List.replicate d AssocList.nil).bind AssocList.toList = [] from this _
+  suffices ∀ d, (List.replicate d AssocList.nil).flatMap AssocList.toList = [] from this _
   intro d
   induction d <;> simp_all [List.replicate]
 
 @[simp]
 theorem computeSize_eq {buckets : Array (AssocList α β)} :
     computeSize buckets = (toListModel buckets).length := by
-  rw [computeSize, toListModel, List.bind_eq_foldl, Array.foldl_eq_foldl_toList]
+  rw [computeSize, toListModel, List.flatMap_eq_foldl, Array.foldl_eq_foldl_toList]
   suffices ∀ (l : List (AssocList α β)) (l' : List ((a : α) × β a)),
       l.foldl (fun d b => d + b.toList.length) l'.length =
         (l.foldl (fun acc a => acc ++ a.toList) l').length
@@ -129,7 +129,7 @@ theorem expand.go_eq [BEq α] [Hashable α] [PartialEquivBEq α] (source : Array
     (target : {d : Array (AssocList α β) // 0 < d.size}) : expand.go 0 source target =
       (toListModel source).foldl (fun acc p => reinsertAux hash acc p.1 p.2) target := by
   suffices ∀ i, expand.go i source target =
-    ((source.toList.drop i).bind AssocList.toList).foldl
+    ((source.toList.drop i).flatMap AssocList.toList).foldl
       (fun acc p => reinsertAux hash acc p.1 p.2) target by
     simpa using this 0
   intro i
@@ -139,10 +139,10 @@ theorem expand.go_eq [BEq α] [Hashable α] [PartialEquivBEq α] (source : Array
     rw [expand.go_pos hi]
     refine ih.trans ?_
     simp only [Array.get_eq_getElem, AssocList.foldl_eq, Array.toList_set]
-    rw [List.drop_eq_getElem_cons hi, List.bind_cons, List.foldl_append,
+    rw [List.drop_eq_getElem_cons hi, List.flatMap_cons, List.foldl_append,
       List.drop_set_of_lt _ _ (by omega), Array.getElem_eq_getElem_toList]
   · next i source target hi =>
-    rw [expand.go_neg hi, List.drop_eq_nil_of_le, bind_nil, foldl_nil]
+    rw [expand.go_neg hi, List.drop_eq_nil_of_le, flatMap_nil, foldl_nil]
     rwa [Array.size_eq_length_toList, Nat.not_lt] at hi
 
 theorem isHashSelf_expand [BEq α] [Hashable α] [LawfulHashable α] [EquivBEq α]

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean

@@ -1112,7 +1112,7 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n)
   let li := derivedLits_arr[i]
   have li_in_derivedLits : li ∈ derivedLits := by
     rw [Array.mem_toList, ← derivedLits_arr_def]
-    simp only [li, Array.getElem?_mem]
+    simp [li, Array.getElem_mem]
   have i_in_bounds : i.1 < derivedLits.length := by
     have i_property := i.2
     simp only [derivedLits_arr_def, Array.size_mk] at i_property

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean

@@ -570,7 +570,7 @@ theorem reduce_postcondition {n : Nat} (c : DefaultClause n) (assignment : Array
         rw [c_clause_rw] at pc1
         have idx_exists : ∃ idx : Fin c_arr.size, c_arr[idx] = (i, false) := by
           rcases List.get_of_mem pc1 with ⟨idx, hidx⟩
-          rw [← Array.getElem_fin_eq_toList_get] at hidx
+          simp only [List.get_eq_getElem] at hidx
           exact Exists.intro idx hidx
         rcases idx_exists with ⟨idx, hidx⟩
         specialize h1 idx idx.2
@@ -580,7 +580,7 @@ theorem reduce_postcondition {n : Nat} (c : DefaultClause n) (assignment : Array
         rw [c_clause_rw] at pc1
         have idx_exists : ∃ idx : Fin c_arr.size, c_arr[idx] = (i, true) := by
           rcases List.get_of_mem pc1 with ⟨idx, hidx⟩
-          rw [← Array.getElem_fin_eq_toList_get] at hidx
+          simp only [List.get_eq_getElem] at hidx
           exact Exists.intro idx hidx
         rcases idx_exists with ⟨idx, hidx⟩
         specialize h1 idx idx.2
@@ -595,7 +595,7 @@ theorem reduce_postcondition {n : Nat} (c : DefaultClause n) (assignment : Array
       rw [c_clause_rw] at pc1
       have idx_exists : ∃ idx : Fin c_arr.size, c_arr[idx] = (i, false) := by
         rcases List.get_of_mem pc1 with ⟨idx, hidx⟩
-        rw [← Array.getElem_fin_eq_toList_get] at hidx
+        simp only [List.get_eq_getElem] at hidx
         exact Exists.intro idx hidx
       rcases idx_exists with ⟨idx, hidx⟩
       apply Exists.intro idx ∘ And.intro idx.2
@@ -606,7 +606,7 @@ theorem reduce_postcondition {n : Nat} (c : DefaultClause n) (assignment : Array
       rw [c_clause_rw] at pc1
       have idx_exists : ∃ idx : Fin c_arr.size, c_arr[idx] = (i, true) := by
         rcases List.get_of_mem pc1 with ⟨idx, hidx⟩
-        rw [← Array.getElem_fin_eq_toList_get] at hidx
+        simp only [List.get_eq_getElem] at hidx
         exact Exists.intro idx hidx
       rcases idx_exists with ⟨idx, hidx⟩
       apply Exists.intro idx ∘ And.intro idx.2

src/Std/Tactic/BVDecide/Normalize/Canonicalize.lean

@@ -81,8 +81,7 @@ attribute [bv_normalize] BitVec.testBit_toNat
 @[bv_normalize]
 theorem BitVec.lt_ult (x y : BitVec w) : (x < y) = (BitVec.ult x y = true) := by
   rw [BitVec.ult]
-  rw [LT.lt]
-  rw [BitVec.instLT]
+  simp only [(· < ·)]
   simp
 
 attribute [bv_normalize] BitVec.natCast_eq_ofNat

src/lake/Lake/Build/Imports.lean

@@ -29,7 +29,7 @@ def buildImportsAndDeps (leanFile : FilePath) (imports : Array Module) : FetchM
     let precompileImports ← computePrecompileImportsAux leanFile imports
     let pkgs := precompileImports.foldl (·.insert ·.pkg) OrdPackageSet.empty |>.toArray
     let externLibJob ← BuildJob.collectArray <| ←
-      pkgs.concatMapM (·.externLibs.mapM (·.dynlib.fetch))
+      pkgs.flatMapM (·.externLibs.mapM (·.dynlib.fetch))
     let precompileJob ← BuildJob.collectArray <| ←
       precompileImports.mapM (·.dynlib.fetch)
     let job ←

src/lake/Lake/Build/Library.lean

@@ -60,7 +60,7 @@ def LeanLib.leanArtsFacetConfig : LibraryFacetConfig leanArtsFacet :=
       ""
   withRegisterJob s!"{self.name}:static{suffix}" do
   let mods ← self.modules.fetch
-  let oJobs ← mods.concatMapM fun mod =>
+  let oJobs ← mods.flatMapM fun mod =>
     mod.nativeFacets shouldExport |>.mapM fun facet => fetch <| mod.facet facet.name
   let libFile := if shouldExport then self.staticExportLibFile else self.staticLibFile
   buildStaticLib libFile oJobs
@@ -80,10 +80,10 @@ protected def LeanLib.recBuildShared
 (self : LeanLib) : FetchM (BuildJob FilePath) := do
   withRegisterJob s!"{self.name}:shared" do
   let mods ← self.modules.fetch
-  let oJobs ← mods.concatMapM fun mod =>
+  let oJobs ← mods.flatMapM fun mod =>
     mod.nativeFacets true |>.mapM fun facet => fetch <| mod.facet facet.name
   let pkgs := mods.foldl (·.insert ·.pkg) OrdPackageSet.empty |>.toArray
-  let externJobs ← pkgs.concatMapM (·.externLibs.mapM (·.shared.fetch))
+  let externJobs ← pkgs.flatMapM (·.externLibs.mapM (·.shared.fetch))
   buildLeanSharedLib self.sharedLibFile (oJobs ++ externJobs) self.weakLinkArgs self.linkArgs
 
 /-- The `LibraryFacetConfig` for the builtin `sharedFacet`. -/

src/lake/Lake/CLI/Build.lean

@@ -113,7 +113,7 @@ def resolveTargetInPackage (ws : Workspace)
     throw <| CliError.missingTarget pkg.name (target.toString false)
 
 def resolveDefaultPackageTarget (ws : Workspace) (pkg : Package) : Except CliError (Array BuildSpec) :=
-  pkg.defaultTargets.concatMapM (resolveTargetInPackage ws pkg · .anonymous)
+  pkg.defaultTargets.flatMapM (resolveTargetInPackage ws pkg · .anonymous)
 
 def resolvePackageTarget (ws : Workspace) (pkg : Package) (facet : Name) : Except CliError (Array BuildSpec) :=
   if facet.isAnonymous then

src/lake/Lake/Util/Compare.lean

@@ -64,7 +64,7 @@ instance : LawfulCmpEq Nat compare where
 
 instance : LawfulCmpEq UInt64 compare where
   eq_of_cmp h := eq_of_compareOfLessAndEq h
-  cmp_rfl := compareOfLessAndEq_rfl <| Nat.lt_irrefl _
+  cmp_rfl := compareOfLessAndEq_rfl <| UInt64.lt_irrefl _
 
 instance : LawfulCmpEq String compare where
   eq_of_cmp := eq_of_compareOfLessAndEq

src/lake/Lake/Util/OrderedTagAttribute.lean

@@ -47,4 +47,4 @@ def OrderedTagAttribute.hasTag (attr : OrderedTagAttribute) (env : Environment)
 /-- Get all tagged declaration names, both those imported and those in the current module. -/
 def OrderedTagAttribute.getAllEntries (attr : OrderedTagAttribute) (env : Environment) : Array Name :=
   let s := attr.ext.toEnvExtension.getState env
-  s.importedEntries.concatMap id ++ s.state
+  s.importedEntries.flatMap id ++ s.state