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

@@ -1506,9 +1506,99 @@ theorem filterMap_eq_push_iff {f : α → Option β} {l : Array α} {l' : Array
 
 /-! 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,
@@ -2122,74 +2212,6 @@ theorem getElem?_modify {as : Array α} {i : Nat} {f : α → α} {j : Nat} :
 
 theorem size_empty : (#[] : Array α).size = 0 := rfl
 
-/-! ### append -/
-
-@[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 α)} :

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/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/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

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

@@ -7,159 +7,44 @@ prelude
 import Init.Core
 import Init.Omega
 
-namespace Lean.Grind.Offset
+namespace Lean.Grind
+def isLt (x y : Nat) : Bool := x < y
 
-abbrev Var := Nat
-abbrev Context := Lean.RArray Nat
+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
 
-def fixedVar := 100000000 -- Any big number should work here
+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
 
-def Var.denote (ctx : Context) (v : Var) : Nat :=
-  bif v == fixedVar then 1 else ctx.get v
+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
 
-structure Cnstr where
-  x : Var
-  y : Var
-  k : Nat  := 0
-  l : Bool := true
-  deriving Repr, DecidableEq, Inhabited
-
-def Cnstr.denote (c : Cnstr) (ctx : Context) : Prop :=
-  if c.l then
-    c.x.denote ctx + c.k ≤ c.y.denote ctx
-  else
-    c.x.denote ctx ≤ c.y.denote ctx + c.k
-
-def trivialCnstr : Cnstr := { x := 0, y := 0, k := 0, l := true }
-
-@[simp] theorem denote_trivial (ctx : Context) : trivialCnstr.denote ctx := by
-  simp [Cnstr.denote, trivialCnstr]
-
-def Cnstr.trans (c₁ c₂ : Cnstr) : Cnstr :=
-  if c₁.y = c₂.x then
-    let { x, k := k₁, l := l₁, .. } := c₁
-    let { y, k := k₂, l := l₂, .. } := c₂
-    match l₁, l₂ with
-    | false, false =>
-      { x, y, k := k₁ + k₂, l := false }
-    | false, true =>
-      if k₁ < k₂ then
-        { x, y, k := k₂ - k₁, l := true }
-      else
-        { x, y, k := k₁ - k₂, l := false }
-    | true, false =>
-      if k₁ < k₂ then
-        { x, y, k := k₂ - k₁, l := false }
-      else
-        { x, y, k := k₁ - k₂, l := true }
-    | true, true =>
-      { x, y, k := k₁ + k₂, l := true }
-  else
-    trivialCnstr
-
-@[simp] theorem Cnstr.denote_trans_easy (ctx : Context) (c₁ c₂ : Cnstr) (h : c₁.y ≠ c₂.x) : (c₁.trans c₂).denote ctx := by
-  simp [*, Cnstr.trans]
-
-@[simp] theorem Cnstr.denote_trans (ctx : Context) (c₁ c₂ : Cnstr) : c₁.denote ctx → c₂.denote ctx → (c₁.trans c₂).denote ctx := by
-  by_cases c₁.y = c₂.x
-  case neg => simp [*]
-  simp [trans, *]
-  let { x, k := k₁, l := l₁, .. } := c₁
-  let { y, k := k₂, l := l₂, .. } := c₂
-  simp_all; split
-  · simp [denote]; omega
-  · split <;> simp [denote] <;> omega
-  · split <;> simp [denote] <;> omega
-  · simp [denote]; omega
-
-def Cnstr.isTrivial (c : Cnstr) : Bool := c.x == c.y && c.k == 0
-
-theorem Cnstr.of_isTrivial (ctx : Context) (c : Cnstr) : c.isTrivial = true → c.denote ctx := by
-  cases c; simp [isTrivial]; intros; simp [*, denote]
-
-def Cnstr.isFalse (c : Cnstr) : Bool := c.x == c.y && c.k != 0 && c.l == true
-
-theorem Cnstr.of_isFalse (ctx : Context) {c : Cnstr} : c.isFalse = true → ¬c.denote ctx := by
-  cases c; simp [isFalse]; intros; simp [*, denote]; omega
-
-def Cnstrs := List Cnstr
-
-def Cnstrs.denoteAnd' (ctx : Context) (c₁ : Cnstr) (c₂ : Cnstrs) : Prop :=
-  match c₂ with
-  | [] => c₁.denote ctx
-  | c::cs => c₁.denote ctx ∧ Cnstrs.denoteAnd' ctx c cs
-
-theorem Cnstrs.denote'_trans (ctx : Context) (c₁ c : Cnstr) (cs : Cnstrs) : c₁.denote ctx → denoteAnd' ctx c cs → denoteAnd' ctx (c₁.trans c) cs := by
-  induction cs
-  next => simp [denoteAnd', *]; apply Cnstr.denote_trans
-  next c cs ih => simp [denoteAnd']; intros; simp [*]
-
-def Cnstrs.trans' (c₁ : Cnstr) (c₂ : Cnstrs) : Cnstr :=
-  match c₂ with
-  | [] => c₁
-  | c::c₂ => trans' (c₁.trans c) c₂
-
-@[simp] theorem Cnstrs.denote'_trans' (ctx : Context) (c₁ : Cnstr) (c₂ : Cnstrs) : denoteAnd' ctx c₁ c₂ → (trans' c₁ c₂).denote ctx := by
-  induction c₂ generalizing c₁
-  next => intros; simp_all [trans', denoteAnd']
-  next c cs ih => simp [denoteAnd']; intros; simp [trans']; apply ih; apply denote'_trans <;> assumption
-
-def Cnstrs.denoteAnd (ctx : Context) (c : Cnstrs) : Prop :=
-  match c with
-  | [] => True
-  | c::cs => denoteAnd' ctx c cs
-
-def Cnstrs.trans (c : Cnstrs) : Cnstr :=
-  match c with
-  | []    => trivialCnstr
-  | c::cs => trans' c cs
-
-theorem Cnstrs.of_denoteAnd_trans {ctx : Context} {c : Cnstrs} : c.denoteAnd ctx → c.trans.denote ctx := by
-  cases c <;> simp [*, trans, denoteAnd] <;> intros <;> simp [*]
-
-def Cnstrs.isFalse (c : Cnstrs) : Bool :=
-  c.trans.isFalse
-
-theorem Cnstrs.unsat' (ctx : Context) (c : Cnstrs) : c.isFalse = true → ¬ c.denoteAnd ctx := by
-  simp [isFalse]; intro h₁ h₂
-  have := of_denoteAnd_trans h₂
-  have := Cnstr.of_isFalse ctx h₁
-  contradiction
-
-/-- `denote ctx [c_1, ..., c_n] C` is `c_1.denote ctx → ... → c_n.denote ctx → C` -/
-def Cnstrs.denote (ctx : Context) (cs : Cnstrs) (C : Prop) : Prop :=
-  match cs with
-  | [] => C
-  | c::cs => c.denote ctx → denote ctx cs C
-
-theorem Cnstrs.not_denoteAnd'_eq (ctx : Context) (c : Cnstr) (cs : Cnstrs) (C : Prop) : (denoteAnd' ctx c cs → C) = denote ctx (c::cs) C := by
-  simp [denote]
-  induction cs generalizing c
-  next => simp [denoteAnd', denote]
-  next c' cs ih =>
-    simp [denoteAnd', denote, *]
-
-theorem Cnstrs.not_denoteAnd_eq (ctx : Context) (cs : Cnstrs) (C : Prop) : (denoteAnd ctx cs → C) = denote ctx cs C := by
-  cases cs
-  next => simp [denoteAnd, denote]
-  next c cs => apply not_denoteAnd'_eq
-
-def Cnstr.isImpliedBy (cs : Cnstrs) (c : Cnstr) : Bool :=
-  cs.trans == c
-
-/-! Main theorems used by `grind`. -/
-
-/-- Auxiliary theorem used by `grind` to prove that a system of offset inequalities is unsatisfiable. -/
-theorem Cnstrs.unsat (ctx : Context) (cs : Cnstrs) : cs.isFalse = true → cs.denote ctx False := by
-  intro h
-  rw [← not_denoteAnd_eq]
-  apply unsat'
-  assumption
-
-/-- Auxiliary theorem used by `grind` to prove an implied offset inequality. -/
-theorem Cnstrs.imp (ctx : Context) (cs : Cnstrs) (c : Cnstr) (h : c.isImpliedBy cs = true)  : cs.denote ctx (c.denote ctx) := by
-  rw [← eq_of_beq h]
-  rw [← not_denoteAnd_eq]
-  apply of_denoteAnd_trans
-
-end Lean.Grind.Offset
+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
   /--

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
@@ -54,4 +59,6 @@ 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/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

@@ -170,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 :=
@@ -468,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
 
 /--
@@ -499,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
 

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

@@ -51,6 +51,13 @@ private def isEqTrueHyp? (proof : Expr) : Option FVarId := Id.run do
   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
@@ -62,12 +69,12 @@ private def addLocalEMatchTheorems (e : Expr) : GoalM Unit := do
   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
+  if let some thm ← mkEMatchTheoremWithKind'? origin proof .fwd then
     activateTheorem thm gen
-  if let some thm ← mkEMatchTheoremWithKind? origin #[] proof .bwd then
+  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
+    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}"

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,12 +54,20 @@ 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 (← getConfig).splitIte && (e.isIte || e.isDIte) then
     addSplitCandidate e
     return ()
+  if isMorallyIff e then
+    addSplitCandidate e
+    return ()
   if (← getConfig).splitMatch then
     if (← isMatcherApp e) then
       if let .reduced _ ← reduceMatcher? e then
@@ -188,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/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. -/
@@ -702,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
@@ -714,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/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⟩