chore: minor

Co-authored-by: Kim Morrison <scott.morrison@gmail.com>

doc/dev/ffi.md

@@ -49,8 +49,9 @@ In the case of `@[extern]` all *irrelevant* types are removed first; see next se
   is represented by the representation of that parameter's type.
 
   For example, `{ x : α // p }`, the `Subtype` structure of a value of type `α` and an irrelevant proof, is represented by the representation of `α`.
-* `Nat` is represented by `lean_object *`.
-  Its runtime value is either a pointer to an opaque bignum object or, if the lowest bit of the "pointer" is 1 (`lean_is_scalar`), an encoded unboxed natural number (`lean_box`/`lean_unbox`).
+  Similarly, the signed integer types `Int8`, ..., `Int64`, `ISize` are also represented by the unsigned C types `uint8_t`, ..., `uint64_t`, `size_t`, respectively, because they have a trivial structure.
+* `Nat` and `Int` are represented by `lean_object *`.
+  Their runtime values is either a pointer to an opaque bignum object or, if the lowest bit of the "pointer" is 1 (`lean_is_scalar`), an encoded unboxed natural number or integer (`lean_box`/`lean_unbox`).
 * A universe `Sort u`, type constructor `... → Sort u`, or proposition `p : Prop` is *irrelevant* and is either statically erased (see above) or represented as a `lean_object *` with the runtime value `lean_box(0)`
 * Any other type is represented by `lean_object *`.
   Its runtime value is a pointer to an object of a subtype of `lean_object` (see the "Inductive types" section below) or the unboxed value `lean_box(cidx)` for the `cidx`th constructor of an inductive type if this constructor does not have any relevant parameters.

doc/dev/release_checklist.md

@@ -37,16 +37,32 @@ We'll use `v4.6.0` as the intended release version as a running example.
     - Create the tag `v4.6.0` from `master`/`main` and push it.
     - Merge the tag `v4.6.0` into the `stable` branch and push it.
   - We do this for the repositories:
