fix: set LLVM sysroot consistently

doc/dev/ffi.md

@@ -49,9 +49,8 @@ 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 `α`.
-  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`).
+* `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`).
 * 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,32 +37,16 @@ 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:
-    - [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)
+    - [Batteries](https://github.com/leanprover-community/batteries)
       - No dependencies
       - Toolchain bump PR
       - Create and push the tag
-      - There is no `stable` branch; skip this step
+      - Merge the tag into `stable`
     - [ProofWidgets4](https://github.com/leanprover-community/ProofWidgets4)
       - Dependencies: `Batteries`
       - Note on versions and branches:
@@ -77,6 +61,17 @@ 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,13 +27,6 @@ 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,10 +150,6 @@ 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.
@@ -171,9 +167,6 @@ 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,7 +244,8 @@ def ofFn {n} (f : Fin n → α) : Array α := go 0 (mkEmpty n) where
 def range (n : Nat) : Array Nat :=
   ofFn fun (i : Fin n) => i
 
-@[inline] protected def singleton (v : α) : Array α := #[v]
+def singleton (v : α) : Array α :=
+  mkArray 1 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, Kim Morrison
+Authors: Mario Carneiro
 -/
 prelude
 import Init.Data.Nat.Lemmas
@@ -124,8 +124,6 @@ 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⟩
@@ -1003,6 +1001,8 @@ 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,6 +1036,11 @@ 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
@@ -1045,18 +1050,6 @@ 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
@@ -1107,59 +1100,17 @@ 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]
@@ -1172,7 +1123,6 @@ theorem mapM_eq_mapM_toList [Monad m] [LawfulMonad m] (f : α → m β) (arr : A
     toList <$> arr.mapM f = arr.toList.mapM f := by
   simp [mapM_eq_mapM_toList]
 
-@[deprecated "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
@@ -1189,416 +1139,13 @@ theorem mapM_map_eq_foldl (as : Array α) (f : α → β) (i) :
     rfl
 termination_by as.size - i
 
-/-! ### 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 map_eq_foldl (as : Array α) (f : α → β) :
+    as.map f = as.foldl (fun r a => r.push (f a)) #[] :=
+  mapM_map_eq_foldl _ _ _
 
 theorem singleton_eq_toArray_singleton (a : α) : #[a] = [a].toArray := 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
-
+@[simp] theorem singleton_def (v : α) : singleton v = #[v] := rfl
 
 -- This is a duplicate of `List.toArray_toList`.
 -- It's confusing to guess which namespace this theorem should live in,
@@ -2140,6 +1687,12 @@ 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)) :
@@ -2208,10 +1761,137 @@ 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 α)} :
@@ -2547,6 +2227,26 @@ 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'
@@ -2668,12 +2368,6 @@ 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,9 +9,7 @@ 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
 
@@ -100,12 +98,6 @@ 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 :=
@@ -450,10 +442,6 @@ 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]
 
@@ -466,9 +454,6 @@ 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]
@@ -2315,12 +2300,6 @@ 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]
@@ -2607,13 +2586,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
-  rfl
+  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)
 
 @[simp]
 theorem zero_udiv {x : BitVec w} : (0#w) / x = 0#w := by
@@ -2649,45 +2628,6 @@ 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} :
@@ -2700,10 +2640,6 @@ 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]
@@ -2731,55 +2667,6 @@ 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
@@ -2936,12 +2823,7 @@ theorem smod_zero {x : BitVec n} : x.smod 0#n = x := by
 
 /-! # Rotate Left -/
 
-/--`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. -/
+/-- 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
@@ -3085,18 +2967,8 @@ 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)`.
@@ -3232,11 +3104,6 @@ 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,8 +1,7 @@
 /-
 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,
-  Kim Morrison
+Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro
 -/
 prelude
 import Init.Data.Bool
@@ -1115,10 +1114,6 @@ 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
 
@@ -1285,7 +1280,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 only [cons_append, filter]; split <;> simp [filter_append l₁]
+  | a :: l₁, l₂ => by simp [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 = Array.singleton a := rfl
+@[simp] theorem toArray_singleton (a : α) : (List.singleton a).toArray = 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,17 +49,4 @@ 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,8 +159,6 @@ 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⟩
@@ -171,8 +169,6 @@ 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 (v : Vector α n) (x : α) : Vector α (n + 1) :=
+@[inline] def push (x : α) (v : Vector α n)  : 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, Kim Morrison
+Authors: Shreyas Srinivas, Francois Dorais
 -/
 prelude
 import Init.Data.Vector.Basic
@@ -153,14 +153,6 @@ 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) :
@@ -1043,6 +1035,8 @@ 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) :
@@ -1050,129 +1044,16 @@ 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,4 +10,3 @@ 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,12 +66,6 @@ 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
@@ -79,8 +73,6 @@ 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,14 +43,8 @@ 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
-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
+-- @[grind_norm↓] theorem imp_eq (p q : Prop) : (p → q) = (¬ p ∨ q) := by
+--  by_cases p <;> by_cases q <;> simp [*]
 
 -- And
 @[grind_norm↓] theorem not_and (p q : Prop) : (¬(p ∧ q)) = (¬p ∨ ¬q) := by

src/Init/Grind/Offset.lean

@@ -1,165 +0,0 @@
-/-
-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.Offset
-
-abbrev Var := Nat
-abbrev Context := Lean.RArray Nat
-
-def fixedVar := 100000000 -- Any big number should work here
-
-def Var.denote (ctx : Context) (v : Var) : Nat :=
-  bif v == fixedVar then 1 else ctx.get v
-
-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

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 := 8
+  splits : Nat := 5
   /-- Maximum number of E-matching (aka heuristic theorem instantiation) rounds before each case split. -/
   ematch : Nat := 5
   /--
@@ -37,14 +37,6 @@ 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/Init/Prelude.lean

@@ -4170,16 +4170,6 @@ def withRef [Monad m] [MonadRef m] {α} (ref : Syntax) (x : m α) : m α :=
   let ref := replaceRef ref oldRef
   MonadRef.withRef ref x
 
-/--
-If `ref? = some ref`, run `x : m α` with a modified value for the `ref` by calling `withRef`.
-Otherwise, run `x` directly.
--/
-@[always_inline, inline]
-def withRef? [Monad m] [MonadRef m] {α} (ref? : Option Syntax) (x : m α) : m α :=
-  match ref? with
-  | some ref => withRef ref x
-  | _        => x
-
 /-- A monad that supports syntax quotations. Syntax quotations (in term
     position) are monadic values that when executed retrieve the current "macro
     scope" from the monad and apply it to every identifier they introduce

src/Lean/Data/Json/Printer.lean

@@ -11,22 +11,6 @@ import Init.Data.List.Impl
 namespace Lean
 namespace Json
 
-set_option maxRecDepth 1024 in
-/--
-This table contains for each UTF-8 byte whether we need to escape a string that contains it.
--/
-private def escapeTable : { xs : ByteArray // xs.size = 256 } :=
-  ⟨ByteArray.mk #[
-    1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1, 1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,
-    0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,1, 0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,
-    0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0, 0,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,
-    0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0, 0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,
-    1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1, 1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,
-    1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1, 1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,
-    1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1, 1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,
-    1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1, 1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1
-  ], by rfl⟩
-
 private def escapeAux (acc : String) (c : Char) : String :=
   -- escape ", \, \n and \r, keep all other characters ≥ 0x20 and render characters < 0x20 with \u
   if c = '"' then -- hack to prevent emacs from regarding the rest of the file as a string: "
@@ -55,27 +39,8 @@ private def escapeAux (acc : String) (c : Char) : String :=
     let d4 := Nat.digitChar (n % 16)
     acc ++ "\\u" |>.push d1 |>.push d2 |>.push d3 |>.push d4
 
-private def needEscape (s : String) : Bool :=
-  go s 0
-where
-  go (s : String) (i : Nat) : Bool :=
-    if h : i < s.utf8ByteSize then
-      let byte := s.getUtf8Byte i h
-      have h1 : byte.toNat < 256 := UInt8.toNat_lt_size byte
-      have h2 : escapeTable.val.size = 256 := escapeTable.property
-      if escapeTable.val.get byte.toNat (Nat.lt_of_lt_of_eq h1 h2.symm) == 0 then
-        go s (i + 1)
-      else
-        true
-    else
-      false
-
 def escape (s : String) (acc : String := "") : String :=
-  -- If we don't have any characters that need to be escaped we can just append right away.
-  if needEscape s then
-    s.foldl escapeAux acc
-  else
-    acc ++ s
+  s.foldl escapeAux acc
 
 def renderString (s : String) (acc : String := "") : String :=
   let acc := acc ++ "\""

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -362,9 +362,9 @@ partial def evalChoiceAux (tactics : Array Syntax) (i : Nat) : TacticM Unit :=
   | `(tactic| intro $h:term $hs:term*) => evalTactic (← `(tactic| intro $h:term; intro $hs:term*))
   | _ => throwUnsupportedSyntax
 where
-  introStep (ref? : Option Syntax) (n : Name) (typeStx? : Option Syntax := none) : TacticM Unit := do
+  introStep (ref : Option Syntax) (n : Name) (typeStx? : Option Syntax := none) : TacticM Unit := do
     let fvarId ← liftMetaTacticAux fun mvarId => do
-      let (fvarId, mvarId) ← withRef? ref? <| mvarId.intro n
+      let (fvarId, mvarId) ← mvarId.intro n
       pure (fvarId, [mvarId])
     if let some typeStx := typeStx? then
       withMainContext do
@@ -374,9 +374,9 @@ where
         unless (← isDefEqGuarded type fvarType) do
           throwError "type mismatch at `intro {fvar}`{← mkHasTypeButIsExpectedMsg fvarType type}"
         liftMetaTactic fun mvarId => return [← mvarId.replaceLocalDeclDefEq fvarId type]
-    if let some ref := ref? then
+    if let some stx := ref then
       withMainContext do
-        Term.addLocalVarInfo ref (mkFVar fvarId)
+        Term.addLocalVarInfo stx (mkFVar fvarId)
 
 @[builtin_tactic Lean.Parser.Tactic.introMatch] def evalIntroMatch : Tactic := fun stx => do
   let matchAlts := stx[1]

src/Lean/Elab/Tactic/Classical.lean

@@ -24,8 +24,11 @@ def classical [Monad m] [MonadEnv m] [MonadFinally m] [MonadLiftT MetaM m] (t :
   finally
     modifyEnv Meta.instanceExtension.popScope
 
-@[builtin_tactic Lean.Parser.Tactic.classical, builtin_incremental]
-def evalClassical : Tactic := fun stx =>
-  classical <| Term.withNarrowedArgTacticReuse (argIdx := 1) Elab.Tactic.evalTactic stx
+@[builtin_tactic Lean.Parser.Tactic.classical]
+def evalClassical : Tactic := fun stx => do
+  match stx with
+  | `(tactic| classical $tacs:tacticSeq) =>
+     classical <| Elab.Tactic.evalTactic tacs
+  | _ => throwUnsupportedSyntax
 
 end Lean.Elab.Tactic

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

@@ -7,10 +7,9 @@ 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 Tactic TryThis
+open Meta
 
 def applySimpResult (result : Simp.Result) : TacticM Unit := do
   if result.proof?.isNone then
@@ -24,19 +23,6 @@ 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))
 
@@ -44,15 +30,4 @@ 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/Elab/Tactic/RCases.lean

@@ -507,7 +507,7 @@ partial def rintroCore (g : MVarId) (fs : FVarSubst) (clears : Array FVarId) (a
   match pat with
   | `(rintroPat| $pat:rcasesPat) =>
     let pat := (← RCasesPatt.parse pat).typed? ref ty?
-    let (v, g) ← withRef pat.ref <| g.intro (pat.name?.getD `_)
+    let (v, g) ← g.intro (pat.name?.getD `_)
     rcasesCore g fs clears (.fvar v) a pat cont
   | `(rintroPat| ($(pats)* $[: $ty?']?)) =>
     let ref := if pats.size == 1 then pat.raw else .missing

src/Lean/Meta/Basic.lean

@@ -1964,22 +1964,15 @@ 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
-  return (← isInductivePredicate? declName).isSome
+  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
 
 def isListLevelDefEqAux : List Level → List Level → MetaM Bool
   | [],    []    => return true

src/Lean/Meta/Tactic/Grind.lean

@@ -53,5 +53,5 @@ 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
+
 end Lean

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

@@ -46,35 +46,15 @@ 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.
 
-Thus, if diagnostics are enabled, we also re-check them using `TransparencyMode.default`. If the result is different
+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
 we report to the user.
 -/
-def canonElemCore (f : Expr) (i : Nat) (e : Expr) (kind : CanonElemKind) : StateT State MetaM Expr := do
+def canonElemCore (f : Expr) (i : Nat) (e : Expr) (isInst : Bool) : StateT State MetaM Expr := do
   let s ← get
   if let some c := s.canon.find? e then
     return c
@@ -86,19 +66,16 @@ def canonElemCore (f : Expr) (i : Nat) (e : Expr) (kind : CanonElemKind) : 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 kind != .type then
-      if (← isTracingEnabledFor `grind.issues <&&> (withDefault <| isDefEq e c)) then
+    if isInst then
+      if (← isDiagnosticsEnabled <&&> pure (c.fvarsSubset e) <&&> (withDefault <| isDefEq e c)) then
         -- TODO: consider storing this information in some structure that can be browsed later.
-        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}"
+        trace[grind.issues] "the following `grind` static elements are definitionally equal with `default` transparency, but not with `instances` transparency{indentExpr e}\nand{indentExpr c}"
   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 .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
+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
 
 /--
 Return type for the `shouldCanon` function.
@@ -108,8 +85,6 @@ 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.
@@ -117,13 +92,6 @@ 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`.
 -/
@@ -134,14 +102,7 @@ def shouldCanon (pinfos : Array ParamInfo) (i : Nat) (arg : Expr) : MetaM Should
       return .canonInst
     else if pinfo.isProp then
       return .visit
-    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
+  if (← isTypeFormer arg) then
     return .canonType
   else
     return .visit
@@ -171,11 +132,9 @@ 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'
@@ -192,8 +151,7 @@ where
     return e'
 
 /-- Canonicalizes nested types, type formers, and instances in `e`. -/
-def canon (e : Expr) : StateT State MetaM Expr := do
-  trace[grind.debug.canon] "{e}"
+def canon (e : Expr) : StateT State MetaM Expr :=
   unsafe canonImpl e
 
 end Canon

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

@@ -141,7 +141,6 @@ 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
     }
@@ -159,13 +158,14 @@ where
       updateMT rhsRoot.self
 
   updateRoots (lhs : Expr) (rootNew : Expr) : GoalM Unit := do
-    traverseEqc lhs fun n =>
-      setENode n.self { n with root := rootNew }
-
-  propagateEqcDown (lhs : Expr) : GoalM Unit := do
-    traverseEqc lhs fun n =>
+    let rec loop (e : Expr) : GoalM Unit := do
+      let n ← getENode e
+      setENode e { n with root := rootNew }
       unless (← isInconsistent) do
-        propagateDown n.self
+        propagateDown e
+      if isSameExpr lhs n.next then return ()
+      loop n.next
+    loop lhs
 
 /-- Ensures collection of equations to be processed is empty. -/
 private def resetNewEqs : GoalM Unit :=
@@ -217,22 +217,14 @@ 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 =>
-      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
-        goEq p lhs rhs isNeg false
+    | Eq _ lhs rhs => 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)
+    | _ =>
+      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,8 +57,7 @@ inductive Origin where
   is the provided grind argument. The `id` is a unique identifier for the call.
   -/
   | stx (id : Name) (ref : Syntax)
-  /-- It is local, but we don't have a local hypothesis for it. -/
-  | local (id : Name)
+  | other (id : Name)
   deriving Inhabited, Repr, BEq
 
 /-- A unique identifier corresponding to the origin. -/
@@ -66,14 +65,14 @@ def Origin.key : Origin → Name
   | .decl declName => declName
   | .fvar fvarId   => fvarId.name
   | .stx id _      => id
-  | .local id      => id
+  | .other 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
-  | .local id      => return id
+  | .other id      => return id
 
 instance : BEq Origin where
   beq a b := a.key == b.key
@@ -170,43 +169,11 @@ 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 :=
@@ -500,8 +467,7 @@ 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
-    let pats := splitWhileForbidden (pat.abstract xs)
-    return (xs.size, pats)
+    return (xs.size, [pat.abstract xs])
   mkEMatchTheoremCore origin levelParams numParams proof patterns
 
 /--
@@ -532,7 +498,7 @@ def addEMatchEqTheorem (declName : Name) : MetaM Unit := do
 def getEMatchTheorems : CoreM EMatchTheorems :=
   return ematchTheoremsExt.getState (← getEnv)
 
-inductive TheoremKind where
+private inductive TheoremKind where
   | eqLhs | eqRhs | eqBoth | fwd | bwd | default
   deriving Inhabited, BEq
 
@@ -632,7 +598,7 @@ private def collectPatterns? (proof : Expr) (xs : Array Expr) (searchPlaces : Ar
     | return none
   return some (ps, s.symbols.toList)
 
-def mkEMatchTheoremWithKind? (origin : Origin) (levelParams : Array Name) (proof : Expr) (kind : TheoremKind) : MetaM (Option EMatchTheorem) := do
+private 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/ForallProp.lean

@@ -46,57 +46,11 @@ where
       -- b = True → (a → b) = True
       pushEqTrue e <| mkApp3 (mkConst ``Grind.imp_eq_of_eq_true_right) a b (← mkEqTrueProof b)
 
-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 ()
+def propagateImpliesDown (e : Expr) : GoalM Unit := do
   if (← isEqFalse e) then
-    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
+    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
 
 end Lean.Meta.Grind

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

@@ -53,36 +53,25 @@ 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
+  if 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
-        -- 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 ()
+  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 ()
     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 (← getConfig).splitIndPred then
-      if (← isInductivePredicate declName) then
-        addSplitCandidate e
+    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.
@@ -109,7 +98,7 @@ private partial def internalizePattern (pattern : Expr) (generation : Nat) : Goa
   else pattern.withApp fun f args => do
     return mkAppN f (← args.mapM (internalizePattern · generation))
 
-partial def activateTheorem (thm : EMatchTheorem) (generation : Nat) : GoalM Unit := do
+private 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

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

@@ -58,12 +58,9 @@ 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 b _ := parent then
+      if let .forallE _ d _ _ := 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

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
-     propagateForallPropDown e
+     propagateImpliesDown 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 (assertAll >> ematchStar >> (splitNext >> assertAll >> ematchStar).iterate) goals
+  applyToAll (ematchStar >> (splitNext >> 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,123 +14,77 @@ namespace Lean.Meta.Grind
 inductive CaseSplitStatus where
   | resolved
   | notReady
-  | ready (numCases : Nat) (isRec := false)
+  | ready
   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 => 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
+  | 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
   | _ =>
     if (← isResolvedCaseSplit e) then
       trace[grind.debug.split] "split resolved: {e}"
       return .resolved
-    if let some info := isMatcherAppCore? (← getEnv) e then
-      return .ready info.numAlts
+    if (← isMatcherApp e) then
+      return .ready
     let .const declName .. := e.getAppFn | unreachable!
-    if let some info ← isInductivePredicate? declName then
-      if (← isEqTrue e) then
-        return .ready info.ctors.length info.isRec
+    if (← isInductivePredicate declName <&&> isEqTrue e) then
+      return .ready
     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 SplitCandidate := do
-  if (← isInconsistent) then return .none
-  if (← checkMaxCaseSplit) then return .none
-  go (← get).splitCandidates .none []
+private def selectNextSplit? : GoalM (Option Expr) := do
+  if (← isInconsistent) then return none
+  if (← checkMaxCaseSplit) then return none
+  go (← get).splitCandidates none []
 where
-  go (cs : List Expr) (c? : SplitCandidate) (cs' : List Expr) : GoalM SplitCandidate := do
+  go (cs : List Expr) (c? : Option Expr) (cs' : List Expr) : GoalM (Option Expr) := do
     match cs with
     | [] =>
       modify fun s => { s with splitCandidates := cs'.reverse }
-      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
+      if c?.isSome then
         -- Remark: we reset `numEmatch` after each case split.
         -- We should consider other strategies in the future.
-        modify fun s => { s with numSplits, numEmatch := 0 }
+        modify fun s => { s with numSplits := s.numSplits + 1, numEmatch := 0 }
       return c?
     | c::cs =>
     match (← checkCaseSplitStatus c) with
     | .notReady => go cs c? (c::cs')
     | .resolved => go cs c? cs'
-    | .ready numCases isRec =>
+    | .ready =>
     match c? with
-    | .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')
+    | none => go cs (some c) cs'
+    | some c' =>
+      if (← getGeneration c) < (← getGeneration c') then
+        go cs (some c) (c'::cs')
       else
         go cs c? (c::cs')
 
@@ -140,11 +94,6 @@ 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. -/
@@ -159,10 +108,9 @@ and returns a new list of goals if successful.
 -/
 def splitNext : GrindTactic := fun goal => do
   let (goals?, _) ← GoalM.run goal do
-    let .some c numCases isRec ← selectNextSplit?
+    let some c ← 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
@@ -171,7 +119,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 [] genNew
+    let goals ← introNewHyp goals [] (gen+1)
     return some goals
   return goals?
 

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

@@ -393,8 +393,6 @@ 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 :=
@@ -702,15 +700,6 @@ 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
@@ -723,7 +712,7 @@ def filterENodes (p : ENode → GoalM Bool) : GoalM (Array ENode) := do
       ref.modify (·.push n)
   ref.get
 
-def forEachEqcRoot (f : ENode → GoalM Unit) : GoalM Unit := do
+def forEachEqc (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,24 +50,18 @@ 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
-    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 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
     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,4 +10,3 @@ import Std.Sync
 import Std.Time
 import Std.Tactic
 import Std.Internal
-import Std.Net

src/Std/Net.lean

@@ -1,7 +0,0 @@
-/-
-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

@@ -1,197 +0,0 @@
-/-
-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,12 +39,6 @@ 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,12 +39,6 @@ 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,13 +40,7 @@ instance {x y : Ordinal} : Decidable (x < y) :=
 or differences in hours.
 -/
 def Offset : Type := UnitVal 3600
-  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))
+  deriving Repr, BEq, Inhabited, Add, Sub, Neg, ToString
 
 instance : OfNat Offset n :=
   ⟨UnitVal.ofNat n⟩

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

@@ -40,12 +40,6 @@ 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,13 +38,7 @@ 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, 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))
+  deriving Repr, BEq, Inhabited, Add, Sub, Neg, ToString
 
 instance : OfNat Offset n :=
   ⟨UnitVal.ofInt <| Int.ofNat n⟩

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

@@ -42,9 +42,6 @@ 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,12 +51,6 @@ 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 uv/net_addr.cpp)
+process.cpp object_ref.cpp mpn.cpp mutex.cpp libuv.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

@@ -1,131 +0,0 @@
-/*
-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

@@ -1,28 +0,0 @@
-/*
-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);
-
-}