-    - [lean4checker](https://github.com/leanprover/lean4checker)
-      - No dependencies
-      - Toolchain bump PR
-      - Create and push the tag
-      - Merge the tag into `stable`
     - [Batteries](https://github.com/leanprover-community/batteries)
       - No dependencies
       - Toolchain bump PR
       - Create and push the tag
       - Merge the tag into `stable`
+    - [lean4checker](https://github.com/leanprover/lean4checker)
+      - No dependencies
+      - Toolchain bump PR
+      - Create and push the tag
+      - Merge the tag into `stable`
+    - [doc-gen4](https://github.com/leanprover/doc-gen4)
+      - Dependencies: exist, but they're not part of the release workflow
+      - Toolchain bump PR including updated Lake manifest
+      - Create and push the tag
+      - There is no `stable` branch; skip this step
+    - [Verso](https://github.com/leanprover/verso)
+      - Dependencies: exist, but they're not part of the release workflow
+      - The `SubVerso` dependency should be compatible with _every_ Lean release simultaneously, rather than following this workflow
+      - Toolchain bump PR including updated Lake manifest
+      - Create and push the tag
+      - There is no `stable` branch; skip this step
+    - [Cli](https://github.com/leanprover/lean4-cli)
+      - No dependencies
+      - Toolchain bump PR
+      - Create and push the tag
+      - There is no `stable` branch; skip this step
     - [ProofWidgets4](https://github.com/leanprover-community/ProofWidgets4)
       - Dependencies: `Batteries`
       - Note on versions and branches:
@@ -61,17 +77,6 @@ We'll use `v4.6.0` as the intended release version as a running example.
       - Toolchain bump PR including updated Lake manifest
       - Create and push the tag
       - Merge the tag into `stable`
-    - [doc-gen4](https://github.com/leanprover/doc-gen4)
-      - Dependencies: exist, but they're not part of the release workflow
-      - Toolchain bump PR including updated Lake manifest
-      - Create and push the tag
-      - There is no `stable` branch; skip this step
-    - [Verso](https://github.com/leanprover/verso)
-      - Dependencies: exist, but they're not part of the release workflow
-      - The `SubVerso` dependency should be compatible with _every_ Lean release simultaneously, rather than following this workflow
-      - Toolchain bump PR including updated Lake manifest
-      - Create and push the tag
-      - There is no `stable` branch; skip this step
     - [import-graph](https://github.com/leanprover-community/import-graph)
       - Toolchain bump PR including updated Lake manifest
       - Create and push the tag

script/release_repos.yml

@@ -27,6 +27,13 @@ repositories:
     branch: main
     dependencies: []
 
+  - name: Cli
+    url: https://github.com/leanprover/lean4-cli
+    toolchain-tag: true
+    stable-branch: false
+    branch: main
+    dependencies: []
+
   - name: ProofWidgets4
     url: https://github.com/leanprover-community/ProofWidgets4
     toolchain-tag: false

src/Init/Conv.lean

@@ -150,6 +150,10 @@ See the `simp` tactic for more information. -/
 syntax (name := simp) "simp" optConfig (discharger)? (&" only")?
   (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*) "]")? : conv
 
+/-- `simp?` takes the same arguments as `simp`, but reports an equivalent call to `simp only`
+that would be sufficient to close the goal. See the `simp?` tactic for more information. -/
+syntax (name := simpTrace) "simp?" optConfig (discharger)? (&" only")? (simpArgs)? : conv
+
 /--
 `dsimp` is the definitional simplifier in `conv`-mode. It differs from `simp` in that it only
 applies theorems that hold by reflexivity.
@@ -167,6 +171,9 @@ example (a : Nat): (0 + 0) = a - a := by
 syntax (name := dsimp) "dsimp" optConfig (discharger)? (&" only")?
   (" [" withoutPosition((simpErase <|> simpLemma),*) "]")? : conv
 
+@[inherit_doc simpTrace]
+syntax (name := dsimpTrace) "dsimp?" optConfig (&" only")? (dsimpArgs)? : conv
+
 /-- `simp_match` simplifies match expressions. For example,
 ```
 match [a, b] with

src/Init/Data/Array/Basic.lean

@@ -244,8 +244,7 @@ def ofFn {n} (f : Fin n → α) : Array α := go 0 (mkEmpty n) where
 def range (n : Nat) : Array Nat :=
   ofFn fun (i : Fin n) => i
 
-def singleton (v : α) : Array α :=
-  mkArray 1 v
+@[inline] protected def singleton (v : α) : Array α := #[v]
 
 def back! [Inhabited α] (a : Array α) : α :=
   a[a.size - 1]!

src/Init/Data/Array/Lemmas.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2022 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mario Carneiro
+Authors: Mario Carneiro, Kim Morrison
 -/
 prelude
 import Init.Data.Nat.Lemmas
@@ -124,6 +124,8 @@ theorem push_eq_push {a b : α} {xs ys : Array α} : xs.push a = ys.push b ↔ a
   · rintro ⟨rfl, rfl⟩
     rfl
 
+theorem push_eq_append_singleton (as : Array α) (x) : as.push x = as ++ #[x] := rfl
+
 theorem exists_push_of_ne_empty {xs : Array α} (h : xs ≠ #[]) :
     ∃ (ys : Array α) (a : α), xs = ys.push a := by
   rcases xs with ⟨xs⟩
@@ -1001,8 +1003,6 @@ private theorem beq_of_beq_singleton [BEq α] {a b : α} : #[a] == #[b] → a ==
   cases l₂
   simp
 
-/-! Content below this point has not yet been aligned with `List`. -/
-
 /-! ### map -/
 
 theorem mapM_eq_foldlM [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) :
@@ -1036,11 +1036,6 @@ where
   simp only [← length_toList]
   simp
 
-@[simp] theorem mapM_empty [Monad m] (f : α → m β) : mapM f #[] = pure #[] := by
-  rw [mapM, mapM.map]; rfl
-
-@[simp] theorem map_empty (f : α → β) : map f #[] = #[] := mapM_empty f
-
 @[simp] theorem getElem_map (f : α → β) (a : Array α) (i : Nat) (hi : i < (a.map f).size) :
     (a.map f)[i] = f (a[i]'(by simpa using hi)) := by
   cases a
@@ -1050,6 +1045,18 @@ where
     (as.map f)[i]? = as[i]?.map f := by
   simp [getElem?_def]
 
+@[simp] theorem mapM_empty [Monad m] (f : α → m β) : mapM f #[] = pure #[] := by
+  rw [mapM, mapM.map]; rfl
+
+@[simp] theorem map_empty (f : α → β) : map f #[] = #[] := mapM_empty f
+
+@[simp] theorem map_push {f : α → β} {as : Array α} {x : α} :
+    (as.push x).map f = (as.map f).push (f x) := by
+  ext
+  · simp
+  · simp only [getElem_map, getElem_push, size_map]
+    split <;> rfl
+
 @[simp] theorem map_id_fun : map (id : α → α) = id := by
   funext l
   induction l <;> simp_all
@@ -1100,17 +1107,59 @@ theorem map_inj : map f = map g ↔ f = g := by
 theorem eq_empty_of_map_eq_empty {f : α → β} {l : Array α} (h : map f l = #[]) : l = #[] :=
   map_eq_empty_iff.mp h
 
+theorem map_eq_push_iff {f : α → β} {l : Array α} {l₂ : Array β} {b : β} :
+    map f l = l₂.push b ↔ ∃ l₁ a, l = l₁.push a ∧ map f l₁ = l₂ ∧ f a = b := by
+  rcases l with ⟨l⟩
+  rcases l₂ with ⟨l₂⟩
+  simp only [List.map_toArray, List.push_toArray, mk.injEq, List.map_eq_append_iff]
+  constructor
+  · rintro ⟨l₁, l₂, rfl, rfl, h⟩
+    simp only [List.map_eq_singleton_iff] at h
+    obtain ⟨a, rfl, rfl⟩ := h
+    refine ⟨l₁.toArray, a, by simp⟩
+  · rintro ⟨⟨l₁⟩, a, h₁, h₂, rfl⟩
+    refine ⟨l₁, [a], by simp_all⟩
+
+@[simp] theorem map_eq_singleton_iff {f : α → β} {l : Array α} {b : β} :
+    map f l = #[b] ↔ ∃ a, l = #[a] ∧ f a = b := by
+  cases l
+  simp
+
+theorem map_eq_map_iff {f g : α → β} {l : Array α} :
+    map f l = map g l ↔ ∀ a ∈ l, f a = g a := by
+  cases l <;> simp_all
+
+theorem map_eq_iff : map f l = l' ↔ ∀ i : Nat, l'[i]? = l[i]?.map f := by
+  cases l
+  cases l'
+  simp [List.map_eq_iff]
+
+theorem map_eq_foldl (f : α → β) (l : Array α) :
+    map f l = foldl (fun bs a => bs.push (f a)) #[] l := by
+  simpa using mapM_eq_foldlM (m := Id) f l
+
+@[simp] theorem map_set {f : α → β} {l : Array α} {i : Nat} {h : i < l.size} {a : α} :
+    (l.set i a).map f = (l.map f).set i (f a) (by simpa using h) := by
+  cases l
+  simp
+
+@[simp] theorem map_setIfInBounds {f : α → β} {l : Array α} {i : Nat} {a : α} :
+    (l.setIfInBounds i a).map f = (l.map f).setIfInBounds i (f a) := by
+  cases l
+  simp
+
+@[simp] theorem map_pop {f : α → β} {l : Array α} : l.pop.map f = (l.map f).pop := by
+  cases l
+  simp
+
+@[simp] theorem back?_map {f : α → β} {l : Array α} : (l.map f).back? = l.back?.map f := by
+  cases l
+  simp
+
 @[simp] theorem map_map {f : α → β} {g : β → γ} {as : Array α} :
     (as.map f).map g = as.map (g ∘ f) := by
   cases as; simp
 
-@[simp] theorem map_push {f : α → β} {as : Array α} {x : α} :
-    (as.push x).map f = (as.map f).push (f x) := by
-  ext
-  · simp
-  · simp only [getElem_map, getElem_push, size_map]
-    split <;> rfl
-
 theorem mapM_eq_mapM_toList [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) :
     arr.mapM f = List.toArray <$> (arr.toList.mapM f) := by
   rw [mapM_eq_foldlM, ← foldlM_toList, ← List.foldrM_reverse]
@@ -1123,6 +1172,7 @@ 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 "Use `mapM_eq_foldlM` instead" (since := "2025-01-08")]
 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
@@ -1139,13 +1189,416 @@ theorem mapM_map_eq_foldl (as : Array α) (f : α → β) (i) :
     rfl
 termination_by as.size - i
 
-theorem map_eq_foldl (as : Array α) (f : α → β) :
-    as.map f = as.foldl (fun r a => r.push (f a)) #[] :=
-  mapM_map_eq_foldl _ _ _
+/-! ### filter -/
+
+@[congr]
+theorem filter_congr {as bs : Array α} (h : as = bs)
+    {f : α → Bool} {g : α → Bool} (h' : f = g) {start stop start' stop' : Nat}
+    (h₁ : start = start') (h₂ : stop = stop') :
+    filter f as start stop = filter g bs start' stop' := by
+  congr
+
+@[simp] theorem toList_filter' (p : α → Bool) (l : Array α) (h : stop = l.size) :
+    (l.filter p 0 stop).toList = l.toList.filter p := by
+  subst h
+  dsimp only [filter]
+  rw [← foldl_toList]
+  generalize l.toList = l
+  suffices ∀ a, (List.foldl (fun r a => if p a = true then push r a else r) a l).toList =
+      a.toList ++ List.filter p l by
+    simpa using this #[]
+  induction l with simp
+  | cons => split <;> simp [*]
+
+theorem toList_filter (p : α → Bool) (l : Array α) :
+    (l.filter p).toList = l.toList.filter p := by
+  simp
+
+@[simp] theorem _root_.List.filter_toArray' (p : α → Bool) (l : List α) (h : stop = l.length) :
+    l.toArray.filter p 0 stop = (l.filter p).toArray := by
+  apply ext'
+  simp [h]
+
+theorem _root_.List.filter_toArray (p : α → Bool) (l : List α) :
+    l.toArray.filter p = (l.filter p).toArray := by
+  simp
+
+@[simp] theorem filter_push_of_pos {p : α → Bool} {a : α} {l : Array α}
+    (h : p a) (w : stop = l.size + 1):
+    (l.push a).filter p 0 stop = (l.filter p).push a := by
+  subst w
+  rcases l with ⟨l⟩
+  simp [h]
+
+@[simp] theorem filter_push_of_neg {p : α → Bool} {a : α} {l : Array α}
+    (h : ¬p a) (w : stop = l.size + 1) :
+    (l.push a).filter p 0 stop = l.filter p := by
+  subst w
+  rcases l with ⟨l⟩
+  simp [h]
+
+theorem filter_push {p : α → Bool} {a : α} {l : Array α} :
+    (l.push a).filter p = if p a then (l.filter p).push a else l.filter p := by
+  split <;> simp [*]
+
+theorem size_filter_le (p : α → Bool) (l : Array α) :
+    (l.filter p).size ≤ l.size := by
+  rcases l with ⟨l⟩
+  simpa using List.length_filter_le p l
+
+@[simp] theorem filter_eq_self {p : α → Bool} {l : Array α} :
+    filter p l = l ↔ ∀ a ∈ l, p a := by
+  rcases l with ⟨l⟩
+  simp
+
+@[simp] theorem filter_size_eq_size {p : α → Bool} {l : Array α} :
+    (filter p l).size = l.size ↔ ∀ a ∈ l, p a := by
+  rcases l with ⟨l⟩
+  simp
+
+@[simp] theorem mem_filter {p : α → Bool} {l : Array α} {a : α} :
+    a ∈ filter p l ↔ a ∈ l ∧ p a := by
+  rcases l with ⟨l⟩
+  simp
+
+@[simp] theorem filter_eq_empty_iff {p : α → Bool} {l : Array α} :
+    filter p l = #[] ↔ ∀ a, a ∈ l → ¬p a := by
+  rcases l with ⟨l⟩
+  simp
+
+theorem forall_mem_filter {p : α → Bool} {l : Array α} {P : α → Prop} :
+    (∀ (i) (_ : i ∈ l.filter p), P i) ↔ ∀ (j) (_ : j ∈ l), p j → P j := by
+  simp
+
+@[simp] theorem filter_filter (q) (l : Array α) :
+    filter p (filter q l) = filter (fun a => p a && q a) l := by
+  apply ext'
+  simp only [toList_filter, List.filter_filter]
+
+theorem foldl_filter (p : α → Bool) (f : β → α → β) (l : Array α) (init : β) :
+    (l.filter p).foldl f init = l.foldl (fun x y => if p y then f x y else x) init := by
+  rcases l with ⟨l⟩
+  rw [List.filter_toArray]
+  simp [List.foldl_filter]
+
+theorem foldr_filter (p : α → Bool) (f : α → β → β) (l : Array α) (init : β) :
+    (l.filter p).foldr f init = l.foldr (fun x y => if p x then f x y else y) init := by
+  rcases l with ⟨l⟩
+  rw [List.filter_toArray]
+  simp [List.foldr_filter]
+
+theorem filter_map (f : β → α) (l : Array β) : filter p (map f l) = map f (filter (p ∘ f) l) := by
+  rcases l with ⟨l⟩
+  simp [List.filter_map]
+
+theorem map_filter_eq_foldl (f : α → β) (p : α → Bool) (l : Array α) :
+    map f (filter p l) = foldl (fun y x => bif p x then y.push (f x) else y) #[] l := by
+  rcases l with ⟨l⟩
+  apply ext'
+  simp only [size_toArray, List.filter_toArray', List.map_toArray, List.foldl_toArray']
+  rw [← List.reverse_reverse l]
+  generalize l.reverse = l
+  simp only [List.filter_reverse, List.map_reverse, List.foldl_reverse]
+  induction l with
+  | nil => rfl
+  | cons x l ih =>
+    simp only [List.filter_cons, List.foldr_cons]
+    split <;> simp_all
+
+@[simp] theorem filter_append {p : α → Bool} (l₁ l₂ : Array α) :
+    filter p (l₁ ++ l₂) = filter p l₁ ++ filter p l₂ := by
+  rcases l₁ with ⟨l₁⟩
+  rcases l₂ with ⟨l₂⟩
+  simp [List.filter_append]
+
+theorem filter_eq_append_iff {p : α → Bool} :
+    filter p l = L₁ ++ L₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ filter p l₁ = L₁ ∧ filter p l₂ = L₂ := by
+  rcases l with ⟨l⟩
+  rcases L₁ with ⟨L₁⟩
+  rcases L₂ with ⟨L₂⟩
+  simp only [size_toArray, List.filter_toArray', List.append_toArray, mk.injEq,
+    List.filter_eq_append_iff]
+  constructor
+  · rintro ⟨l₁, l₂, rfl, rfl, rfl⟩
+    refine ⟨l₁.toArray, l₂.toArray, by simp⟩
+  · rintro ⟨⟨l₁⟩, ⟨l₂⟩, h₁, h₂, h₃⟩
+    refine ⟨l₁, l₂, by simp_all⟩
+
+theorem filter_eq_push_iff {p : α → Bool} {l l' : Array α} {a : α} :
+    filter p l = l'.push a ↔
+      ∃ l₁ l₂, l = l₁.push a ++ l₂ ∧ filter p l₁ = l' ∧ p a ∧ (∀ x, x ∈ l₂ → ¬p x) := by
+  rcases l with ⟨l⟩
+  rcases l' with ⟨l'⟩
+  simp only [size_toArray, List.filter_toArray', List.push_toArray, mk.injEq, Bool.not_eq_true]
+  rw [← List.reverse_inj]
+  simp only [← List.filter_reverse]
+  simp only [List.reverse_append, List.reverse_cons, List.reverse_nil, List.nil_append,
+    List.singleton_append]
+  rw [List.filter_eq_cons_iff]
+  constructor
+  · rintro ⟨l₁, l₂, h₁, h₂, h₃, h₄⟩
+    refine ⟨l₂.reverse.toArray, l₁.reverse.toArray, by simp_all⟩
+  · rintro ⟨⟨l₁⟩, ⟨l₂⟩, h₁, h₂, h₃, h₄⟩
+    refine ⟨l₂.reverse, l₁.reverse, by simp_all⟩
+
+@[deprecated filter_map (since := "2024-06-15")] abbrev map_filter := @filter_map
+
+theorem mem_of_mem_filter {a : α} {l} (h : a ∈ filter p l) : a ∈ l :=
+  (mem_filter.mp h).1
+
+/-! ### filterMap -/
+
+@[congr]
+theorem filterMap_congr {as bs : Array α} (h : as = bs)
+    {f : α → Option β} {g : α → Option β} (h' : f = g) {start stop start' stop' : Nat}
+    (h₁ : start = start') (h₂ : stop = stop') :
+    filterMap f as start stop = filterMap g bs start' stop' := by
+  congr
+
+@[simp] theorem toList_filterMap' (f : α → Option β) (l : Array α) (w : stop = l.size) :
+    (l.filterMap f 0 stop).toList = l.toList.filterMap f := by
+  subst w
+  dsimp only [filterMap, filterMapM]
+  rw [← foldlM_toList]
+  generalize l.toList = l
+  have this : ∀ a : Array β, (Id.run (List.foldlM (m := Id) ?_ a l)).toList =
+    a.toList ++ List.filterMap f l := ?_
+  exact this #[]
+  induction l
+  · simp_all [Id.run]
+  · simp_all [Id.run, List.filterMap_cons]
+    split <;> simp_all
+
+theorem toList_filterMap (f : α → Option β) (l : Array α) :
+    (l.filterMap f).toList = l.toList.filterMap f := by
+  simp [toList_filterMap']
+
+
+@[simp] theorem _root_.List.filterMap_toArray' (f : α → Option β) (l : List α) (h : stop = l.length) :
+    l.toArray.filterMap f 0 stop = (l.filterMap f).toArray := by
+  apply ext'
+  simp [h]
+
+theorem _root_.List.filterMap_toArray (f : α → Option β) (l : List α) :
+    l.toArray.filterMap f = (l.filterMap f).toArray := by
+  simp
+
+@[simp] theorem filterMap_push_none {f : α → Option β} {a : α} {l : Array α}
+    (h : f a = none) (w : stop = l.size + 1) :
+    filterMap f (l.push a) 0 stop = filterMap f l := by
+  subst w
+  rcases l with ⟨l⟩
+  simp [h]
+
+@[simp] theorem filterMap_push_some {f : α → Option β} {a : α} {l : Array α} {b : β}
+    (h : f a = some b) (w : stop = l.size + 1) :
+    filterMap f (l.push a) 0 stop = (filterMap f l).push b := by
+  subst w
+  rcases l with ⟨l⟩
+  simp [h]
+
+@[simp] theorem filterMap_eq_map (f : α → β) : filterMap (some ∘ f) = map f := by
+  funext l
+  cases l
+  simp
+
+theorem filterMap_some_fun : filterMap (some : α → Option α) = id := by
+  funext l
+  cases l
+  simp
+
+@[simp] theorem filterMap_some (l : Array α) : filterMap some l = l := by
+  cases l
+  simp
+
+theorem map_filterMap_some_eq_filterMap_isSome (f : α → Option β) (l : Array α) :
+    (l.filterMap f).map some = (l.map f).filter fun b => b.isSome := by
+  cases l
+  simp [List.map_filterMap_some_eq_filter_map_isSome]
+
+theorem size_filterMap_le (f : α → Option β) (l : Array α) :
+    (filterMap f l).size ≤ l.size := by
+  cases l
+  simp [List.length_filterMap_le]
+
+@[simp] theorem filterMap_size_eq_size {l} :
+    (filterMap f l).size = l.size ↔ ∀ a, a ∈ l → (f a).isSome := by
+  cases l
+  simp [List.filterMap_length_eq_length]
+
+@[simp]
+theorem filterMap_eq_filter (p : α → Bool) :
+    filterMap (Option.guard (p ·)) = filter p := by
+  funext l
+  cases l
+  simp
+
+theorem filterMap_filterMap (f : α → Option β) (g : β → Option γ) (l : Array α) :
+    filterMap g (filterMap f l) = filterMap (fun x => (f x).bind g) l := by
+  cases l
+  simp [List.filterMap_filterMap]
+
+theorem map_filterMap (f : α → Option β) (g : β → γ) (l : Array α) :
+    map g (filterMap f l) = filterMap (fun x => (f x).map g) l := by
+  cases l
+  simp [List.map_filterMap]
+
+@[simp] theorem filterMap_map (f : α → β) (g : β → Option γ) (l : Array α) :
+    filterMap g (map f l) = filterMap (g ∘ f) l := by
+  cases l
+  simp [List.filterMap_map]
+
+theorem filter_filterMap (f : α → Option β) (p : β → Bool) (l : Array α) :
+    filter p (filterMap f l) = filterMap (fun x => (f x).filter p) l := by
+  cases l
+  simp [List.filter_filterMap]
+
+theorem filterMap_filter (p : α → Bool) (f : α → Option β) (l : Array α) :
+    filterMap f (filter p l) = filterMap (fun x => if p x then f x else none) l := by
+  cases l
+  simp [List.filterMap_filter]
+
+@[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]
+
+theorem forall_mem_filterMap {f : α → Option β} {l : Array α} {P : β → Prop} :
+    (∀ (i) (_ : i ∈ filterMap f l), P i) ↔ ∀ (j) (_ : j ∈ l) (b), f j = some b → P b := by
+  simp only [mem_filterMap, forall_exists_index, and_imp]
+  rw [forall_comm]
+  apply forall_congr'
+  intro a
+  rw [forall_comm]
+
+@[simp] theorem filterMap_append {α β : Type _} (l l' : Array α) (f : α → Option β) :
+    filterMap f (l ++ l') = filterMap f l ++ filterMap f l' := by
+  cases l
+  cases l'
+  simp
+
+theorem map_filterMap_of_inv (f : α → Option β) (g : β → α) (H : ∀ x : α, (f x).map g = some x)
+    (l : Array α) : map g (filterMap f l) = l := by simp only [map_filterMap, H, filterMap_some, id]
+
+theorem forall_none_of_filterMap_eq_empty (h : filterMap f xs = #[]) : ∀ x ∈ xs, f x = none := by
+  cases xs
+  simpa using h
+
+@[simp] theorem filterMap_eq_nil_iff {l} : filterMap f l = #[] ↔ ∀ a, a ∈ l → f a = none := by
+  cases l
+  simp
+
+theorem filterMap_eq_push_iff {f : α → Option β} {l : Array α} {l' : Array β} {b : β} :
+    filterMap f l = l'.push b ↔ ∃ l₁ a l₂,
+      l = l₁.push a ++ l₂ ∧ filterMap f l₁ = l' ∧ f a = some b ∧ (∀ x, x ∈ l₂ → f x = none) := by
+  rcases l with ⟨l⟩
+  rcases l' with ⟨l'⟩
+  simp only [size_toArray, List.filterMap_toArray', List.push_toArray, mk.injEq]
+  rw [← List.reverse_inj]
+  simp only [← List.filterMap_reverse]
+  simp only [List.reverse_append, List.reverse_cons, List.reverse_nil, List.nil_append,
+    List.singleton_append]
+  rw [List.filterMap_eq_cons_iff]
+  constructor
+  · rintro ⟨l₁, a, l₂, h₁, h₂, h₃, h₄⟩
+    refine ⟨l₂.reverse.toArray, a, l₁.reverse.toArray, by simp_all⟩
+  · rintro ⟨⟨l₁⟩, a, ⟨l₂⟩, h₁, h₂, h₃, h₄⟩
+    refine ⟨l₂.reverse, a, l₁.reverse, by simp_all⟩
+
+/-! Content below this point has not yet been aligned with `List`. -/
+
+/-! ### singleton -/
+
+@[simp] theorem singleton_def (v : α) : Array.singleton v = #[v] := rfl
+
+/-! ### append -/
+
+@[simp] theorem toArray_eq_append_iff {xs : List α} {as bs : Array α} :
+    xs.toArray = as ++ bs ↔ xs = as.toList ++ bs.toList := by
+  cases as
+  cases bs
+  simp
+
+@[simp] theorem append_eq_toArray_iff {as bs : Array α} {xs : List α} :
+    as ++ bs = xs.toArray ↔ as.toList ++ bs.toList = xs := by
+  cases as
+  cases bs
+  simp
 
 theorem singleton_eq_toArray_singleton (a : α) : #[a] = [a].toArray := rfl
 
-@[simp] theorem singleton_def (v : α) : singleton v = #[v] := rfl
+@[simp] theorem empty_append_fun : ((#[] : Array α) ++ ·) = id := by
+  funext ⟨l⟩
+  simp
+
+@[simp] theorem mem_append {a : α} {s t : Array α} : a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t := by
+  simp only [mem_def, toList_append, List.mem_append]
+
+theorem mem_append_left {a : α} {l₁ : Array α} (l₂ : Array α) (h : a ∈ l₁) : a ∈ l₁ ++ l₂ :=
+  mem_append.2 (Or.inl h)
+
+theorem mem_append_right {a : α} (l₁ : Array α) {l₂ : Array α} (h : a ∈ l₂) : a ∈ l₁ ++ l₂ :=
+  mem_append.2 (Or.inr h)
+
+@[simp] theorem size_append (as bs : Array α) : (as ++ bs).size = as.size + bs.size := by
+  simp only [size, toList_append, List.length_append]
+
+theorem empty_append (as : Array α) : #[] ++ as = as := by simp
+
+theorem append_empty (as : Array α) : as ++ #[] = as := by simp
+
+theorem getElem_append {as bs : Array α} (h : i < (as ++ bs).size) :
+    (as ++ bs)[i] = if h' : i < as.size then as[i] else bs[i - as.size]'(by simp at h; omega) := by
+  cases as; cases bs
+  simp [List.getElem_append]
+
+theorem getElem_append_left {as bs : Array α} {h : i < (as ++ bs).size} (hlt : i < as.size) :
+    (as ++ bs)[i] = as[i] := by
+  simp only [← getElem_toList]
+  have h' : i < (as.toList ++ bs.toList).length := by rwa [← length_toList, toList_append] at h
+  conv => rhs; rw [← List.getElem_append_left (bs := bs.toList) (h' := h')]
+  apply List.get_of_eq; rw [toList_append]
+
+theorem getElem_append_right {as bs : Array α} {h : i < (as ++ bs).size} (hle : as.size ≤ i) :
+    (as ++ bs)[i] = bs[i - as.size]'(Nat.sub_lt_left_of_lt_add hle (size_append .. ▸ h)) := by
+  simp only [← getElem_toList]
+  have h' : i < (as.toList ++ bs.toList).length := by rwa [← length_toList, toList_append] at h
+  conv => rhs; rw [← List.getElem_append_right (h₁ := hle) (h₂ := h')]
+  apply List.get_of_eq; rw [toList_append]
+
+theorem getElem?_append_left {as bs : Array α} {i : Nat} (hn : i < as.size) :
+    (as ++ bs)[i]? = as[i]? := by
+  have hn' : i < (as ++ bs).size := Nat.lt_of_lt_of_le hn <|
+    size_append .. ▸ Nat.le_add_right ..
+  simp_all [getElem?_eq_getElem, getElem_append]
+
+theorem getElem?_append_right {as bs : Array α} {i : Nat} (h : as.size ≤ i) :
+    (as ++ bs)[i]? = bs[i - as.size]? := by
+  cases as
+  cases bs
+  simp at h
+  simp [List.getElem?_append_right, h]
+
+theorem getElem?_append {as bs : Array α} {i : Nat} :
+    (as ++ bs)[i]? = if i < as.size then as[i]? else bs[i - as.size]? := by
+  split <;> rename_i h
+  · exact getElem?_append_left h
+  · exact getElem?_append_right (by simpa using h)
+
+/-- Variant of `getElem_append_left` useful for rewriting from the small array to the big array. -/
+theorem getElem_append_left' (l₂ : Array α) {l₁ : Array α} {i : Nat} (hi : i < l₁.size) :
+    l₁[i] = (l₁ ++ l₂)[i]'(by simpa using Nat.lt_add_right l₂.size hi) := by
+  rw [getElem_append_left] <;> simp
+
+/-- Variant of `getElem_append_right` useful for rewriting from the small array to the big array. -/
+theorem getElem_append_right' (l₁ : Array α) {l₂ : Array α} {i : Nat} (hi : i < l₂.size) :
+    l₂[i] = (l₁ ++ l₂)[i + l₁.size]'(by simpa [Nat.add_comm] using Nat.add_lt_add_left hi _) := by
+  rw [getElem_append_right] <;> simp [*, Nat.le_add_left]
+
+theorem getElem_of_append {l l₁ l₂ : Array α} (eq : l = l₁.push a ++ l₂) (h : l₁.size = i) :
+    l[i]'(eq ▸ h ▸ by simp_arith) = a := Option.some.inj <| by
+  rw [← getElem?_eq_getElem, eq, getElem?_append_left (by simp; omega), ← h]
+  simp
+
 
 -- This is a duplicate of `List.toArray_toList`.
 -- It's confusing to guess which namespace this theorem should live in,
@@ -1687,12 +2140,6 @@ theorem foldr_hom (f : β₁ → β₂) (g₁ : α → β₁ → β₁) (g₂ :
 
 /-! ### map -/
 
-@[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]
-
 @[deprecated "Use `toList_map` or `List.map_toArray` to characterize `Array.map`." (since := "2025-01-06")]
 theorem map_induction (as : Array α) (f : α → β) (motive : Nat → Prop) (h0 : motive 0)
     (p : Fin as.size → β → Prop) (hs : ∀ i, motive i.1 → p i (f as[i]) ∧ motive (i+1)) :
@@ -1761,137 +2208,10 @@ theorem getElem?_modify {as : Array α} {i : Nat} {f : α → α} {j : Nat} :
   simp only [getElem?_def, size_modify, getElem_modify, Option.map_dif]
   split <;> split <;> rfl
 
-/-! ### filter -/
-
-@[simp] theorem toList_filter (p : α → Bool) (l : Array α) :
-    (l.filter p).toList = l.toList.filter p := by
-  dsimp only [filter]
-  rw [← foldl_toList]
-  generalize l.toList = l
-  suffices ∀ a, (List.foldl (fun r a => if p a = true then push r a else r) a l).toList =
-      a.toList ++ List.filter p l by
-    simpa using this #[]
-  induction l with simp
-  | cons => split <;> simp [*]
-
-@[simp] theorem filter_filter (q) (l : Array α) :
-    filter p (filter q l) = filter (fun a => p a && q a) l := by
-  apply ext'
-  simp only [toList_filter, List.filter_filter]
-
-@[simp] theorem mem_filter : x ∈ filter p as ↔ x ∈ as ∧ p x := by
-  simp only [mem_def, toList_filter, List.mem_filter]
-
-theorem mem_of_mem_filter {a : α} {l} (h : a ∈ filter p l) : a ∈ l :=
-  (mem_filter.mp h).1
-
-@[congr]
-theorem filter_congr {as bs : Array α} (h : as = bs)
-    {f : α → Bool} {g : α → Bool} (h' : f = g) {start stop start' stop' : Nat}
-    (h₁ : start = start') (h₂ : stop = stop') :
-    filter f as start stop = filter g bs start' stop' := by
-  congr
-
-/-! ### filterMap -/
-
-@[simp] theorem toList_filterMap (f : α → Option β) (l : Array α) :
-    (l.filterMap f).toList = l.toList.filterMap f := by
-  dsimp only [filterMap, filterMapM]
-  rw [← foldlM_toList]
-  generalize l.toList = l
-  have this : ∀ a : Array β, (Id.run (List.foldlM (m := Id) ?_ a l)).toList =
-    a.toList ++ List.filterMap f l := ?_
-  exact this #[]
-  induction l
-  · simp_all [Id.run]
-  · simp_all [Id.run, List.filterMap_cons]
-    split <;> simp_all
-
-@[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]
-
-@[congr]
-theorem filterMap_congr {as bs : Array α} (h : as = bs)
-    {f : α → Option β} {g : α → Option β} (h' : f = g) {start stop start' stop' : Nat}
-    (h₁ : start = start') (h₂ : stop = stop') :
-    filterMap f as start stop = filterMap g bs start' stop' := by
-  congr
-
 /-! ### empty -/
 
 theorem size_empty : (#[] : Array α).size = 0 := rfl
 
-/-! ### append -/
-
-theorem push_eq_append_singleton (as : Array α) (x) : as.push x = as ++ #[x] := rfl
-
-@[simp] theorem mem_append {a : α} {s t : Array α} : a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t := by
-  simp only [mem_def, toList_append, List.mem_append]
-
-theorem mem_append_left {a : α} {l₁ : Array α} (l₂ : Array α) (h : a ∈ l₁) : a ∈ l₁ ++ l₂ :=
-  mem_append.2 (Or.inl h)
-
-theorem mem_append_right {a : α} (l₁ : Array α) {l₂ : Array α} (h : a ∈ l₂) : a ∈ l₁ ++ l₂ :=
-  mem_append.2 (Or.inr h)
-
-@[simp] theorem size_append (as bs : Array α) : (as ++ bs).size = as.size + bs.size := by
-  simp only [size, toList_append, List.length_append]
-
-theorem empty_append (as : Array α) : #[] ++ as = as := by simp
-
-theorem append_empty (as : Array α) : as ++ #[] = as := by simp
-
-theorem getElem_append {as bs : Array α} (h : i < (as ++ bs).size) :
-    (as ++ bs)[i] = if h' : i < as.size then as[i] else bs[i - as.size]'(by simp at h; omega) := by
-  cases as; cases bs
-  simp [List.getElem_append]
-
-theorem getElem_append_left {as bs : Array α} {h : i < (as ++ bs).size} (hlt : i < as.size) :
-    (as ++ bs)[i] = as[i] := by
-  simp only [← getElem_toList]
-  have h' : i < (as.toList ++ bs.toList).length := by rwa [← length_toList, toList_append] at h
-  conv => rhs; rw [← List.getElem_append_left (bs := bs.toList) (h' := h')]
-  apply List.get_of_eq; rw [toList_append]
-
-theorem getElem_append_right {as bs : Array α} {h : i < (as ++ bs).size} (hle : as.size ≤ i) :
-    (as ++ bs)[i] = bs[i - as.size]'(Nat.sub_lt_left_of_lt_add hle (size_append .. ▸ h)) := by
-  simp only [← getElem_toList]
-  have h' : i < (as.toList ++ bs.toList).length := by rwa [← length_toList, toList_append] at h
-  conv => rhs; rw [← List.getElem_append_right (h₁ := hle) (h₂ := h')]
-  apply List.get_of_eq; rw [toList_append]
-
-theorem getElem?_append_left {as bs : Array α} {i : Nat} (hn : i < as.size) :
-    (as ++ bs)[i]? = as[i]? := by
-  have hn' : i < (as ++ bs).size := Nat.lt_of_lt_of_le hn <|
-    size_append .. ▸ Nat.le_add_right ..
-  simp_all [getElem?_eq_getElem, getElem_append]
-
-theorem getElem?_append_right {as bs : Array α} {i : Nat} (h : as.size ≤ i) :
-    (as ++ bs)[i]? = bs[i - as.size]? := by
-  cases as
-  cases bs
-  simp at h
-  simp [List.getElem?_append_right, h]
-
-theorem getElem?_append {as bs : Array α} {i : Nat} :
-    (as ++ bs)[i]? = if i < as.size then as[i]? else bs[i - as.size]? := by
-  split <;> rename_i h
-  · exact getElem?_append_left h
-  · exact getElem?_append_right (by simpa using h)
-
-@[simp] theorem toArray_eq_append_iff {xs : List α} {as bs : Array α} :
-    xs.toArray = as ++ bs ↔ xs = as.toList ++ bs.toList := by
-  cases as
-  cases bs
-  simp
-
-@[simp] theorem append_eq_toArray_iff {as bs : Array α} {xs : List α} :
-    as ++ bs = xs.toArray ↔ as.toList ++ bs.toList = xs := by
-  cases as
-  cases bs
-  simp
-
 /-! ### flatten -/
 
 @[simp] theorem toList_flatten {l : Array (Array α)} :
@@ -2227,26 +2547,6 @@ theorem uset_toArray (l : List α) (i : USize) (a : α) (h : i.toNat < l.toArray
   apply ext'
   simp
 
-@[simp] theorem filter_toArray' (p : α → Bool) (l : List α) (h : stop = l.toArray.size) :
-    l.toArray.filter p 0 stop = (l.filter p).toArray := by
-  subst h
-  apply ext'
-  rw [toList_filter]
-
-@[simp] theorem filterMap_toArray' (f : α → Option β) (l : List α) (h : stop = l.toArray.size) :
-    l.toArray.filterMap f 0 stop = (l.filterMap f).toArray := by
-  subst h
-  apply ext'
-  rw [toList_filterMap]
-
-theorem filter_toArray (p : α → Bool) (l : List α) :
-    l.toArray.filter p = (l.filter p).toArray := by
-  simp
-
-theorem filterMap_toArray (f : α → Option β) (l : List α) :
-    l.toArray.filterMap f = (l.filterMap f).toArray := by
-  simp
-
 @[simp] theorem flatten_toArray (l : List (List α)) :
     (l.toArray.map List.toArray).flatten = l.flatten.toArray := by
   apply ext'
@@ -2368,6 +2668,12 @@ theorem foldr_map' (g : α → β) (f : α → α → α) (f' : β → β → β
   | nil => simp
   | cons xs xss ih => simp [ih]
 
+/-! ### mkArray -/
+
+@[simp] theorem mem_mkArray (a : α) (n : Nat) : b ∈ mkArray n a ↔ n ≠ 0 ∧ b = a := by
+  rw [mkArray, mem_toArray]
+  simp
+
 /-! ### reverse -/
 
 @[simp] theorem mem_reverse {x : α} {as : Array α} : x ∈ as.reverse ↔ x ∈ as := by

src/Init/Data/BitVec/Lemmas.lean

@@ -9,7 +9,9 @@ import Init.Data.Bool
 import Init.Data.BitVec.Basic
 import Init.Data.Fin.Lemmas
 import Init.Data.Nat.Lemmas
+import Init.Data.Nat.Div.Lemmas
 import Init.Data.Nat.Mod
+import Init.Data.Nat.Div.Lemmas
 import Init.Data.Int.Bitwise.Lemmas
 import Init.Data.Int.Pow
 
@@ -98,6 +100,12 @@ theorem ofFin_eq_ofNat : @BitVec.ofFin w (Fin.mk x lt) = BitVec.ofNat w x := by
 theorem eq_of_toNat_eq {n} : ∀ {x y : BitVec n}, x.toNat = y.toNat → x = y
   | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
 
+/-- Prove nonequality of bitvectors in terms of nat operations. -/
+theorem toNat_ne_iff_ne {n} {x y : BitVec n} : x.toNat ≠ y.toNat ↔ x ≠ y := by
+  constructor
+  · rintro h rfl; apply h rfl
+  · intro h h_eq; apply h <| eq_of_toNat_eq h_eq
+
 @[simp] theorem val_toFin (x : BitVec w) : x.toFin.val = x.toNat := rfl
 
 @[bv_toNat] theorem toNat_eq {x y : BitVec n} : x = y ↔ x.toNat = y.toNat :=
@@ -442,6 +450,10 @@ theorem toInt_eq_toNat_cond (x : BitVec n) :
         (x.toNat : Int) - (2^n : Nat) :=
   rfl
 
+theorem toInt_eq_toNat_of_lt {x : BitVec n} (h : 2 * x.toNat < 2^n) :
+    x.toInt = x.toNat := by
+  simp [toInt_eq_toNat_cond, h]
+
 theorem msb_eq_false_iff_two_mul_lt {x : BitVec w} : x.msb = false ↔ 2 * x.toNat < 2^w := by
   cases w <;> simp [Nat.pow_succ, Nat.mul_comm _ 2, msb_eq_decide, toNat_of_zero_length]
 
@@ -454,6 +466,9 @@ theorem toInt_eq_msb_cond (x : BitVec w) :
   simp only [BitVec.toInt, ← msb_eq_false_iff_two_mul_lt]
   cases x.msb <;> rfl
 
+theorem toInt_eq_toNat_of_msb {x : BitVec w} (h : x.msb = false) :
+    x.toInt = x.toNat := by
+  simp [toInt_eq_msb_cond, h]
 
 theorem toInt_eq_toNat_bmod (x : BitVec n) : x.toInt = Int.bmod x.toNat (2^n) := by
   simp only [toInt_eq_toNat_cond]
@@ -2300,6 +2315,12 @@ theorem ofNat_sub_ofNat {n} (x y : Nat) : BitVec.ofNat n x - BitVec.ofNat n y =
 @[simp, bv_toNat] theorem toNat_neg (x : BitVec n) : (- x).toNat = (2^n - x.toNat) % 2^n := by
   simp [Neg.neg, BitVec.neg]
 
+theorem toNat_neg_of_pos {x : BitVec n} (h : 0#n < x) :
+    (- x).toNat = 2^n - x.toNat := by
+  change 0 < x.toNat at h
+  rw [toNat_neg, Nat.mod_eq_of_lt]
+  omega
+
 theorem toInt_neg {x : BitVec w} :
     (-x).toInt = (-x.toInt).bmod (2 ^ w) := by
   rw [← BitVec.zero_sub, toInt_sub]
@@ -2586,13 +2607,13 @@ theorem udiv_def {x y : BitVec n} : x / y = BitVec.ofNat n (x.toNat / y.toNat) :
   rw [← udiv_eq]
   simp [udiv, bv_toNat, h, Nat.mod_eq_of_lt]
 
+@[simp]
+theorem toFin_udiv {x y : BitVec n} : (x / y).toFin = x.toFin / y.toFin := by
+  rfl
+
 @[simp, bv_toNat]
 theorem toNat_udiv {x y : BitVec n} : (x / y).toNat = x.toNat / y.toNat := by
-  rw [udiv_def]
-  by_cases h : y = 0
-  · simp [h]
-  · rw [toNat_ofNat, Nat.mod_eq_of_lt]
-    exact Nat.lt_of_le_of_lt (Nat.div_le_self ..) (by omega)
+  rfl
 
 @[simp]
 theorem zero_udiv {x : BitVec w} : (0#w) / x = 0#w := by
@@ -2628,6 +2649,45 @@ theorem udiv_self {x : BitVec w} :
       ↓reduceIte, toNat_udiv]
     rw [Nat.div_self (by omega), Nat.mod_eq_of_lt (by omega)]
 
+theorem msb_udiv (x y : BitVec w) :
+    (x / y).msb = (x.msb && y == 1#w) := by
+  cases msb_x : x.msb
+  · suffices x.toNat / y.toNat < 2 ^ (w - 1) by simpa [msb_eq_decide]
+    calc
+      x.toNat / y.toNat ≤ x.toNat     := by apply Nat.div_le_self
+                      _ < 2 ^ (w - 1) := by simpa [msb_eq_decide] using msb_x
+  . rcases w with _|w
+    · contradiction
+    · have : (y == 1#_) = decide (y.toNat = 1) := by
+        simp [(· == ·), toNat_eq]
+      simp only [this, Bool.true_and]
+      match hy : y.toNat with
+      | 0 =>
+        obtain rfl : y = 0#_ := eq_of_toNat_eq hy
+        simp
+      | 1 =>
+        obtain rfl : y = 1#_ := eq_of_toNat_eq (by simp [hy])
+        simpa using msb_x
+      | y + 2 =>
+        suffices x.toNat / (y + 2) < 2 ^ w by
+          simp_all [msb_eq_decide, hy]
+        calc
+          x.toNat / (y + 2)
+            ≤ x.toNat / 2 := by apply Nat.div_add_le_right (by omega)
+          _ < 2 ^ w       := by omega
+
+theorem msb_udiv_eq_false_of {x : BitVec w} (h : x.msb = false) (y : BitVec w) :
+    (x / y).msb = false := by
+  simp [msb_udiv, h]
+
+/--
+If `x` is nonnegative (i.e., does not have its msb set),
+then `x / y` is nonnegative, thus `toInt` and `toNat` coincide.
+-/
+theorem toInt_udiv_of_msb {x : BitVec w} (h : x.msb = false) (y : BitVec w) :
+    (x / y).toInt = x.toNat / y.toNat := by
+  simp [toInt_eq_msb_cond, msb_udiv_eq_false_of h]
+
 /-! ### umod -/
 
 theorem umod_def {x y : BitVec n} :
@@ -2640,6 +2700,10 @@ theorem umod_def {x y : BitVec n} :
 theorem toNat_umod {x y : BitVec n} :
     (x % y).toNat = x.toNat % y.toNat := rfl
 
+@[simp]
+theorem toFin_umod {x y : BitVec w} :
+    (x % y).toFin = x.toFin % y.toFin := rfl
+
 @[simp]
 theorem umod_zero {x : BitVec n} : x % 0#n = x := by
   simp [umod_def]
@@ -2667,6 +2731,55 @@ theorem umod_eq_and {x y : BitVec 1} : x % y = x &&& (~~~y) := by
     rcases hy with rfl | rfl <;>
       rfl
 
+theorem umod_eq_of_lt {x y : BitVec w} (h : x < y) :
+    x % y = x := by
+  apply eq_of_toNat_eq
+  simp [Nat.mod_eq_of_lt h]
+
+@[simp]
+theorem msb_umod {x y : BitVec w} :
+    (x % y).msb = (x.msb && (x < y || y == 0#w)) := by
+  rw [msb_eq_decide, toNat_umod]
+  cases msb_x : x.msb
+  · suffices x.toNat % y.toNat < 2 ^ (w - 1) by simpa
+    calc
+      x.toNat % y.toNat ≤ x.toNat     := by apply Nat.mod_le
+                      _ < 2 ^ (w - 1) := by simpa [msb_eq_decide] using msb_x
+  . by_cases hy : y = 0
+    · simp_all [msb_eq_decide]
+    · suffices 2 ^ (w - 1) ≤ x.toNat % y.toNat ↔ x < y by simp_all
+      by_cases x_lt_y : x < y
+      . simp_all [Nat.mod_eq_of_lt x_lt_y, msb_eq_decide]
+      · suffices x.toNat % y.toNat < 2 ^ (w - 1) by
+          simpa [x_lt_y]
+        have y_le_x : y.toNat ≤ x.toNat := by
+          simpa using x_lt_y
+        replace hy : y.toNat ≠ 0 :=
+          toNat_ne_iff_ne.mpr hy
+        by_cases msb_y : y.toNat < 2 ^ (w - 1)
+        · have : x.toNat % y.toNat < y.toNat := Nat.mod_lt _ (by omega)
+          omega
+        · rcases w with _|w
+          · contradiction
+          simp only [Nat.add_one_sub_one]
+          replace msb_y : 2 ^ w ≤ y.toNat := by
+            simpa using msb_y
+          have : y.toNat ≤ y.toNat * (x.toNat / y.toNat) := by
+              apply Nat.le_mul_of_pos_right
+              apply Nat.div_pos y_le_x
+              omega
+          have : x.toNat % y.toNat ≤ x.toNat - y.toNat := by
+            rw [Nat.mod_eq_sub]; omega
+          omega
+
+theorem toInt_umod {x y : BitVec w} :
+    (x % y).toInt = (x.toNat % y.toNat : Int).bmod (2 ^ w) := by
+  simp [toInt_eq_toNat_bmod]
+
+theorem toInt_umod_of_msb {x y : BitVec w} (h : x.msb = false) :
+    (x % y).toInt = x.toInt % y.toNat := by
+  simp [toInt_eq_msb_cond, h]
+
 /-! ### smtUDiv -/
 
 theorem smtUDiv_eq (x y : BitVec w) : smtUDiv x y = if y = 0#w then allOnes w else x / y := by
@@ -2823,7 +2936,12 @@ theorem smod_zero {x : BitVec n} : x.smod 0#n = x := by
 
 /-! # Rotate Left -/
 
-/-- rotateLeft is invariant under `mod` by the bitwidth. -/
+/--`rotateLeft` is defined in terms of left and right shifts. -/
+theorem rotateLeft_def {x : BitVec w} {r : Nat} :
+    x.rotateLeft r = (x <<< (r % w)) ||| (x >>> (w - r % w)) := by
+  simp only [rotateLeft, rotateLeftAux]
+
+/-- `rotateLeft` is invariant under `mod` by the bitwidth. -/
 @[simp]
 theorem rotateLeft_mod_eq_rotateLeft {x : BitVec w} {r : Nat} :
     x.rotateLeft (r % w) = x.rotateLeft r := by
@@ -2967,8 +3085,18 @@ theorem msb_rotateLeft {m w : Nat} {x : BitVec w} :
   · simp
     omega
 
+@[simp]
+theorem toNat_rotateLeft {x : BitVec w} {r : Nat} :
+    (x.rotateLeft r).toNat = (x.toNat <<< (r % w)) % (2^w) ||| x.toNat >>> (w - r % w) := by
+  simp only [rotateLeft_def, toNat_shiftLeft, toNat_ushiftRight, toNat_or]
+
 /-! ## Rotate Right -/
 
+/-- `rotateRight` is defined in terms of left and right shifts. -/
+theorem rotateRight_def {x : BitVec w} {r : Nat} :
+    x.rotateRight r = (x >>> (r % w)) ||| (x <<< (w - r % w)) := by
+  simp only [rotateRight, rotateRightAux]
+
 /--
 Accessing bits in `x.rotateRight r` the range `[0, w-r)` is equal to
 accessing bits `x` in the range `[r, w)`.
@@ -3104,6 +3232,11 @@ theorem msb_rotateRight {r w : Nat} {x : BitVec w} :
     simp [h₁]
   · simp [show w = 0 by omega]
 
+@[simp]
+theorem toNat_rotateRight {x : BitVec w} {r : Nat} :
+    (x.rotateRight r).toNat = (x.toNat >>> (r % w)) ||| x.toNat <<< (w - r % w) % (2^w) := by
+  simp only [rotateRight_def, toNat_shiftLeft, toNat_ushiftRight, toNat_or]
+
 /- ## twoPow -/
 
 theorem twoPow_eq (w : Nat) (i : Nat) : twoPow w i = 1#w <<< i := by

src/Init/Data/List/Lemmas.lean

@@ -1,7 +1,8 @@
 /-
 Copyright (c) 2014 Parikshit Khanna. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro
+Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro,
+  Kim Morrison
 -/
 prelude
 import Init.Data.Bool
@@ -1114,6 +1115,10 @@ theorem map_eq_cons_iff' {f : α → β} {l : List α} :
 
 @[deprecated map_eq_cons' (since := "2024-09-05")] abbrev map_eq_cons' := @map_eq_cons_iff'
 
+@[simp] theorem map_eq_singleton_iff {f : α → β} {l : List α} {b : β} :
+    map f l = [b] ↔ ∃ a, l = [a] ∧ f a = b := by
+  simp [map_eq_cons_iff]
+
 theorem map_eq_map_iff : map f l = map g l ↔ ∀ a ∈ l, f a = g a := by
   induction l <;> simp
 
@@ -1280,7 +1285,7 @@ theorem map_filter_eq_foldr (f : α → β) (p : α → Bool) (as : List α) :
 @[simp] theorem filter_append {p : α → Bool} :
     ∀ (l₁ l₂ : List α), filter p (l₁ ++ l₂) = filter p l₁ ++ filter p l₂
   | [], _ => rfl
-  | a :: l₁, l₂ => by simp [filter]; split <;> simp [filter_append l₁]
+  | a :: l₁, l₂ => by simp only [cons_append, filter]; split <;> simp [filter_append l₁]
 
 theorem filter_eq_cons_iff {l} {a} {as} :
     filter p l = a :: as ↔

src/Init/Data/List/ToArray.lean

@@ -46,7 +46,7 @@ theorem toArray_cons (a : α) (l : List α) : (a :: l).toArray = #[a] ++ l.toArr
 @[simp] theorem isEmpty_toArray (l : List α) : l.toArray.isEmpty = l.isEmpty := by
   cases l <;> simp [Array.isEmpty]
 
-@[simp] theorem toArray_singleton (a : α) : (List.singleton a).toArray = singleton a := rfl
+@[simp] theorem toArray_singleton (a : α) : (List.singleton a).toArray = Array.singleton a := rfl
 
 @[simp] theorem back!_toArray [Inhabited α] (l : List α) : l.toArray.back! = l.getLast! := by
   simp only [back!, size_toArray, Array.get!_eq_getElem!, getElem!_toArray, getLast!_eq_getElem!]

src/Init/Data/Nat/Div/Lemmas.lean

@@ -49,4 +49,17 @@ theorem lt_div_mul_self (h : 0 < k) (w : k ≤ x) : x - k < x / k * k := by
   have : x % k < k := mod_lt x h
   omega
 
+theorem div_pos (hba : b ≤ a) (hb : 0 < b) : 0 < a / b := by
+  cases b
+  · contradiction
+  · simp [Nat.pos_iff_ne_zero, div_eq_zero_iff_lt, hba]
+
+theorem div_le_div_left (hcb : c ≤ b) (hc : 0 < c) : a / b ≤ a / c :=
+  (Nat.le_div_iff_mul_le hc).2 <|
+    Nat.le_trans (Nat.mul_le_mul_left _ hcb) (Nat.div_mul_le_self a b)
+
+theorem div_add_le_right {z : Nat} (h : 0 < z) (x y : Nat) :
+    x / (y + z) ≤ x / z :=
+  div_le_div_left (Nat.le_add_left z y) h
+
 end Nat

src/Init/Data/UInt/Basic.lean

@@ -159,6 +159,8 @@ def UInt32.xor (a b : UInt32) : UInt32 := ⟨a.toBitVec ^^^ b.toBitVec⟩
 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.toBitVec >>> (mod b 32).toBitVec⟩
+def UInt32.lt (a b : UInt32) : Prop := a.toBitVec < b.toBitVec
+def UInt32.le (a b : UInt32) : Prop := a.toBitVec ≤ b.toBitVec
 
 instance : Add UInt32       := ⟨UInt32.add⟩
 instance : Sub UInt32       := ⟨UInt32.sub⟩
@@ -169,6 +171,8 @@ set_option linter.deprecated false in
 instance : HMod UInt32 Nat UInt32 := ⟨UInt32.modn⟩
 
 instance : Div UInt32       := ⟨UInt32.div⟩
+instance : LT UInt32        := ⟨UInt32.lt⟩
+instance : LE UInt32        := ⟨UInt32.le⟩
 
 @[extern "lean_uint32_complement"]
 def UInt32.complement (a : UInt32) : UInt32 := ⟨~~~a.toBitVec⟩

src/Init/Data/Vector/Basic.lean

@@ -103,7 +103,7 @@ of bounds.
 @[inline] def head [NeZero n] (v : Vector α n) := v[0]'(Nat.pos_of_neZero n)
 
 /-- Push an element `x` to the end of a vector. -/
-@[inline] def push (x : α) (v : Vector α n)  : Vector α (n + 1) :=
+@[inline] def push (v : Vector α n) (x : α) : Vector α (n + 1) :=
   ⟨v.toArray.push x, by simp⟩
 
 /-- Remove the last element of a vector. -/

src/Init/Data/Vector/Lemmas.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Shreyas Srinivas. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Shreyas Srinivas, Francois Dorais
+Authors: Shreyas Srinivas, Francois Dorais, Kim Morrison
 -/
 prelude
 import Init.Data.Vector.Basic
@@ -153,6 +153,14 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a
 @[simp] theorem all_mk (p : α → Bool) (a : Array α) (h : a.size = n) :
     (Vector.mk a h).all p = a.all p := rfl
 
+@[simp] theorem eq_mk : v = Vector.mk a h ↔ v.toArray = a := by
+  cases v
+  simp
+
+@[simp] theorem mk_eq : Vector.mk a h = v ↔ a = v.toArray := by
+  cases v
+  simp
+
 /-! ### toArray lemmas -/
 
 @[simp] theorem getElem_toArray {α n} (xs : Vector α n) (i : Nat) (h : i < xs.toArray.size) :
@@ -1035,8 +1043,6 @@ theorem mem_setIfInBounds (v : Vector α n) (i : Nat) (hi : i < n) (a : α) :
   cases l₂
   simp
 
-/-! Content below this point has not yet been aligned with `List` and `Array`. -/
-
 /-! ### map -/
 
 @[simp] theorem getElem_map (f : α → β) (a : Vector α n) (i : Nat) (hi : i < n) :
@@ -1044,16 +1050,129 @@ theorem mem_setIfInBounds (v : Vector α n) (i : Nat) (hi : i < n) (a : α) :
   cases a
   simp
 
-@[simp] theorem getElem_ofFn {α n} (f : Fin n → α) (i : Nat) (h : i < n) :
-    (Vector.ofFn f)[i] = f ⟨i, by simpa using h⟩ := by
-  simp [ofFn]
-
 /-- The empty vector maps to the empty vector. -/
 @[simp]
 theorem map_empty (f : α → β) : map f #v[] = #v[] := by
   rw [map, mk.injEq]
   exact Array.map_empty f
 
+@[simp] theorem map_push {f : α → β} {as : Vector α n} {x : α} :
+    (as.push x).map f = (as.map f).push (f x) := by
+  cases as
+  simp
+
+@[simp] theorem map_id_fun : map (n := n) (id : α → α) = id := by
+  funext l
+  induction l <;> simp_all
+
+/-- `map_id_fun'` differs from `map_id_fun` by representing the identity function as a lambda, rather than `id`. -/
+@[simp] theorem map_id_fun' : map (n := n) (fun (a : α) => a) = id := map_id_fun
+
+-- This is not a `@[simp]` lemma because `map_id_fun` will apply.
+theorem map_id (l : Vector α n) : map (id : α → α) l = l := by
+  cases l <;> simp_all
+
+/-- `map_id'` differs from `map_id` by representing the identity function as a lambda, rather than `id`. -/
+-- This is not a `@[simp]` lemma because `map_id_fun'` will apply.
+theorem map_id' (l : Vector α n) : map (fun (a : α) => a) l = l := map_id l
+
+/-- Variant of `map_id`, with a side condition that the function is pointwise the identity. -/
+theorem map_id'' {f : α → α} (h : ∀ x, f x = x) (l : Vector α n) : map f l = l := by
+  simp [show f = id from funext h]
+
+theorem map_singleton (f : α → β) (a : α) : map f #v[a] = #v[f a] := rfl
+
+@[simp] theorem mem_map {f : α → β} {l : Vector α n} : b ∈ l.map f ↔ ∃ a, a ∈ l ∧ f a = b := by
+  cases l
+  simp
+
+theorem exists_of_mem_map (h : b ∈ map f l) : ∃ a, a ∈ l ∧ f a = b := mem_map.1 h
+
+theorem mem_map_of_mem (f : α → β) (h : a ∈ l) : f a ∈ map f l := mem_map.2 ⟨_, h, rfl⟩
+
+theorem forall_mem_map {f : α → β} {l : Vector α n} {P : β → Prop} :
+    (∀ (i) (_ : i ∈ l.map f), P i) ↔ ∀ (j) (_ : j ∈ l), P (f j) := by
+  simp
+
+@[simp] theorem map_inj_left {f g : α → β} : map f l = map g l ↔ ∀ a ∈ l, f a = g a := by
+  cases l <;> simp_all
+
+theorem map_congr_left (h : ∀ a ∈ l, f a = g a) : map f l = map g l :=
+  map_inj_left.2 h
+
+theorem map_inj [NeZero n] : map (n := n) f = map g ↔ f = g := by
+  constructor
+  · intro h
+    ext a
+    replace h := congrFun h (mkVector n a)
+    simp only [mkVector, map_mk, mk.injEq, Array.map_inj_left, Array.mem_mkArray,  and_imp,
+      forall_eq_apply_imp_iff] at h
+    exact h (NeZero.ne n)
+  · intro h; subst h; rfl
+
+theorem map_eq_push_iff {f : α → β} {l : Vector α (n + 1)} {l₂ : Vector β n} {b : β} :
+    map f l = l₂.push b ↔ ∃ l₁ a, l = l₁.push a ∧ map f l₁ = l₂ ∧ f a = b := by
+  rcases l with ⟨l, h⟩
+  rcases l₂ with ⟨l₂, rfl⟩
+  simp only [map_mk, push_mk, mk.injEq, Array.map_eq_push_iff]
+  constructor
+  · rintro ⟨l₁, a, rfl, rfl, rfl⟩
+    refine ⟨⟨l₁, by simp⟩, a, by simp⟩
+  · rintro ⟨l₁, a, h₁, h₂, rfl⟩
+    refine ⟨l₁.toArray, a, by simp_all⟩
+
+@[simp] theorem map_eq_singleton_iff {f : α → β} {l : Vector α 1} {b : β} :
+    map f l = #v[b] ↔ ∃ a, l = #v[a] ∧ f a = b := by
+  cases l
+  simp
+
+theorem map_eq_map_iff {f g : α → β} {l : Vector α n} :
+    map f l = map g l ↔ ∀ a ∈ l, f a = g a := by
+  cases l <;> simp_all
+
+theorem map_eq_iff {f : α → β} {l : Vector α n} {l' : Vector β n} :
+    map f l = l' ↔ ∀ i (h : i < n), l'[i] = f l[i] := by
+  rcases l with ⟨l, rfl⟩
+  rcases l' with ⟨l', h'⟩
+  simp only [map_mk, eq_mk, Array.map_eq_iff, getElem_mk]
+  constructor
+  · intro w i h
+    simpa [h, h'] using w i
+  · intro w i
+    if h : i < l.size then
+      simpa [h, h'] using w i h
+    else
+      rw [getElem?_neg, getElem?_neg, Option.map_none'] <;> omega
+
+@[simp] theorem map_set {f : α → β} {l : Vector α n} {i : Nat} {h : i < n} {a : α} :
+    (l.set i a).map f = (l.map f).set i (f a) (by simpa using h) := by
+  cases l
+  simp
+
+@[simp] theorem map_setIfInBounds {f : α → β} {l : Vector α n} {i : Nat} {a : α} :
+    (l.setIfInBounds i a).map f = (l.map f).setIfInBounds i (f a) := by
+  cases l
+  simp
+
+@[simp] theorem map_pop {f : α → β} {l : Vector α n} : l.pop.map f = (l.map f).pop := by
+  cases l
+  simp
+
+@[simp] theorem back?_map {f : α → β} {l : Vector α n} : (l.map f).back? = l.back?.map f := by
+  cases l
+  simp
+
+@[simp] theorem map_map {f : α → β} {g : β → γ} {as : Vector α n} :
+    (as.map f).map g = as.map (g ∘ f) := by
+  cases as
+  simp
+
+/-! Content below this point has not yet been aligned with `List` and `Array`. -/
+
+@[simp] theorem getElem_ofFn {α n} (f : Fin n → α) (i : Nat) (h : i < n) :
+    (Vector.ofFn f)[i] = f ⟨i, by simpa using h⟩ := by
+  simp [ofFn]
+
 @[simp] theorem getElem_push_last {v : Vector α n} {x : α} : (v.push x)[n] = x := by
   rcases v with ⟨data, rfl⟩
   simp

src/Init/Grind.lean

@@ -10,3 +10,4 @@ import Init.Grind.Lemmas
 import Init.Grind.Cases
 import Init.Grind.Propagator
 import Init.Grind.Util
+import Init.Grind.Offset

src/Init/Grind/Lemmas.lean

@@ -66,6 +66,12 @@ theorem eq_eq_of_eq_true_right {a b : Prop} (h : b = True) : (a = b) = a := by s
 theorem eq_congr  {α : Sort u} {a₁ b₁ a₂ b₂ : α} (h₁ : a₁ = a₂) (h₂ : b₁ = b₂) : (a₁ = b₁) = (a₂ = b₂) := by simp [*]
 theorem eq_congr' {α : Sort u} {a₁ b₁ a₂ b₂ : α} (h₁ : a₁ = b₂) (h₂ : b₁ = a₂) : (a₁ = b₁) = (a₂ = b₂) := by rw [h₁, h₂, Eq.comm (a := a₂)]
 
+/- The following two helper theorems are used to case-split `a = b` representing `iff`. -/
+theorem of_eq_eq_true {a b : Prop} (h : (a = b) = True) : (¬a ∨ b) ∧ (¬b ∨ a) := by
+  by_cases a <;> by_cases b <;> simp_all
+theorem of_eq_eq_false {a b : Prop} (h : (a = b) = False) : (¬a ∨ ¬b) ∧ (b ∨ a) := by
+  by_cases a <;> by_cases b <;> simp_all
+
 /-! Forall -/
 
 theorem forall_propagator (p : Prop) (q : p → Prop) (q' : Prop) (h₁ : p = True) (h₂ : q (of_eq_true h₁) = q') : (∀ hp : p, q hp) = q' := by
@@ -73,6 +79,8 @@ theorem forall_propagator (p : Prop) (q : p → Prop) (q' : Prop) (h₁ : p = Tr
   · intro h'; exact Eq.mp h₂ (h' (of_eq_true h₁))
   · intro h'; intros; exact Eq.mpr h₂ h'
 
+theorem of_forall_eq_false (α : Sort u) (p : α → Prop) (h : (∀ x : α, p x) = False) : ∃ x : α, ¬ p x := by simp_all
+
 /-! dite -/
 
 theorem dite_cond_eq_true' {α : Sort u} {c : Prop} {_ : Decidable c} {a : c → α} {b : ¬ c → α} {r : α} (h₁ : c = True) (h₂ : a (of_eq_true h₁) = r) : (dite c a b) = r := by simp [h₁, h₂]

src/Init/Grind/Norm.lean

@@ -43,8 +43,14 @@ attribute [grind_norm] not_false_eq_true
 
 -- Remark: we disabled the following normalization rule because we want this information when implementing splitting heuristics
 -- Implication as a clause
--- @[grind_norm↓] theorem imp_eq (p q : Prop) : (p → q) = (¬ p ∨ q) := by
---  by_cases p <;> by_cases q <;> simp [*]
+theorem imp_eq (p q : Prop) : (p → q) = (¬ p ∨ q) := by
+  by_cases p <;> by_cases q <;> simp [*]
+
+@[grind_norm] theorem true_imp_eq (p : Prop) : (True → p) = p := by simp
+@[grind_norm] theorem false_imp_eq (p : Prop) : (False → p) = True := by simp
+@[grind_norm] theorem imp_true_eq (p : Prop) : (p → True) = True := by simp
+@[grind_norm] theorem imp_false_eq (p : Prop) : (p → False) = ¬p := by simp
+@[grind_norm] theorem imp_self_eq (p : Prop) : (p → p) = True := by simp
 
 -- And
 @[grind_norm↓] theorem not_and (p q : Prop) : (¬(p ∧ q)) = (¬p ∨ ¬q) := by

src/Init/Grind/Offset.lean

@@ -0,0 +1,50 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Core
+import Init.Omega
+
+namespace Lean.Grind
+def isLt (x y : Nat) : Bool := x < y
+
+theorem Nat.le_ro (u w v k : Nat) : u ≤ w → w ≤ v + k → u ≤ v + k := by
+  omega
+theorem Nat.le_lo (u w v k : Nat) : u ≤ w → w + k ≤ v → u + k ≤ v := by
+  omega
+theorem Nat.lo_le (u w v k : Nat) : u + k ≤ w → w ≤ v → u + k ≤ v := by
+  omega
+theorem Nat.lo_lo (u w v k₁ k₂ : Nat) : u + k₁ ≤ w → w + k₂ ≤ v → u + (k₁ + k₂) ≤ v := by
+  omega
+theorem Nat.lo_ro_1 (u w v k₁ k₂ : Nat) : isLt k₂ k₁ = true → u + k₁ ≤ w → w ≤ v + k₂ → u + (k₁ - k₂) ≤ v := by
+  simp [isLt]; omega
+theorem Nat.lo_ro_2 (u w v k₁ k₂ : Nat) : u + k₁ ≤ w → w ≤ v + k₂ → u ≤ v + (k₂ - k₁) := by
+  omega
+theorem Nat.ro_le (u w v k : Nat) : u ≤ w + k → w ≤ v → u ≤ v + k := by
+  omega
+theorem Nat.ro_lo_1 (u w v k₁ k₂ : Nat) : u ≤ w + k₁ → w + k₂ ≤ v → u ≤ v + (k₁ - k₂) := by
+  omega
+theorem Nat.ro_lo_2 (u w v k₁ k₂ : Nat) : isLt k₁ k₂ = true → u ≤ w + k₁ → w + k₂ ≤ v → u + (k₂ - k₁) ≤ v := by
+  simp [isLt]; omega
+theorem Nat.ro_ro (u w v k₁ k₂ : Nat) : u ≤ w + k₁ → w ≤ v + k₂ → u ≤ v + (k₁ + k₂) := by
+  omega
+
+theorem Nat.of_le_eq_false (u v : Nat) : ((u ≤ v) = False) → v + 1 ≤ u := by
+  simp; omega
+theorem Nat.of_lo_eq_false_1 (u v : Nat) : ((u + 1 ≤ v) = False) → v ≤ u := by
+  simp; omega
+theorem Nat.of_lo_eq_false (u v k : Nat) : ((u + k ≤ v) = False) → v ≤ u + (k-1) := by
+  simp; omega
+theorem Nat.of_ro_eq_false (u v k : Nat) : ((u ≤ v + k) = False) → v + (k+1) ≤ u := by
+  simp; omega
+
+theorem Nat.unsat_le_lo (u v k : Nat) : isLt 0 k = true → u ≤ v → v + k ≤ u → False := by
+  simp [isLt]; omega
+theorem Nat.unsat_lo_lo (u v k₁ k₂ : Nat) : isLt 0 (k₁+k₂) = true → u + k₁ ≤ v → v + k₂ ≤ u → False := by
+  simp [isLt]; omega
+theorem Nat.unsat_lo_ro (u v k₁ k₂ : Nat) : isLt k₂ k₁ = true → u + k₁ ≤ v → v ≤ u + k₂ → False := by
+  simp [isLt]; omega
+
+end Lean.Grind

src/Init/Grind/Tactics.lean

@@ -25,7 +25,7 @@ Passed to `grind` using, for example, the `grind (config := { matchEqs := true }
 -/
 structure Config where
   /-- Maximum number of case-splits in a proof search branch. It does not include splits performed during normalization. -/
-  splits : Nat := 5
+  splits : Nat := 8
   /-- Maximum number of E-matching (aka heuristic theorem instantiation) rounds before each case split. -/
   ematch : Nat := 5
   /--
@@ -37,6 +37,14 @@ structure Config where
   instances : Nat := 1000
   /-- If `matchEqs` is `true`, `grind` uses `match`-equations as E-matching theorems. -/
   matchEqs : Bool := true
+  /-- If `splitMatch` is `true`, `grind` performs case-splitting on `match`-expressions during the search. -/
+  splitMatch : Bool := true
+  /-- If `splitIte` is `true`, `grind` performs case-splitting on `if-then-else` expressions during the search. -/
+  splitIte : Bool := true
+  /--
+  If `splitIndPred` is `true`, `grind` performs case-splitting on inductive predicates.
+  Otherwise, it performs case-splitting only on types marked with `[grind_split]` attribute. -/
+  splitIndPred : Bool := true
   deriving Inhabited, BEq
 
 end Lean.Grind

src/Lean/Data/AssocList.lean

@@ -24,7 +24,7 @@ abbrev empty : AssocList α β :=
 
 instance : EmptyCollection (AssocList α β) := ⟨empty⟩
 
-abbrev insert (m : AssocList α β) (k : α) (v : β) : AssocList α β :=
+abbrev insertNew (m : AssocList α β) (k : α) (v : β) : AssocList α β :=
   m.cons k v
 
 def isEmpty : AssocList α β → Bool
@@ -77,6 +77,12 @@ def replace [BEq α] (a : α) (b : β) : AssocList α β → AssocList α β
     | true  => cons a b es
     | false => cons k v (replace a b es)
 
+def insert [BEq α] (m : AssocList α β) (k : α) (v : β) : AssocList α β :=
+  if m.contains k then
+    m.replace k v
+  else
+    m.insertNew k v
+
 def erase [BEq α] (a : α) : AssocList α β → AssocList α β
   | nil         => nil
   | cons k v es => match k == a with

src/Lean/Elab/Tactic/Conv/Simp.lean

@@ -7,9 +7,10 @@ prelude
 import Lean.Elab.Tactic.Simp
 import Lean.Elab.Tactic.Split
 import Lean.Elab.Tactic.Conv.Basic
+import Lean.Elab.Tactic.SimpTrace
 
 namespace Lean.Elab.Tactic.Conv
-open Meta
+open Meta Tactic TryThis
 
 def applySimpResult (result : Simp.Result) : TacticM Unit := do
   if result.proof?.isNone then
@@ -23,6 +24,19 @@ def applySimpResult (result : Simp.Result) : TacticM Unit := do
   let (result, _) ← dischargeWrapper.with fun d? => simp lhs ctx (simprocs := simprocs) (discharge? := d?)
   applySimpResult result
 
+@[builtin_tactic Lean.Parser.Tactic.Conv.simpTrace] def evalSimpTrace : Tactic := fun stx => withMainContext do
+  match stx with
+  | `(conv| simp?%$tk $cfg:optConfig $(discharger)? $[only%$o]? $[[$args,*]]?) => do
+    let stx ← `(tactic| simp%$tk $cfg:optConfig $[$discharger]? $[only%$o]? $[[$args,*]]?)
+    let { ctx, simprocs, dischargeWrapper, .. } ← mkSimpContext stx (eraseLocal := false)
+    let lhs ← getLhs
+    let (result, stats) ← dischargeWrapper.with fun d? =>
+      simp lhs ctx (simprocs := simprocs) (discharge? := d?)
+    applySimpResult result
+    let stx ← mkSimpCallStx stx stats.usedTheorems
+    addSuggestion tk stx (origSpan? := ← getRef)
+  | _ => throwUnsupportedSyntax
+
 @[builtin_tactic Lean.Parser.Tactic.Conv.simpMatch] def evalSimpMatch : Tactic := fun _ => withMainContext do
   applySimpResult (← Split.simpMatch (← getLhs))
 
@@ -30,4 +44,15 @@ def applySimpResult (result : Simp.Result) : TacticM Unit := do
   let { ctx, .. } ← mkSimpContext stx (eraseLocal := false) (kind := .dsimp)
   changeLhs (← Lean.Meta.dsimp (← getLhs) ctx).1
 
+@[builtin_tactic Lean.Parser.Tactic.Conv.dsimpTrace] def evalDSimpTrace : Tactic := fun stx => withMainContext do
+  match stx with
+  | `(conv| dsimp?%$tk $cfg:optConfig $[only%$o]? $[[$args,*]]?) =>
+    let stx ← `(tactic| dsimp%$tk $cfg:optConfig $[only%$o]? $[[$args,*]]?)
+    let { ctx, .. } ← mkSimpContext stx (eraseLocal := false) (kind := .dsimp)
+    let (result, stats) ← Lean.Meta.dsimp (← getLhs) ctx
+    changeLhs result
+    let stx ← mkSimpCallStx stx stats.usedTheorems
+    addSuggestion tk stx (origSpan? := ← getRef)
+  | _ => throwUnsupportedSyntax
+
 end Lean.Elab.Tactic.Conv

src/Lean/Meta/AppBuilder.lean

@@ -569,12 +569,16 @@ def mkLetBodyCongr (a h : Expr) : MetaM Expr :=
   mkAppM ``let_body_congr #[a, h]
 
 /-- Return `of_eq_true h` -/
-def mkOfEqTrue (h : Expr) : MetaM Expr :=
-  mkAppM ``of_eq_true #[h]
+def mkOfEqTrue (h : Expr) : MetaM Expr := do
+  match_expr h with
+  | eq_true _ h => return h
+  | _ => mkAppM ``of_eq_true #[h]
 
 /-- Return `eq_true h` -/
-def mkEqTrue (h : Expr) : MetaM Expr :=
-  mkAppM ``eq_true #[h]
+def mkEqTrue (h : Expr) : MetaM Expr := do
+  match_expr h with
+  | of_eq_true _ h => return h
+  | _ => return mkApp2 (mkConst ``eq_true) (← inferType h) h
 
 /--
   Return `eq_false h`

src/Lean/Meta/Basic.lean

@@ -1964,15 +1964,22 @@ def sortFVarIds (fvarIds : Array FVarId) : MetaM (Array FVarId) := do
 
 end Methods
 
+/--
+Return `some info` if `declName` is an inductive predicate where `info : InductiveVal`.
+That is, `inductive` type in `Prop`.
+-/
+def isInductivePredicate? (declName : Name) : MetaM (Option InductiveVal) := do
+  match (← getEnv).find? declName with
+  | some (.inductInfo info) =>
+    forallTelescopeReducing info.type fun _ type => do
+      match (← whnfD type) with
+      | .sort u .. => if u == levelZero then return some info else return none
+      | _ => return none
+  | _ => return none
+
 /-- Return `true` if `declName` is an inductive predicate. That is, `inductive` type in `Prop`. -/
 def isInductivePredicate (declName : Name) : MetaM Bool := do
-  match (← getEnv).find? declName with
-  | some (.inductInfo { type := type, ..}) =>
-    forallTelescopeReducing type fun _ type => do
-      match (← whnfD type) with
-      | .sort u .. => return u == levelZero
-      | _ => return false
-  | _ => return false
+  return (← isInductivePredicate? declName).isSome
 
 def isListLevelDefEqAux : List Level → List Level → MetaM Bool
   | [],    []    => return true

src/Lean/Meta/Tactic/FVarSubst.lean

@@ -35,7 +35,7 @@ def insert (s : FVarSubst) (fvarId : FVarId) (v : Expr) : FVarSubst :=
   if s.contains fvarId then s
   else
     let map := s.map.mapVal fun e => e.replaceFVarId fvarId v;
-    { map := map.insert fvarId v }
+    { map := map.insertNew fvarId v }
 
 def erase (s : FVarSubst) (fvarId : FVarId) : FVarSubst :=
   { map := s.map.erase fvarId }

src/Lean/Meta/Tactic/Grind.lean

@@ -24,6 +24,7 @@ import Lean.Meta.Tactic.Grind.EMatchTheorem
 import Lean.Meta.Tactic.Grind.EMatch
 import Lean.Meta.Tactic.Grind.Main
 import Lean.Meta.Tactic.Grind.CasesMatch
+import Lean.Meta.Tactic.Grind.Arith
 
 namespace Lean
 
@@ -42,6 +43,10 @@ builtin_initialize registerTraceClass `grind.simp
 builtin_initialize registerTraceClass `grind.split
 builtin_initialize registerTraceClass `grind.split.candidate
 builtin_initialize registerTraceClass `grind.split.resolved
+builtin_initialize registerTraceClass `grind.offset
+builtin_initialize registerTraceClass `grind.offset.dist
+builtin_initialize registerTraceClass `grind.offset.internalize
+builtin_initialize registerTraceClass `grind.offset.internalize.term (inherited := true)
 
 /-! Trace options for `grind` developers -/
 builtin_initialize registerTraceClass `grind.debug
@@ -53,5 +58,7 @@ builtin_initialize registerTraceClass `grind.debug.parent
 builtin_initialize registerTraceClass `grind.debug.final
 builtin_initialize registerTraceClass `grind.debug.forallPropagator
 builtin_initialize registerTraceClass `grind.debug.split
-
+builtin_initialize registerTraceClass `grind.debug.canon
+builtin_initialize registerTraceClass `grind.debug.offset
+builtin_initialize registerTraceClass `grind.debug.offset.proof
 end Lean

src/Lean/Meta/Tactic/Grind/Arith.lean

@@ -0,0 +1,10 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.Tactic.Grind.Arith.Util
+import Lean.Meta.Tactic.Grind.Arith.Types
+import Lean.Meta.Tactic.Grind.Arith.Offset
+import Lean.Meta.Tactic.Grind.Arith.Main

src/Lean/Meta/Tactic/Grind/Arith/Internalize.lean

@@ -0,0 +1,33 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.Tactic.Grind.Arith.Offset
+
+namespace Lean.Meta.Grind.Arith
+
+namespace Offset
+
+def internalizeTerm (_e : Expr) (_a : Expr) (_k : Nat) : GoalM Unit := do
+  -- TODO
+  return ()
+
+def internalizeCnstr (e : Expr) : GoalM Unit := do
+  let some c := isNatOffsetCnstr? e | return ()
+  let c := { c with
+    a := (← mkNode c.a)
+    b := (← mkNode c.b)
+  }
+  trace[grind.offset.internalize] "{e} ↦ {c}"
+  modify' fun s => { s with
+    cnstrs := s.cnstrs.insert { expr := e } c
+  }
+
+end Offset
+
+def internalize (e : Expr) : GoalM Unit := do
+  Offset.internalizeCnstr e
+
+end Lean.Meta.Grind.Arith

src/Lean/Meta/Tactic/Grind/Arith/Inv.lean

@@ -0,0 +1,14 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.Tactic.Grind.Arith.Offset
+
+namespace Lean.Meta.Grind.Arith
+
+def checkInvariants : GoalM Unit :=
+  Offset.checkInvariants
+
+end Lean.Meta.Grind.Arith

src/Lean/Meta/Tactic/Grind/Arith/Main.lean

@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.Tactic.Grind.PropagatorAttr
+import Lean.Meta.Tactic.Grind.Arith.Offset
+
+namespace Lean.Meta.Grind.Arith
+
+namespace Offset
+def isCnstr? (e : Expr) : GoalM (Option (Cnstr NodeId)) :=
+  return (← get).arith.offset.cnstrs.find? { expr := e }
+
+def assertTrue (c : Cnstr NodeId) (p : Expr) : GoalM Unit := do
+  addEdge c.a c.b c.k (← mkOfEqTrue p)
+
+def assertFalse (c : Cnstr NodeId) (p : Expr) : GoalM Unit := do
+  let p := mkOfNegEqFalse (← get').nodes c p
+  let c := c.neg
+  addEdge c.a c.b c.k p
+
+end Offset
+
+builtin_grind_propagator propagateLE ↓LE.le := fun e => do
+  if (← isEqTrue e) then
+    if let some c ← Offset.isCnstr? e then
+      Offset.assertTrue c (← mkEqTrueProof e)
+  if (← isEqFalse e) then
+    if let some c ← Offset.isCnstr? e then
+      Offset.assertFalse c (← mkEqFalseProof e)
+
+end Lean.Meta.Grind.Arith

src/Lean/Meta/Tactic/Grind/Arith/Offset.lean

@@ -0,0 +1,173 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Grind.Offset
+import Lean.Meta.Tactic.Grind.Types
+import Lean.Meta.Tactic.Grind.Arith.ProofUtil
+
+namespace Lean.Meta.Grind.Arith.Offset
+/-!
+This module implements a decision procedure for offset constraints of the form:
+```
+x + k ≤ y
+x ≤ y + k
+```
+where `k` is a numeral.
+Each constraint is represented as an edge in a weighted graph.
+The constraint `x + k ≤ y` is represented as a negative edge.
+The shortest path between two nodes in the graph corresponds to an implied inequality.
+When adding a new edge, the state is considered unsatisfiable if the new edge creates a negative cycle.
+An incremental Floyd-Warshall algorithm is used to find the shortest paths between all nodes.
+This module can also handle offset equalities of the form `x + k = y` by representing them with two edges:
+```
+x + k ≤ y
+y ≤ x + k
+```
+The main advantage of this module over a full linear integer arithmetic procedure is
+its ability to efficiently detect all implied equalities and inequalities.
+-/
+
+def get' : GoalM State := do
+  return (← get).arith.offset
+
+@[inline] def modify' (f : State → State) : GoalM Unit := do
+  modify fun s => { s with arith.offset := f s.arith.offset }
+
+def mkNode (expr : Expr) : GoalM NodeId := do
+  if let some nodeId := (← get').nodeMap.find? { expr } then
+    return nodeId
+  let nodeId : NodeId := (← get').nodes.size
+  trace[grind.offset.internalize.term] "{expr} ↦ #{nodeId}"
+  modify' fun s => { s with
+    nodes   := s.nodes.push expr
+    nodeMap := s.nodeMap.insert { expr } nodeId
+    sources := s.sources.push {}
+    targets := s.targets.push {}
+    proofs  := s.proofs.push {}
+  }
+  return nodeId
+
+private def getDist? (u v : NodeId) : GoalM (Option Int) := do
+  return (← get').targets[u]!.find? v
+
+private def getProof? (u v : NodeId) : GoalM (Option ProofInfo) := do
+  return (← get').proofs[u]!.find? v
+
+partial def extractProof (u v : NodeId) : GoalM Expr := do
+  go (← getProof? u v).get!
+where
+  go (p : ProofInfo) : GoalM Expr := do
+    if u == p.w then
+      return p.proof
+    else
+      let p' := (← getProof? u p.w).get!
+      go (mkTrans (← get').nodes p' p v)
+
+private def setUnsat (u v : NodeId) (kuv : Int) (huv : Expr) (kvu : Int) : GoalM Unit := do
+  assert! kuv + kvu < 0
+  let hvu ← extractProof v u
+  let u := (← get').nodes[u]!
+  let v := (← get').nodes[v]!
+  if kuv == 0 then
+    assert! kvu < 0
+    closeGoal (mkApp6 (mkConst ``Grind.Nat.unsat_le_lo) u v (toExpr (-kvu).toNat) rfl_true huv hvu)
+  else if kvu == 0 then
+    assert! kuv < 0
+    closeGoal (mkApp6 (mkConst ``Grind.Nat.unsat_le_lo) v u (toExpr (-kuv).toNat) rfl_true hvu huv)
+  else if kuv < 0 then
+    if kvu > 0 then
+      closeGoal (mkApp7 (mkConst ``Grind.Nat.unsat_lo_ro) u v (toExpr (-kuv).toNat) (toExpr kvu.toNat) rfl_true huv hvu)
+    else
+      assert! kvu < 0
+      closeGoal (mkApp7 (mkConst ``Grind.Nat.unsat_lo_lo) u v (toExpr (-kuv).toNat) (toExpr (-kvu).toNat) rfl_true huv hvu)
+  else
+    assert! kuv > 0 && kvu < 0
+    closeGoal (mkApp7 (mkConst ``Grind.Nat.unsat_lo_ro) v u (toExpr (-kvu).toNat) (toExpr kuv.toNat) rfl_true hvu huv)
+
+private def setDist (u v : NodeId) (k : Int) : GoalM Unit := do
+  trace[grind.offset.dist] "{({ a := u, b := v, k : Cnstr NodeId})}"
+  modify' fun s => { s with
+    targets := s.targets.modify u fun es => es.insert v k
+    sources := s.sources.modify v fun es => es.insert u k
+  }
+
+private def setProof (u v : NodeId) (p : ProofInfo) : GoalM Unit := do
+  modify' fun s => { s with
+    proofs := s.proofs.modify u fun es => es.insert v p
+  }
+
+@[inline]
+private def forEachSourceOf (u : NodeId) (f : NodeId → Int → GoalM Unit) : GoalM Unit := do
+  (← get').sources[u]!.forM f
+
+@[inline]
+private def forEachTargetOf (u : NodeId) (f : NodeId → Int → GoalM Unit) : GoalM Unit := do
+  (← get').targets[u]!.forM f
+
+private def isShorter (u v : NodeId) (k : Int) : GoalM Bool := do
+  if let some k' ← getDist? u v then
+    return k < k'
+  else
+    return true
+
+private def updateIfShorter (u v : NodeId) (k : Int) (w : NodeId) : GoalM Unit := do
+  if (← isShorter u v k) then
+    setDist u v k
+    setProof u v (← getProof? w v).get!
+
+def addEdge (u : NodeId) (v : NodeId) (k : Int) (p : Expr) : GoalM Unit := do
+  if (← isInconsistent) then return ()
+  if let some k' ← getDist? v u then
+    if k'+k < 0 then
+      setUnsat u v k p k'
+      return ()
+  if (← isShorter u v k) then
+    setDist u v k
+    setProof u v { w := u, k, proof := p }
+    update
+where
+  update : GoalM Unit := do
+    forEachTargetOf v fun j k₂ => do
+      /- Check whether new path: `u -(k)-> v -(k₂)-> j` is shorter -/
+      updateIfShorter u j (k+k₂) v
+    forEachSourceOf u fun i k₁ => do
+      /- Check whether new path: `i -(k₁)-> u -(k)-> v` is shorter -/
+      updateIfShorter i v (k₁+k) u
+      forEachTargetOf v fun j k₂ => do
+        /- Check whether new path: `i -(k₁)-> u -(k)-> v -(k₂) -> j` is shorter -/
+        updateIfShorter i j (k₁+k+k₂) v
+
+def traceDists : GoalM Unit := do
+  let s ← get'
+  for u in [:s.targets.size], es in s.targets.toArray do
+    for (v, k) in es do
+      trace[grind.offset.dist] "#{u} -({k})-> #{v}"
+
+def Cnstr.toExpr (c : Cnstr NodeId) : GoalM Expr := do
+  let a := (← get').nodes[c.a]!
+  let b := (← get').nodes[c.b]!
+  let mk := if c.le then mkNatLE else mkNatEq
+  if c.k == 0 then
+    return mk a b
+  else if c.k < 0 then
+    return mk (mkNatAdd a (Lean.toExpr ((-c.k).toNat))) b
+  else
+    return mk a (mkNatAdd b (Lean.toExpr c.k.toNat))
+
+def checkInvariants : GoalM Unit := do
+  let s ← get'
+  for u in [:s.targets.size], es in s.targets.toArray do
+    for (v, k) in es do
+      let c : Cnstr NodeId := { a := u, b := v, k }
+      trace[grind.debug.offset] "{c}"
+      let p ← extractProof u v
+      trace[grind.debug.offset.proof] "{p} : {← inferType p}"
+      check p
+      unless (← withDefault <| isDefEq (← inferType p) (← Cnstr.toExpr c)) do
+        trace[grind.debug.offset.proof] "failed: {← inferType p} =?= {← Cnstr.toExpr c}"
+        unreachable!
+
+end Lean.Meta.Grind.Arith.Offset

src/Lean/Meta/Tactic/Grind/Arith/ProofUtil.lean

@@ -0,0 +1,89 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Grind.Offset
+import Lean.Meta.Tactic.Grind.Types
+
+namespace Lean.Meta.Grind.Arith
+
+/-!
+Helper functions for constructing proof terms in the arithmetic procedures.
+-/
+
+namespace Offset
+
+/-- `Eq.refl true` -/
+def rfl_true : Expr := mkApp2 (mkConst ``Eq.refl [levelOne]) (mkConst ``Bool) (mkConst ``Bool.true)
+
+open Lean.Grind in
+/--
+Assume `pi₁` is `{ w := u, k := k₁, proof := p₁ }` and `pi₂` is `{ w := w, k := k₂, proof := p₂ }`
+`p₁` is the proof for edge `u -(k₁) → w` and `p₂` the proof for edge `w -(k₂)-> v`.
+Then, this function returns a proof for edge `u -(k₁+k₂) -> v`.
+-/
+def mkTrans (nodes : PArray Expr) (pi₁ : ProofInfo) (pi₂ : ProofInfo) (v : NodeId) : ProofInfo :=
+  let { w := u, k := k₁, proof := p₁ } := pi₁
+  let { w, k := k₂, proof := p₂ } := pi₂
+  let u := nodes[u]!
+  let w := nodes[w]!
+  let v := nodes[v]!
+  let p := if k₁ == 0 then
+    if k₂ == 0 then
+      -- u ≤ w, w ≤ v
+      mkApp5 (mkConst ``Nat.le_trans) u w v p₁ p₂
+    else if k₂ > 0 then
+      -- u ≤ v, w ≤ v + k₂
+      mkApp6 (mkConst ``Nat.le_ro) u w v (toExpr k₂.toNat) p₁ p₂
+    else
+      let k₂ := - k₂
+      -- u ≤ w, w + k₂ ≤ v
+      mkApp6 (mkConst ``Nat.le_lo) u w v (toExpr k₂.toNat) p₁ p₂
+  else if k₁ < 0 then
+    let k₁ := -k₁
+    if k₂ == 0 then
+      mkApp6 (mkConst ``Nat.lo_le) u w v (toExpr k₁.toNat) p₁ p₂
+    else if k₂ < 0 then
+      let k₂ := -k₂
+      mkApp7 (mkConst ``Nat.lo_lo) u w v (toExpr k₁.toNat) (toExpr k₂.toNat) p₁ p₂
+    else
+      let ke₁ := toExpr k₁.toNat
+      let ke₂ := toExpr k₂.toNat
+      if k₁ > k₂ then
+        mkApp8 (mkConst ``Nat.lo_ro_1) u w v ke₁ ke₂ rfl_true p₁ p₂
+      else
+        mkApp7 (mkConst ``Nat.lo_ro_2) u w v ke₁ ke₂ p₁ p₂
+  else
+    let ke₁ := toExpr k₁.toNat
+    if k₂ == 0 then
+      mkApp6 (mkConst ``Nat.ro_le) u w v ke₁ p₁ p₂
+    else if k₂ < 0 then
+      let k₂  := -k₂
+      let ke₂ := toExpr k₂.toNat
+       if k₂ > k₁ then
+         mkApp8 (mkConst ``Nat.ro_lo_2) u w v ke₁ ke₂ rfl_true p₁ p₂
+       else
+         mkApp7 (mkConst ``Nat.ro_lo_1) u w v ke₁ ke₂ p₁ p₂
+    else
+      let ke₂ := toExpr k₂.toNat
+      mkApp7 (mkConst ``Nat.ro_ro) u w v ke₁ ke₂ p₁ p₂
+  { w := pi₁.w, k := k₁+k₂, proof := p }
+
+open Lean.Grind in
+def mkOfNegEqFalse (nodes : PArray Expr) (c : Cnstr NodeId) (h : Expr) : Expr :=
+  let u := nodes[c.a]!
+  let v := nodes[c.b]!
+  if c.k == 0 then
+    mkApp3 (mkConst ``Nat.of_le_eq_false) u v h
+  else if c.k == -1 && c.le then
+    mkApp3 (mkConst ``Nat.of_lo_eq_false_1) u v h
+  else if c.k < 0 then
+    mkApp4 (mkConst ``Nat.of_lo_eq_false) u v (toExpr (-c.k).toNat) h
+  else
+    mkApp4 (mkConst ``Nat.of_ro_eq_false) u v (toExpr c.k.toNat) h
+
+end Offset
+
+end Lean.Meta.Grind.Arith

src/Lean/Meta/Tactic/Grind/Arith/Types.lean

@@ -0,0 +1,58 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Data.PersistentArray
+import Lean.Meta.Tactic.Grind.ENodeKey
+import Lean.Meta.Tactic.Grind.Arith.Util
+
+namespace Lean.Meta.Grind.Arith
+
+namespace Offset
+
+abbrev NodeId := Nat
+
+instance : ToMessageData (Offset.Cnstr NodeId) where
+  toMessageData c := Offset.toMessageData (α := NodeId) (inst := { toMessageData n := m!"#{n}" }) c
+
+/-- Auxiliary structure used for proof extraction.  -/
+structure ProofInfo where
+  w     : NodeId
+  k     : Int
+  proof : Expr
+  deriving Inhabited
+
+/-- State of the constraint offset procedure. -/
+structure State where
+  nodes   : PArray Expr := {}
+  nodeMap : PHashMap ENodeKey NodeId := {}
+  cnstrs  : PHashMap ENodeKey (Cnstr NodeId) := {}
+  /--
+  For each node with id `u`, `sources[u]` contains
+  pairs `(v, k)` s.t. there is a path from `v` to `u` with weight `k`.
+  -/
+  sources : PArray (AssocList NodeId Int) := {}
+  /--
+  For each node with id `u`, `targets[u]` contains
+  pairs `(v, k)` s.t. there is a path from `u` to `v` with weight `k`.
+  -/
+  targets : PArray (AssocList NodeId Int) := {}
+  /--
+  Proof reconstruction information. For each node with id `u`, `proofs[u]` contains
+  pairs `(v, { w, proof })` s.t. there is a path from `u` to `v`, and
+  `w` is the penultimate node in the path, and `proof` is the justification for
+  the last edge.
+  -/
+  proofs  : PArray (AssocList NodeId ProofInfo) := {}
+  deriving Inhabited
+
+end Offset
+
+/-- State for the arithmetic procedures. -/
+structure State where
+  offset : Offset.State := {}
+  deriving Inhabited
+
+end Lean.Meta.Grind.Arith

src/Lean/Meta/Tactic/Grind/Arith/Util.lean

@@ -0,0 +1,89 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Expr
+import Lean.Message
+
+namespace Lean.Meta.Grind.Arith
+
+/-- Returns `true` if `e` is of the form `Nat` -/
+def isNatType (e : Expr) : Bool :=
+  e.isConstOf ``Nat
+
+/-- Returns `true` if `e` is of the form `@instHAdd Nat instAddNat` -/
+def isInstAddNat (e : Expr) : Bool :=
+  let_expr instHAdd a b := e | false
+  isNatType a && b.isConstOf ``instAddNat
+
+/-- Returns `true` if `e` is `instLENat` -/
+def isInstLENat (e : Expr) : Bool :=
+  e.isConstOf ``instLENat
+
+/--
+Returns `some (a, b)` if `e` is of the form
+```
+@HAdd.hAdd Nat Nat Nat (instHAdd Nat instAddNat) a b
+```
+-/
+def isNatAdd? (e : Expr) : Option (Expr × Expr) :=
+  let_expr HAdd.hAdd _ _ _ i a b := e | none
+  if isInstAddNat i then some (a, b) else none
+
+/-- Returns `some k` if `e` `@OfNat.ofNat Nat _ (instOfNatNat k)` -/
+def isNatNum? (e : Expr) : Option Nat := Id.run do
+  let_expr OfNat.ofNat _ _ inst := e | none
+  let_expr instOfNatNat k := inst | none
+  let .lit (.natVal k) := k | none
+  some k
+
+/-- Returns `some (a, k)` if `e` is of the form `a + k`.  -/
+def isNatOffset? (e : Expr) : Option (Expr × Nat) := Id.run do
+  let some (a, b) := isNatAdd? e | none
+  let some k := isNatNum? b | none
+  some (a, k)
+
+/-- An offset constraint. -/
+structure Offset.Cnstr (α : Type) where
+  a  : α
+  b  : α
+  k  : Int := 0
+  le : Bool := true
+  deriving Inhabited
+
+def Offset.Cnstr.neg : Cnstr α → Cnstr α
+  | { a, b, k, le } => { a := b, b := a, le, k := -k - 1 }
+
+example (c : Offset.Cnstr α) : c.neg.neg = c := by
+  cases c; simp [Offset.Cnstr.neg]; omega
+
+def Offset.toMessageData [inst : ToMessageData α] (c : Offset.Cnstr α) : MessageData :=
+  match c.k, c.le with
+  | .ofNat 0,   true  => m!"{c.a} ≤ {c.b}"
+  | .ofNat 0,   false => m!"{c.a} = {c.b}"
+  | .ofNat k,   true  => m!"{c.a} ≤ {c.b} + {k}"
+  | .ofNat k,   false => m!"{c.a} = {c.b} + {k}"
+  | .negSucc k, true  => m!"{c.a} + {k + 1} ≤ {c.b}"
+  | .negSucc k, false => m!"{c.a} + {k + 1} = {c.b}"
+
+instance : ToMessageData (Offset.Cnstr Expr) where
+  toMessageData c := Offset.toMessageData c
+
+/-- Returns `some cnstr` if `e` is offset constraint. -/
+def isNatOffsetCnstr? (e : Expr) : Option (Offset.Cnstr Expr) :=
+  match_expr e with
+  | LE.le _ inst a b => if isInstLENat inst then go a b true else none
+  | Eq α a b => if isNatType α then go a b false else none
+  | _ => none
+where
+  go (a b : Expr) (le : Bool) :=
+    if let some (a, k) := isNatOffset? a then
+      some { a, k := - k, b, le }
+    else if let some (b, k) := isNatOffset? b then
+      some { a, b, k := k, le }
+    else
+      some { a, b, le }
+
+end Lean.Meta.Grind.Arith

src/Lean/Meta/Tactic/Grind/Canon.lean

@@ -46,15 +46,35 @@ structure State where
   proofCanon : PHashMap Expr Expr := {}
   deriving Inhabited
 
+inductive CanonElemKind where
+  | /--
+    Type class instances are canonicalized using `TransparencyMode.instances`.
+    -/
+    instance
+  | /--
+    Types and Type formers are canonicalized using `TransparencyMode.default`.
+    Remark: propositions are just visited. We do not invoke `canonElemCore` for them.
+    -/
+    type
+  | /--
+    Implicit arguments that are not types, type formers, or instances, are canonicalized
+    using `TransparencyMode.reducible`
+    -/
+    implicit
+  deriving BEq
+
+def CanonElemKind.explain : CanonElemKind → String
+  | .instance => "type class instances"
+  | .type => "types (or type formers)"
+  | .implicit => "implicit arguments (which are not type class instances or types)"
+
 /--
 Helper function for canonicalizing `e` occurring as the `i`th argument of an `f`-application.
-`isInst` is true if `e` is an type class instance.
 
-Recall that we use `TransparencyMode.instances` for checking whether two instances are definitionally equal or not.
-Thus, if diagnostics are enabled, we also check them using `TransparencyMode.default`. If the result is different
+Thus, if diagnostics are enabled, we also re-check them using `TransparencyMode.default`. If the result is different
 we report to the user.
 -/
-def canonElemCore (f : Expr) (i : Nat) (e : Expr) (isInst : Bool) : StateT State MetaM Expr := do
+def canonElemCore (f : Expr) (i : Nat) (e : Expr) (kind : CanonElemKind) : StateT State MetaM Expr := do
   let s ← get
   if let some c := s.canon.find? e then
     return c
@@ -66,16 +86,19 @@ def canonElemCore (f : Expr) (i : Nat) (e : Expr) (isInst : Bool) : StateT State
       -- in general safe to replace `e` with `c` if `c` has more free variables than `e`.
       -- However, we don't revert previously canonicalized elements in the `grind` tactic.
       modify fun s => { s with canon := s.canon.insert e c }
+      trace[grind.debug.canon] "found {e} ===> {c}"
       return c
-    if isInst then
-      if (← isDiagnosticsEnabled <&&> pure (c.fvarsSubset e) <&&> (withDefault <| isDefEq e c)) then
+    if kind != .type then
+      if (← isTracingEnabledFor `grind.issues <&&> (withDefault <| isDefEq e c)) then
         -- TODO: consider storing this information in some structure that can be browsed later.
-        trace[grind.issues] "the following `grind` static elements are definitionally equal with `default` transparency, but not with `instances` transparency{indentExpr e}\nand{indentExpr c}"
+        trace[grind.issues] "the following {kind.explain} are definitionally equal with `default` transparency but not with a more restrictive transparency{indentExpr e}\nand{indentExpr c}"
+  trace[grind.debug.canon] "({f}, {i}) ↦ {e}"
   modify fun s => { s with canon := s.canon.insert e e, argMap := s.argMap.insert key (e::cs) }
   return e
 
-abbrev canonType (f : Expr) (i : Nat) (e : Expr) := withDefault <| canonElemCore f i e false
-abbrev canonInst (f : Expr) (i : Nat) (e : Expr) := withReducibleAndInstances <| canonElemCore f i e true
+abbrev canonType (f : Expr) (i : Nat) (e : Expr) := withDefault <| canonElemCore f i e .type
+abbrev canonInst (f : Expr) (i : Nat) (e : Expr) := withReducibleAndInstances <| canonElemCore f i e .instance
+abbrev canonImplicit (f : Expr) (i : Nat) (e : Expr) := withReducible <| canonElemCore f i e .implicit
 
 /--
 Return type for the `shouldCanon` function.
@@ -85,6 +108,8 @@ private inductive ShouldCanonResult where
     canonType
   | /- Nested instances are canonicalized. -/
     canonInst
+  | /- Implicit argument that is not an instance nor a type. -/
+    canonImplicit
   | /-
     Term is not a proof, type (former), nor an instance.
     Thus, it must be recursively visited by the canonizer.
@@ -92,6 +117,13 @@ private inductive ShouldCanonResult where
     visit
   deriving Inhabited
 
+instance : Repr ShouldCanonResult where
+  reprPrec r _ := match r with
+    | .canonType => "canonType"
+    | .canonInst => "canonInst"
+    | .canonImplicit => "canonImplicit"
+    | .visit => "visit"
+
 /--
 See comments at `ShouldCanonResult`.
 -/
@@ -102,7 +134,14 @@ def shouldCanon (pinfos : Array ParamInfo) (i : Nat) (arg : Expr) : MetaM Should
       return .canonInst
     else if pinfo.isProp then
       return .visit
-  if (← isTypeFormer arg) then
+    else if pinfo.isImplicit then
+      if (← isTypeFormer arg) then
+        return .canonType
+      else
+        return .canonImplicit
+  if (← isProp arg) then
+    return .visit
+  else if (← isTypeFormer arg) then
     return .canonType
   else
     return .visit
@@ -132,9 +171,11 @@ where
           let mut args := args.toVector
           for h : i in [:args.size] do
             let arg := args[i]
+            trace[grind.debug.canon] "[{repr (← shouldCanon pinfos i arg)}]: {arg} : {← inferType arg}"
             let arg' ← match (← shouldCanon pinfos i arg) with
             | .canonType  => canonType f i arg
             | .canonInst  => canonInst f i arg
+            | .canonImplicit => canonImplicit f i (← visit arg)
             | .visit      => visit arg
             unless ptrEq arg arg' do
               args := args.set i arg'
@@ -151,7 +192,8 @@ where
     return e'
 
 /-- Canonicalizes nested types, type formers, and instances in `e`. -/
-def canon (e : Expr) : StateT State MetaM Expr :=
+def canon (e : Expr) : StateT State MetaM Expr := do
+  trace[grind.debug.canon] "{e}"
   unsafe canonImpl e
 
 end Canon

src/Lean/Meta/Tactic/Grind/Core.lean

@@ -141,6 +141,7 @@ where
     updateRoots lhs rhsNode.root
     trace_goal[grind.debug] "{← ppENodeRef lhs} new root {← ppENodeRef rhsNode.root}, {← ppENodeRef (← getRoot lhs)}"
     reinsertParents parents
+    propagateEqcDown lhs
     setENode lhsNode.root { (← getENode lhsRoot.self) with -- We must retrieve `lhsRoot` since it was updated.
       next := rhsRoot.next
     }
@@ -158,14 +159,13 @@ where
       updateMT rhsRoot.self
 
   updateRoots (lhs : Expr) (rootNew : Expr) : GoalM Unit := do
-    let rec loop (e : Expr) : GoalM Unit := do
-      let n ← getENode e
-      setENode e { n with root := rootNew }
+    traverseEqc lhs fun n =>
+      setENode n.self { n with root := rootNew }
+
+  propagateEqcDown (lhs : Expr) : GoalM Unit := do
+    traverseEqc lhs fun n =>
       unless (← isInconsistent) do
-        propagateDown e
-      if isSameExpr lhs n.next then return ()
-      loop n.next
-    loop lhs
+        propagateDown n.self
 
 /-- Ensures collection of equations to be processed is empty. -/
 private def resetNewEqs : GoalM Unit :=
@@ -217,14 +217,22 @@ def add (fact : Expr) (proof : Expr) (generation := 0) : GoalM Unit := do
 where
   go (p : Expr) (isNeg : Bool) : GoalM Unit := do
     match_expr p with
-    | Eq _ lhs rhs => goEq p lhs rhs isNeg false
-    | HEq _ lhs _ rhs => goEq p lhs rhs isNeg true
-    | _ =>
-      internalize p generation
-      if isNeg then
-        addEq p (← getFalseExpr) (← mkEqFalse proof)
+    | Eq α lhs rhs =>
+      if α.isProp then
+        -- It is morally an iff.
+        -- We do not use the `goEq` optimization because we want to register `p` as a case-split
+        goFact p isNeg
       else
-        addEq p (← getTrueExpr) (← mkEqTrue proof)
+        goEq p lhs rhs isNeg false
+    | HEq _ lhs _ rhs => goEq p lhs rhs isNeg true
+    | _ => goFact p isNeg
+
+  goFact (p : Expr) (isNeg : Bool) : GoalM Unit := do
+    internalize p generation
+    if isNeg then
+      addEq p (← getFalseExpr) (← mkEqFalse proof)
+    else
+      addEq p (← getTrueExpr) (← mkEqTrue proof)
 
   goEq (p : Expr) (lhs rhs : Expr) (isNeg : Bool) (isHEq : Bool) : GoalM Unit := do
     if isNeg then

src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean

@@ -57,7 +57,8 @@ inductive Origin where
   is the provided grind argument. The `id` is a unique identifier for the call.
   -/
   | stx (id : Name) (ref : Syntax)
-  | other (id : Name)
+  /-- It is local, but we don't have a local hypothesis for it. -/
+  | local (id : Name)
   deriving Inhabited, Repr, BEq
 
 /-- A unique identifier corresponding to the origin. -/
@@ -65,14 +66,14 @@ def Origin.key : Origin → Name
   | .decl declName => declName
   | .fvar fvarId   => fvarId.name
   | .stx id _      => id
-  | .other id      => id
+  | .local id      => id
 
 def Origin.pp [Monad m] [MonadEnv m] [MonadError m] (o : Origin) : m MessageData := do
   match o with
   | .decl declName => return MessageData.ofConst (← mkConstWithLevelParams declName)
   | .fvar fvarId   => return mkFVar fvarId
   | .stx _ ref     => return ref
-  | .other id      => return id
+  | .local id      => return id
 
 instance : BEq Origin where
   beq a b := a.key == b.key
@@ -169,11 +170,43 @@ private builtin_initialize ematchTheoremsExt : SimpleScopedEnvExtension EMatchTh
     initial  := {}
   }
 
+/--
+Symbols with built-in support in `grind` are unsuitable as pattern candidates for E-matching.
+This is because `grind` performs normalization operations and uses specialized data structures
+to implement these symbols, which may interfere with E-matching behavior.
+-/
 -- TODO: create attribute?
 private def forbiddenDeclNames := #[``Eq, ``HEq, ``Iff, ``And, ``Or, ``Not]
 
 private def isForbidden (declName : Name) := forbiddenDeclNames.contains declName
 
+/--
+Auxiliary function to expand a pattern containing forbidden application symbols
+into a multi-pattern.
+
+This function enhances the usability of the `[grind =]` attribute by automatically handling
+forbidden pattern symbols. For example, consider the following theorem tagged with this attribute:
+```
+getLast?_eq_some_iff {xs : List α} {a : α} : xs.getLast? = some a ↔ ∃ ys, xs = ys ++ [a]
+```
+Here, the selected pattern is `xs.getLast? = some a`, but `Eq` is a forbidden pattern symbol.
+Instead of producing an error, this function converts the pattern into a multi-pattern,
+allowing the attribute to be used conveniently.
+
+The function recursively expands patterns with forbidden symbols by splitting them
+into their sub-components. If the pattern does not contain forbidden symbols,
+it is returned as-is.
+-/
+partial def splitWhileForbidden (pat : Expr) : List Expr :=
+  match_expr pat with
+  | Not p => splitWhileForbidden p
+  | And p₁ p₂ => splitWhileForbidden p₁ ++ splitWhileForbidden p₂
+  | Or p₁ p₂ => splitWhileForbidden p₁ ++ splitWhileForbidden p₂
+  | Eq _ lhs rhs => splitWhileForbidden lhs ++ splitWhileForbidden rhs
+  | Iff lhs rhs => splitWhileForbidden lhs ++ splitWhileForbidden rhs
+  | HEq _ lhs _ rhs => splitWhileForbidden lhs ++ splitWhileForbidden rhs
+  | _ => [pat]
+
 private def dontCare := mkConst (Name.mkSimple "[grind_dontcare]")
 
 def mkGroundPattern (e : Expr) : Expr :=
@@ -467,7 +500,8 @@ def mkEMatchEqTheoremCore (origin : Origin) (levelParams : Array Name) (proof :
       | _ => throwError "invalid E-matching equality theorem, conclusion must be an equality{indentExpr type}"
     let pat := if useLhs then lhs else rhs
     let pat ← preprocessPattern pat normalizePattern
-    return (xs.size, [pat.abstract xs])
+    let pats := splitWhileForbidden (pat.abstract xs)
+    return (xs.size, pats)
   mkEMatchTheoremCore origin levelParams numParams proof patterns
 
 /--
@@ -498,7 +532,7 @@ def addEMatchEqTheorem (declName : Name) : MetaM Unit := do
 def getEMatchTheorems : CoreM EMatchTheorems :=
   return ematchTheoremsExt.getState (← getEnv)
 
-private inductive TheoremKind where
+inductive TheoremKind where
   | eqLhs | eqRhs | eqBoth | fwd | bwd | default
   deriving Inhabited, BEq
 
@@ -598,7 +632,7 @@ private def collectPatterns? (proof : Expr) (xs : Array Expr) (searchPlaces : Ar
     | return none
   return some (ps, s.symbols.toList)
 
-private def mkEMatchTheoremWithKind? (origin : Origin) (levelParams : Array Name) (proof : Expr) (kind : TheoremKind) : MetaM (Option EMatchTheorem) := do
+def mkEMatchTheoremWithKind? (origin : Origin) (levelParams : Array Name) (proof : Expr) (kind : TheoremKind) : MetaM (Option EMatchTheorem) := do
   if kind == .eqLhs then
     return (← mkEMatchEqTheoremCore origin levelParams proof (normalizePattern := false) (useLhs := true))
   else if kind == .eqRhs then

src/Lean/Meta/Tactic/Grind/ENodeKey.lean

@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Expr
+
+namespace Lean.Meta.Grind
+
+@[inline] def isSameExpr (a b : Expr) : Bool :=
+  -- It is safe to use pointer equality because we hashcons all expressions
+  -- inserted into the E-graph
+  unsafe ptrEq a b
+
+/--
+Key for the `ENodeMap` and `ParentMap` map.
+We use pointer addresses and rely on the fact all internalized expressions
+have been hash-consed, i.e., we have applied `shareCommon`.
+-/
+structure ENodeKey where
+  expr : Expr
+
+instance : Hashable ENodeKey where
+  hash k := unsafe (ptrAddrUnsafe k.expr).toUInt64
+
+instance : BEq ENodeKey where
+  beq k₁ k₂ := isSameExpr k₁.expr k₂.expr
+
+end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/ForallProp.lean

@@ -46,11 +46,57 @@ where
       -- b = True → (a → b) = True
       pushEqTrue e <| mkApp3 (mkConst ``Grind.imp_eq_of_eq_true_right) a b (← mkEqTrueProof b)
 
-def propagateImpliesDown (e : Expr) : GoalM Unit := do
+private def isEqTrueHyp? (proof : Expr) : Option FVarId := Id.run do
+  let_expr eq_true _ p := proof | return none
+  let .fvar fvarId := p | return none
+  return some fvarId
+
+/-- Similar to `mkEMatchTheoremWithKind?`, but swallow any exceptions. -/
+private def mkEMatchTheoremWithKind'? (origin : Origin) (proof : Expr) (kind : TheoremKind) : MetaM (Option EMatchTheorem) := do
+  try
+    mkEMatchTheoremWithKind? origin #[] proof kind
+  catch _ =>
+    return none
+
+private def addLocalEMatchTheorems (e : Expr) : GoalM Unit := do
+  let proof ← mkEqTrueProof e
+  let origin ← if let some fvarId := isEqTrueHyp? proof then
+    pure <| .fvar fvarId
+  else
+    let idx ← modifyGet fun s => (s.nextThmIdx, { s with nextThmIdx := s.nextThmIdx + 1 })
+    pure <| .local ((`local).appendIndexAfter idx)
+  let proof := mkApp2 (mkConst ``of_eq_true) e proof
+  let size := (← get).newThms.size
+  let gen ← getGeneration e
+  -- TODO: we should have a flag for collecting all unary patterns in a local theorem
+  if let some thm ← mkEMatchTheoremWithKind'? origin proof .fwd then
+    activateTheorem thm gen
+  if let some thm ← mkEMatchTheoremWithKind'? origin proof .bwd then
+    activateTheorem thm gen
+  if (← get).newThms.size == size then
+    if let some thm ← mkEMatchTheoremWithKind'? origin proof .default then
+      activateTheorem thm gen
+  if (← get).newThms.size == size then
+    trace[grind.issues] "failed to create E-match local theorem for{indentExpr e}"
+
+def propagateForallPropDown (e : Expr) : GoalM Unit := do
+  let .forallE n a b bi := e | return ()
   if (← isEqFalse e) then
-    let .forallE _ a b _ := e | return ()
-    let h ← mkEqFalseProof e
-    pushEqTrue a <| mkApp3 (mkConst ``Grind.eq_true_of_imp_eq_false) a b h
-    pushEqFalse b <| mkApp3 (mkConst ``Grind.eq_false_of_imp_eq_false) a b h
+    if b.hasLooseBVars then
+      let α := a
+      let p := b
+      -- `e` is of the form `∀ x : α, p x`
+      -- Add fact `∃ x : α, ¬ p x`
+      let u ← getLevel α
+      let prop := mkApp2 (mkConst ``Exists [u]) α (mkLambda n bi α (mkNot p))
+      let proof := mkApp3 (mkConst ``Grind.of_forall_eq_false [u]) α (mkLambda n bi α p) (← mkEqFalseProof e)
+      addNewFact proof prop (← getGeneration e)
+    else
+      let h ← mkEqFalseProof e
+      pushEqTrue a <| mkApp3 (mkConst ``Grind.eq_true_of_imp_eq_false) a b h
+      pushEqFalse b <| mkApp3 (mkConst ``Grind.eq_false_of_imp_eq_false) a b h
+  else if (← isEqTrue e) then
+    if b.hasLooseBVars then
+      addLocalEMatchTheorems e
 
 end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/Internalize.lean

@@ -11,6 +11,7 @@ import Lean.Meta.Match.MatcherInfo
 import Lean.Meta.Match.MatchEqsExt
 import Lean.Meta.Tactic.Grind.Types
 import Lean.Meta.Tactic.Grind.Util
+import Lean.Meta.Tactic.Grind.Arith.Internalize
 
 namespace Lean.Meta.Grind
 
@@ -53,25 +54,36 @@ private def addSplitCandidate (e : Expr) : GoalM Unit := do
 -- TODO: add attribute to make this extensible
 private def forbiddenSplitTypes := [``Eq, ``HEq, ``True, ``False]
 
+/-- Returns `true` if `e` is of the form `@Eq Prop a b` -/
+def isMorallyIff (e : Expr) : Bool :=
+  let_expr Eq α _ _ := e | false
+  α.isProp
+
 /-- Inserts `e` into the list of case-split candidates if applicable. -/
 private def checkAndAddSplitCandidate (e : Expr) : GoalM Unit := do
   unless e.isApp do return ()
-  if e.isIte || e.isDIte then
+  if (← getConfig).splitIte && (e.isIte || e.isDIte) then
     addSplitCandidate e
-  else if (← isMatcherApp e) then
-    if let .reduced _ ← reduceMatcher? e then
-      -- When instantiating `match`-equations, we add `match`-applications that can be reduced,
-      -- and consequently don't need to be splitted.
-      return ()
-    else
-      addSplitCandidate e
-  else
-    let .const declName _  := e.getAppFn | return ()
+    return ()
+  if isMorallyIff e then
+    addSplitCandidate e
+    return ()
+  if (← getConfig).splitMatch then
+    if (← isMatcherApp e) then
+      if let .reduced _ ← reduceMatcher? e then
+        -- When instantiating `match`-equations, we add `match`-applications that can be reduced,
+        -- and consequently don't need to be splitted.
+        return ()
+      else
+        addSplitCandidate e
+        return ()
+  let .const declName _  := e.getAppFn | return ()
     if forbiddenSplitTypes.contains declName then return ()
     -- We should have a mechanism for letting users to select types to case-split.
     -- Right now, we just consider inductive predicates that are not in the forbidden list
-    if (← isInductivePredicate declName) then
-      addSplitCandidate e
+    if (← getConfig).splitIndPred then
+      if (← isInductivePredicate declName) then
+        addSplitCandidate e
 
 /--
 If `e` is a `cast`-like term (e.g., `cast h a`), add `HEq e a` to the to-do list.
@@ -98,7 +110,7 @@ private partial def internalizePattern (pattern : Expr) (generation : Nat) : Goa
   else pattern.withApp fun f args => do
     return mkAppN f (← args.mapM (internalizePattern · generation))
 
-private partial def activateTheorem (thm : EMatchTheorem) (generation : Nat) : GoalM Unit := do
+partial def activateTheorem (thm : EMatchTheorem) (generation : Nat) : GoalM Unit := do
   -- Recall that we use the proof as part of the key for a set of instances found so far.
   -- We don't want to use structural equality when comparing keys.
   let proof ← shareCommon thm.proof
@@ -185,6 +197,7 @@ partial def internalize (e : Expr) (generation : Nat) : GoalM Unit := do
       mkENode e generation
       addCongrTable e
       updateAppMap e
+      Arith.internalize e
       propagateUp e
 end
 

src/Lean/Meta/Tactic/Grind/Inv.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Lean.Meta.Tactic.Grind.Types
 import Lean.Meta.Tactic.Grind.Proof
+import Lean.Meta.Tactic.Grind.Arith.Inv
 
 namespace Lean.Meta.Grind
 
@@ -58,9 +59,12 @@ private def checkParents (e : Expr) : GoalM Unit := do
           found := true
           break
       -- Recall that we have support for `Expr.forallE` propagation. See `ForallProp.lean`.
-      if let .forallE _ d _ _ := parent then
+      if let .forallE _ d b _ := parent then
         if (← checkChild d) then
           found := true
+        unless b.hasLooseBVars do
+          if (← checkChild b) then
+            found := true
       unless found do
         assert! (← checkChild parent.getAppFn)
   else
@@ -100,6 +104,7 @@ def checkInvariants (expensive := false) : GoalM Unit := do
         checkEqc node
     if expensive then
       checkPtrEqImpliesStructEq
+    Arith.checkInvariants
   if expensive && grind.debug.proofs.get (← getOptions) then
     checkProofs
 

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

@@ -30,7 +30,7 @@ def mkMethods (fallback : Fallback) : CoreM Methods := do
      if let some prop := builtinPropagators.up[declName]? then
        prop e
     propagateDown := fun e => do
-     propagateImpliesDown e
+     propagateForallPropDown e
      let .const declName _ := e.getAppFn | return ()
      if let some prop := builtinPropagators.down[declName]? then
        prop e
@@ -70,7 +70,7 @@ def all (goals : List Goal) (f : Goal → GrindM (List Goal)) : GrindM (List Goa
 
 /-- A very simple strategy -/
 private def simple (goals : List Goal) : GrindM (List Goal) := do
-  applyToAll (ematchStar >> (splitNext >> ematchStar).iterate) goals
+  applyToAll (assertAll >> ematchStar >> (splitNext >> assertAll >> ematchStar).iterate) goals
 
 def main (mvarId : MVarId) (config : Grind.Config) (mainDeclName : Name) (fallback : Fallback) : MetaM (List MVarId) := do
   let go : GrindM (List MVarId) := do

src/Lean/Meta/Tactic/Grind/Split.lean

@@ -14,77 +14,123 @@ namespace Lean.Meta.Grind
 inductive CaseSplitStatus where
   | resolved
   | notReady
-  | ready
+  | ready (numCases : Nat) (isRec := false)
   deriving Inhabited, BEq
 
+/-- Given `c`, the condition of an `if-then-else`, check whether we need to case-split on the `if-then-else` or not -/
+private def checkIteCondStatus (c : Expr) : GoalM CaseSplitStatus := do
+  if (← isEqTrue c <||> isEqFalse c) then
+    return .resolved
+  else
+    return .ready 2
+
+/--
+Given `e` of the form `a ∨ b`, check whether we are ready to case-split on `e`.
+That is, `e` is `True`, but neither `a` nor `b` is `True`."
+-/
+private def checkDisjunctStatus (e a b : Expr) : GoalM CaseSplitStatus := do
+  if (← isEqTrue e) then
+    if (← isEqTrue a <||> isEqTrue b) then
+      return .resolved
+    else
+      return .ready 2
+  else if (← isEqFalse e) then
+    return .resolved
+  else
+    return .notReady
+
+/--
+Given `e` of the form `a ∧ b`, check whether we are ready to case-split on `e`.
+That is, `e` is `False`, but neither `a` nor `b` is `False`.
+ -/
+private def checkConjunctStatus (e a b : Expr) : GoalM CaseSplitStatus := do
+  if (← isEqTrue e) then
+    return .resolved
+  else if (← isEqFalse e) then
+    if (← isEqFalse a <||> isEqFalse b) then
+      return .resolved
+    else
+      return .ready 2
+  else
+    return .notReady
+
+/--
+Given `e` of the form `@Eq Prop a b`, check whether we are ready to case-split on `e`.
+There are two cases:
+1- `e` is `True`, but neither both `a` and `b` are `True`, nor both `a` and `b` are `False`.
+2- `e` is `False`, but neither `a` is `True` and `b` is `False`, nor `a` is `False` and `b` is `True`.
+-/
+private def checkIffStatus (e a b : Expr) : GoalM CaseSplitStatus := do
+  if (← isEqTrue e) then
+    if (← (isEqTrue a <&&> isEqTrue b) <||> (isEqFalse a <&&> isEqFalse b)) then
+      return .resolved
+    else
+      return .ready 2
+  else if (← isEqFalse e) then
+    if (← (isEqTrue a <&&> isEqFalse b) <||> (isEqFalse a <&&> isEqTrue b)) then
+      return .resolved
+    else
+      return .ready 2
+  else
+    return .notReady
+
 private def checkCaseSplitStatus (e : Expr) : GoalM CaseSplitStatus := do
   match_expr e with
-  | Or a b =>
-    if (← isEqTrue e) then
-      if (← isEqTrue a <||> isEqTrue b) then
-        return .resolved
-      else
-        return .ready
-    else if (← isEqFalse e) then
-      return .resolved
-    else
-      return .notReady
-  | And a b =>
-    if (← isEqTrue e) then
-      return .resolved
-    else if (← isEqFalse e) then
-      if (← isEqFalse a <||> isEqFalse b) then
-        return .resolved
-      else
-        return .ready
-    else
-      return .notReady
-  | ite _ c _ _ _ =>
-    if (← isEqTrue c <||> isEqFalse c) then
-      return .resolved
-    else
-      return .ready
-  | dite _ c _ _ _ =>
-    if (← isEqTrue c <||> isEqFalse c) then
-      return .resolved
-    else
-      return .ready
+  | Or a b => checkDisjunctStatus e a b
+  | And a b => checkConjunctStatus e a b
+  | Eq _ a b => checkIffStatus e a b
+  | ite _ c _ _ _ => checkIteCondStatus c
+  | dite _ c _ _ _ => checkIteCondStatus c
   | _ =>
     if (← isResolvedCaseSplit e) then
       trace[grind.debug.split] "split resolved: {e}"
       return .resolved
-    if (← isMatcherApp e) then
-      return .ready
+    if let some info := isMatcherAppCore? (← getEnv) e then
+      return .ready info.numAlts
     let .const declName .. := e.getAppFn | unreachable!
-    if (← isInductivePredicate declName <&&> isEqTrue e) then
-      return .ready
+    if let some info ← isInductivePredicate? declName then
+      if (← isEqTrue e) then
+        return .ready info.ctors.length info.isRec
     return .notReady
 
+private inductive SplitCandidate where
+  | none
+  | some (c : Expr) (numCases : Nat) (isRec : Bool)
+
 /-- Returns the next case-split to be performed. It uses a very simple heuristic. -/
-private def selectNextSplit? : GoalM (Option Expr) := do
-  if (← isInconsistent) then return none
-  if (← checkMaxCaseSplit) then return none
-  go (← get).splitCandidates none []
+private def selectNextSplit? : GoalM SplitCandidate := do
+  if (← isInconsistent) then return .none
+  if (← checkMaxCaseSplit) then return .none
+  go (← get).splitCandidates .none []
 where
-  go (cs : List Expr) (c? : Option Expr) (cs' : List Expr) : GoalM (Option Expr) := do
+  go (cs : List Expr) (c? : SplitCandidate) (cs' : List Expr) : GoalM SplitCandidate := do
     match cs with
     | [] =>
       modify fun s => { s with splitCandidates := cs'.reverse }
-      if c?.isSome then
+      if let .some _ numCases isRec := c? then
+        let numSplits := (← get).numSplits
+        -- We only increase the number of splits if there is more than one case or it is recursive.
+        let numSplits := if numCases > 1 || isRec then numSplits + 1 else numSplits
         -- Remark: we reset `numEmatch` after each case split.
         -- We should consider other strategies in the future.
-        modify fun s => { s with numSplits := s.numSplits + 1, numEmatch := 0 }
+        modify fun s => { s with numSplits, numEmatch := 0 }
       return c?
     | c::cs =>
     match (← checkCaseSplitStatus c) with
     | .notReady => go cs c? (c::cs')
     | .resolved => go cs c? cs'
-    | .ready =>
+    | .ready numCases isRec =>
     match c? with
-    | none => go cs (some c) cs'
-    | some c' =>
-      if (← getGeneration c) < (← getGeneration c') then
-        go cs (some c) (c'::cs')
+    | .none => go cs (.some c numCases isRec) cs'
+    | .some c' numCases' _ =>
+     let isBetter : GoalM Bool := do
+       if numCases == 1 && !isRec && numCases' > 1 then
+         return true
+       if (← getGeneration c) < (← getGeneration c') then
+         return true
+       return numCases < numCases'
+     if (← isBetter) then
+        go cs (.some c numCases isRec) (c'::cs')
       else
         go cs c? (c::cs')
 
@@ -94,6 +140,11 @@ private def mkCasesMajor (c : Expr) : GoalM Expr := do
   | And a b => return mkApp3 (mkConst ``Grind.or_of_and_eq_false) a b (← mkEqFalseProof c)
   | ite _ c _ _ _ => return mkEM c
   | dite _ c _ _ _ => return mkEM c
+  | Eq _ a b =>
+    if (← isEqTrue c) then
+      return mkApp3 (mkConst ``Grind.of_eq_eq_true) a b (← mkEqTrueProof c)
+    else
+      return mkApp3 (mkConst ``Grind.of_eq_eq_false) a b (← mkEqFalseProof c)
   | _ => return mkApp2 (mkConst ``of_eq_true) c (← mkEqTrueProof c)
 
 /-- Introduces new hypotheses in each goal. -/
@@ -108,9 +159,10 @@ and returns a new list of goals if successful.
 -/
 def splitNext : GrindTactic := fun goal => do
   let (goals?, _) ← GoalM.run goal do
-    let some c ← selectNextSplit?
+    let .some c numCases isRec ← selectNextSplit?
       | return none
     let gen ← getGeneration c
+    let genNew := if numCases > 1 || isRec then gen+1 else gen
     trace_goal[grind.split] "{c}, generation: {gen}"
     let mvarIds ← if (← isMatcherApp c) then
       casesMatch (← get).mvarId c
@@ -119,7 +171,7 @@ def splitNext : GrindTactic := fun goal => do
       cases (← get).mvarId major
     let goal ← get
     let goals := mvarIds.map fun mvarId => { goal with mvarId }
-    let goals ← introNewHyp goals [] (gen+1)
+    let goals ← introNewHyp goals [] genNew
     return some goals
   return goals?
 

src/Lean/Meta/Tactic/Grind/Types.lean

@@ -13,17 +13,14 @@ import Lean.Meta.CongrTheorems
 import Lean.Meta.AbstractNestedProofs
 import Lean.Meta.Tactic.Simp.Types
 import Lean.Meta.Tactic.Util
+import Lean.Meta.Tactic.Grind.ENodeKey
 import Lean.Meta.Tactic.Grind.Canon
 import Lean.Meta.Tactic.Grind.Attr
+import Lean.Meta.Tactic.Grind.Arith.Types
 import Lean.Meta.Tactic.Grind.EMatchTheorem
 
 namespace Lean.Meta.Grind
 
-@[inline] def isSameExpr (a b : Expr) : Bool :=
-  -- It is safe to use pointer equality because we hashcons all expressions
-  -- inserted into the E-graph
-  unsafe ptrEq a b
-
 /-- We use this auxiliary constant to mark delayed congruence proofs. -/
 def congrPlaceholderProof := mkConst (Name.mkSimple "[congruence]")
 
@@ -224,20 +221,6 @@ structure NewEq where
   proof : Expr
   isHEq : Bool
 
-/--
-Key for the `ENodeMap` and `ParentMap` map.
-We use pointer addresses and rely on the fact all internalized expressions
-have been hash-consed, i.e., we have applied `shareCommon`.
--/
-private structure ENodeKey where
-  expr : Expr
-
-instance : Hashable ENodeKey where
-  hash k := unsafe (ptrAddrUnsafe k.expr).toUInt64
-
-instance : BEq ENodeKey where
-  beq k₁ k₂ := isSameExpr k₁.expr k₂.expr
-
 abbrev ENodeMap := PHashMap ENodeKey ENode
 
 /--
@@ -368,6 +351,8 @@ structure Goal where
   gmt          : Nat := 0
   /-- Next unique index for creating ENodes -/
   nextIdx      : Nat := 0
+  /-- State of arithmetic procedures -/
+  arith        : Arith.State := {}
   /-- Active theorems that we have performed ematching at least once. -/
   thms         : PArray EMatchTheorem := {}
   /-- Active theorems that we have not performed any round of ematching yet. -/
@@ -393,6 +378,8 @@ structure Goal where
   numSplits : Nat := 0
   /-- Case-splits that do not have to be performed anymore. -/
   resolvedSplits : PHashSet ENodeKey := {}
+  /-- Next local E-match theorem idx. -/
+  nextThmIdx : Nat := 0
   deriving Inhabited
 
 def Goal.admit (goal : Goal) : MetaM Unit :=
@@ -700,6 +687,15 @@ def getENodes : GoalM (Array ENode) := do
   let nodes := (← get).enodes.toArray.map (·.2)
   return nodes.qsort fun a b => a.idx < b.idx
 
+/-- Executes `f` to each term in the equivalence class containing `e` -/
+@[inline] def traverseEqc (e : Expr) (f : ENode → GoalM Unit) : GoalM Unit := do
+  let mut curr := e
+  repeat
+    let n ← getENode curr
+    f n
+    if isSameExpr n.next e then return ()
+    curr := n.next
+
 def forEachENode (f : ENode → GoalM Unit) : GoalM Unit := do
   let nodes ← getENodes
   for n in nodes do
@@ -712,7 +708,7 @@ def filterENodes (p : ENode → GoalM Bool) : GoalM (Array ENode) := do
       ref.modify (·.push n)
   ref.get
 
-def forEachEqc (f : ENode → GoalM Unit) : GoalM Unit := do
+def forEachEqcRoot (f : ENode → GoalM Unit) : GoalM Unit := do
   let nodes ← getENodes
   for n in nodes do
     if isSameExpr n.self n.root then

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

@@ -50,18 +50,24 @@ def simpCnstr? (e : Expr) : MetaM (Option (Expr × Expr)) := do
   if let some arg := e.not? then
     let mut eNew?   := none
     let mut thmName := Name.anonymous
-    if arg.isAppOfArity ``LE.le 4 then
-      eNew?   := some (← mkLE (← mkAdd (arg.getArg! 3) (mkNatLit 1)) (arg.getArg! 2))
-      thmName := ``Nat.not_le_eq
-    else if arg.isAppOfArity ``GE.ge 4 then
-      eNew?   := some (← mkLE (← mkAdd (arg.getArg! 2) (mkNatLit 1)) (arg.getArg! 3))
-      thmName := ``Nat.not_ge_eq
-    else if arg.isAppOfArity ``LT.lt 4 then
-      eNew?   := some (← mkLE (arg.getArg! 3) (arg.getArg! 2))
-      thmName := ``Nat.not_lt_eq
-    else if arg.isAppOfArity ``GT.gt 4 then
-      eNew?   := some (← mkLE (arg.getArg! 2) (arg.getArg! 3))
-      thmName := ``Nat.not_gt_eq
+    match_expr arg with
+    | LE.le α _ _ _ =>
+      if α.isConstOf ``Nat then
+        eNew?   := some (← mkLE (← mkAdd (arg.getArg! 3) (mkNatLit 1)) (arg.getArg! 2))
+        thmName := ``Nat.not_le_eq
+    | GE.ge α _ _ _ =>
+      if α.isConstOf ``Nat then
+        eNew?   := some (← mkLE (← mkAdd (arg.getArg! 2) (mkNatLit 1)) (arg.getArg! 3))
+        thmName := ``Nat.not_ge_eq
+    | LT.lt α _ _ _ =>
+      if α.isConstOf ``Nat then
+        eNew?   := some (← mkLE (arg.getArg! 3) (arg.getArg! 2))
+        thmName := ``Nat.not_lt_eq
+    | GT.gt α _ _ _ =>
+      if α.isConstOf ``Nat then
+        eNew?   := some (← mkLE (arg.getArg! 2) (arg.getArg! 3))
+        thmName := ``Nat.not_gt_eq
+    | _ => pure ()
     if let some eNew := eNew? then
       let h₁ := mkApp2 (mkConst thmName) (arg.getArg! 2) (arg.getArg! 3)
       if let some (eNew', h₂) ← simpCnstrPos? eNew then

src/Std.lean

@@ -10,3 +10,4 @@ import Std.Sync
 import Std.Time
 import Std.Tactic
 import Std.Internal
+import Std.Net

src/Std/Net.lean

@@ -0,0 +1,7 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+prelude
+import Std.Net.Addr

src/Std/Net/Addr.lean

@@ -0,0 +1,197 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+prelude
+import Init.Data.Vector.Basic
+
+/-!
+This module contains Lean representations of IP and socket addresses:
+- `IPv4Addr`: Representing IPv4 addresses.
+- `SocketAddressV4`: Representing a pair of IPv4 address and port.
+- `IPv6Addr`: Representing IPv6 addresses.
+- `SocketAddressV6`: Representing a pair of IPv6 address and port.
+- `IPAddr`: Can either be an `IPv4Addr` or an `IPv6Addr`.
+- `SocketAddress`: Can either be a `SocketAddressV4` or `SocketAddressV6`.
+-/
+
+namespace Std
+namespace Net
+
+/--
+Representation of an IPv4 address.
+-/
+structure IPv4Addr where
+  /--
+  This structure represents the address: `octets[0].octets[1].octets[2].octets[3]`.
+  -/
+  octets : Vector UInt8 4
+  deriving Inhabited, DecidableEq
+
+/--
+A pair of an `IPv4Addr` and a port.
+-/
+structure SocketAddressV4 where
+  addr : IPv4Addr
+  port : UInt16
+  deriving Inhabited, DecidableEq
+
+/--
+Representation of an IPv6 address.
+-/
+structure IPv6Addr where
+  /--
+  This structure represents the address: `segments[0]:segments[1]:...`.
+  -/
+  segments : Vector UInt16 8
+  deriving Inhabited, DecidableEq
+
+/--
+A pair of an `IPv6Addr` and a port.
+-/
+structure SocketAddressV6 where
+  addr : IPv6Addr
+  port : UInt16
+  deriving Inhabited, DecidableEq
+
+/--
+An IP address, either IPv4 or IPv6.
+-/
+inductive IPAddr where
+  | v4 (addr : IPv4Addr)
+  | v6 (addr : IPv6Addr)
+  deriving Inhabited, DecidableEq
+
+/--
+Either a `SocketAddressV4` or `SocketAddressV6`.
+-/
+inductive SocketAddress where
+  | v4 (addr : SocketAddressV4)
+  | v6 (addr : SocketAddressV6)
+  deriving Inhabited, DecidableEq
+
+/--
+The kinds of address families supported by Lean, currently only IP variants.
+-/
+inductive AddressFamily where
+  | ipv4
+  | ipv6
+  deriving Inhabited, DecidableEq
+
+namespace IPv4Addr
+
+/--
+Build the IPv4 address `a.b.c.d`.
+-/
+def ofParts (a b c d : UInt8) : IPv4Addr :=
+  { octets := #v[a, b, c, d] }
+
+/--
+Try to parse `s` as an IPv4 address, returning `none` on failure.
+-/
+@[extern "lean_uv_pton_v4"]
+opaque ofString (s : @&String) : Option IPv4Addr
+
+/--
+Turn `addr` into a `String` in the usual IPv4 format.
+-/
+@[extern "lean_uv_ntop_v4"]
+opaque toString (addr : @&IPv4Addr) : String
+
+instance : ToString IPv4Addr where
+  toString := toString
+
+instance : Coe IPv4Addr IPAddr where
+  coe addr := .v4 addr
+
+end IPv4Addr
+
+namespace SocketAddressV4
+
+instance : Coe SocketAddressV4 SocketAddress where
+  coe addr := .v4 addr
+
+end SocketAddressV4
+
+namespace IPv6Addr
+
+/--
+Build the IPv6 address `a:b:c:d:e:f:g:h`.
+-/
+def ofParts (a b c d e f g h : UInt16) : IPv6Addr :=
+  { segments := #v[a, b, c, d, e, f, g, h] }
+
+/--
+Try to parse `s` as an IPv6 address according to
+[RFC 2373](https://datatracker.ietf.org/doc/html/rfc2373), returning `none` on failure.
+-/
+@[extern "lean_uv_pton_v6"]
+opaque ofString (s : @&String) : Option IPv6Addr
+
+/--
+Turn `addr` into a `String` in the IPv6 format described in
+[RFC 2373](https://datatracker.ietf.org/doc/html/rfc2373).
+-/
+@[extern "lean_uv_ntop_v6"]
+opaque toString (addr : @&IPv6Addr) : String
+
+instance : ToString IPv6Addr where
+  toString := toString
+
+instance : Coe IPv6Addr IPAddr where
+  coe addr := .v6 addr
+
+end IPv6Addr
+
+namespace SocketAddressV6
+
+instance : Coe SocketAddressV6 SocketAddress where
+  coe addr := .v6 addr
+
+end SocketAddressV6
+
+namespace IPAddr
+
+/--
+Obtain the `AddressFamily` associated with an `IPAddr`.
+-/
+def family : IPAddr → AddressFamily
+  | .v4 .. => .ipv4
+  | .v6 .. => .ipv6
+
+def toString : IPAddr → String
+  | .v4 addr => addr.toString
+  | .v6 addr => addr.toString
+
+instance : ToString IPAddr where
+  toString := toString
+
+end IPAddr
+
+namespace SocketAddress
+
+/--
+Obtain the `AddressFamily` associated with a `SocketAddress`.
+-/
+def family : SocketAddress → AddressFamily
+  | .v4 .. => .ipv4
+  | .v6 .. => .ipv6
+
+/--
+Obtain the `IPAddr` contained in a `SocketAddress`.
+-/
+def ipAddr : SocketAddress → IPAddr
+  | .v4 sa  => .v4 sa.addr
+  | .v6 sa  => .v6 sa.addr
+
+/--
+Obtain the port contained in a `SocketAddress`.
+-/
+def port : SocketAddress → UInt16
+  | .v4 sa | .v6 sa => sa.port
+
+end SocketAddress
+
+end Net
+end Std

src/Std/Time/Date/Unit/Month.lean

@@ -39,6 +39,12 @@ instance {x y : Ordinal} : Decidable (x < y) :=
 def Offset : Type := Int
   deriving Repr, BEq, Inhabited, Add, Sub, Mul, Div, Neg, ToString, LT, LE, DecidableEq
 
+instance {x y : Offset} : Decidable (x ≤ y) :=
+  Int.decLe x y
+
+instance {x y : Offset} : Decidable (x < y) :=
+  Int.decLt x y
+
 instance : OfNat Offset n :=
   ⟨Int.ofNat n⟩
 

src/Std/Time/Date/Unit/Week.lean

@@ -39,6 +39,12 @@ instance : Inhabited Ordinal where
 def Offset : Type := UnitVal (86400 * 7)
   deriving Repr, BEq, Inhabited, Add, Sub, Neg, LE, LT, ToString
 
+instance {x y : Offset} : Decidable (x ≤ y) :=
+  inferInstanceAs (Decidable (x.val ≤ y.val))
+
+instance {x y : Offset} : Decidable (x < y) :=
+  inferInstanceAs (Decidable (x.val < y.val))
+
 instance : OfNat Offset n := ⟨UnitVal.ofNat n⟩
 
 namespace Ordinal

src/Std/Time/Time/Unit/Hour.lean

@@ -40,7 +40,13 @@ instance {x y : Ordinal} : Decidable (x < y) :=
 or differences in hours.
 -/
 def Offset : Type := UnitVal 3600
-  deriving Repr, BEq, Inhabited, Add, Sub, Neg, ToString
+  deriving Repr, BEq, Inhabited, Add, Sub, Neg, ToString, LT, LE
+
+instance { x y : Offset } : Decidable (x ≤ y) :=
+  inferInstanceAs (Decidable (x.val ≤ y.val))
+
+instance { x y : Offset } : Decidable (x < y) :=
+  inferInstanceAs (Decidable (x.val < y.val))
 
 instance : OfNat Offset n :=
   ⟨UnitVal.ofNat n⟩

src/Std/Time/Time/Unit/Millisecond.lean

@@ -40,6 +40,12 @@ instance {x y : Ordinal} : Decidable (x < y) :=
 def Offset : Type := UnitVal (1 / 1000)
   deriving Repr, BEq, Inhabited, Add, Sub, Neg, LE, LT, ToString
 
+instance { x y : Offset } : Decidable (x ≤ y) :=
+  inferInstanceAs (Decidable (x.val ≤ y.val))
+
+instance { x y : Offset } : Decidable (x < y) :=
+  inferInstanceAs (Decidable (x.val < y.val))
+
 instance : OfNat Offset n :=
   ⟨UnitVal.ofNat n⟩
 

src/Std/Time/Time/Unit/Minute.lean

@@ -38,7 +38,13 @@ instance {x y : Ordinal} : Decidable (x < y) :=
 `Offset` represents a duration offset in minutes.
 -/
 def Offset : Type := UnitVal 60
-  deriving Repr, BEq, Inhabited, Add, Sub, Neg, ToString
+  deriving Repr, BEq, Inhabited, Add, Sub, Neg, ToString, LT, LE
+
+instance { x y : Offset } : Decidable (x ≤ y) :=
+  inferInstanceAs (Decidable (x.val ≤ y.val))
+
+instance { x y : Offset } : Decidable (x < y) :=
+  inferInstanceAs (Decidable (x.val < y.val))
 
 instance : OfNat Offset n :=
   ⟨UnitVal.ofInt <| Int.ofNat n⟩

src/Std/Time/Time/Unit/Nanosecond.lean

@@ -42,6 +42,9 @@ def Offset : Type := UnitVal (1 / 1000000000)
 instance { x y : Offset } : Decidable (x ≤ y) :=
   inferInstanceAs (Decidable (x.val ≤ y.val))
 
+instance { x y : Offset } : Decidable (x < y) :=
+  inferInstanceAs (Decidable (x.val < y.val))
+
 instance : OfNat Offset n :=
   ⟨UnitVal.ofNat n⟩
 

src/Std/Time/Time/Unit/Second.lean

@@ -51,6 +51,12 @@ instance {x y : Ordinal l} : Decidable (x < y) :=
 def Offset : Type := UnitVal 1
   deriving Repr, BEq, Inhabited, Add, Sub, Neg, LE, LT, ToString
 
+instance { x y : Offset } : Decidable (x ≤ y) :=
+  inferInstanceAs (Decidable (x.val ≤ y.val))
+
+instance { x y : Offset } : Decidable (x < y) :=
+  inferInstanceAs (Decidable (x.val < y.val))
+
 instance : OfNat Offset n :=
   ⟨UnitVal.ofNat n⟩
 

src/runtime/CMakeLists.txt

@@ -2,7 +2,7 @@ set(RUNTIME_OBJS debug.cpp thread.cpp mpz.cpp utf8.cpp
 object.cpp apply.cpp exception.cpp interrupt.cpp memory.cpp
 stackinfo.cpp compact.cpp init_module.cpp load_dynlib.cpp io.cpp hash.cpp
 platform.cpp alloc.cpp allocprof.cpp sharecommon.cpp stack_overflow.cpp
-process.cpp object_ref.cpp mpn.cpp mutex.cpp libuv.cpp)
+process.cpp object_ref.cpp mpn.cpp mutex.cpp libuv.cpp uv/net_addr.cpp)
 add_library(leanrt_initial-exec STATIC ${RUNTIME_OBJS})
 set_target_properties(leanrt_initial-exec PROPERTIES
   ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR})

src/runtime/uv/net_addr.cpp

@@ -0,0 +1,131 @@
+/*
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Henrik Böving
+*/
+
+#include "runtime/uv/net_addr.h"
+#include <cstring>
+
+namespace lean {
+
+#ifndef LEAN_EMSCRIPTEN
+
+void lean_ipv4_addr_to_in_addr(b_obj_arg ipv4_addr, in_addr* out) {
+    out->s_addr = 0;
+    for (int i = 0; i < 4; i++) {
+        uint32_t octet = (uint32_t)(uint8_t)lean_unbox(array_uget(ipv4_addr, i));
+        out->s_addr |= octet << (3 - i) * 8;
+    }
+    out->s_addr = htonl(out->s_addr);
+}
+
+void lean_ipv6_addr_to_in6_addr(b_obj_arg ipv6_addr, in6_addr* out) {
+    for (int i = 0; i < 8; i++) {
+        uint16_t segment = htons((uint16_t)lean_unbox(array_uget(ipv6_addr, i)));
+        out->s6_addr[2 * i] = (uint8_t)segment;
+        out->s6_addr[2 * i + 1] = (uint8_t)(segment >> 8);
+    }
+}
+
+lean_obj_res lean_in_addr_to_ipv4_addr(const in_addr* ipv4_addr) {
+    obj_res ret = alloc_array(0, 4);
+    uint32_t hostaddr = ntohl(ipv4_addr->s_addr);
+
+    for (int i = 0; i < 4; i++) {
+        uint8_t octet = (uint8_t)(hostaddr >> (3 - i) * 8);
+        array_push(ret, lean_box(octet));
+    }
+
+    lean_assert(array_size(ret) == 4);
+    return ret;
+}
+
+lean_obj_res lean_in6_addr_to_ipv6_addr(const in6_addr* ipv6_addr) {
+    obj_res ret = alloc_array(0, 8);
+
+    for (int i = 0; i < 16; i += 2) {
+        uint16_t part1 = (uint16_t)ipv6_addr->s6_addr[i];
+        uint16_t part2 = (uint16_t)ipv6_addr->s6_addr[i + 1];
+        uint16_t segment = ntohs((part2 << 8) | part1);
+        array_push(ret, lean_box(segment));
+    }
+
+    lean_assert(array_size(ret) == 8);
+    return ret;
+}
+
+/* Std.Net.IPV4Addr.ofString (s : @&String) : Option IPV4Addr */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_pton_v4(b_obj_arg str_obj) {
+    const char* str = string_cstr(str_obj);
+    in_addr internal;
+    if (uv_inet_pton(AF_INET, str, &internal) == 0) {
+        return mk_option_some(lean_in_addr_to_ipv4_addr(&internal));
+    } else {
+        return mk_option_none();
+    }
+}
+
+/* Std.Net.IPV4Addr.toString (addr : @&IPV4Addr) : String */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ntop_v4(b_obj_arg ipv4_addr) {
+    in_addr internal;
+    lean_ipv4_addr_to_in_addr(ipv4_addr, &internal);
+    char dst[INET_ADDRSTRLEN];
+    int ret = uv_inet_ntop(AF_INET, &internal, dst, sizeof(dst));
+    lean_always_assert(ret == 0);
+    return lean_mk_string(dst);
+}
+
+/* Std.Net.IPV6Addr.ofString (s : @&String) : Option IPV6Addr */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_pton_v6(b_obj_arg str_obj) {
+    const char* str = string_cstr(str_obj);
+    in6_addr internal;
+    if (uv_inet_pton(AF_INET6, str, &internal) == 0) {
+        return mk_option_some(lean_in6_addr_to_ipv6_addr(&internal));
+    } else {
+        return mk_option_none();
+    }
+}
+
+/* Std.Net.IPV6Addr.toString (addr : @&IPV6Addr) : String */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ntop_v6(b_obj_arg ipv6_addr) {
+    in6_addr internal;
+    lean_ipv6_addr_to_in6_addr(ipv6_addr, &internal);
+    char dst[INET6_ADDRSTRLEN];
+    int ret = uv_inet_ntop(AF_INET6, &internal, dst, sizeof(dst));
+    lean_always_assert(ret == 0);
+    return lean_mk_string(dst);
+}
+
+#else
+
+/* Std.Net.IPV4Addr.ofString (s : @&String) : Option IPV4Addr */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_pton_v4(b_obj_arg str_obj) {
+    lean_always_assert(
+        false && ("Please build a version of Lean4 with libuv to invoke this.")
+    );
+}
+
+/* Std.Net.IPV4Addr.toString (addr : @&IPV4Addr) : String */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ntop_v4(b_obj_arg ipv4_addr) {
+    lean_always_assert(
+        false && ("Please build a version of Lean4 with libuv to invoke this.")
+    );
+}
+
+/* Std.Net.IPV6Addr.ofString (s : @&String) : Option IPV6Addr */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_pton_v6(b_obj_arg str_obj) {
+    lean_always_assert(
+        false && ("Please build a version of Lean4 with libuv to invoke this.")
+    );
+}
+
+/* Std.Net.IPV6Addr.toString (addr : @&IPV6Addr) : String */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ntop_v6(b_obj_arg ipv6_addr) {
+    lean_always_assert(
+        false && ("Please build a version of Lean4 with libuv to invoke this.")
+    );
+}
+
+#endif
+}

src/runtime/uv/net_addr.h

@@ -0,0 +1,28 @@
+/*
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Henrik Böving
+*/
+#pragma once
+#include <lean/lean.h>
+#include "runtime/object.h"
+
+
+namespace lean {
+
+#ifndef LEAN_EMSCRIPTEN
+#include <uv.h>
+
+void lean_ipv4_addr_to_in_addr(b_obj_arg ipv4_addr, struct in_addr* out);
+void lean_ipv6_addr_to_in6_addr(b_obj_arg ipv6_addr, struct in6_addr* out);
+lean_obj_res lean_in_addr_to_ipv4_addr(const struct in_addr* ipv4_addr);
+lean_obj_res lean_in6_addr_to_ipv6_addr(const struct in6_addr* ipv6_addr);
+
+#endif
+
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_pton_v4(b_obj_arg str_obj);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ntop_v4(b_obj_arg ipv4_addr);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_pton_v6(b_obj_arg str_obj);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ntop_v6(b_obj_arg ipv6_addr);
+
+}