chore: upstream Subarray.empty

Makes it possible to `extend` another structure through an abbreviation.
Also inserts a `withSynthesize` checkpoint for parents.

Closes #5417

.github/workflows/pr-release.yml

@@ -164,10 +164,10 @@ jobs:
 
             # Use GitHub API to check if a comment already exists
             existing_comment="$(curl --retry 3 --location --silent \
-                                    -H "Authorization: token ${{ secrets.MATHLIB4_BOT }}" \
+                                    -H "Authorization: token ${{ secrets.MATHLIB4_COMMENT_BOT }}" \
                                     -H "Accept: application/vnd.github.v3+json" \
                                     "https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments" \
-                                    | jq 'first(.[] | select(.body | test("^- . Mathlib") or startswith("Mathlib CI status")) | select(.user.login == "leanprover-community-mathlib4-bot"))')"
+                                    | jq 'first(.[] | select(.body | test("^- . Mathlib") or startswith("Mathlib CI status")) | select(.user.login == "leanprover-community-bot"))')"
             existing_comment_id="$(echo "$existing_comment" | jq -r .id)"
             existing_comment_body="$(echo "$existing_comment" | jq -r .body)"
 
@@ -177,14 +177,14 @@ jobs:
               echo "Posting message to the comments: $MESSAGE"
 
               # Append new result to the existing comment or post a new comment
-              # It's essential we use the MATHLIB4_BOT token here, so that Mathlib CI can subsequently edit the comment.
+              # It's essential we use the MATHLIB4_COMMENT_BOT token here, so that Mathlib CI can subsequently edit the comment.
               if [ -z "$existing_comment_id" ]; then
                 INTRO="Mathlib CI status ([docs](https://leanprover-community.github.io/contribute/tags_and_branches.html)):"
                 # Post new comment with a bullet point
                 echo "Posting as new comment at leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments"
                 curl -L -s \
                   -X POST \
-                  -H "Authorization: token ${{ secrets.MATHLIB4_BOT }}" \
+                  -H "Authorization: token ${{ secrets.MATHLIB4_COMMENT_BOT }}" \
                   -H "Accept: application/vnd.github.v3+json" \
                   -d "$(jq --null-input --arg intro "$INTRO" --arg val "$MESSAGE" '{"body":($intro + "\n" + $val)}')" \
                   "https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments"
@@ -193,7 +193,7 @@ jobs:
                 echo "Appending to existing comment at leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments"
                 curl -L -s \
                   -X PATCH \
-                  -H "Authorization: token ${{ secrets.MATHLIB4_BOT }}" \
+                  -H "Authorization: token ${{ secrets.MATHLIB4_COMMENT_BOT }}" \
                   -H "Accept: application/vnd.github.v3+json" \
                   -d "$(jq --null-input --arg existing "$existing_comment_body" --arg message "$MESSAGE" '{"body":($existing + "\n" + $message)}')" \
                   "https://api.github.com/repos/leanprover/lean4/issues/comments/$existing_comment_id"
@@ -340,6 +340,7 @@ jobs:
             # (This should no longer be possible once `nightly-testing-YYYY-MM-DD` is a tag, but it is still safe to merge.)
             git merge "$BASE" --strategy-option ours --no-commit --allow-unrelated-histories
             lake update batteries
+            get add lake-manifest.json
             git commit --allow-empty -m "Trigger CI for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
           fi
 

src/Init/Control/Lawful/Basic.lean

@@ -33,6 +33,10 @@ attribute [simp] id_map
 @[simp] theorem id_map' [Functor m] [LawfulFunctor m] (x : m α) : (fun a => a) <$> x = x :=
   id_map x
 
+@[simp] theorem Functor.map_map [Functor f] [LawfulFunctor f] (m : α → β) (g : β → γ) (x : f α) :
+    g <$> m <$> x = (fun a => g (m a)) <$> x :=
+  (comp_map _ _ _).symm
+
 /--
 The `Applicative` typeclass only contains the operations of an applicative functor.
 `LawfulApplicative` further asserts that these operations satisfy the laws of an applicative functor:
@@ -83,12 +87,16 @@ class LawfulMonad (m : Type u → Type v) [Monad m] extends LawfulApplicative m
   seq_assoc x g h := (by simp [← bind_pure_comp, ← bind_map, bind_assoc, pure_bind])
 
 export LawfulMonad (bind_pure_comp bind_map pure_bind bind_assoc)
-attribute [simp] pure_bind bind_assoc
+attribute [simp] pure_bind bind_assoc bind_pure_comp
 
 @[simp] theorem bind_pure [Monad m] [LawfulMonad m] (x : m α) : x >>= pure = x := by
   show x >>= (fun a => pure (id a)) = x
   rw [bind_pure_comp, id_map]
 
+/--
+Use `simp [← bind_pure_comp]` rather than `simp [map_eq_pure_bind]`,
+as `bind_pure_comp` is in the default simp set, so also using `map_eq_pure_bind` would cause a loop.
+-/
 theorem map_eq_pure_bind [Monad m] [LawfulMonad m] (f : α → β) (x : m α) : f <$> x = x >>= fun a => pure (f a) := by
   rw [← bind_pure_comp]
 
@@ -109,10 +117,21 @@ theorem seq_eq_bind {α β : Type u} [Monad m] [LawfulMonad m] (mf : m (α →
 
 theorem seqRight_eq_bind [Monad m] [LawfulMonad m] (x : m α) (y : m β) : x *> y = x >>= fun _ => y := by
   rw [seqRight_eq]
-  simp [map_eq_pure_bind, seq_eq_bind_map, const]
+  simp only [map_eq_pure_bind, const, seq_eq_bind_map, bind_assoc, pure_bind, id_eq, bind_pure]
 
 theorem seqLeft_eq_bind [Monad m] [LawfulMonad m] (x : m α) (y : m β) : x <* y = x >>= fun a => y >>= fun _ => pure a := by
-  rw [seqLeft_eq]; simp [map_eq_pure_bind, seq_eq_bind_map]
+  rw [seqLeft_eq]
+  simp only [map_eq_pure_bind, seq_eq_bind_map, bind_assoc, pure_bind, const_apply]
+
+@[simp] theorem map_bind [Monad m] [LawfulMonad m] (f : β → γ) (x : m α) (g : α → m β) :
+    f <$> (x >>= g) = x >>= fun a => f <$> g a := by
+  rw [← bind_pure_comp, LawfulMonad.bind_assoc]
+  simp [bind_pure_comp]
+
+@[simp] theorem bind_map_left [Monad m] [LawfulMonad m] (f : α → β) (x : m α) (g : β → m γ) :
+    ((f <$> x) >>= fun b => g b) = (x >>= fun a => g (f a)) := by
+  rw [← bind_pure_comp]
+  simp only [bind_assoc, pure_bind]
 
 /--
 An alternative constructor for `LawfulMonad` which has more

src/Init/Control/Lawful/Instances.lean

@@ -25,7 +25,7 @@ theorem ext {x y : ExceptT ε m α} (h : x.run = y.run) : x = y := by
 @[simp] theorem run_throw [Monad m] : run (throw e : ExceptT ε m β) = pure (Except.error e) := rfl
 
 @[simp] theorem run_bind_lift [Monad m] [LawfulMonad m] (x : m α) (f : α → ExceptT ε m β) : run (ExceptT.lift x >>= f : ExceptT ε m β) = x >>= fun a => run (f a) := by
-  simp[ExceptT.run, ExceptT.lift, bind, ExceptT.bind, ExceptT.mk, ExceptT.bindCont, map_eq_pure_bind]
+  simp [ExceptT.run, ExceptT.lift, bind, ExceptT.bind, ExceptT.mk, ExceptT.bindCont]
 
 @[simp] theorem bind_throw [Monad m] [LawfulMonad m] (f : α → ExceptT ε m β) : (throw e >>= f) = throw e := by
   simp [throw, throwThe, MonadExceptOf.throw, bind, ExceptT.bind, ExceptT.bindCont, ExceptT.mk]
@@ -43,7 +43,7 @@ theorem run_bind [Monad m] (x : ExceptT ε m α)
 
 @[simp] theorem run_map [Monad m] [LawfulMonad m] (f : α → β) (x : ExceptT ε m α)
     : (f <$> x).run = Except.map f <$> x.run := by
-  simp [Functor.map, ExceptT.map, map_eq_pure_bind]
+  simp [Functor.map, ExceptT.map, ←bind_pure_comp]
   apply bind_congr
   intro a; cases a <;> simp [Except.map]
 
@@ -62,7 +62,7 @@ protected theorem seqLeft_eq {α β ε : Type u} {m : Type u → Type v} [Monad
   intro
   | Except.error _ => simp
   | Except.ok _ =>
-    simp [map_eq_pure_bind]; apply bind_congr; intro b;
+    simp [←bind_pure_comp]; apply bind_congr; intro b;
     cases b <;> simp [comp, Except.map, const]
 
 protected theorem seqRight_eq [Monad m] [LawfulMonad m] (x : ExceptT ε m α) (y : ExceptT ε m β) : x *> y = const α id <$> x <*> y := by
@@ -175,7 +175,7 @@ theorem ext {x y : StateT σ m α} (h : ∀ s, x.run s = y.run s) : x = y :=
   simp [bind, StateT.bind, run]
 
 @[simp] theorem run_map {α β σ : Type u} [Monad m] [LawfulMonad m] (f : α → β) (x : StateT σ m α) (s : σ) : (f <$> x).run s = (fun (p : α × σ) => (f p.1, p.2)) <$> x.run s := by
-  simp [Functor.map, StateT.map, run, map_eq_pure_bind]
+  simp [Functor.map, StateT.map, run, ←bind_pure_comp]
 
 @[simp] theorem run_get [Monad m] (s : σ)    : (get : StateT σ m σ).run s = pure (s, s) := rfl
 
@@ -210,13 +210,13 @@ theorem run_bind_lift {α σ : Type u} [Monad m] [LawfulMonad m] (x : m α) (f :
 
 theorem seqRight_eq [Monad m] [LawfulMonad m] (x : StateT σ m α) (y : StateT σ m β) : x *> y = const α id <$> x <*> y := by
   apply ext; intro s
-  simp [map_eq_pure_bind, const]
+  simp [←bind_pure_comp, const]
   apply bind_congr; intro p; cases p
   simp [Prod.eta]
 
 theorem seqLeft_eq [Monad m] [LawfulMonad m] (x : StateT σ m α) (y : StateT σ m β) : x <* y = const β <$> x <*> y := by
   apply ext; intro s
-  simp [map_eq_pure_bind]
+  simp [←bind_pure_comp]
 
 instance [Monad m] [LawfulMonad m] : LawfulMonad (StateT σ m) where
   id_map         := by intros; apply ext; intros; simp[Prod.eta]
@@ -224,7 +224,7 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (StateT σ m) where
   seqLeft_eq     := seqLeft_eq
   seqRight_eq    := seqRight_eq
   pure_seq       := by intros; apply ext; intros; simp
-  bind_pure_comp := by intros; apply ext; intros; simp; apply LawfulMonad.bind_pure_comp
+  bind_pure_comp := by intros; apply ext; intros; simp
   bind_map       := by intros; rfl
   pure_bind      := by intros; apply ext; intros; simp
   bind_assoc     := by intros; apply ext; intros; simp

src/Init/Core.lean

@@ -823,6 +823,7 @@ theorem iff_iff_implies_and_implies {a b : Prop} : (a ↔ b) ↔ (a → b) ∧ (
 protected theorem Iff.rfl {a : Prop} : a ↔ a :=
   Iff.refl a
 
+-- And, also for backward compatibility, we try `Iff.rfl.` using `exact` (see #5366)
 macro_rules | `(tactic| rfl) => `(tactic| exact Iff.rfl)
 
 theorem Iff.of_eq (h : a = b) : a ↔ b := h ▸ Iff.rfl
@@ -837,6 +838,9 @@ instance : Trans Iff Iff Iff where
 theorem Eq.comm {a b : α} : a = b ↔ b = a := Iff.intro Eq.symm Eq.symm
 theorem eq_comm {a b : α} : a = b ↔ b = a := Eq.comm
 
+theorem HEq.comm {a : α} {b : β} : HEq a b ↔ HEq b a := Iff.intro HEq.symm HEq.symm
+theorem heq_comm {a : α} {b : β} : HEq a b ↔ HEq b a := HEq.comm
+
 @[symm] theorem Iff.symm (h : a ↔ b) : b ↔ a := Iff.intro h.mpr h.mp
 theorem Iff.comm: (a ↔ b) ↔ (b ↔ a) := Iff.intro Iff.symm Iff.symm
 theorem iff_comm : (a ↔ b) ↔ (b ↔ a) := Iff.comm

src/Init/Data/Array/Lemmas.lean

@@ -23,11 +23,33 @@ namespace Array
 
 @[simp] theorem getElem_mk {xs : List α} {i : Nat} (h : i < xs.length) : (Array.mk xs)[i] = xs[i] := rfl
 
-theorem getElem_eq_toList_getElem (a : Array α) (h : i < a.size) : a[i] = a.toList[i] := by
+theorem getElem_eq_getElem_toList {a : Array α} (h : i < a.size) : a[i] = a.toList[i] := by
   by_cases i < a.size <;> (try simp [*]) <;> rfl
 
+theorem getElem?_eq_getElem {a : Array α} {i : Nat} (h : i < a.size) : a[i]? = some a[i] :=
+  getElem?_pos ..
+
+@[simp] theorem getElem?_eq_none_iff {a : Array α} : a[i]? = none ↔ a.size ≤ i := by
+  by_cases h : i < a.size
+  · simp [getElem?_eq_getElem, h]
+  · rw [getElem?_neg a i h]
+    simp_all
+
+theorem getElem?_eq {a : Array α} {i : Nat} :
+    a[i]? = if h : i < a.size then some a[i] else none := by
+  split
+  · simp_all [getElem?_eq_getElem]
+  · simp_all
+
+theorem getElem?_eq_getElem?_toList (a : Array α) (i : Nat) : a[i]? = a.toList[i]? := by
+  rw [getElem?_eq]
+  split <;> simp_all
+
+@[deprecated getElem_eq_getElem_toList (since := "2024-09-25")]
+abbrev getElem_eq_toList_getElem := @getElem_eq_getElem_toList
+
 @[deprecated getElem_eq_toList_getElem (since := "2024-09-09")]
-abbrev getElem_eq_data_getElem := @getElem_eq_toList_getElem
+abbrev getElem_eq_data_getElem := @getElem_eq_getElem_toList
 
 @[deprecated getElem_eq_toList_getElem (since := "2024-06-12")]
 theorem getElem_eq_toList_get (a : Array α) (h : i < a.size) : a[i] = a.toList.get ⟨i, h⟩ := by
@@ -36,11 +58,11 @@ theorem getElem_eq_toList_get (a : Array α) (h : i < a.size) : a[i] = a.toList.
 theorem get_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
     have : i < (a.push x).size := by simp [*, Nat.lt_succ_of_le, Nat.le_of_lt]
     (a.push x)[i] = a[i] := by
-  simp only [push, getElem_eq_toList_getElem, List.concat_eq_append, List.getElem_append_left, h]
+  simp only [push, getElem_eq_getElem_toList, List.concat_eq_append, List.getElem_append_left, h]
 
 @[simp] theorem get_push_eq (a : Array α) (x : α) : (a.push x)[a.size] = x := by
-  simp only [push, getElem_eq_toList_getElem, List.concat_eq_append]
+  simp only [push, getElem_eq_getElem_toList, List.concat_eq_append]
-  rw [List.getElem_append_right] <;> simp [getElem_eq_toList_getElem, Nat.zero_lt_one]
+  rw [List.getElem_append_right] <;> simp [getElem_eq_getElem_toList, Nat.zero_lt_one]
 
 theorem get_push (a : Array α) (x : α) (i : Nat) (h : i < (a.push x).size) :
     (a.push x)[i] = if h : i < a.size then a[i] else x := by
@@ -69,11 +91,38 @@ abbrev toArray_data := @toArray_toList
 @[simp] theorem getElem_toArray {a : List α} {i : Nat} (h : i < a.toArray.size) :
     a.toArray[i] = a[i]'(by simpa using h) := rfl
 
-@[simp] theorem toArray_concat {as : List α} {x : α} :
+@[deprecated "Use the reverse direction of `List.push_toArray`." (since := "2024-09-27")]
+theorem toArray_concat {as : List α} {x : α} :
     (as ++ [x]).toArray = as.toArray.push x := by
   apply ext'
   simp
 
+@[simp] theorem push_toArray (l : List α) (a : α) : l.toArray.push a = (l ++ [a]).toArray := by
+  apply Array.ext'
+  simp
+
+/-- Unapplied variant of `push_toArray`, useful for monadic reasoning. -/
+@[simp] theorem push_toArray_fun (l : List α) : l.toArray.push = fun a => (l ++ [a]).toArray := by
+  funext a
+  simp
+
+@[simp] theorem foldrM_toArray [Monad m] (f : α → β → m β) (init : β) (l : List α) :
+    l.toArray.foldrM f init = l.foldrM f init := by
+  rw [foldrM_eq_reverse_foldlM_toList]
+  simp
+
+@[simp] theorem foldlM_toArray [Monad m] (f : β → α → m β) (init : β) (l : List α) :
+    l.toArray.foldlM f init = l.foldlM f init := by
+  rw [foldlM_eq_foldlM_toList]
+
+@[simp] theorem foldr_toArray (f : α → β → β) (init : β) (l : List α) :
+    l.toArray.foldr f init = l.foldr f init := by
+  rw [foldr_eq_foldr_toList]
+
+@[simp] theorem foldl_toArray (f : β → α → β) (init : β) (l : List α) :
+    l.toArray.foldl f init = l.foldl f init := by
+  rw [foldl_eq_foldl_toList]
+
 end List
 
 namespace Array
@@ -220,11 +269,11 @@ theorem get!_eq_getD [Inhabited α] (a : Array α) : a.get! n = a.getD n default
 @[simp] theorem getElem_set_eq (a : Array α) (i : Fin a.size) (v : α) {j : Nat}
       (eq : i.val = j) (p : j < (a.set i v).size) :
     (a.set i v)[j]'p = v := by
-  simp [set, getElem_eq_toList_getElem, ←eq]
+  simp [set, getElem_eq_getElem_toList, ←eq]
 
 @[simp] theorem getElem_set_ne (a : Array α) (i : Fin a.size) (v : α) {j : Nat} (pj : j < (a.set i v).size)
     (h : i.val ≠ j) : (a.set i v)[j]'pj = a[j]'(size_set a i v ▸ pj) := by
-  simp only [set, getElem_eq_toList_getElem, List.getElem_set_ne h]
+  simp only [set, getElem_eq_getElem_toList, List.getElem_set_ne h]
 
 theorem getElem_set (a : Array α) (i : Fin a.size) (v : α) (j : Nat)
     (h : j < (a.set i v).size) :
@@ -314,7 +363,7 @@ termination_by n - i
 abbrev mkArray_data := @toList_mkArray
 
 @[simp] theorem getElem_mkArray (n : Nat) (v : α) (h : i < (mkArray n v).size) :
-    (mkArray n v)[i] = v := by simp [Array.getElem_eq_toList_getElem]
+    (mkArray n v)[i] = v := by simp [Array.getElem_eq_getElem_toList]
 
 /-- # mem -/
 
@@ -355,7 +404,7 @@ theorem lt_of_getElem {x : α} {a : Array α} {idx : Nat} {hidx : idx < a.size}
   hidx
 
 theorem getElem?_mem {l : Array α} {i : Fin l.size} : l[i] ∈ l := by
-  erw [Array.mem_def, getElem_eq_toList_getElem]
+  erw [Array.mem_def, getElem_eq_getElem_toList]
   apply List.get_mem
 
 theorem getElem_fin_eq_toList_get (a : Array α) (i : Fin _) : a[i] = a.toList.get i := rfl
@@ -366,14 +415,11 @@ abbrev getElem_fin_eq_data_get := @getElem_fin_eq_toList_get
 @[simp] theorem ugetElem_eq_getElem (a : Array α) {i : USize} (h : i.toNat < a.size) :
   a[i] = a[i.toNat] := rfl
 
-theorem getElem?_eq_getElem (a : Array α) (i : Nat) (h : i < a.size) : a[i]? = some a[i] :=
-  getElem?_pos ..
-
 theorem get?_len_le (a : Array α) (i : Nat) (h : a.size ≤ i) : a[i]? = none := by
   simp [getElem?_neg, h]
 
 theorem getElem_mem_toList (a : Array α) (h : i < a.size) : a[i] ∈ a.toList := by
-  simp only [getElem_eq_toList_getElem, List.getElem_mem]
+  simp only [getElem_eq_getElem_toList, List.getElem_mem]
 
 @[deprecated getElem_mem_toList (since := "2024-09-09")]
 abbrev getElem_mem_data := @getElem_mem_toList
@@ -433,7 +479,7 @@ abbrev data_set := @toList_set
 
 theorem get_set_eq (a : Array α) (i : Fin a.size) (v : α) :
     (a.set i v)[i.1] = v := by
-  simp only [set, getElem_eq_toList_getElem, List.getElem_set_self]
+  simp only [set, getElem_eq_getElem_toList, List.getElem_set_self]
 
 theorem get?_set_eq (a : Array α) (i : Fin a.size) (v : α) :
     (a.set i v)[i.1]? = v := by simp [getElem?_pos, i.2]
@@ -452,7 +498,7 @@ theorem get_set (a : Array α) (i : Fin a.size) (j : Nat) (hj : j < a.size) (v :
 
 @[simp] theorem get_set_ne (a : Array α) (i : Fin a.size) {j : Nat} (v : α) (hj : j < a.size)
     (h : i.1 ≠ j) : (a.set i v)[j]'(by simp [*]) = a[j] := by
-  simp only [set, getElem_eq_toList_getElem, List.getElem_set_ne h]
+  simp only [set, getElem_eq_getElem_toList, List.getElem_set_ne h]
 
 theorem getElem_setD (a : Array α) (i : Nat) (v : α) (h : i < (setD a i v).size) :
   (setD a i v)[i] = v := by
@@ -468,7 +514,7 @@ theorem swap_def (a : Array α) (i j : Fin a.size) :
     a.swap i j = (a.set i (a.get j)).set ⟨j.1, by simp [j.2]⟩ (a.get i) := by
   simp [swap, fin_cast_val]
 
-theorem toList_swap (a : Array α) (i j : Fin a.size) :
+@[simp] theorem toList_swap (a : Array α) (i j : Fin a.size) :
     (a.swap i j).toList = (a.toList.set i (a.get j)).set j (a.get i) := by simp [swap_def]
 
 @[deprecated toList_swap (since := "2024-09-09")]
@@ -481,7 +527,7 @@ theorem get?_swap (a : Array α) (i j : Fin a.size) (k : Nat) : (a.swap i j)[k]?
 @[simp] theorem swapAt_def (a : Array α) (i : Fin a.size) (v : α) :
     a.swapAt i v = (a[i.1], a.set i v) := rfl
 
--- @[simp] -- FIXME: gives a weird linter error
+@[simp]
 theorem swapAt!_def (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
     a.swapAt! i v = (a[i], a.set ⟨i, h⟩ v) := by simp [swapAt!, h]
 
@@ -554,7 +600,7 @@ abbrev data_range := @toList_range
 
 @[simp]
 theorem getElem_range {n : Nat} {x : Nat} (h : x < (Array.range n).size) : (Array.range n)[x] = x := by
-  simp [getElem_eq_toList_getElem]
+  simp [getElem_eq_getElem_toList]
 
 set_option linter.deprecated false in
 @[simp] theorem reverse_toList (a : Array α) : a.reverse.toList = a.toList.reverse := by
@@ -600,6 +646,32 @@ set_option linter.deprecated false in
 
 /-! ### foldl / foldr -/
 
+@[simp] theorem foldlM_loop_empty [Monad m] (f : β → α → m β) (init : β) (i j : Nat) :
+    foldlM.loop f #[] s h i j init = pure init := by
+  unfold foldlM.loop; split
+  · split
+    · rfl
+    · simp at h
+      omega
+  · rfl
+
+@[simp] theorem foldlM_empty [Monad m] (f : β → α → m β) (init : β) :
+    foldlM f init #[] start stop = return init := by
+  simp [foldlM]
+
+@[simp] theorem foldrM_fold_empty [Monad m] (f : α → β → m β) (init : β) (i j : Nat) (h) :
+    foldrM.fold f #[] i j h init = pure init := by
+  unfold foldrM.fold
+  split <;> rename_i h₁
+  · rfl
+  · split <;> rename_i h₂
+    · rfl
+    · simp at h₂
+
+@[simp] theorem foldrM_empty [Monad m] (f : α → β → m β) (init : β) :
+    foldrM f init #[] start stop = return init := by
+  simp [foldrM]
+
 -- This proof is the pure version of `Array.SatisfiesM_foldlM`,
 -- reproduced to avoid a dependency on `SatisfiesM`.
 theorem foldl_induction
@@ -644,7 +716,7 @@ theorem mapM_eq_mapM_toList [Monad m] [LawfulMonad m] (f : α → m β) (arr : A
   conv => rhs; rw [← List.reverse_reverse arr.toList]
   induction arr.toList.reverse with
   | nil => simp
-  | cons a l ih => simp [ih]; simp [map_eq_pure_bind]
+  | cons a l ih => simp [ih]
 
 @[deprecated mapM_eq_mapM_toList (since := "2024-09-09")]
 abbrev mapM_eq_mapM_data := @mapM_eq_mapM_toList
@@ -785,7 +857,7 @@ theorem get_modify {arr : Array α} {x i} (h : i < arr.size) :
 
 /-! ### filter -/
 
-@[simp] theorem filter_toList (p : α → Bool) (l : Array α) :
+@[simp] theorem toList_filter (p : α → Bool) (l : Array α) :
     (l.filter p).toList = l.toList.filter p := by
   dsimp only [filter]
   rw [foldl_eq_foldl_toList]
@@ -796,23 +868,23 @@ theorem get_modify {arr : Array α} {x i} (h : i < arr.size) :
   induction l with simp
   | cons => split <;> simp [*]
 
-@[deprecated filter_toList (since := "2024-09-09")]
+@[deprecated toList_filter (since := "2024-09-09")]
-abbrev filter_data := @filter_toList
+abbrev filter_data := @toList_filter
 
 @[simp] theorem filter_filter (q) (l : Array α) :
     filter p (filter q l) = filter (fun a => p a && q a) l := by
   apply ext'
-  simp only [filter_toList, List.filter_filter]
+  simp only [toList_filter, List.filter_filter]
 
 @[simp] theorem mem_filter : x ∈ filter p as ↔ x ∈ as ∧ p x := by
-  simp only [mem_def, filter_toList, List.mem_filter]
+  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
 
 /-! ### filterMap -/
 
-@[simp] theorem filterMap_toList (f : α → Option β) (l : Array α) :
+@[simp] theorem toList_filterMap (f : α → Option β) (l : Array α) :
     (l.filterMap f).toList = l.toList.filterMap f := by
   dsimp only [filterMap, filterMapM]
   rw [foldlM_eq_foldlM_toList]
@@ -825,12 +897,12 @@ theorem mem_of_mem_filter {a : α} {l} (h : a ∈ filter p l) : a ∈ l :=
   · simp_all [Id.run, List.filterMap_cons]
     split <;> simp_all
 
-@[deprecated filterMap_toList (since := "2024-09-09")]
+@[deprecated toList_filterMap (since := "2024-09-09")]
-abbrev filterMap_data := @filterMap_toList
+abbrev filterMap_data := @toList_filterMap
 
 @[simp] theorem mem_filterMap {f : α → Option β} {l : Array α} {b : β} :
     b ∈ filterMap f l ↔ ∃ a, a ∈ l ∧ f a = some b := by
-  simp only [mem_def, filterMap_toList, List.mem_filterMap]
+  simp only [mem_def, toList_filterMap, List.mem_filterMap]
 
 /-! ### empty -/
 
@@ -853,7 +925,7 @@ theorem size_append (as bs : Array α) : (as ++ bs).size = as.size + bs.size :=
 
 theorem get_append_left {as bs : Array α} {h : i < (as ++ bs).size} (hlt : i < as.size) :
     (as ++ bs)[i] = as[i] := by
-  simp only [getElem_eq_toList_getElem]
+  simp only [getElem_eq_getElem_toList]
   have h' : i < (as.toList ++ bs.toList).length := by rwa [← toList_length, append_toList] at h
   conv => rhs; rw [← List.getElem_append_left (bs := bs.toList) (h' := h')]
   apply List.get_of_eq; rw [append_toList]
@@ -861,7 +933,7 @@ theorem get_append_left {as bs : Array α} {h : i < (as ++ bs).size} (hlt : i <
 theorem get_append_right {as bs : Array α} {h : i < (as ++ bs).size} (hle : as.size ≤ i)
     (hlt : i - as.size < bs.size := Nat.sub_lt_left_of_lt_add hle (size_append .. ▸ h)) :
     (as ++ bs)[i] = bs[i - as.size] := by
-  simp only [getElem_eq_toList_getElem]
+  simp only [getElem_eq_getElem_toList]
   have h' : i < (as.toList ++ bs.toList).length := by rwa [← toList_length, append_toList] at h
   conv => rhs; rw [← List.getElem_append_right (h₁ := hle) (h₂ := h')]
   apply List.get_of_eq; rw [append_toList]
@@ -1009,6 +1081,33 @@ theorem extract_empty_of_size_le_start (as : Array α) {start stop : Nat} (h : a
 
 /-! ### any -/
 
+theorem anyM_loop_cons [Monad m] (p : α → m Bool) (a : α) (as : List α) (stop start : Nat) (h : stop + 1 ≤ (a :: as).length) :
+    anyM.loop p ⟨a :: as⟩ (stop + 1) h (start + 1) = anyM.loop p ⟨as⟩ stop (by simpa using h) start := by
+  rw [anyM.loop]
+  conv => rhs; rw [anyM.loop]
+  split <;> rename_i h'
+  · simp only [Nat.add_lt_add_iff_right] at h'
+    rw [dif_pos h']
+    rw [anyM_loop_cons]
+    simp
+  · rw [dif_neg]
+    omega
+
+@[simp] theorem anyM_toList [Monad m] (p : α → m Bool) (as : Array α) :
+    as.toList.anyM p = as.anyM p :=
+  match as with
+  | ⟨[]⟩  => rfl
+  | ⟨a :: as⟩ => by
+    simp only [List.anyM, anyM, size_toArray, List.length_cons, Nat.le_refl, ↓reduceDIte]
+    rw [anyM.loop, dif_pos (by omega)]
+    congr 1
+    funext b
+    split
+    · simp
+    · simp only [Bool.false_eq_true, ↓reduceIte]
+      rw [anyM_loop_cons]
+      simpa [anyM] using anyM_toList p ⟨as⟩
+
 -- Auxiliary for `any_iff_exists`.
 theorem anyM_loop_iff_exists {p : α → Bool} {as : Array α} {start stop} (h : stop ≤ as.size) :
     anyM.loop (m := Id) p as stop h start = true ↔
@@ -1053,6 +1152,17 @@ theorem any_def {p : α → Bool} (as : Array α) : as.any p = as.toList.any p :
 
 /-! ### all -/
 
+theorem allM_eq_not_anyM_not [Monad m] [LawfulMonad m] (p : α → m Bool) (as : Array α) :
+    allM p as = (! ·) <$> anyM ((! ·) <$> p ·) as := by
+  dsimp [allM, anyM]
+  simp
+
+@[simp] theorem allM_toList [Monad m] [LawfulMonad m] (p : α → m Bool) (as : Array α) :
+    as.toList.allM p = as.allM p := by
+  rw [allM_eq_not_anyM_not]
+  rw [← anyM_toList]
+  rw [List.allM_eq_not_anyM_not]
+
 theorem all_eq_not_any_not (p : α → Bool) (as : Array α) (start stop) :
     all as p start stop = !(any as (!p ·) start stop) := by
   dsimp [all, allM]
@@ -1074,10 +1184,10 @@ theorem all_def {p : α → Bool} (as : Array α) : as.all p = as.toList.all p :
   rw [Bool.eq_iff_iff, all_eq_true, List.all_eq_true]; simp only [List.mem_iff_getElem]
   constructor
   · rintro w x ⟨r, h, rfl⟩
-    rw [← getElem_eq_toList_getElem]
+    rw [← getElem_eq_getElem_toList]
     exact w ⟨r, h⟩
   · intro w i
-    exact w as[i] ⟨i, i.2, (getElem_eq_toList_getElem as i.2).symm⟩
+    exact w as[i] ⟨i, i.2, (getElem_eq_getElem_toList i.2).symm⟩
 
 theorem all_eq_true_iff_forall_mem {l : Array α} : l.all p ↔ ∀ x, x ∈ l → p x := by
   simp only [all_def, List.all_eq_true, mem_def]
@@ -1149,3 +1259,117 @@ theorem swap_comm (a : Array α) {i j : Fin a.size} : a.swap i j = a.swap j i :=
     · split <;> simp_all
 
 end Array
+
+
+open Array
+
+namespace List
+
+/-!
+### More theorems about `List.toArray`, followed by an `Array` operation.
+
+Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible.
+-/
+
+@[simp] theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by
+  simp [mem_def]
+
+@[simp] theorem getElem?_toArray (l : List α) (i : Nat) : l.toArray[i]? = l[i]? := by
+  simp [getElem?_eq_getElem?_toList]
+
+@[simp] theorem toListRev_toArray (l : List α) : l.toArray.toListRev = l.reverse := by
+  simp
+
+@[simp] theorem push_append_toArray (as : Array α) (a : α) (l : List α) :
+    as.push a ++ l.toArray = as ++ (a :: l).toArray := by
+  apply ext'
+  simp
+
+@[simp] theorem mapM_toArray [Monad m] [LawfulMonad m] (f : α → m β) (l : List α) :
+    l.toArray.mapM f = List.toArray <$> l.mapM f := by
+  simp only [← mapM'_eq_mapM, mapM_eq_foldlM]
+  suffices ∀ init : Array β,
+      foldlM (fun bs a => bs.push <$> f a) init l.toArray = (init ++ toArray ·) <$> mapM' f l by
+    simpa using this #[]
+  intro init
+  induction l generalizing init with
+  | nil => simp
+  | cons a l ih =>
+    simp only [foldlM_toArray] at ih
+    rw [size_toArray, mapM'_cons, foldlM_toArray]
+    simp [ih]
+
+@[simp] theorem map_toArray (f : α → β) (l : List α) : l.toArray.map f = (l.map f).toArray := by
+  apply ext'
+  simp
+
+@[simp] theorem toArray_appendList (l₁ l₂ : List α) :
+    l₁.toArray ++ l₂ = (l₁ ++ l₂).toArray := by
+  apply ext'
+  simp
+
+@[simp] theorem set_toArray (l : List α) (i : Fin l.toArray.size) (a : α) :
+    l.toArray.set i a = (l.set i a).toArray := by
+  apply ext'
+  simp
+
+@[simp] theorem uset_toArray (l : List α) (i : USize) (a : α) (h : i.toNat < l.toArray.size) :
+    l.toArray.uset i a h = (l.set i.toNat a).toArray := by
+  apply ext'
+  simp
+
+@[simp] theorem setD_toArray (l : List α) (i : Nat) (a : α) :
+    l.toArray.setD i a  = (l.set i a).toArray := by
+  apply ext'
+  simp only [setD]
+  split
+  · simp
+  · simp_all [List.set_eq_of_length_le]
+
+@[simp] theorem anyM_toArray [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) :
+    l.toArray.anyM p = l.anyM p := by
+  rw [← anyM_toList]
+
+@[simp] theorem any_toArray (p : α → Bool) (l : List α) : l.toArray.any p = l.any p := by
+  rw [Array.any_def]
+
+@[simp] theorem allM_toArray [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) :
+    l.toArray.allM p = l.allM p := by
+  rw [← allM_toList]
+
+@[simp] theorem all_toArray (p : α → Bool) (l : List α) : l.toArray.all p = l.all p := by
+  rw [Array.all_def]
+
+@[simp] theorem swap_toArray (l : List α) (i j : Fin l.toArray.size) :
+    l.toArray.swap i j = ((l.set i l[j]).set j l[i]).toArray := by
+  apply ext'
+  simp
+
+@[simp] theorem pop_toArray (l : List α) : l.toArray.pop = l.dropLast.toArray := by
+  apply ext'
+  simp
+
+@[simp] theorem reverse_toArray (l : List α) : l.toArray.reverse = l.reverse.toArray := by
+  apply ext'
+  simp
+
+@[simp] theorem filter_toArray (p : α → Bool) (l : List α) :
+    l.toArray.filter p = (l.filter p).toArray := by
+  apply ext'
+  erw [toList_filter] -- `erw` required to unify `l.length` with `l.toArray.size`.
+
+@[simp] theorem filterMap_toArray (f : α → Option β) (l : List α) :
+    l.toArray.filterMap f = (l.filterMap f).toArray := by
+  apply ext'
+  erw [toList_filterMap] -- `erw` required to unify `l.length` with `l.toArray.size`.
+
+@[simp] theorem append_toArray (l₁ l₂ : List α) :
+    l₁.toArray ++ l₂.toArray = (l₁ ++ l₂).toArray := by
+  apply ext'
+  simp
+
+@[simp] theorem toArray_range (n : Nat) : (range n).toArray = Array.range n := by
+  apply ext'
+  simp
+
+end List

src/Init/Data/Array/Subarray.lean

@@ -59,6 +59,22 @@ def popFront (s : Subarray α) : Subarray α :=
   else
     s
 
+/--
+The empty subarray.
+-/
+protected def empty : Subarray α where
+  array := #[]
+  start := 0
+  stop := 0
+  start_le_stop := Nat.le_refl 0
+  stop_le_array_size := Nat.le_refl 0
+
+instance : EmptyCollection (Subarray α) :=
+  ⟨Subarray.empty⟩
+
+instance : Inhabited (Subarray α) :=
+  ⟨{}⟩
+
 @[inline] unsafe def forInUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (s : Subarray α) (b : β) (f : α → β → m (ForInStep β)) : m β :=
   let sz := USize.ofNat s.stop
   let rec @[specialize] loop (i : USize) (b : β) : m β := do

src/Init/Data/Array/TakeDrop.lean

@@ -12,7 +12,7 @@ namespace Array
 theorem exists_of_uset (self : Array α) (i d h) :
     ∃ l₁ l₂, self.toList = l₁ ++ self[i] :: l₂ ∧ List.length l₁ = i.toNat ∧
       (self.uset i d h).toList = l₁ ++ d :: l₂ := by
-  simpa only [ugetElem_eq_getElem, getElem_eq_toList_getElem, uset, toList_set] using
+  simpa only [ugetElem_eq_getElem, getElem_eq_getElem_toList, uset, toList_set] using
     List.exists_of_set _
 
 end Array

src/Init/Data/BitVec/Basic.lean

@@ -269,8 +269,8 @@ Return the absolute value of a signed bitvector.
 protected def abs (x : BitVec n) : BitVec n := if x.msb then .neg x else x
 
 /--
-Multiplication for bit vectors. This can be interpreted as either signed or unsigned negation
+Multiplication for bit vectors. This can be interpreted as either signed or unsigned
-modulo `2^n`.
+multiplication modulo `2^n`.
 
 SMT-Lib name: `bvmul`.
 -/
@@ -676,6 +676,13 @@ result of appending a single bit to the front in the naive implementation).
     That is, the new bit is the least significant bit. -/
 def concat {n} (msbs : BitVec n) (lsb : Bool) : BitVec (n+1) := msbs ++ (ofBool lsb)
 
+/--
+`x.shiftConcat b` shifts all bits of `x` to the left by `1` and sets the least significant bit to `b`.
+It is a non-dependent version of `concat` that does not change the total bitwidth.
+-/
+def shiftConcat (x : BitVec n) (b : Bool) : BitVec n :=
+  (x.concat b).truncate n
+
 /-- Prepend a single bit to the front of a bitvector, using big endian order (see `append`).
     That is, the new bit is the most significant bit. -/
 def cons {n} (msb : Bool) (lsbs : BitVec n) : BitVec (n+1) :=

src/Init/Data/BitVec/Bitblast.lean

@@ -438,6 +438,386 @@ theorem shiftLeft_eq_shiftLeftRec (x : BitVec w₁) (y : BitVec w₂) :
   · simp [of_length_zero]
   · simp [shiftLeftRec_eq]
 
+/-! # udiv/urem recurrence for bitblasting
+
+In order to prove the correctness of the division algorithm on the integers,
+one shows that `n.div d = q` and `n.mod d = r` iff `n = d * q + r` and `0 ≤ r < d`.
+Mnemonic: `n` is the numerator, `d` is the denominator, `q` is the quotient, and `r` the remainder.
+
+This *uniqueness of decomposition* is not true for bitvectors.
+For `n = 0, d = 3, w = 3`, we can write:
+- `0 = 0 * 3 + 0` (`q = 0`, `r = 0 < 3`.)
+- `0 = 2 * 3 + 2 = 6 + 2 ≃ 0 (mod 8)` (`q = 2`, `r = 2 < 3`).
+
+Such examples can be created by choosing different `(q, r)` for a fixed `(d, n)`
+such that `(d * q + r)` overflows and wraps around to equal `n`.
+
+This tells us that the division algorithm must have more restrictions than just the ones
+we have for integers. These restrictions are captured in `DivModState.Lawful`.
+The key idea is to state the relationship in terms of the toNat values of {n, d, q, r}.
+If the division equation `d.toNat * q.toNat + r.toNat = n.toNat` holds,
+then `n.udiv d = q` and `n.umod d = r`.
+
+Following this, we implement the division algorithm by repeated shift-subtract.
+
+References:
+- Fast 32-bit Division on the DSP56800E: Minimized nonrestoring division algorithm by David Baca
+- Bitwuzla sources for bitblasting.h
+-/
+
+private theorem Nat.div_add_eq_left_of_lt {x y z : Nat} (hx : z ∣ x) (hy : y < z) (hz : 0 < z) :
+    (x + y) / z = x / z := by
+  refine Nat.div_eq_of_lt_le ?lo ?hi
+  · apply Nat.le_trans
+    · exact div_mul_le_self x z
+    · omega
+  · simp only [succ_eq_add_one, Nat.add_mul, Nat.one_mul]
+    apply Nat.add_lt_add_of_le_of_lt
+    · apply Nat.le_of_eq
+      exact (Nat.div_eq_iff_eq_mul_left hz hx).mp rfl
+    · exact hy
+
+/-- If the division equation `d.toNat * q.toNat + r.toNat = n.toNat` holds,
+then `n.udiv d = q`. -/
+theorem udiv_eq_of_mul_add_toNat {d n q r : BitVec w} (hd : 0 < d)
+    (hrd : r < d)
+    (hdqnr : d.toNat * q.toNat + r.toNat = n.toNat) :
+    n.udiv d = q := by
+  apply BitVec.eq_of_toNat_eq
+  rw [toNat_udiv]
+  replace hdqnr : (d.toNat * q.toNat + r.toNat) / d.toNat = n.toNat / d.toNat := by
+    simp [hdqnr]
+  rw [Nat.div_add_eq_left_of_lt] at hdqnr
+  · rw [← hdqnr]
+    exact mul_div_right q.toNat hd
+  · exact Nat.dvd_mul_right d.toNat q.toNat
+  · exact hrd
+  · exact hd
+
+/-- If the division equation `d.toNat * q.toNat + r.toNat = n.toNat` holds,
+then `n.umod d = r`. -/
+theorem umod_eq_of_mul_add_toNat {d n q r : BitVec w} (hrd : r < d)
+    (hdqnr : d.toNat * q.toNat + r.toNat = n.toNat) :
+    n.umod d = r := by
+  apply BitVec.eq_of_toNat_eq
+  rw [toNat_umod]
+  replace hdqnr : (d.toNat * q.toNat + r.toNat) % d.toNat = n.toNat % d.toNat := by
+    simp [hdqnr]
+  rw [Nat.add_mod, Nat.mul_mod_right] at hdqnr
+  simp only [Nat.zero_add, mod_mod] at hdqnr
+  replace hrd : r.toNat < d.toNat := by
+    simpa [BitVec.lt_def] using hrd
+  rw [Nat.mod_eq_of_lt hrd] at hdqnr
+  simp [hdqnr]
+
+/-! ### DivModState -/
+
+/-- `DivModState` is a structure that maintains the state of recursive `divrem` calls. -/
+structure DivModState (w : Nat) : Type where
+  /-- The number of bits in the numerator that are not yet processed -/
+  wn : Nat
+  /-- The number of bits in the remainder (and quotient) -/
+  wr : Nat
+  /-- The current quotient. -/
+  q : BitVec w
+  /-- The current remainder. -/
+  r : BitVec w
+
+
+/-- `DivModArgs` contains the arguments to a `divrem` call which remain constant throughout
+execution. -/
+structure DivModArgs (w : Nat) where
+  /-- the numerator (aka, dividend) -/
+  n : BitVec w
+  /-- the denumerator (aka, divisor)-/
+  d : BitVec w
+
+/-- A `DivModState` is lawful if the remainder width `wr` plus the numerator width `wn` equals `w`,
+and the bitvectors `r` and `n` have values in the bounds given by bitwidths `wr`, resp. `wn`.
+
+This is a proof engineering choice: an alternative world could have been
+`r : BitVec wr` and `n : BitVec wn`, but this required much more dependent typing coercions.
+
+Instead, we choose to declare all involved bitvectors as length `w`, and then prove that
+the values are within their respective bounds.
+
+We start with `wn = w` and `wr = 0`, and then in each step, we decrement `wn` and increment `wr`.
+In this way, we grow a legal remainder in each loop iteration.
+-/
+structure DivModState.Lawful {w : Nat} (args : DivModArgs w) (qr : DivModState w) : Prop where
+  /-- The sum of widths of the dividend and remainder is `w`. -/
+  hwrn : qr.wr + qr.wn = w
+  /-- The denominator is positive. -/
+  hdPos : 0 < args.d
+  /-- The remainder is strictly less than the denominator. -/
+  hrLtDivisor : qr.r.toNat < args.d.toNat
+  /-- The remainder is morally a `Bitvec wr`, and so has value less than `2^wr`. -/
+  hrWidth : qr.r.toNat < 2^qr.wr
+  /-- The quotient is morally a `Bitvec wr`, and so has value less than `2^wr`. -/
+  hqWidth : qr.q.toNat < 2^qr.wr
+  /-- The low `(w - wn)` bits of `n` obey the invariant for division. -/
+  hdiv : args.n.toNat >>> qr.wn = args.d.toNat * qr.q.toNat + qr.r.toNat
+
+/-- A lawful DivModState implies `w > 0`. -/
+def DivModState.Lawful.hw {args : DivModArgs w} {qr : DivModState w}
+    {h : DivModState.Lawful args qr} : 0 < w := by
+  have hd := h.hdPos
+  rcases w with rfl | w
+  · have hcontra : args.d = 0#0 := by apply Subsingleton.elim
+    rw [hcontra] at hd
+    simp at hd
+  · omega
+
+/-- An initial value with both `q, r = 0`. -/
+def DivModState.init (w : Nat) : DivModState w := {
+  wn := w
+  wr := 0
+  q := 0#w
+  r := 0#w
+}
+
+/-- The initial state is lawful. -/
+def DivModState.lawful_init {w : Nat} (args : DivModArgs w) (hd : 0#w < args.d) :
+    DivModState.Lawful args (DivModState.init w) := by
+  simp only [BitVec.DivModState.init]
+  exact {
+    hwrn := by simp only; omega,
+    hdPos := by assumption
+    hrLtDivisor := by simp [BitVec.lt_def] at hd ⊢; assumption
+    hrWidth := by simp [DivModState.init],
+    hqWidth := by simp [DivModState.init],
+    hdiv := by
+      simp only [DivModState.init, toNat_ofNat, zero_mod, Nat.mul_zero, Nat.add_zero];
+      rw [Nat.shiftRight_eq_div_pow]
+      apply Nat.div_eq_of_lt args.n.isLt
+  }
+
+/--
+A lawful DivModState with a fully consumed dividend (`wn = 0`) witnesses that the
+quotient has been correctly computed.
+-/
+theorem DivModState.udiv_eq_of_lawful {n d : BitVec w} {qr : DivModState w}
+    (h_lawful : DivModState.Lawful {n, d} qr)
+    (h_final  : qr.wn = 0) :
+    n.udiv d = qr.q := by
+  apply udiv_eq_of_mul_add_toNat h_lawful.hdPos h_lawful.hrLtDivisor
+  have hdiv := h_lawful.hdiv
+  simp only [h_final] at *
+  omega
+
+/--
+A lawful DivModState with a fully consumed dividend (`wn = 0`) witnesses that the
+remainder has been correctly computed.
+-/
+theorem DivModState.umod_eq_of_lawful {qr : DivModState w}
+    (h : DivModState.Lawful {n, d} qr)
+    (h_final  : qr.wn = 0) :
+    n.umod d = qr.r := by
+  apply umod_eq_of_mul_add_toNat h.hrLtDivisor
+  have hdiv := h.hdiv
+  simp only [shiftRight_zero] at hdiv
+  simp only [h_final] at *
+  exact hdiv.symm
+
+/-! ### DivModState.Poised -/
+
+/--
+A `Poised` DivModState is a state which is `Lawful` and furthermore, has at least
+one numerator bit left to process `(0 < wn)`
+
+The input to the shift subtractor is a legal input to `divrem`, and we also need to have an
+input bit to perform shift subtraction on, and thus we need `0 < wn`.
+-/
+structure DivModState.Poised {w : Nat} (args : DivModArgs w) (qr : DivModState w)
+  extends DivModState.Lawful args qr : Type where
+  /-- Only perform a round of shift-subtract if we have dividend bits. -/
+  hwn_lt : 0 < qr.wn
+
+/--
+In the shift subtract input, the dividend is at least one bit long (`wn > 0`), so
+the remainder has bits to be computed (`wr < w`).
+-/
+def DivModState.wr_lt_w {qr : DivModState w} (h : qr.Poised args) : qr.wr < w := by
+  have hwrn := h.hwrn
+  have hwn_lt := h.hwn_lt
+  omega
+
+/-! ### Division shift subtractor -/
+
+/--
+One round of the division algorithm, that tries to perform a subtract shift.
+Note that this should only be called when `r.msb = false`, so we will not overflow.
+-/
+def divSubtractShift (args : DivModArgs w) (qr : DivModState w) : DivModState w :=
+  let {n, d} := args
+  let wn := qr.wn - 1
+  let wr := qr.wr + 1
+  let r' := shiftConcat qr.r (n.getLsbD wn)
+  if r' < d then {
+    q := qr.q.shiftConcat false, -- If `r' < d`, then we do not have a quotient bit.
+    r := r'
+    wn, wr
+  } else {
+    q := qr.q.shiftConcat true, -- Otherwise, `r' ≥ d`, and we have a quotient bit.
+    r := r' - d -- we subtract to maintain the invariant that `r < d`.
+    wn, wr
+  }
+
+/-- The value of shifting right by `wn - 1` equals shifting by `wn` and grabbing the lsb at `(wn - 1)`. -/
+theorem DivModState.toNat_shiftRight_sub_one_eq
+    {args : DivModArgs w} {qr : DivModState w} (h : qr.Poised args) :
+    args.n.toNat >>> (qr.wn - 1)
+    = (args.n.toNat >>> qr.wn) * 2 + (args.n.getLsbD (qr.wn - 1)).toNat := by
+  show BitVec.toNat (args.n >>> (qr.wn - 1)) = _
+  have {..} := h -- break the structure down for `omega`
+  rw [shiftRight_sub_one_eq_shiftConcat args.n h.hwn_lt]
+  rw [toNat_shiftConcat_eq_of_lt (k := w - qr.wn)]
+  · simp
+  · omega
+  · apply BitVec.toNat_ushiftRight_lt
+    omega
+
+/--
+This is used when proving the correctness of the divison algorithm,
+where we know that `r < d`.
+We then want to show that `((r.shiftConcat b) - d) < d` as the loop invariant.
+In arithmetic, this is the same as showing that
+`r * 2 + 1 - d < d`, which this theorem establishes.
+-/
+private theorem two_mul_add_sub_lt_of_lt_of_lt_two (h : a < x) (hy : y < 2) :
+    2 * a + y - x < x := by omega
+
+/-- We show that the output of `divSubtractShift` is lawful, which tells us that it
+obeys the division equation. -/
+theorem lawful_divSubtractShift (qr : DivModState w) (h : qr.Poised args) :
+    DivModState.Lawful args (divSubtractShift args qr) := by
+  rcases args with ⟨n, d⟩
+  simp only [divSubtractShift, decide_eq_true_eq]
+  -- We add these hypotheses for `omega` to find them later.
+  have ⟨⟨hrwn, hd, hrd, hr, hn, hrnd⟩, hwn_lt⟩ := h
+  have : d.toNat * (qr.q.toNat * 2) = d.toNat * qr.q.toNat * 2 := by rw [Nat.mul_assoc]
+  by_cases rltd : shiftConcat qr.r (n.getLsbD (qr.wn - 1)) < d
+  · simp only [rltd, ↓reduceIte]
+    constructor <;> try bv_omega
+    case pos.hrWidth => apply toNat_shiftConcat_lt_of_lt <;> omega
+    case pos.hqWidth => apply toNat_shiftConcat_lt_of_lt <;> omega
+    case pos.hdiv =>
+      simp [qr.toNat_shiftRight_sub_one_eq h, h.hdiv, this,
+        toNat_shiftConcat_eq_of_lt (qr.wr_lt_w h) h.hrWidth,
+        toNat_shiftConcat_eq_of_lt (qr.wr_lt_w h) h.hqWidth]
+      omega
+  · simp only [rltd, ↓reduceIte]
+    constructor <;> try bv_omega
+    case neg.hrLtDivisor =>
+      simp only [lt_def, Nat.not_lt] at rltd
+      rw [BitVec.toNat_sub_of_le rltd,
+        toNat_shiftConcat_eq_of_lt (hk := qr.wr_lt_w h) (hx := h.hrWidth),
+        Nat.mul_comm]
+      apply two_mul_add_sub_lt_of_lt_of_lt_two <;> bv_omega
+    case neg.hrWidth =>
+      simp only
+      have hdr' : d ≤ (qr.r.shiftConcat (n.getLsbD (qr.wn - 1))) :=
+        BitVec.not_lt_iff_le.mp rltd
+      have hr' : ((qr.r.shiftConcat (n.getLsbD (qr.wn - 1)))).toNat < 2 ^ (qr.wr + 1) := by
+        apply toNat_shiftConcat_lt_of_lt <;> bv_omega
+      rw [BitVec.toNat_sub_of_le hdr']
+      omega
+    case neg.hqWidth =>
+      apply toNat_shiftConcat_lt_of_lt <;> omega
+    case neg.hdiv =>
+      have rltd' := (BitVec.not_lt_iff_le.mp rltd)
+      simp only [qr.toNat_shiftRight_sub_one_eq h,
+        BitVec.toNat_sub_of_le rltd',
+        toNat_shiftConcat_eq_of_lt (qr.wr_lt_w h) h.hrWidth]
+      simp only [BitVec.le_def,
+        toNat_shiftConcat_eq_of_lt (qr.wr_lt_w h) h.hrWidth] at rltd'
+      simp only [toNat_shiftConcat_eq_of_lt (qr.wr_lt_w h) h.hqWidth, h.hdiv, Nat.mul_add]
+      bv_omega
+
+/-! ### Core division algorithm circuit -/
+
+/-- A recursive definition of division for bitblasting, in terms of a shift-subtraction circuit. -/
+def divRec {w : Nat} (m : Nat) (args : DivModArgs w) (qr : DivModState w) :
+    DivModState w :=
+  match m with
+  | 0 => qr
+  | m + 1 => divRec m args <| divSubtractShift args qr
+
+@[simp]
+theorem divRec_zero (qr : DivModState w) :
+    divRec 0 args qr = qr := rfl
+
+@[simp]
+theorem divRec_succ (m : Nat) (args : DivModArgs w) (qr : DivModState w) :
+    divRec (m + 1) args qr =
+      divRec m args (divSubtractShift args qr) := rfl
+
+/-- The output of `divRec` is a lawful state -/
+theorem lawful_divRec {args : DivModArgs w} {qr : DivModState w}
+    (h : DivModState.Lawful args qr) :
+    DivModState.Lawful args (divRec qr.wn args qr) := by
+  generalize hm : qr.wn = m
+  induction m generalizing qr
+  case zero =>
+    exact h
+  case succ wn' ih =>
+    simp only [divRec_succ]
+    apply ih
+    · apply lawful_divSubtractShift
+      constructor
+      · assumption
+      · omega
+    · simp only [divSubtractShift, hm]
+      split <;> rfl
+
+/-- The output of `divRec` has no more bits left to process (i.e., `wn = 0`) -/
+@[simp]
+theorem wn_divRec (args : DivModArgs w) (qr : DivModState w) :
+    (divRec qr.wn args qr).wn = 0 := by
+  generalize hm : qr.wn = m
+  induction m generalizing qr
+  case zero =>
+    assumption
+  case succ wn' ih =>
+    apply ih
+    simp only [divSubtractShift, hm]
+    split <;> rfl
+
+/-- The result of `udiv` agrees with the result of the division recurrence. -/
+theorem udiv_eq_divRec (hd : 0#w < d) :
+    let out := divRec w {n, d} (DivModState.init w)
+    n.udiv d = out.q := by
+  have := DivModState.lawful_init {n, d} hd
+  have := lawful_divRec this
+  apply DivModState.udiv_eq_of_lawful this (wn_divRec ..)
+
+/-- The result of `umod` agrees with the result of the division recurrence. -/
+theorem umod_eq_divRec (hd : 0#w < d) :
+    let out := divRec w {n, d} (DivModState.init w)
+    n.umod d = out.r := by
+  have := DivModState.lawful_init {n, d} hd
+  have := lawful_divRec this
+  apply DivModState.umod_eq_of_lawful this (wn_divRec ..)
+
+@[simp]
+theorem divRec_succ' (m : Nat) (args : DivModArgs w) (qr : DivModState w) :
+    divRec (m+1) args qr =
+    let wn := qr.wn - 1
+    let wr := qr.wr + 1
+    let r' := shiftConcat qr.r (args.n.getLsbD wn)
+    let input : DivModState _ :=
+      if r' < args.d then {
+        q := qr.q.shiftConcat false,
+        r := r'
+        wn, wr
+      } else {
+        q := qr.q.shiftConcat true,
+        r := r' - args.d
+        wn, wr
+      }
+    divRec m args input := by
+  simp [divRec_succ, divSubtractShift]
+
 /- ### Arithmetic shift right (sshiftRight) recurrence -/
 
 /--

src/Init/Data/BitVec/Lemmas.lean

@@ -11,6 +11,7 @@ import Init.Data.Fin.Lemmas
 import Init.Data.Nat.Lemmas
 import Init.Data.Nat.Mod
 import Init.Data.Int.Bitwise.Lemmas
+import Init.Data.Int.Pow
 
 set_option linter.missingDocs true
 
@@ -164,7 +165,8 @@ theorem getMsbD_eq_getMsb?_getD (x : BitVec w) (i : Nat) :
   · simp [getMsb?, h]
   · rw [getLsbD_eq_getElem?_getD, getMsb?_eq_getLsb?]
     split <;>
-    · simp
+    · simp only [getLsb?_eq_getElem?, Bool.and_iff_right_iff_imp, decide_eq_true_eq,
+        Option.getD_none, Bool.and_eq_false_imp]
       intros
       omega
 
@@ -271,6 +273,10 @@ theorem getLsbD_ofNat (n : Nat) (x : Nat) (i : Nat) :
 @[simp] theorem toNat_mod_cancel (x : BitVec n) : x.toNat % (2^n) = x.toNat :=
   Nat.mod_eq_of_lt x.isLt
 
+@[simp] theorem toNat_mod_cancel' {x : BitVec n} :
+    (x.toNat : Int) % (((2 ^ n) : Nat) : Int) = x.toNat := by
+  rw_mod_cast [toNat_mod_cancel]
+
 @[simp] theorem sub_toNat_mod_cancel {x : BitVec w} (h : ¬ x = 0#w) :
     (2 ^ w - x.toNat) % 2 ^ w = 2 ^ w - x.toNat := by
   simp only [toNat_eq, toNat_ofNat, Nat.zero_mod] at h
@@ -298,7 +304,7 @@ theorem getElem?_zero_ofNat_one : (BitVec.ofNat (w+1) 1)[0]? = some true := by
 
 -- This does not need to be a `@[simp]` theorem as it is already handled by `getElem?_eq_getElem`.
 theorem getElem?_zero_ofBool (b : Bool) : (ofBool b)[0]? = some b := by
-  simp [ofBool, cond_eq_if]
+  simp only [ofBool, ofNat_eq_ofNat, cond_eq_if]
   split <;> simp_all
 
 @[simp] theorem getElem_zero_ofBool (b : Bool) : (ofBool b)[0] = b := by
@@ -327,7 +333,7 @@ theorem getElem_ofBool {b : Bool} {i : Nat} : (ofBool b)[0] = b := by
 
 theorem msb_eq_getLsbD_last (x : BitVec w) :
     x.msb = x.getLsbD (w - 1) := by
-  simp [BitVec.msb, getMsbD, getLsbD]
+  simp only [BitVec.msb, getMsbD]
   rcases w  with rfl | w
   · simp [BitVec.eq_nil x]
   · simp
@@ -355,7 +361,7 @@ theorem toNat_ge_of_msb_true {x : BitVec n} (p : BitVec.msb x = true) : x.toNat
   | 0 =>
     simp [BitVec.msb, BitVec.getMsbD] at p
   | n + 1 =>
-    simp [BitVec.msb_eq_decide] at p
+    simp only [msb_eq_decide, Nat.add_one_sub_one, decide_eq_true_eq] at p
     simp only [Nat.add_sub_cancel]
     exact p
 
@@ -415,7 +421,7 @@ theorem toInt_eq_toNat_bmod (x : BitVec n) : x.toInt = Int.bmod x.toNat (2^n) :=
 /-- Prove equality of bitvectors in terms of nat operations. -/
 theorem eq_of_toInt_eq {x y : BitVec n} : x.toInt = y.toInt → x = y := by
   intro eq
-  simp [toInt_eq_toNat_cond] at eq
+  simp only [toInt_eq_toNat_cond] at eq
   apply eq_of_toNat_eq
   revert eq
   have _xlt := x.isLt
@@ -895,8 +901,8 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
     rw [← h]
     rw [Nat.testBit_two_pow_sub_succ (isLt _)]
     · cases w : decide (i < v)
-      · simp at w
+      · simp only [decide_eq_false_iff_not, Nat.not_lt] at w
-        simp [w]
+        simp only [Bool.false_bne, Bool.false_and]
         rw [Nat.testBit_lt_two_pow]
         calc BitVec.toNat x < 2 ^ v := isLt _
           _ ≤ 2 ^ i := Nat.pow_le_pow_of_le_right Nat.zero_lt_two w
@@ -927,6 +933,10 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
   ext
   simp
 
+@[simp] theorem not_allOnes : ~~~ allOnes w = 0#w := by
+  ext
+  simp
+
 @[simp] theorem xor_allOnes {x : BitVec w} : x ^^^ allOnes w = ~~~ x := by
   ext i
   simp
@@ -935,6 +945,21 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
   ext i
   simp
 
+@[simp]
+theorem not_not {b : BitVec w} : ~~~(~~~b) = b := by
+  ext i
+  simp
+
+@[simp] theorem getMsb_not {x : BitVec w} :
+    (~~~x).getMsbD i = (decide (i < w) && !(x.getMsbD i)) := by
+  simp only [getMsbD]
+  by_cases h : i < w
+  · simp [h]; omega
+  · simp [h];
+
+@[simp] theorem msb_not {x : BitVec w} : (~~~x).msb = (decide (0 < w) && !x.msb) := by
+  simp [BitVec.msb]
+
 /-! ### cast -/
 
 @[simp] theorem not_cast {x : BitVec w} (h : w = w') : ~~~(cast h x) = cast h (~~~x) := by
@@ -1017,7 +1042,8 @@ theorem shiftLeft_or_distrib (x y : BitVec w) (n : Nat) :
   simp only [t]
   simp only [decide_True, Nat.sub_sub, Bool.true_and, Nat.add_assoc]
   by_cases h₁ : k < w <;> by_cases h₂ : w - (1 + k) < i <;> by_cases h₃ : k + i < w
-    <;> simp [h₁, h₂, h₃]
+    <;> simp only [h₁, h₂, h₃, decide_False, h₂, decide_True, Bool.not_true, Bool.false_and, Bool.and_self,
+      Bool.true_and, Bool.false_eq, Bool.false_and, Bool.not_false]
     <;> (first | apply getLsbD_ge | apply Eq.symm; apply getLsbD_ge)
     <;> omega
 
@@ -1068,6 +1094,16 @@ theorem shiftLeft_add {w : Nat} (x : BitVec w) (n m : Nat) :
   cases h₅ : decide (i < n + m) <;>
     simp at * <;> omega
 
+@[simp]
+theorem allOnes_shiftLeft_and_shiftLeft {x : BitVec w} {n : Nat} :
+    BitVec.allOnes w <<< n &&& x <<< n = x <<< n := by
+  simp [← BitVec.shiftLeft_and_distrib]
+
+@[simp]
+theorem allOnes_shiftLeft_or_shiftLeft {x : BitVec w} {n : Nat} :
+    BitVec.allOnes w <<< n ||| x <<< n = BitVec.allOnes w <<< n := by
+  simp [← shiftLeft_or_distrib]
+
 @[deprecated shiftLeft_add (since := "2024-06-02")]
 theorem shiftLeft_shiftLeft {w : Nat} (x : BitVec w) (n m : Nat) :
     (x <<< n) <<< m = x <<< (n + m) := by
@@ -1125,6 +1161,17 @@ theorem ushiftRight_or_distrib (x y : BitVec w)  (n : Nat) :
 theorem ushiftRight_zero_eq (x : BitVec w) : x >>> 0 = x := by
   simp [bv_toNat]
 
+/--
+Shifting right by `n < w` yields a bitvector whose value is less than `2 ^ (w - n)`.
+-/
+theorem toNat_ushiftRight_lt (x : BitVec w) (n : Nat) (hn : n ≤ w) :
+    (x >>> n).toNat < 2 ^ (w - n) := by
+  rw [toNat_ushiftRight, Nat.shiftRight_eq_div_pow, Nat.div_lt_iff_lt_mul]
+  · rw [Nat.pow_sub_mul_pow]
+    · apply x.isLt
+    · apply hn
+  · apply Nat.pow_pos (by decide)
+
 /-! ### ushiftRight reductions from BitVec to Nat -/
 
 @[simp]
@@ -1258,6 +1305,22 @@ theorem sshiftRight_add {x : BitVec w} {m n : Nat} :
         omega
       · simp [h₃, sshiftRight_msb_eq_msb]
 
+theorem not_sshiftRight {b : BitVec w} :
+    ~~~b.sshiftRight n = (~~~b).sshiftRight n := by
+  ext i
+  simp only [getLsbD_not, Fin.is_lt, decide_True, getLsbD_sshiftRight, Bool.not_and, Bool.not_not,
+    Bool.true_and, msb_not]
+  by_cases h : w ≤ i
+  <;> by_cases h' : n + i < w
+  <;> by_cases h'' : 0 < w
+  <;> simp [h, h', h'']
+  <;> omega
+
+@[simp]
+theorem not_sshiftRight_not {x : BitVec w} {n : Nat} :
+    ~~~((~~~x).sshiftRight n) = x.sshiftRight n := by
+  simp [not_sshiftRight]
+
 /-! ### sshiftRight reductions from BitVec to Nat -/
 
 @[simp]
@@ -1288,6 +1351,69 @@ theorem umod_eq {x y : BitVec n} :
 theorem toNat_umod {x y : BitVec n} :
     (x.umod y).toNat = x.toNat % y.toNat := rfl
 
+/-! ### sdiv -/
+
+/-- Equation theorem for `sdiv` in terms of `udiv`. -/
+theorem sdiv_eq (x y : BitVec w) : x.sdiv y =
+  match x.msb, y.msb with
+  | false, false => udiv x y
+  | false, true  =>  - (x.udiv (- y))
+  | true,  false => - ((- x).udiv y)
+  | true,  true  => (- x).udiv (- y) := by
+  rw [BitVec.sdiv]
+  rcases x.msb <;> rcases y.msb <;> simp
+
+@[bv_toNat]
+theorem toNat_sdiv {x y : BitVec w} : (x.sdiv y).toNat =
+    match x.msb, y.msb with
+    | false, false => (udiv x y).toNat
+    | false, true  =>  (- (x.udiv (- y))).toNat
+    | true,  false => (- ((- x).udiv y)).toNat
+    | true,  true  => ((- x).udiv (- y)).toNat := by
+  simp only [sdiv_eq, toNat_udiv]
+  by_cases h : x.msb <;> by_cases h' : y.msb <;> simp [h, h']
+
+theorem sdiv_eq_and (x y : BitVec 1) : x.sdiv y = x &&& y := by
+  have hx : x = 0#1 ∨ x = 1#1 := by bv_omega
+  have hy : y = 0#1 ∨ y = 1#1 := by bv_omega
+  rcases hx with rfl | rfl <;>
+    rcases hy with rfl | rfl <;>
+      rfl
+
+/-! ### smod -/
+
+/-- Equation theorem for `smod` in terms of `umod`. -/
+theorem smod_eq (x y : BitVec w) : x.smod y =
+  match x.msb, y.msb with
+  | false, false => x.umod y
+  | false, true =>
+    let u := x.umod (- y)
+    (if u = 0#w then u else u + y)
+  | true, false =>
+    let u := umod (- x) y
+    (if u = 0#w then u else y - u)
+  | true, true => - ((- x).umod (- y)) := by
+  rw [BitVec.smod]
+  rcases x.msb <;> rcases y.msb <;> simp
+
+@[bv_toNat]
+theorem toNat_smod {x y : BitVec w} : (x.smod y).toNat =
+    match x.msb, y.msb with
+    | false, false => (x.umod y).toNat
+    | false, true =>
+      let u := x.umod (- y)
+      (if u = 0#w then u.toNat else (u + y).toNat)
+    | true, false =>
+      let u := (-x).umod y
+      (if u = 0#w then u.toNat else (y - u).toNat)
+    | true, true => (- ((- x).umod (- y))).toNat := by
+  simp only [smod_eq, toNat_umod]
+  by_cases h : x.msb <;> by_cases h' : y.msb
+  <;> by_cases h'' : (-x).umod y = 0#w <;> by_cases h''' : x.umod (-y) = 0#w
+  <;> simp only [h, h', h'', h''']
+  <;> simp only [umod, toNat_eq, toNat_ofNatLt, toNat_ofNat, Nat.zero_mod] at h'' h'''
+  <;> simp [h'', h''']
+
 /-! ### signExtend -/
 
 /-- Equation theorem for `Int.sub` when both arguments are `Int.ofNat` -/
@@ -1372,18 +1498,18 @@ theorem getLsbD_append {x : BitVec n} {y : BitVec m} :
   simp only [append_def, getLsbD_or, getLsbD_shiftLeftZeroExtend, getLsbD_setWidth']
   by_cases h : i < m
   · simp [h]
-  · simp [h]; simp_all
+  · simp_all [h]
 
 theorem getElem_append {x : BitVec n} {y : BitVec m} (h : i < n + m) :
     (x ++ y)[i] = bif i < m then getLsbD y i else getLsbD x (i - m) := by
   simp only [append_def, getElem_or, getElem_shiftLeftZeroExtend, getElem_setWidth']
   by_cases h' : i < m
   · simp [h']
-  · simp [h']; simp_all
+  · simp_all [h']
 
 @[simp] theorem getMsbD_append {x : BitVec n} {y : BitVec m} :
     getMsbD (x ++ y) i = bif n ≤ i then getMsbD y (i - n) else getMsbD x i := by
-  simp [append_def]
+  simp only [append_def]
   by_cases h : n ≤ i
   · simp [h]
   · simp [h]
@@ -1391,7 +1517,7 @@ theorem getElem_append {x : BitVec n} {y : BitVec m} (h : i < n + m) :
 theorem msb_append {x : BitVec w} {y : BitVec v} :
     (x ++ y).msb = bif (w == 0) then (y.msb) else (x.msb) := by
   rw [← append_eq, append]
-  simp [msb_setWidth']
+  simp only [msb_or, msb_shiftLeftZeroExtend, msb_setWidth']
   by_cases h : w = 0
   · subst h
     simp [BitVec.msb, getMsbD]
@@ -1410,6 +1536,10 @@ theorem msb_append {x : BitVec w} {y : BitVec v} :
   rw [getLsbD_append]
   simpa using lt_of_getLsbD
 
+@[simp] theorem zero_append_zero : 0#v ++ 0#w = 0#(v + w) := by
+  ext
+  simp only [getLsbD_append, getLsbD_zero, Bool.cond_self]
+
 @[simp] theorem cast_append_right (h : w + v = w + v') (x : BitVec w) (y : BitVec v) :
     cast h (x ++ y) = x ++ cast (by omega) y := by
   ext
@@ -1484,6 +1614,21 @@ theorem shiftRight_add {w : Nat} (x : BitVec w) (n m : Nat) :
   ext i
   simp [Nat.add_assoc n m i]
 
+theorem shiftLeft_ushiftRight {x : BitVec w} {n : Nat}:
+    x >>> n <<< n = x &&& BitVec.allOnes w <<< n := by
+  induction n generalizing x
+  case zero =>
+    ext; simp
+  case succ n ih =>
+    rw [BitVec.shiftLeft_add, Nat.add_comm, BitVec.shiftRight_add, ih,
+       Nat.add_comm, BitVec.shiftLeft_add, BitVec.shiftLeft_and_distrib]
+    ext i
+    by_cases hw : w = 0
+    · simp [hw]
+    · by_cases hi₂ : i.val = 0
+      · simp [hi₂]
+      · simp [Nat.lt_one_iff, hi₂, show 1 + (i.val - 1) = i by omega]
+
 @[deprecated shiftRight_add (since := "2024-06-02")]
 theorem shiftRight_shiftRight {w : Nat} (x : BitVec w) (n m : Nat) :
     (x >>> n) >>> m = x >>> (n + m) := by
@@ -1493,13 +1638,13 @@ theorem shiftRight_shiftRight {w : Nat} (x : BitVec w) (n m : Nat) :
 
 theorem getLsbD_rev (x : BitVec w) (i : Fin w) :
     x.getLsbD i.rev = x.getMsbD i := by
-  simp [getLsbD, getMsbD]
+  simp only [getLsbD, Fin.val_rev, getMsbD, Fin.is_lt, decide_True, Bool.true_and]
   congr 1
   omega
 
 theorem getElem_rev {x : BitVec w} {i : Fin w}:
     x[i.rev] = x.getMsbD i := by
-  simp [getMsbD]
+  simp only [Fin.getElem_fin, Fin.val_rev, getMsbD, Fin.is_lt, decide_True, Bool.true_and]
   congr 1
   omega
 
@@ -1524,13 +1669,13 @@ theorem toNat_cons' {x : BitVec w} :
 
 theorem getLsbD_cons (b : Bool) {n} (x : BitVec n) (i : Nat) :
     getLsbD (cons b x) i = if i = n then b else getLsbD x i := by
-  simp only [getLsbD, toNat_cons, Nat.testBit_or]
+  simp only [getLsbD, toNat_cons, Nat.testBit_or, Nat.testBit_shiftLeft, ge_iff_le]
-  rw [Nat.testBit_shiftLeft]
   rcases Nat.lt_trichotomy i n with i_lt_n | i_eq_n | n_lt_i
   · have p1 : ¬(n ≤ i) := by omega
     have p2 : i ≠ n := by omega
     simp [p1, p2]
-  · simp [i_eq_n, testBit_toNat]
+  · simp only [i_eq_n, ge_iff_le, Nat.le_refl, decide_True, Nat.sub_self, Nat.testBit_zero,
+    Bool.true_and, testBit_toNat, getLsbD_ge, Bool.or_false, ↓reduceIte]
     cases b <;> trivial
   · have p1 : i ≠ n := by omega
     have p2 : i - n ≠ 0 := by omega
@@ -1544,7 +1689,8 @@ theorem getElem_cons {b : Bool} {n} {x : BitVec n} {i : Nat} (h : i < n + 1) :
   · have p1 : ¬(n ≤ i) := by omega
     have p2 : i ≠ n := by omega
     simp [p1, p2]
-  · simp [i_eq_n, testBit_toNat]
+  · simp only [i_eq_n, ge_iff_le, Nat.le_refl, decide_True, Nat.sub_self, Nat.testBit_zero,
+    Bool.true_and, testBit_toNat, getLsbD_ge, Bool.or_false, ↓reduceIte]
     cases b <;> trivial
   · have p1 : i ≠ n := by omega
     have p2 : i - n ≠ 0 := by omega
@@ -1655,6 +1801,55 @@ theorem getElem_concat (x : BitVec w) (b : Bool) (i : Nat) (h : i < w + 1) :
     (concat x a) ^^^ (concat y b) = concat (x ^^^ y) (a ^^ b) := by
   ext i; cases i using Fin.succRecOn <;> simp
 
+/-! ### shiftConcat -/
+
+theorem getLsbD_shiftConcat (x : BitVec w) (b : Bool) (i : Nat) :
+    (shiftConcat x b).getLsbD i
+    = (decide (i < w) && (if (i = 0) then b else x.getLsbD (i - 1))) := by
+  simp only [shiftConcat, getLsbD_setWidth, getLsbD_concat]
+
+theorem getLsbD_shiftConcat_eq_decide (x : BitVec w) (b : Bool) (i : Nat) :
+    (shiftConcat x b).getLsbD i
+    = (decide (i < w) && ((decide (i = 0) && b) || (decide (0 < i) && x.getLsbD (i - 1)))) := by
+  simp only [getLsbD_shiftConcat]
+  split <;> simp [*, show ((0 < i) ↔ ¬(i = 0)) by omega]
+
+theorem shiftRight_sub_one_eq_shiftConcat (n : BitVec w) (hwn : 0 < wn) :
+    n >>> (wn - 1) = (n >>> wn).shiftConcat (n.getLsbD (wn - 1)) := by
+  ext i
+  simp only [getLsbD_ushiftRight, getLsbD_shiftConcat, Fin.is_lt, decide_True, Bool.true_and]
+  split
+  · simp [*]
+  · congr 1; omega
+
+@[simp, bv_toNat]
+theorem toNat_shiftConcat {x : BitVec w} {b : Bool} :
+    (x.shiftConcat b).toNat
+    = (x.toNat <<< 1 + b.toNat) % 2 ^ w  := by
+  simp [shiftConcat, Nat.shiftLeft_eq]
+
+/-- `x.shiftConcat b` does not overflow if `x < 2^k` for `k < w`, and so
+`x.shiftConcat b |>.toNat = x.toNat * 2 + b.toNat`. -/
+theorem toNat_shiftConcat_eq_of_lt {x : BitVec w} {b : Bool} {k : Nat}
+    (hk : k < w) (hx : x.toNat < 2 ^ k) :
+    (x.shiftConcat b).toNat = x.toNat * 2 + b.toNat := by
+  simp only [toNat_shiftConcat, Nat.shiftLeft_eq, Nat.pow_one]
+  have : 2 ^ k < 2 ^ w := Nat.pow_lt_pow_of_lt (by omega) (by omega)
+  have : 2 ^ k * 2 ≤ 2 ^ w := (Nat.pow_lt_pow_iff_pow_mul_le_pow (by omega)).mp this
+  rw [Nat.mod_eq_of_lt (by cases b <;> simp [bv_toNat] <;> omega)]
+
+theorem toNat_shiftConcat_lt_of_lt {x : BitVec w} {b : Bool} {k : Nat}
+    (hk : k < w) (hx : x.toNat < 2 ^ k) :
+    (x.shiftConcat b).toNat < 2 ^ (k + 1) := by
+  rw [toNat_shiftConcat_eq_of_lt hk hx]
+  have : 2 ^ (k + 1) ≤ 2 ^ w := Nat.pow_le_pow_of_le_right (by decide) (by assumption)
+  have := Bool.toNat_lt b
+  omega
+
+@[simp] theorem zero_concat_false : concat 0#w false = 0#(w + 1) := by
+  ext
+  simp [getLsbD_concat]
+
 /-! ### add -/
 
 theorem add_def {n} (x y : BitVec n) : x + y = .ofNat n (x.toNat + y.toNat) := rfl
@@ -1705,6 +1900,15 @@ theorem ofInt_add {n} (x y : Int) : BitVec.ofInt n (x + y) =
   apply eq_of_toInt_eq
   simp
 
+@[simp]
+theorem shiftLeft_add_distrib {x y : BitVec w} {n : Nat} :
+    (x + y) <<< n = x <<< n + y <<< n := by
+  induction n
+  case zero =>
+    simp
+  case succ n ih =>
+    simp [ih, toNat_eq, Nat.shiftLeft_eq, ← Nat.add_mul]
+
 /-! ### sub/neg -/
 
 theorem sub_def {n} (x y : BitVec n) : x - y = .ofNat n ((2^n - y.toNat) + x.toNat) := by rfl
@@ -1744,13 +1948,28 @@ 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 toInt_neg {x : BitVec w} :
+    (-x).toInt = (-x.toInt).bmod (2 ^ w) := by
+  simp only [toInt_eq_toNat_bmod, toNat_neg, Int.ofNat_emod, Int.emod_bmod_congr]
+  rw [← Int.subNatNat_of_le (by omega), Int.subNatNat_eq_coe, Int.sub_eq_add_neg, Int.add_comm,
+    Int.bmod_add_cancel]
+  by_cases h : x.toNat < ((2 ^ w) + 1) / 2
+  · rw [Int.bmod_pos (x := x.toNat)]
+    all_goals simp only [toNat_mod_cancel']
+    norm_cast
+  · rw [Int.bmod_neg (x := x.toNat)]
+    · simp only [toNat_mod_cancel']
+      rw_mod_cast [Int.neg_sub, Int.sub_eq_add_neg, Int.add_comm, Int.bmod_add_cancel]
+    · norm_cast
+      simp_all
+
 @[simp] theorem toFin_neg (x : BitVec n) :
     (-x).toFin = Fin.ofNat' (2^n) (2^n - x.toNat) :=
   rfl
 
 theorem sub_toAdd {n} (x y : BitVec n) : x - y = x + - y := by
   apply eq_of_toNat_eq
-  simp
+  simp only [toNat_sub, toNat_add, toNat_neg, Nat.add_mod_mod]
   rw [Nat.add_comm]
 
 @[simp] theorem neg_zero (n:Nat) : -BitVec.ofNat n 0 = BitVec.ofNat n 0 := by apply eq_of_toNat_eq ; simp
@@ -1799,6 +2018,17 @@ theorem neg_ne_iff_ne_neg {x y : BitVec w} : -x ≠ y ↔ x ≠ -y := by
     subst h'
     simp at h
 
+/-! ### abs -/
+
+@[simp, bv_toNat]
+theorem toNat_abs {x : BitVec w} : x.abs.toNat = if x.msb then 2^w - x.toNat else x.toNat := by
+  simp only [BitVec.abs, neg_eq]
+  by_cases h : x.msb = true
+  · simp only [h, ↓reduceIte, toNat_neg]
+    have : 2 * x.toNat ≥ 2 ^ w := BitVec.msb_eq_true_iff_two_mul_ge.mp h
+    rw [Nat.mod_eq_of_lt (by omega)]
+  · simp [h]
+
 /-! ### mul -/
 
 theorem mul_def {n} {x y : BitVec n} : x * y = (ofFin <| x.toFin * y.toFin) := by rfl
@@ -1921,6 +2151,10 @@ protected theorem umod_lt (x : BitVec n) {y : BitVec n} : 0 < y → x.umod y < y
   simp only [ofNat_eq_ofNat, lt_def, toNat_ofNat, Nat.zero_mod, umod, toNat_ofNatLt]
   apply Nat.mod_lt
 
+theorem not_lt_iff_le {x y : BitVec w} : (¬ x < y) ↔ y ≤ x := by
+  constructor <;>
+    (intro h; simp only [lt_def, Nat.not_lt, le_def] at h ⊢; omega)
+
 /-! ### ofBoolList -/
 
 @[simp] theorem getMsbD_ofBoolListBE : (ofBoolListBE bs).getMsbD i = bs.getD i false := by
@@ -2166,6 +2400,27 @@ theorem twoPow_zero {w : Nat} : twoPow w 0 = 1#w := by
 theorem getLsbD_one {w i : Nat} : (1#w).getLsbD i = (decide (0 < w) && decide (0 = i)) := by
   rw [← twoPow_zero, getLsbD_twoPow]
 
+theorem shiftLeft_eq_mul_twoPow (x : BitVec w) (n : Nat) :
+    x <<< n = x * (BitVec.twoPow w n) := by
+  ext i
+  simp [getLsbD_shiftLeft, Fin.is_lt, decide_True, Bool.true_and, mul_twoPow_eq_shiftLeft]
+
+/- ### cons -/
+
+@[simp] theorem true_cons_zero : cons true 0#w = twoPow (w + 1) w := by
+  ext
+  simp [getLsbD_cons]
+  omega
+
+@[simp] theorem false_cons_zero : cons false 0#w = 0#(w + 1) := by
+  ext
+  simp [getLsbD_cons]
+
+@[simp] theorem zero_concat_true : concat 0#w true = 1#(w + 1) := by
+  ext
+  simp [getLsbD_concat]
+  omega
+
 /- ### setWidth, setWidth, and bitwise operations -/
 
 /--
@@ -2258,10 +2513,28 @@ theorem getLsbD_intMin (w : Nat) : (intMin w).getLsbD i = decide (i + 1 = w) :=
   simp only [intMin, getLsbD_twoPow, boolToPropSimps]
   omega
 
+/--
+The RHS is zero in case `w = 0` which is modeled by wrapping the expression in `... % 2 ^ w`.
+-/
 @[simp, bv_toNat]
 theorem toNat_intMin : (intMin w).toNat = 2 ^ (w - 1) % 2 ^ w := by
   simp [intMin]
 
+/--
+The RHS is zero in case `w = 0` which is modeled by wrapping the expression in `... % 2 ^ w`.
+-/
+@[simp]
+theorem toInt_intMin {w : Nat} :
+    (intMin w).toInt = -((2 ^ (w - 1) % 2 ^ w) : Nat) := by
+  by_cases h : w = 0
+  · subst h
+    simp [BitVec.toInt]
+  · have w_pos : 0 < w := by omega
+    simp only [BitVec.toInt, toNat_intMin, w_pos, Nat.two_pow_pred_mod_two_pow,
+      Int.two_pow_pred_sub_two_pow, ite_eq_right_iff]
+    rw [Nat.mul_comm]
+    simp [w_pos]
+
 @[simp]
 theorem neg_intMin {w : Nat} : -intMin w = intMin w := by
   by_cases h : 0 < w
@@ -2269,6 +2542,22 @@ theorem neg_intMin {w : Nat} : -intMin w = intMin w := by
   · simp only [Nat.not_lt, Nat.le_zero_eq] at h
     simp [bv_toNat, h]
 
+theorem toInt_neg_of_ne_intMin {x : BitVec w} (rs : x ≠ intMin w) :
+    (-x).toInt = -(x.toInt) := by
+  simp only [ne_eq, toNat_eq, toNat_intMin] at rs
+  by_cases x_zero : x = 0
+  · subst x_zero
+    simp [BitVec.toInt]
+    omega
+  by_cases w_0 : w = 0
+  · subst w_0
+    simp [BitVec.eq_nil x]
+  have : 0 < w := by omega
+  rw [Nat.two_pow_pred_mod_two_pow (by omega)] at rs
+  simp only [BitVec.toInt, BitVec.toNat_neg, BitVec.sub_toNat_mod_cancel x_zero]
+  have := @Nat.two_pow_pred_mul_two w (by omega)
+  split <;> split <;> omega
+
 /-! ### intMax -/
 
 /-- The bitvector of width `w` that has the largest value when interpreted as an integer. -/

src/Init/Data/Bool.lean

@@ -368,13 +368,14 @@ theorem and_or_inj_left_iff :
 /-- convert a `Bool` to a `Nat`, `false -> 0`, `true -> 1` -/
 def toNat (b : Bool) : Nat := cond b 1 0
 
-@[simp] theorem toNat_false : false.toNat = 0 := rfl
+@[simp, bv_toNat] theorem toNat_false : false.toNat = 0 := rfl
 
-@[simp] theorem toNat_true : true.toNat = 1 := rfl
+@[simp, bv_toNat] theorem toNat_true : true.toNat = 1 := rfl
 
 theorem toNat_le (c : Bool) : c.toNat ≤ 1 := by
   cases c <;> trivial
 
+@[bv_toNat]
 theorem toNat_lt (b : Bool) : b.toNat < 2 :=
   Nat.lt_succ_of_le (toNat_le _)
 

src/Init/Data/Int/Pow.lean

@@ -5,6 +5,7 @@ Authors: Jeremy Avigad, Deniz Aydin, Floris van Doorn, Mario Carneiro
 -/
 prelude
 import Init.Data.Int.Lemmas
+import Init.Data.Nat.Lemmas
 
 namespace Int
 
@@ -35,10 +36,24 @@ theorem pow_le_pow_of_le_right {n : Nat} (hx : n > 0) {i : Nat} : ∀ {j}, i ≤
 theorem pos_pow_of_pos {n : Nat} (m : Nat) (h : 0 < n) : 0 < n^m :=
   pow_le_pow_of_le_right h (Nat.zero_le _)
 
+@[norm_cast]
 theorem natCast_pow (b n : Nat) : ((b^n : Nat) : Int) = (b : Int) ^ n := by
   match n with
   | 0 => rfl
   | n + 1 =>
     simp only [Nat.pow_succ, Int.pow_succ, natCast_mul, natCast_pow _ n]
 
+@[simp]
+protected theorem two_pow_pred_sub_two_pow {w : Nat} (h : 0 < w) :
+    ((2 ^ (w - 1) : Nat) - (2 ^ w : Nat) : Int) = - ((2 ^ (w - 1) : Nat) : Int) := by
+  rw [← Nat.two_pow_pred_add_two_pow_pred h]
+  omega
+
+@[simp]
+protected theorem two_pow_pred_sub_two_pow' {w : Nat} (h : 0 < w) :
+    (2 : Int) ^ (w - 1) - (2 : Int) ^ w = - (2 : Int) ^ (w - 1) := by
+  norm_cast
+  rw [← Nat.two_pow_pred_add_two_pow_pred h]
+  simp [h]
+
 end Int

src/Init/Data/List/Lemmas.lean

@@ -1654,6 +1654,11 @@ theorem filterMap_eq_cons_iff {l} {b} {bs} :
 
 /-! ### append -/
 
+@[simp] theorem nil_append_fun : (([] : List α) ++ ·) = id := rfl
+
+@[simp] theorem cons_append_fun (a : α) (as : List α) :
+    (fun bs => ((a :: as) ++ bs)) = fun bs => a :: (as ++ bs) := rfl
+
 theorem getElem_append {l₁ l₂ : List α} (n : Nat) (h) :
     (l₁ ++ l₂)[n] = if h' : n < l₁.length then l₁[n] else l₂[n - l₁.length]'(by simp at h h'; exact Nat.sub_lt_left_of_lt_add h' h) := by
   split <;> rename_i h'
@@ -2392,6 +2397,12 @@ theorem map_eq_replicate_iff {l : List α} {f : α → β} {b : β} :
 theorem map_const' (l : List α) (b : β) : map (fun _ => b) l = replicate l.length b :=
   map_const l b
 
+@[simp] theorem set_replicate_self : (replicate n a).set i a = replicate n a := by
+  apply ext_getElem
+  · simp
+  · intro i h₁ h₂
+    simp [getElem_set]
+
 @[simp] theorem append_replicate_replicate : replicate n a ++ replicate m a = replicate (n + m) a := by
   rw [eq_replicate_iff]
   constructor

src/Init/Data/List/Monadic.lean

@@ -51,6 +51,27 @@ theorem mapM'_eq_mapM [Monad m] [LawfulMonad m] (f : α → m β) (l : List α)
 @[simp] theorem mapM_append [Monad m] [LawfulMonad m] (f : α → m β) {l₁ l₂ : List α} :
     (l₁ ++ l₂).mapM f = (return (← l₁.mapM f) ++ (← l₂.mapM f)) := by induction l₁ <;> simp [*]
 
+/-- Auxiliary lemma for `mapM_eq_reverse_foldlM_cons`. -/
+theorem foldlM_cons_eq_append [Monad m] [LawfulMonad m] (f : α → m β) (as : List α) (b : β) (bs : List β) :
+    (as.foldlM (init := b :: bs) fun acc a => return ((← f a) :: acc)) =
+      (· ++ b :: bs) <$> as.foldlM (init := []) fun acc a => return ((← f a) :: acc) := by
+  induction as generalizing b bs with
+  | nil => simp
+  | cons a as ih =>
+    simp only [bind_pure_comp] at ih
+    simp [ih, _root_.map_bind, Functor.map_map, Function.comp_def]
+
+theorem mapM_eq_reverse_foldlM_cons [Monad m] [LawfulMonad m] (f : α → m β) (l : List α) :
+    mapM f l = reverse <$> (l.foldlM (fun acc a => return ((← f a) :: acc)) []) := by
+  rw [← mapM'_eq_mapM]
+  induction l with
+  | nil => simp
+  | cons a as ih =>
+    simp only [mapM'_cons, ih, bind_map_left, foldlM_cons, LawfulMonad.bind_assoc, pure_bind,
+      foldlM_cons_eq_append, _root_.map_bind, Functor.map_map, Function.comp_def, reverse_append,
+      reverse_cons, reverse_nil, nil_append, singleton_append]
+    simp [bind_pure_comp]
+
 /-! ### forM -/
 
 -- We use `List.forM` as the simp normal form, rather that `ForM.forM`.
@@ -66,4 +87,16 @@ theorem mapM'_eq_mapM [Monad m] [LawfulMonad m] (f : α → m β) (l : List α)
     (l₁ ++ l₂).forM f = (do l₁.forM f; l₂.forM f) := by
   induction l₁ <;> simp [*]
 
+/-! ### allM -/
+
+theorem allM_eq_not_anyM_not [Monad m] [LawfulMonad m] (p : α → m Bool) (as : List α) :
+    allM p as = (! ·) <$> anyM ((! ·) <$> p ·) as := by
+  induction as with
+  | nil => simp
+  | cons a as ih =>
+    simp only [allM, anyM, bind_map_left, _root_.map_bind]
+    congr
+    funext b
+    split <;> simp_all
+
 end List

src/Init/Data/List/Sublist.lean

@@ -725,12 +725,21 @@ theorem infix_iff_suffix_prefix {l₁ l₂ : List α} : l₁ <:+: l₂ ↔ ∃ t
 theorem IsInfix.eq_of_length (h : l₁ <:+: l₂) : l₁.length = l₂.length → l₁ = l₂ :=
   h.sublist.eq_of_length
 
+theorem IsInfix.eq_of_length_le (h : l₁ <:+: l₂) : l₂.length ≤ l₁.length → l₁ = l₂ :=
+  h.sublist.eq_of_length_le
+
 theorem IsPrefix.eq_of_length (h : l₁ <+: l₂) : l₁.length = l₂.length → l₁ = l₂ :=
   h.sublist.eq_of_length
 
+theorem IsPrefix.eq_of_length_le (h : l₁ <+: l₂) : l₂.length ≤ l₁.length → l₁ = l₂ :=
+  h.sublist.eq_of_length_le
+
 theorem IsSuffix.eq_of_length (h : l₁ <:+ l₂) : l₁.length = l₂.length → l₁ = l₂ :=
   h.sublist.eq_of_length
 
+theorem IsSuffix.eq_of_length_le (h : l₁ <:+ l₂) : l₂.length ≤ l₁.length → l₁ = l₂ :=
+  h.sublist.eq_of_length_le
+
 theorem prefix_of_prefix_length_le :
     ∀ {l₁ l₂ l₃ : List α}, l₁ <+: l₃ → l₂ <+: l₃ → length l₁ ≤ length l₂ → l₁ <+: l₂
   | [], l₂, _, _, _, _ => nil_prefix
@@ -829,6 +838,24 @@ theorem isPrefix_iff : l₁ <+: l₂ ↔ ∀ i (h : i < l₁.length), l₂[i]? =
       rw (config := {occs := .pos [2]}) [← Nat.and_forall_add_one]
       simp [Nat.succ_lt_succ_iff, eq_comm]
 
+theorem isPrefix_iff_getElem {l₁ l₂ : List α} :
+    l₁ <+: l₂ ↔ ∃ (h : l₁.length ≤ l₂.length), ∀ x (hx : x < l₁.length),
+      l₁[x] = l₂[x]'(Nat.lt_of_lt_of_le hx h) where
+  mp h := ⟨h.length_le, fun _ _ ↦ h.getElem _⟩
+  mpr h := by
+    obtain ⟨hl, h⟩ := h
+    induction l₂ generalizing l₁ with
+    | nil =>
+      simpa using hl
+    | cons _ _ tail_ih =>
+      cases l₁ with
+      | nil =>
+        exact nil_prefix
+      | cons _ _ =>
+        simp only [length_cons, Nat.add_le_add_iff_right, Fin.getElem_fin] at hl h
+        simp only [cons_prefix_cons]
+        exact ⟨h 0 (zero_lt_succ _), tail_ih hl fun a ha ↦ h a.succ (succ_lt_succ ha)⟩
+
 -- See `Init.Data.List.Nat.Sublist` for `isSuffix_iff` and `ifInfix_iff`.
 
 theorem isPrefix_filterMap_iff {β} {f : α → Option β} {l₁ : List α} {l₂ : List β} :

src/Init/Data/Nat/Basic.lean

@@ -634,6 +634,8 @@ theorem lt_succ_of_lt (h : a < b) : a < succ b := le_succ_of_le h
 
 theorem lt_add_one_of_lt (h : a < b) : a < b + 1 := le_succ_of_le h
 
+@[simp] theorem lt_one_iff : n < 1 ↔ n = 0 := Nat.lt_succ_iff.trans <| by rw [le_zero_eq]
+
 theorem succ_pred_eq_of_ne_zero : ∀ {n}, n ≠ 0 → succ (pred n) = n
   | _+1, _ => rfl
 

src/Init/Data/Nat/Lemmas.lean

@@ -605,6 +605,9 @@ theorem add_mod (a b n : Nat) : (a + b) % n = ((a % n) + (b % n)) % n := by
     | zero => simp_all
     | succ k => omega
 
+@[simp] theorem mod_mul_mod {a b c : Nat} : (a % c * b) % c = a * b % c := by
+  rw [mul_mod, mod_mod, ← mul_mod]
+
 /-! ### pow -/
 
 theorem pow_succ' {m n : Nat} : m ^ n.succ = m * m ^ n := by
@@ -767,6 +770,16 @@ protected theorem two_pow_pred_mod_two_pow (h : 0 < w) :
   rw [mod_eq_of_lt]
   apply Nat.pow_pred_lt_pow (by omega) h
 
+protected theorem pow_lt_pow_iff_pow_mul_le_pow {a n m : Nat} (h : 1 < a) :
+    a ^ n < a ^ m ↔ a ^ n * a ≤ a ^ m := by
+  rw [←Nat.pow_add_one, Nat.pow_le_pow_iff_right (by omega), Nat.pow_lt_pow_iff_right (by omega)]
+  omega
+
+@[simp]
+theorem two_pow_pred_mul_two (h : 0 < w) :
+    2 ^ (w - 1) * 2 = 2 ^ w := by
+  simp [← Nat.pow_succ, Nat.sub_add_cancel h]
+
 /-! ### log2 -/
 
 @[simp]

src/Init/Data/NeZero.lean

@@ -35,4 +35,4 @@ theorem neZero_iff {n : R} : NeZero n ↔ n ≠ 0 :=
   ⟨fun h ↦ h.out, NeZero.mk⟩
 
 @[simp] theorem neZero_zero_iff_false {α : Type _} [Zero α] : NeZero (0 : α) ↔ False :=
-  ⟨fun h ↦ h.ne rfl, fun h ↦ h.elim⟩
+  ⟨fun _ ↦ NeZero.ne (0 : α) rfl, fun h ↦ h.elim⟩

src/Init/Tactics.lean

@@ -149,26 +149,27 @@ syntax (name := assumption) "assumption" : tactic
 
 /--
 `contradiction` closes the main goal if its hypotheses are "trivially contradictory".
+
 - Inductive type/family with no applicable constructors
-```lean
+  ```lean
-example (h : False) : p := by contradiction
+  example (h : False) : p := by contradiction
-```
+  ```
 - Injectivity of constructors
-```lean
+  ```lean
-example (h : none = some true) : p := by contradiction  --
+  example (h : none = some true) : p := by contradiction  --
-```
+  ```
 - Decidable false proposition
-```lean
+  ```lean
-example (h : 2 + 2 = 3) : p := by contradiction
+  example (h : 2 + 2 = 3) : p := by contradiction
-```
+  ```
 - Contradictory hypotheses
-```lean
+  ```lean
-example (h : p) (h' : ¬ p) : q := by contradiction
+  example (h : p) (h' : ¬ p) : q := by contradiction
-```
+  ```
 - Other simple contradictions such as
-```lean
+  ```lean
-example (x : Nat) (h : x ≠ x) : p := by contradiction
+  example (x : Nat) (h : x ≠ x) : p := by contradiction
-```
+  ```
 -/
 syntax (name := contradiction) "contradiction" : tactic
 
@@ -363,31 +364,24 @@ syntax (name := fail) "fail" (ppSpace str)? : tactic
 syntax (name := eqRefl) "eq_refl" : tactic
 
 /--
-`rfl` tries to close the current goal using reflexivity.
+This tactic applies to a goal whose target has the form `x ~ x`,
-This is supposed to be an extensible tactic and users can add their own support
+where `~` is equality, heterogeneous equality or any relation that
-for new reflexive relations.
+has a reflexivity lemma tagged with the attribute @[refl].
-
-Remark: `rfl` is an extensible tactic. We later add `macro_rules` to try different
-reflexivity theorems (e.g., `Iff.rfl`).
 -/
-macro "rfl" : tactic => `(tactic| case' _ => fail "The rfl tactic failed. Possible reasons:
+syntax "rfl" : tactic
-- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
-- The arguments of the relation are not equal.
-Try using the reflexivity lemma for your relation explicitly, e.g. `exact Eq.refl _` or
-`exact HEq.rfl` etc.")
-
-macro_rules | `(tactic| rfl) => `(tactic| eq_refl)
-macro_rules | `(tactic| rfl) => `(tactic| exact HEq.rfl)
 
 /--
-This tactic applies to a goal whose target has the form `x ~ x`,
+The same as `rfl`, but without trying `eq_refl` at the end.
-where `~` is a reflexive relation other than `=`,
-that is, a relation which has a reflexive lemma tagged with the attribute @[refl].
 -/
 syntax (name := applyRfl) "apply_rfl" : tactic
 
+-- We try `apply_rfl` first, beause it produces a nice error message
 macro_rules | `(tactic| rfl) => `(tactic| apply_rfl)
 
+-- But, mostly for backward compatibility, we try `eq_refl` too (reduces more aggressively)
+macro_rules | `(tactic| rfl) => `(tactic| eq_refl)
+-- Als for backward compatibility, because `exact` can trigger the implicit lambda feature (see #5366)
+macro_rules | `(tactic| rfl) => `(tactic| exact HEq.rfl)
 /--
 `rfl'` is similar to `rfl`, but disables smart unfolding and unfolds all kinds of definitions,
 theorems included (relevant for declarations defined by well-founded recursion).
@@ -794,7 +788,7 @@ syntax inductionAlt  := ppDedent(ppLine) inductionAltLHS+ " => " (hole <|> synth
 After `with`, there is an optional tactic that runs on all branches, and
 then a list of alternatives.
 -/
-syntax inductionAlts := " with" (ppSpace tactic)? withPosition((colGe inductionAlt)+)
+syntax inductionAlts := " with" (ppSpace colGt tactic)? withPosition((colGe inductionAlt)+)
 
 /--
 Assuming `x` is a variable in the local context with an inductive type,

src/Lean/Elab/App.lean

@@ -411,21 +411,23 @@ private def finalize : M Expr := do
   synthesizeAppInstMVars
   return e
 
-/-- Return `true` if there is a named argument that depends on the next argument. -/
+/--
-private def anyNamedArgDependsOnCurrent : M Bool := do
+Returns a named argument that depends on the next argument, otherwise `none`.
+-/
+private def findNamedArgDependsOnCurrent? : M (Option NamedArg) := do
   let s ← get
   if s.namedArgs.isEmpty then
-    return false
+    return none
   else
     forallTelescopeReducing s.fType fun xs _ => do
       let curr := xs[0]!
       for i in [1:xs.size] do
         let xDecl ← xs[i]!.fvarId!.getDecl
-        if s.namedArgs.any fun arg => arg.name == xDecl.userName then
+        if let some arg := s.namedArgs.find? fun arg => arg.name == xDecl.userName then
           /- Remark: a default value at `optParam` does not count as a dependency -/
           if (← exprDependsOn xDecl.type.cleanupAnnotations curr.fvarId!) then
-            return true
+            return arg
-      return false
+      return none
 
 
 /-- Return `true` if there are regular or named arguments to be processed. -/
@@ -433,11 +435,13 @@ private def hasArgsToProcess : M Bool := do
   let s ← get
   return !s.args.isEmpty || !s.namedArgs.isEmpty
 
-/-- Return `true` if the next argument at `args` is of the form `_` -/
+/--
-private def isNextArgHole : M Bool := do
+Returns the argument syntax if the next argument at `args` is of the form `_`.
+-/
+private def nextArgHole? : M (Option Syntax) := do
   match (← get).args with
-  | Arg.stx (Syntax.node _ ``Lean.Parser.Term.hole _) :: _ => pure true
+  | Arg.stx stx@(Syntax.node _ ``Lean.Parser.Term.hole _) :: _ => pure stx
-  | _ => pure false
+  | _ => pure none
 
 /--
   Return `true` if the next argument to be processed is the outparam of a local instance, and it the result type
@@ -512,8 +516,9 @@ where
 
 mutual
   /--
-    Create a fresh local variable with the current binder name and argument type, add it to `etaArgs` and `f`,
+  Create a fresh local variable with the current binder name and argument type, add it to `etaArgs` and `f`,
-    and then execute the main loop.-/
+  and then execute the main loop.
+  -/
   private partial def addEtaArg (argName : Name) : M Expr := do
     let n    ← getBindingName
     let type ← getArgExpectedType
@@ -522,6 +527,9 @@ mutual
       addNewArg argName x
       main
 
+  /--
+  Create a fresh metavariable for the implicit argument, add it to `f`, and thn execute the main loop.
+  -/
   private partial def addImplicitArg (argName : Name) : M Expr := do
     let argType ← getArgExpectedType
     let arg ← if (← isNextOutParamOfLocalInstanceAndResult) then
@@ -539,35 +547,47 @@ mutual
     main
 
   /--
-    Process a `fType` of the form `(x : A) → B x`.
+  Process a `fType` of the form `(x : A) → B x`.
-    This method assume `fType` is a function type -/
+  This method assume `fType` is a function type.
+  -/
   private partial def processExplicitArg (argName : Name) : M Expr := do
     match (← get).args with
     | arg::args =>
-      if (← anyNamedArgDependsOnCurrent) then
+      -- Note: currently the following test never succeeds in explicit mode since `@x.f` notation does not exist.
+      if let some true := NamedArg.suppressDeps <$> (← findNamedArgDependsOnCurrent?) then
         /-
-        We treat the explicit argument `argName` as implicit if we have named arguments that depend on it.
+        We treat the explicit argument `argName` as implicit
-        The idea is that this explicit argument can be inferred using the type of the named argument one.
+        if we have a named arguments that depends on it whose `suppressDeps` flag set to `true`.
-        Note that we also use this approach in the branch where there are no explicit arguments left.
+        The motivation for this is class projections (issue #1851).
-        This is important to make sure the system behaves in a uniform way.
+        In some cases, class projections can have explicit parameters. For example, in
-        Moreover, users rely on this behavior. For example, consider the example on issue #1851
         ```
         class Approx {α : Type} (a : α) (X : Type) : Type where
           val : X
-
-        variable {α β X Y : Type} {f' : α → β} {x' : α} [f : Approx f' (X → Y)] [x : Approx x' X]
-
-        #check f.val
-        #check f.val x.val
         ```
-        The type of `Approx.val` is `{α : Type} → (a : α) → {X : Type} → [self : Approx a X] → X`
+        the type of `Approx.val` is `{α : Type} → (a : α) → {X : Type} → [self : Approx a X] → X`.
-        Note that the argument `a` is explicit since there is no way to infer it from the expected
+        Note that the parameter `a` is explicit since there is no way to infer it from the expected
-        type or the type of other explicit arguments.
+        type or from the types of other explicit parameters.
-        Recall that `f.val` is sugar for `Approx.val (self := f)`. In both `#check` commands above
+        Being a parameter of the class, `a` is determined by the type of `self`.
-        the user assumed that `a` does not need to be provided since it can be inferred from the type
+
-        of `self`.
+        Consider
-        We used to that only in the branch where `(← get).args` was empty, but it created an asymmetry
+        ```
-        because `#check f.val` worked as expected, but one would have to write `#check f.val _ x.val`
+        variable {α β X Y : Type} {f' : α → β} {x' : α} [f : Approx f' (X → Y)]
+        ```
+        Recall that `f.val` is, to first approximation, sugar for `Approx.val (self := f)`.
+        Without further refinement, this would expand to `fun f'' : α → β => Approx.val f'' f`,
+        which is a type error, since `f''` must be defeq to `f'`.
+        Furthermore, with projection notation, users expect all structure parameters
+        to be uniformly implicit; after all, they are determined by `self`.
+        To handle this, the `(self := f)` named argument is annotated with the `suppressDeps` flag.
+        This causes the `a` parameter to become implicit, and `f.val` instead expands to `Approx.val f' f`.
+
+        This feature previously was enabled for *all* explicit arguments, which confused users
+        and was frequently reported as a bug (issue #1867).
+        Now it is only enabled for the `self` argument in structure projections.
+
+        We used to do this only when `(← get).args` was empty,
+        but it created an asymmetry because `f.val` worked as expected,
+        yet one would have to write `f.val _ x` when there are further arguments.
         -/
         return (← addImplicitArg argName)
       propagateExpectedType arg
@@ -584,7 +604,6 @@ mutual
         match evalSyntaxConstant env opts tacticDecl with
         | Except.error err       => throwError err
         | Except.ok tacticSyntax =>
-          -- TODO(Leo): does this work correctly for tactic sequences?
           let tacticBlock ← `(by $(⟨tacticSyntax⟩))
           /-
           We insert position information from the current ref into `stx` everywhere, simulating this being
@@ -596,24 +615,32 @@ mutual
           -/
           let info := (← getRef).getHeadInfo
           let tacticBlock := tacticBlock.raw.rewriteBottomUp (·.setInfo info)
-          let argNew := Arg.stx tacticBlock
+          let mvar ← mkTacticMVar argType.consumeTypeAnnotations tacticBlock (.autoParam argName)
+          -- Note(kmill): We are adding terminfo to simulate a previous implementation that elaborated `tacticBlock`.
+          -- We should look into removing this since terminfo for synthetic syntax is suspect,
+          -- but we noted it was necessary to preserve the behavior of the unused variable linter.
+          addTermInfo' tacticBlock mvar
+          let argNew := Arg.expr mvar
           propagateExpectedType argNew
           elabAndAddNewArg argName argNew
           main
       | false, _, some _ =>
         throwError "invalid autoParam, argument must be a constant"
       | _, _, _ =>
-        if !(← get).namedArgs.isEmpty then
+        if (← read).ellipsis then
-          if (← anyNamedArgDependsOnCurrent) then
+          addImplicitArg argName
-            addImplicitArg argName
+        else if !(← get).namedArgs.isEmpty then
-          else if (← read).ellipsis then
+          if let some _ ← findNamedArgDependsOnCurrent? then
+            /-
+            Dependencies of named arguments cannot be turned into eta arguments
+            since they are determined by the named arguments.
+            Instead we can turn them into implicit arguments.
+            -/
             addImplicitArg argName
           else
             addEtaArg argName
         else if !(← read).explicit then
-          if (← read).ellipsis then
+          if (← fTypeHasOptAutoParams) then
-            addImplicitArg argName
-          else if (← fTypeHasOptAutoParams) then
             addEtaArg argName
           else
             finalize
@@ -641,24 +668,30 @@ mutual
       finalize
 
   /--
-    Process a `fType` of the form `[x : A] → B x`.
+  Process a `fType` of the form `[x : A] → B x`.
-    This method assume `fType` is a function type -/
+  This method assume `fType` is a function type.
+  -/
   private partial def processInstImplicitArg (argName : Name) : M Expr := do
     if (← read).explicit then
-      if (← isNextArgHole) then
+      if let some stx ← nextArgHole? then
-        /- Recall that if '@' has been used, and the argument is '_', then we still use type class resolution -/
+        -- We still use typeclass resolution for `_` arguments.
-        let arg ← mkFreshExprMVar (← getArgExpectedType) MetavarKind.synthetic
+        -- This behavior can be suppressed with `(_)`.
+        let ty ← getArgExpectedType
+        let arg ← mkInstMVar ty
+        addTermInfo' stx arg ty
         modify fun s => { s with args := s.args.tail! }
-        addInstMVar arg.mvarId!
-        addNewArg argName arg
         main
       else
         processExplicitArg argName
     else
-      let arg ← mkFreshExprMVar (← getArgExpectedType) MetavarKind.synthetic
+      discard <| mkInstMVar (← getArgExpectedType)
+      main
+  where
+    mkInstMVar (ty : Expr) : M Expr := do
+      let arg ← mkFreshExprMVar ty MetavarKind.synthetic
       addInstMVar arg.mvarId!
       addNewArg argName arg
-      main
+      return arg
 
   /-- Elaborate function application arguments. -/
   partial def main : M Expr := do
@@ -689,6 +722,104 @@ end
 
 end ElabAppArgs
 
+
+/-! # Eliminator-like function application elaborator -/
+
+/--
+Information about an eliminator used by the elab-as-elim elaborator.
+This is not to be confused with `Lean.Meta.ElimInfo`, which is for `induction` and `cases`.
+The elab-as-elim routine is less restrictive in what counts as an eliminator, and it doesn't need
+to have a strict notion of what is a "target" — all it cares about are
+1. that the return type of a function is of the form `m ...` where `m` is a parameter
+   (unlike `induction` and `cases` eliminators, the arguments to `m`, known as "discriminants",
+   can be any expressions, not just parameters), and
+2. which arguments should be eagerly elaborated, to make discriminants be as elaborated as
+   possible for the expected type generalization procedure,
+   and which should be postponed (since they are the "minor premises").
+
+Note that the routine isn't doing induction/cases *on* particular expressions.
+The purpose of elab-as-elim is to successfully solve the higher-order unification problem
+between the return type of the function and the expected type.
+-/
+structure ElabElimInfo where
+  /-- The eliminator. -/
+  elimExpr   : Expr
+  /-- The type of the eliminator. -/
+  elimType   : Expr
+  /-- The position of the motive parameter. -/
+  motivePos  : Nat
+  /--
+  Positions of "major" parameters (those that should be eagerly elaborated
+  because they can contribute to the motive inference procedure).
+  All parameters that are neither the motive nor a major parameter are "minor" parameters.
+  The major parameters include all of the parameters that transitively appear in the motive's arguments,
+  as well as "first-order" arguments that include such parameters,
+  since they too can help with elaborating discriminants.
+
+  For example, in the following theorem the argument `h : a = b`
+  should be elaborated eagerly because it contains `b`, which occurs in `motive b`.
+  ```
+  theorem Eq.subst' {α} {motive : α → Prop} {a b : α} (h : a = b) : motive a → motive b
+  ```
+  For another example, the term `isEmptyElim (α := α)` is an underapplied eliminator, and it needs
+  argument `α` to be elaborated eagerly to create a type-correct motive.
+  ```
+  def isEmptyElim [IsEmpty α] {p : α → Sort _} (a : α) : p a := ...
+  example {α : Type _} [IsEmpty α] : id (α → False) := isEmptyElim (α := α)
+  ```
+  -/
+  majorsPos : Array Nat := #[]
+  deriving Repr, Inhabited
+
+def getElabElimExprInfo (elimExpr : Expr) : MetaM ElabElimInfo := do
+  let elimType ← inferType elimExpr
+  trace[Elab.app.elab_as_elim] "eliminator {indentExpr elimExpr}\nhas type{indentExpr elimType}"
+  forallTelescopeReducing elimType fun xs type => do
+    let motive  := type.getAppFn
+    let motiveArgs := type.getAppArgs
+    unless motive.isFVar do
+      throwError "unexpected eliminator resulting type{indentExpr type}"
+    let motiveType ← inferType motive
+    forallTelescopeReducing motiveType fun motiveParams motiveResultType => do
+      unless motiveParams.size == motiveArgs.size do
+        throwError "unexpected number of arguments at motive type{indentExpr motiveType}"
+      unless motiveResultType.isSort do
+        throwError "motive result type must be a sort{indentExpr motiveType}"
+    let some motivePos ← pure (xs.indexOf? motive) |
+      throwError "unexpected eliminator type{indentExpr elimType}"
+    /-
+    Compute transitive closure of fvars appearing in arguments to the motive.
+    These are the primary set of major parameters.
+    -/
+    let initMotiveFVars : CollectFVars.State := motiveArgs.foldl (init := {}) collectFVars
+    let motiveFVars ← xs.size.foldRevM (init := initMotiveFVars) fun i s => do
+      let x := xs[i]!
+      if s.fvarSet.contains x.fvarId! then
+        return collectFVars s (← inferType x)
+      else
+        return s
+    /- Collect the major parameter positions -/
+    let mut majorsPos := #[]
+    for i in [:xs.size] do
+      let x := xs[i]!
+      unless motivePos == i do
+        let xType ← x.fvarId!.getType
+        /-
+        We also consider "first-order" types because we can reliably "extract" information from them.
+        We say a term is "first-order" if all applications are of the form `f ...` where `f` is a constant.
+        -/
+        let isFirstOrder (e : Expr) : Bool := Option.isNone <| e.find? fun e => e.isApp && !e.getAppFn.isConst
+        if motiveFVars.fvarSet.contains x.fvarId!
+            || (isFirstOrder xType
+                && Option.isSome (xType.find? fun e => e.isFVar && motiveFVars.fvarSet.contains e.fvarId!)) then
+          majorsPos := majorsPos.push i
+    trace[Elab.app.elab_as_elim] "motivePos: {motivePos}"
+    trace[Elab.app.elab_as_elim] "majorsPos: {majorsPos}"
+    return { elimExpr, elimType,  motivePos, majorsPos }
+
+def getElabElimInfo (elimName : Name) : MetaM ElabElimInfo := do
+  getElabElimExprInfo (← mkConstWithFreshMVarLevels elimName)
+
 builtin_initialize elabAsElim : TagAttribute ←
   registerTagAttribute `elab_as_elim
     "instructs elaborator that the arguments of the function application should be elaborated as were an eliminator"
@@ -703,33 +834,15 @@ builtin_initialize elabAsElim : TagAttribute ←
         let info ← getConstInfo declName
         if (← hasOptAutoParams info.type) then
           throwError "[elab_as_elim] attribute cannot be used in declarations containing optional and auto parameters"
-        discard <| getElimInfo declName
+        discard <| getElabElimInfo declName
       go.run' {} {}
 
-/-! # Eliminator-like function application elaborator -/
 namespace ElabElim
 
 /-- Context of the `elab_as_elim` elaboration procedure. -/
 structure Context where
-  elimInfo : ElimInfo
+  elimInfo : ElabElimInfo
   expectedType : Expr
-  /--
-  Position of additional arguments that should be elaborated eagerly
-  because they can contribute to the motive inference procedure.
-  For example, in the following theorem the argument `h : a = b`
-  should be elaborated eagerly because it contains `b` which occurs
-  in `motive b`.
-  ```
-  theorem Eq.subst' {α} {motive : α → Prop} {a b : α} (h : a = b) : motive a → motive b
-  ```
-  For another example, the term `isEmptyElim (α := α)` is an underapplied eliminator, and it needs
-  argument `α` to be elaborated eagerly to create a type-correct motive.
-  ```
-  def isEmptyElim [IsEmpty α] {p : α → Sort _} (a : α) : p a := ...
-  example {α : Type _} [IsEmpty α] : id (α → False) := isEmptyElim (α := α)
-  ```
-  -/
-  extraArgsPos : Array Nat
 
 /-- State of the `elab_as_elim` elaboration procedure. -/
 structure State where
@@ -741,8 +854,6 @@ structure State where
   namedArgs    : List NamedArg
   /-- User-provided arguments that still have to be processed. -/
   args         : List Arg
-  /-- Discriminants (targets) processed so far. -/
-  discrs       : Array (Option Expr)
   /-- Instance implicit arguments collected so far. -/
   instMVars    : Array MVarId := #[]
   /-- Position of the next argument to be processed. We use it to decide whether the argument is the motive or a discriminant. -/
@@ -788,7 +899,7 @@ def finalize : M Expr := do
   let some motive := (← get).motive?
     | throwError "failed to elaborate eliminator, insufficient number of arguments"
   trace[Elab.app.elab_as_elim] "motive: {motive}"
-  forallTelescope (← get).fType fun xs _ => do
+  forallTelescope (← get).fType fun xs fType => do
     trace[Elab.app.elab_as_elim] "xs: {xs}"
     let mut expectedType := (← read).expectedType
     trace[Elab.app.elab_as_elim] "expectedType:{indentD expectedType}"
@@ -797,6 +908,7 @@ def finalize : M Expr := do
     let mut f := (← get).f
     if xs.size > 0 then
       -- under-application, specialize the expected type using `xs`
+      -- Note: if we ever wanted to support optParams and autoParams, this is where it could be.
       assert! (← get).args.isEmpty
       for x in xs do
         let .forallE _ t b _ ← whnf expectedType | throwInsufficient
@@ -813,18 +925,11 @@ def finalize : M Expr := do
     trace[Elab.app.elab_as_elim] "expectedType after processing:{indentD expectedType}"
     let result := mkAppN f xs
     trace[Elab.app.elab_as_elim] "result:{indentD result}"
-    let mut discrs := (← get).discrs
+    unless fType.getAppFn == (← get).motive? do
-    let idx := (← get).idx
+      throwError "Internal error, eliminator target type isn't an application of the motive"
-    if discrs.any Option.isNone then
+    let discrs := fType.getAppArgs
-      for i in [idx:idx + xs.size], x in xs do
+    trace[Elab.app.elab_as_elim] "discrs: {discrs}"
-        if let some tidx := (← read).elimInfo.targetsPos.indexOf? i then
+    let motiveVal ← mkMotive discrs expectedType
-          discrs := discrs.set! tidx x
-    if let some idx := discrs.findIdx? Option.isNone then
-      -- This should not happen.
-      trace[Elab.app.elab_as_elim] "Internal error, missing target with index {idx}"
-      throwError "failed to elaborate eliminator, insufficient number of arguments"
-    trace[Elab.app.elab_as_elim] "discrs: {discrs.map Option.get!}"
-    let motiveVal ← mkMotive (discrs.map Option.get!) expectedType
     unless (← isTypeCorrect motiveVal) do
       throwError "failed to elaborate eliminator, motive is not type correct:{indentD motiveVal}"
     unless (← isDefEq motive motiveVal) do
@@ -858,10 +963,6 @@ def getNextArg? (binderName : Name) (binderInfo : BinderInfo) : M (LOption Arg)
 def setMotive (motive : Expr) : M Unit :=
   modify fun s => { s with motive? := motive }
 
-/-- Push the given expression into the `discrs` field in the state, where `i` is which target it is for. -/
-def addDiscr (i : Nat) (discr : Expr) : M Unit :=
-  modify fun s => { s with discrs := s.discrs.set! i discr }
-
 /-- Elaborate the given argument with the given expected type. -/
 private def elabArg (arg : Arg) (argExpectedType : Expr) : M Expr := do
   match arg with
@@ -904,18 +1005,13 @@ partial def main : M Expr := do
         mkImplicitArg binderType binderInfo
     setMotive motive
     addArgAndContinue motive
-  else if let some tidx := (← read).elimInfo.targetsPos.indexOf? idx then
+  else if (← read).elimInfo.majorsPos.contains idx then
     match (← getNextArg? binderName binderInfo) with
-    | .some arg => let discr ← elabArg arg binderType; addDiscr tidx discr; addArgAndContinue discr
+    | .some arg => let discr ← elabArg arg binderType; addArgAndContinue discr
     | .undef => finalize
-    | .none => let discr ← mkImplicitArg binderType binderInfo; addDiscr tidx discr; addArgAndContinue discr
+    | .none => let discr ← mkImplicitArg binderType binderInfo; addArgAndContinue discr
   else match (← getNextArg? binderName binderInfo) with
-    | .some (.stx stx) =>
+    | .some (.stx stx) => addArgAndContinue (← postponeElabTerm stx binderType)
-      if (← read).extraArgsPos.contains idx then
-        let arg ← elabArg (.stx stx) binderType
-        addArgAndContinue arg
-      else
-        addArgAndContinue (← postponeElabTerm stx binderType)
     | .some (.expr val) => addArgAndContinue (← ensureArgType (← get).f val binderType)
     | .undef => finalize
     | .none => addArgAndContinue (← mkImplicitArg binderType binderInfo)
@@ -969,13 +1065,10 @@ def elabAppArgs (f : Expr) (namedArgs : Array NamedArg) (args : Array Arg)
     let some expectedType := expectedType? | throwError "failed to elaborate eliminator, expected type is not available"
     let expectedType ← instantiateMVars expectedType
     if expectedType.getAppFn.isMVar then throwError "failed to elaborate eliminator, expected type is not available"
-    let extraArgsPos ← getElabAsElimExtraArgsPos elimInfo
+    ElabElim.main.run { elimInfo, expectedType } |>.run' {
-    trace[Elab.app.elab_as_elim] "extraArgsPos: {extraArgsPos}"
-    ElabElim.main.run { elimInfo, expectedType, extraArgsPos } |>.run' {
       f, fType
       args := args.toList
       namedArgs := namedArgs.toList
-      discrs := mkArray elimInfo.targetsPos.size none
     }
   else
     ElabAppArgs.main.run { explicit, ellipsis, resultIsOutParamSupport } |>.run' {
@@ -986,12 +1079,12 @@ def elabAppArgs (f : Expr) (namedArgs : Array NamedArg) (args : Array Arg)
     }
 where
   /-- Return `some info` if we should elaborate as an eliminator. -/
-  elabAsElim? : TermElabM (Option ElimInfo) := do
+  elabAsElim? : TermElabM (Option ElabElimInfo) := do
     unless (← read).heedElabAsElim do return none
     if explicit || ellipsis then return none
     let .const declName _ := f | return none
     unless (← shouldElabAsElim declName) do return none
-    let elimInfo ← getElimInfo declName
+    let elimInfo ← getElabElimInfo declName
     forallTelescopeReducing (← inferType f) fun xs _ => do
       /- Process arguments similar to `Lean.Elab.Term.ElabElim.main` to see if the motive has been
          provided, in which case we use the standard app elaborator.
@@ -1022,41 +1115,6 @@ where
             return none
         | _, _ => return some elimInfo
 
-  /--
-  Collect extra argument positions that must be elaborated eagerly when using `elab_as_elim`.
-  The idea is that they contribute to motive inference. See comment at `ElamElim.Context.extraArgsPos`.
-  -/
-  getElabAsElimExtraArgsPos (elimInfo : ElimInfo) : MetaM (Array Nat) := do
-    forallTelescope elimInfo.elimType fun xs type => do
-      let targets := type.getAppArgs
-      /- Compute transitive closure of fvars appearing in the motive and the targets. -/
-      let initMotiveFVars : CollectFVars.State := targets.foldl (init := {}) collectFVars
-      let motiveFVars ← xs.size.foldRevM (init := initMotiveFVars) fun i s => do
-        let x := xs[i]!
-        if elimInfo.motivePos == i || elimInfo.targetsPos.contains i || s.fvarSet.contains x.fvarId! then
-          return collectFVars s (← inferType x)
-        else
-          return s
-      /- Collect the extra argument positions -/
-      let mut extraArgsPos := #[]
-      for i in [:xs.size] do
-        let x := xs[i]!
-        unless elimInfo.motivePos == i || elimInfo.targetsPos.contains i do
-          let xType ← x.fvarId!.getType
-          /- We only consider "first-order" types because we can reliably "extract" information from them. -/
-          if motiveFVars.fvarSet.contains x.fvarId!
-             || (isFirstOrder xType
-                 && Option.isSome (xType.find? fun e => e.isFVar && motiveFVars.fvarSet.contains e.fvarId!)) then
-            extraArgsPos := extraArgsPos.push i
-      return extraArgsPos
-
-  /-
-  Helper function for implementing `elab_as_elim`.
-  We say a term is "first-order" if all applications are of the form `f ...` where `f` is a constant.
-  -/
-  isFirstOrder (e : Expr) : Bool :=
-    Option.isNone <| e.find? fun e =>
-      e.isApp && !e.getAppFn.isConst
 
 /-- Auxiliary inductive datatype that represents the resolution of an `LVal`. -/
 inductive LValResolution where
@@ -1221,7 +1279,7 @@ private partial def mkBaseProjections (baseStructName : Name) (structName : Name
     let mut e := e
     for projFunName in path do
       let projFn ← mkConst projFunName
-      e ← elabAppArgs projFn #[{ name := `self, val := Arg.expr e }] (args := #[]) (expectedType? := none) (explicit := false) (ellipsis := false)
+      e ← elabAppArgs projFn #[{ name := `self, val := Arg.expr e, suppressDeps := true }] (args := #[]) (expectedType? := none) (explicit := false) (ellipsis := false)
     return e
 
 private def typeMatchesBaseName (type : Expr) (baseName : Name) : MetaM Bool := do
@@ -1305,10 +1363,10 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp
         let projFn ← mkConst info.projFn
         let projFn ← addProjTermInfo lval.getRef projFn
         if lvals.isEmpty then
-          let namedArgs ← addNamedArg namedArgs { name := `self, val := Arg.expr f }
+          let namedArgs ← addNamedArg namedArgs { name := `self, val := Arg.expr f, suppressDeps := true }
           elabAppArgs projFn namedArgs args expectedType? explicit ellipsis
         else
-          let f ← elabAppArgs projFn #[{ name := `self, val := Arg.expr f }] #[] (expectedType? := none) (explicit := false) (ellipsis := false)
+          let f ← elabAppArgs projFn #[{ name := `self, val := Arg.expr f, suppressDeps := true }] #[] (expectedType? := none) (explicit := false) (ellipsis := false)
           loop f lvals
       else
         unreachable!

src/Lean/Elab/Arg.lean

@@ -9,18 +9,22 @@ import Lean.Elab.Term
 namespace Lean.Elab.Term
 
 /--
-  Auxiliary inductive datatype for combining unelaborated syntax
+Auxiliary inductive datatype for combining unelaborated syntax
-  and already elaborated expressions. It is used to elaborate applications. -/
+and already elaborated expressions. It is used to elaborate applications.
+-/
 inductive Arg where
   | stx  (val : Syntax)
   | expr (val : Expr)
   deriving Inhabited
 
-/-- Named arguments created using the notation `(x := val)` -/
+/-- Named arguments created using the notation `(x := val)`. -/
 structure NamedArg where
   ref  : Syntax := Syntax.missing
   name : Name
   val  : Arg
+  /-- If `true`, then make all parameters that depend on this one become implicit.
+  This is used for projection notation, since structure parameters might be explicit for classes. -/
+  suppressDeps : Bool := false
   deriving Inhabited
 
 /--

src/Lean/Elab/BuiltinTerm.lean

@@ -150,26 +150,10 @@ private def getMVarFromUserName (ident : Syntax) : MetaM Expr := do
     elabTerm b expectedType?
   | _ => throwUnsupportedSyntax
 
-private def mkTacticMVar (type : Expr) (tacticCode : Syntax) : TermElabM Expr := do
-  let mvar ← mkFreshExprMVar type MetavarKind.syntheticOpaque
-  let mvarId := mvar.mvarId!
-  let ref ← getRef
-  registerSyntheticMVar ref mvarId <| SyntheticMVarKind.tactic tacticCode (← saveContext)
-  return mvar
-
-register_builtin_option debug.byAsSorry : Bool := {
-  defValue := false
-  group    := "debug"
-  descr    := "replace `by ..` blocks with `sorry` IF the expected type is a proposition"
-}
-
 @[builtin_term_elab byTactic] def elabByTactic : TermElab := fun stx expectedType? => do
   match expectedType? with
   | some expectedType =>
-    if ← pure (debug.byAsSorry.get (← getOptions)) <&&> isProp expectedType then
+    mkTacticMVar expectedType stx .term
-      mkSorry expectedType false
-    else
-      mkTacticMVar expectedType stx
   | none =>
     tryPostpone
     throwError ("invalid 'by' tactic, expected type has not been provided")

src/Lean/Elab/StructInst.lean

@@ -682,7 +682,12 @@ private partial def elabStruct (s : Struct) (expectedType? : Option Expr) : Term
               -- We add info to get reliable positions for messages from evaluating the tactic script.
               let info := field.ref.getHeadInfo
               let stx := stx.raw.rewriteBottomUp (·.setInfo info)
-              cont (← elabTermEnsuringType stx (d.getArg! 0).consumeTypeAnnotations) field
+              let type := (d.getArg! 0).consumeTypeAnnotations
+              let mvar ← mkTacticMVar type stx (.fieldAutoParam fieldName s.structName)
+              -- Note(kmill): We are adding terminfo to simulate a previous implementation that elaborated `tacticBlock`.
+              -- (See the aformentioned `processExplicitArg` for a comment about this.)
+              addTermInfo' stx mvar
+              cont mvar field
           | _ =>
             if bi == .instImplicit then
               let val ← withRef field.ref <| mkFreshExprMVar d .synthetic

src/Lean/Elab/Structure.lean

@@ -468,7 +468,8 @@ where
     if h : i < view.parents.size then
       let parentStx := view.parents.get ⟨i, h⟩
       withRef parentStx do
-      let parentType ← Term.elabType parentStx
+      let parentType ← Term.withSynthesize <| Term.elabType parentStx
+      let parentType ← whnf parentType
       let parentStructName ← getStructureName parentType
       if let some existingFieldName ← findExistingField? infos parentStructName then
         if structureDiamondWarning.get (← getOptions) then

src/Lean/Elab/SyntheticMVars.lean

@@ -316,6 +316,18 @@ def PostponeBehavior.ofBool : Bool → PostponeBehavior
   | true  => .yes
   | false => .no
 
+private def TacticMVarKind.logError (tacticCode : Syntax) (kind : TacticMVarKind) : TermElabM Unit := do
+  match kind with
+  | term => pure ()
+  | autoParam argName => logErrorAt tacticCode m!"could not synthesize default value for parameter '{argName}' using tactics"
+  | fieldAutoParam fieldName structName => logErrorAt tacticCode m!"could not synthesize default value for field '{fieldName}' of '{structName}' using tactics"
+
+private def TacticMVarKind.maybeWithoutRecovery (kind : TacticMVarKind) (m : TacticM α) : TacticM α := do
+  if kind matches .autoParam .. | .fieldAutoParam .. then
+    withoutErrToSorry <| Tactic.withoutRecover <| m
+  else
+    m
+
 mutual
 
   /--
@@ -325,7 +337,7 @@ mutual
 
   If `report := false`, then `runTactic` will not capture exceptions nor will report unsolved goals. Unsolved goals become exceptions.
   -/
-  partial def runTactic (mvarId : MVarId) (tacticCode : Syntax) (report := true) : TermElabM Unit := withoutAutoBoundImplicit do
+  partial def runTactic (mvarId : MVarId) (tacticCode : Syntax) (kind : TacticMVarKind) (report := true) : TermElabM Unit := withoutAutoBoundImplicit do
     instantiateMVarDeclMVars mvarId
     /-
     TODO: consider using `runPendingTacticsAt` at `mvarId` local context and target type.
@@ -342,7 +354,7 @@ mutual
     in more complicated scenarios.
     -/
     tryCatchRuntimeEx
-      (do let remainingGoals ← withInfoHole mvarId <| Tactic.run mvarId do
+      (do let remainingGoals ← withInfoHole mvarId <| Tactic.run mvarId <| kind.maybeWithoutRecovery do
             withTacticInfoContext tacticCode do
               -- also put an info node on the `by` keyword specifically -- the token may be `canonical` and thus shown in the info
               -- view even though it is synthetic while a node like `tacticCode` never is (#1990)
@@ -354,10 +366,13 @@ mutual
               synthesizeSyntheticMVars (postpone := .no)
           unless remainingGoals.isEmpty do
             if report then
+              kind.logError tacticCode
               reportUnsolvedGoals remainingGoals
             else
               throwError "unsolved goals\n{goalsToMessageData remainingGoals}")
       fun ex => do
+        if report then
+          kind.logError tacticCode
         if report && (← read).errToSorry then
           for mvarId in (← getMVars (mkMVar mvarId)) do
             mvarId.admit
@@ -385,10 +400,10 @@ mutual
       return false
     -- NOTE: actual processing at `synthesizeSyntheticMVarsAux`
     | .postponed savedContext => resumePostponed savedContext mvarSyntheticDecl.stx mvarId postponeOnError
-    | .tactic tacticCode savedContext =>
+    | .tactic tacticCode savedContext kind =>
       withSavedContext savedContext do
         if runTactics then
-          runTactic mvarId tacticCode
+          runTactic mvarId tacticCode kind
           return true
         else
           return false
@@ -529,9 +544,9 @@ the result of a tactic block.
 def runPendingTacticsAt (e : Expr) : TermElabM Unit := do
   for mvarId in (← getMVars e) do
     let mvarId ← getDelayedMVarRoot mvarId
-    if let some { kind := .tactic tacticCode savedContext, .. } ← getSyntheticMVarDecl? mvarId then
+    if let some { kind := .tactic tacticCode savedContext kind, .. } ← getSyntheticMVarDecl? mvarId then
       withSavedContext savedContext do
-        runTactic mvarId tacticCode
+        runTactic mvarId tacticCode kind
         markAsResolved mvarId
 
 builtin_initialize

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean

@@ -75,9 +75,7 @@ instance : ToExpr Gate where
   toExpr x :=
     match x with
     | .and => mkConst ``Gate.and
-    | .or => mkConst ``Gate.or
     | .xor => mkConst ``Gate.xor
-    | .imp => mkConst ``Gate.imp
     | .beq => mkConst ``Gate.beq
   toTypeExpr := mkConst ``Gate
 

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.lean

@@ -343,7 +343,7 @@ where
     return mkApp4 congrProof (toExpr inner.width) innerExpr innerEval innerProof
 
   goBvLit (x : Expr) : M (Option ReifiedBVExpr) := do
-    let some ⟨width, bvVal⟩ ← getBitVecValue? x | return none
+    let some ⟨width, bvVal⟩ ← getBitVecValue? x | return ← ofAtom x
     let bvExpr : BVExpr width := .const bvVal
     let expr := mkApp2 (mkConst ``BVExpr.const) (toExpr width) (toExpr bvVal)
     let proof := do

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.lean

@@ -65,7 +65,6 @@ partial def of (t : Expr) : M (Option ReifiedBVLogical) := do
       let subProof ← sub.evalsAtAtoms
       return mkApp3 (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.not_congr) subExpr subEvalExpr subProof
     return some ⟨boolExpr, proof, expr⟩
-  | Bool.or lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .or ``Std.Tactic.BVDecide.Reflect.Bool.or_congr
   | Bool.and lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .and ``Std.Tactic.BVDecide.Reflect.Bool.and_congr
   | Bool.xor lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .xor ``Std.Tactic.BVDecide.Reflect.Bool.xor_congr
   | BEq.beq α _ lhsExpr rhsExpr =>

src/Lean/Elab/Tactic/Rfl.lean

@@ -16,6 +16,10 @@ provided the reflexivity lemma has been marked as `@[refl]`.
 
 namespace Lean.Elab.Tactic.Rfl
 
+/--
+This tactic applies to a goal whose target has the form `x ~ x`, where `~` is a reflexive
+relation, that is, a relation which has a reflexive lemma tagged with the attribute [refl].
+-/
 @[builtin_tactic Lean.Parser.Tactic.applyRfl] def evalApplyRfl : Tactic := fun stx =>
   match stx with
   | `(tactic| apply_rfl) => withMainContext do liftMetaFinishingTactic (·.applyRfl)

src/Lean/Elab/Tactic/Simp.lean

@@ -47,7 +47,7 @@ def tacticToDischarge (tacticCode : Syntax) : TacticM (IO.Ref Term.State × Simp
         -/
         withoutModifyingStateWithInfoAndMessages do
           Term.withSynthesize (postpone := .no) do
-            Term.runTactic (report := false) mvar.mvarId! tacticCode
+            Term.runTactic (report := false) mvar.mvarId! tacticCode .term
           let result ← instantiateMVars mvar
           if result.hasExprMVar then
             return none

src/Lean/Elab/Term.lean

@@ -29,6 +29,15 @@ structure SavedContext where
   errToSorry : Bool
   levelNames : List Name
 
+/-- The kind of a tactic metavariable, used for additional error reporting. -/
+inductive TacticMVarKind
+  /-- Standard tactic metavariable, arising from `by ...` syntax. -/
+  | term
+  /-- Tactic metavariable arising from an autoparam for a function application. -/
+  | autoParam (argName : Name)
+  /-- Tactic metavariable arising from an autoparam for a structure field. -/
+  | fieldAutoParam (fieldName structName : Name)
+
 /-- We use synthetic metavariables as placeholders for pending elaboration steps. -/
 inductive SyntheticMVarKind where
   /--
@@ -43,7 +52,7 @@ inductive SyntheticMVarKind where
   Otherwise, we generate the error `("type mismatch" ++ e ++ "has type" ++ eType ++ "but it is expected to have type" ++ expectedType)` -/
   | coe (header? : Option String) (expectedType : Expr) (e : Expr) (f? : Option Expr)
   /-- Use tactic to synthesize value for metavariable. -/
-  | tactic (tacticCode : Syntax) (ctx : SavedContext)
+  | tactic (tacticCode : Syntax) (ctx : SavedContext) (kind : TacticMVarKind)
   /-- Metavariable represents a hole whose elaboration has been postponed. -/
   | postponed (ctx : SavedContext)
   deriving Inhabited
@@ -1191,6 +1200,26 @@ private def postponeElabTermCore (stx : Syntax) (expectedType? : Option Expr) :
 def getSyntheticMVarDecl? (mvarId : MVarId) : TermElabM (Option SyntheticMVarDecl) :=
   return (← get).syntheticMVars.find? mvarId
 
+register_builtin_option debug.byAsSorry : Bool := {
+  defValue := false
+  group    := "debug"
+  descr    := "replace `by ..` blocks with `sorry` IF the expected type is a proposition"
+}
+
+/--
+Creates a new metavariable of type `type` that will be synthesized using the tactic code.
+The `tacticCode` syntax is the full `by ..` syntax.
+-/
+def mkTacticMVar (type : Expr) (tacticCode : Syntax) (kind : TacticMVarKind) : TermElabM Expr := do
+  if ← pure (debug.byAsSorry.get (← getOptions)) <&&> isProp type then
+    mkSorry type false
+  else
+    let mvar ← mkFreshExprMVar type MetavarKind.syntheticOpaque
+    let mvarId := mvar.mvarId!
+    let ref ← getRef
+    registerSyntheticMVar ref mvarId <| SyntheticMVarKind.tactic tacticCode (← saveContext) kind
+    return mvar
+
 /--
   Create an auxiliary annotation to make sure we create an `Info` even if `e` is a metavariable.
   See `mkTermInfo`.

src/Lean/Environment.lean

@@ -515,11 +515,11 @@ def addEntry {α β σ : Type} (ext : PersistentEnvExtension α β σ) (env : En
 def getState {α β σ : Type} [Inhabited σ] (ext : PersistentEnvExtension α β σ) (env : Environment) : σ :=
   (ext.toEnvExtension.getState env).state
 
-/-- Set the current state of the given extension in the given environment. This change is *not* persisted across files. -/
+/-- Set the current state of the given extension in the given environment. -/
 def setState {α β σ : Type} (ext : PersistentEnvExtension α β σ) (env : Environment) (s : σ) : Environment :=
   ext.toEnvExtension.modifyState env fun ps => { ps with  state := s }
 
-/-- Modify the state of the given extension in the given environment by applying the given function. This change is *not* persisted across files. -/
+/-- Modify the state of the given extension in the given environment by applying the given function. -/
 def modifyState {α β σ : Type} (ext : PersistentEnvExtension α β σ) (env : Environment) (f : σ → σ) : Environment :=
   ext.toEnvExtension.modifyState env fun ps => { ps with state := f (ps.state) }
 

src/Lean/Meta/Eval.lean

@@ -6,6 +6,7 @@ Authors: Sebastian Ullrich, Leonardo de Moura
 prelude
 import Lean.AddDecl
 import Lean.Meta.Check
+import Lean.Util.CollectLevelParams
 
 namespace Lean.Meta
 
@@ -13,12 +14,13 @@ unsafe def evalExprCore (α) (value : Expr) (checkType : Expr → MetaM Unit) (s
   withoutModifyingEnv do
     let name ← mkFreshUserName `_tmp
     let value ← instantiateMVars value
+    let us := collectLevelParams {} value |>.params
     if value.hasMVar then
       throwError "failed to evaluate expression, it contains metavariables{indentExpr value}"
     let type ← inferType value
     checkType type
     let decl := Declaration.defnDecl {
-       name, levelParams := [], type
+       name, levelParams := us.toList, type
        value, hints := ReducibilityHints.opaque,
        safety
     }

src/Lean/Meta/Instances.lean

@@ -101,7 +101,7 @@ private def mkInstanceKey (e : Expr) : MetaM (Array InstanceKey) := do
     DiscrTree.mkPath type tcDtConfig
 
 /--
-Compute the order the arguments of `inst` should by synthesized.
+Compute the order the arguments of `inst` should be synthesized.
 
 The synthesization order makes sure that all mvars in non-out-params of the
 subgoals are assigned before we try to synthesize it.  Otherwise it goes left

src/Lean/Meta/Tactic/Rfl.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2022 Newell Jensen. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Newell Jensen, Thomas Murrills
+Authors: Newell Jensen, Thomas Murrills, Joachim Breitner
 -/
 prelude
 import Lean.Meta.Tactic.Apply
@@ -58,13 +58,13 @@ def _root_.Lean.MVarId.applyRfl (goal : MVarId) : MetaM Unit := goal.withContext
   -- NB: uses whnfR, we do not want to unfold the relation itself
   let t ← whnfR <|← instantiateMVars <|← goal.getType
   if t.getAppNumArgs < 2 then
-    throwError "rfl can only be used on binary relations, not{indentExpr (← goal.getType)}"
+    throwTacticEx `rfl goal "expected goal to be a binary relation"
 
   -- Special case HEq here as it has a different argument order.
   if t.isAppOfArity ``HEq 4 then
     let gs ← goal.applyConst ``HEq.refl
     unless gs.isEmpty do
-      throwError MessageData.tagged `Tactic.unsolvedGoals <| m!"unsolved goals\n{
+      throwTacticEx `rfl goal <| MessageData.tagged `Tactic.unsolvedGoals <| m!"unsolved goals\n{
         goalsToMessageData gs}"
     return
 
@@ -76,8 +76,8 @@ def _root_.Lean.MVarId.applyRfl (goal : MVarId) : MetaM Unit := goal.withContext
   unless success do
     let explanation := MessageData.ofLazyM (es := #[lhs, rhs]) do
       let (lhs, rhs) ← addPPExplicitToExposeDiff lhs rhs
-      return m!"The lhs{indentExpr lhs}\nis not definitionally equal to rhs{indentExpr rhs}"
+      return m!"the left-hand side{indentExpr lhs}\nis not definitionally equal to the right-hand side{indentExpr rhs}"
-    throwTacticEx `apply_rfl goal explanation
+    throwTacticEx `rfl goal explanation
 
   if rel.isAppOfArity `Eq 1 then
     -- The common case is equality: just use `Eq.refl`
@@ -86,6 +86,9 @@ def _root_.Lean.MVarId.applyRfl (goal : MVarId) : MetaM Unit := goal.withContext
     goal.assign (mkApp2 (mkConst ``Eq.refl us) α lhs)
   else
     -- Else search through `@refl` keyed by the relation
+    -- We change the type to `lhs ~ lhs` so that we do not the (possibly costly) `lhs =?= rhs` check
+    -- again.
+    goal.setType (.app t.appFn! lhs)
     let s ← saveState
     let mut ex? := none
     for lem in ← (reflExt.getState (← getEnv)).getMatch rel reflExt.config do
@@ -102,7 +105,7 @@ def _root_.Lean.MVarId.applyRfl (goal : MVarId) : MetaM Unit := goal.withContext
       sErr.restore
       throw e
     else
-      throwError "rfl failed, no @[refl] lemma registered for relation{indentExpr rel}"
+      throwTacticEx `rfl goal m!"no @[refl] lemma registered for relation{indentExpr rel}"
 
 /-- Helper theorem for `Lean.MVarId.liftReflToEq`. -/
 private theorem rel_of_eq_and_refl {α : Sort _} {R : α → α → Prop}

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

@@ -228,8 +228,16 @@ builtin_dsimproc [simp, seval] reduceOfNat (BitVec.ofNat _ _) := fun e => do
   if bv.toNat == v then return .continue -- already normalized
   return .done <| toExpr (BitVec.ofNat n v)
 
+/-- Simplification procedure for `=` on `BitVec`s. -/
 builtin_simproc [simp, seval] reduceEq  (( _ : BitVec _) = _)  := reduceBinPred ``Eq 3 (. = .)
+/-- Simplification procedure for `≠` on `BitVec`s. -/
 builtin_simproc [simp, seval] reduceNe  (( _ : BitVec _) ≠ _)  := reduceBinPred ``Ne 3 (. ≠ .)
+/-- Simplification procedure for `==` on `BitVec`s. -/
+builtin_dsimproc [simp, seval] reduceBEq  (( _ : BitVec _) == _)  :=
+  reduceBoolPred ``BEq.beq 4 (· == ·)
+/-- Simplification procedure for `!=` on `BitVec`s. -/
+builtin_dsimproc [simp, seval] reduceBNe  (( _ : BitVec _) != _)  :=
+  reduceBoolPred ``bne 4 (· != ·)
 
 /-- Simplification procedure for `<` on `BitVec`s. -/
 builtin_simproc [simp, seval] reduceLT (( _ : BitVec _) < _)  := reduceBinPred ``LT.lt 4 (· < ·)

src/Lean/MetavarContext.lean

@@ -17,13 +17,13 @@ assignments. It is used in the elaborator, tactic framework, unifier
 the requirements imposed by these modules.
 
 - We may invoke TC while executing `isDefEq`. We need this feature to
-  WellFoundedRelationbe able to solve unification problems such as:
+  be able to solve unification problems such as:
   ```
   f ?a (ringAdd ?s) ?x ?y =?= f Int intAdd n m
   ```
   where `(?a : Type) (?s : Ring ?a) (?x ?y : ?a)`.
 
-  During `isDefEq` (i.e., unification), it will need to solve the constrain
+  During `isDefEq` (i.e., unification), it will need to solve the constraint
   ```
   ringAdd ?s =?= intAdd
   ```
@@ -179,7 +179,7 @@ the requirements imposed by these modules.
   an exception instead of return `false` whenever it tries to assign
   a metavariable owned by its caller. The idea is to sign to the caller that
   it cannot solve the TC problem at this point, and more information is needed.
-  That is, the caller must make progress an assign its metavariables before
+  That is, the caller must make progress and assign its metavariables before
   trying to invoke TC again.
 
   In Lean4, we are using a simpler design for the `MetavarContext`.

src/Lean/Util/Heartbeats.lean

@@ -21,7 +21,6 @@ Remember that user facing heartbeats (e.g. as used in `set_option maxHeartbeats`
 differ from the internally tracked heartbeats by a factor of 1000,
 so you need to divide the results here by 1000 before comparing with user facing numbers.
 -/
--- See also `Lean.withSeconds`
 def withHeartbeats [Monad m] [MonadLiftT BaseIO m] (x : m α) : m (α × Nat) := do
   let start ← IO.getNumHeartbeats
   let r ← x

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

@@ -140,7 +140,7 @@ theorem expand.go_eq [BEq α] [Hashable α] [PartialEquivBEq α] (source : Array
     refine ih.trans ?_
     simp only [Array.get_eq_getElem, AssocList.foldl_eq, Array.toList_set]
     rw [List.drop_eq_getElem_cons hi, List.bind_cons, List.foldl_append,
-      List.drop_set_of_lt _ _ (by omega), Array.getElem_eq_toList_getElem]
+      List.drop_set_of_lt _ _ (by omega), Array.getElem_eq_getElem_toList]
   · next i source target hi =>
     rw [expand.go_neg hi, List.drop_eq_nil_of_le, bind_nil, foldl_nil]
     rwa [Array.size_eq_length_toList, Nat.not_lt] at hi

src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Basic.lean

@@ -16,26 +16,20 @@ namespace Std.Tactic.BVDecide
 
 inductive Gate
   | and
-  | or
   | xor
   | beq
-  | imp
 
 namespace Gate
 
 def toString : Gate → String
   | and => "&&"
-  | or  => "||"
   | xor => "^^"
   | beq => "=="
-  | imp => "→"
 
 def eval : Gate → Bool → Bool → Bool
   | and => (· && ·)
-  | or => (· || ·)
   | xor => (· ^^ ·)
   | beq => (· == ·)
-  | imp => (!· || ·)
 
 end Gate
 

src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Circuit.lean

@@ -51,10 +51,6 @@ where
         let ret := aig.mkAndCached input
         have := LawfulOperator.le_size (f := mkAndCached) aig input
         ⟨ret, by dsimp only [ret] at lextend rextend ⊢; omega⟩
-      | .or =>
-        let ret := aig.mkOrCached input
-        have := LawfulOperator.le_size (f := mkOrCached) aig input
-        ⟨ret, by dsimp only [ret] at lextend rextend ⊢; omega⟩
       | .xor =>
         let ret := aig.mkXorCached input
         have := LawfulOperator.le_size (f := mkXorCached) aig input
@@ -63,11 +59,6 @@ where
         let ret := aig.mkBEqCached input
         have := LawfulOperator.le_size (f := mkBEqCached) aig input
         ⟨ret, by dsimp only [ret] at lextend rextend ⊢; omega⟩
-      | .imp =>
-        let ret := aig.mkImpCached input
-        have := LawfulOperator.le_size (f := mkImpCached) aig input
-        ⟨ret, by dsimp only [ret] at lextend rextend ⊢; omega⟩
-
 
 variable (atomHandler : AIG β → α → Entrypoint β) [LawfulOperator β (fun _ => α) atomHandler]
 
@@ -99,18 +90,12 @@ theorem ofBoolExprCached.go_decl_eq (idx) (aig : AIG β) (h : idx < aig.decls.si
     | and =>
       simp only [go]
       rw [AIG.LawfulOperator.decl_eq (f := mkAndCached), rih, lih]
-    | or =>
-      simp only [go]
-      rw [AIG.LawfulOperator.decl_eq (f := mkOrCached), rih, lih]
     | xor =>
       simp only [go]
       rw [AIG.LawfulOperator.decl_eq (f := mkXorCached), rih, lih]
     | beq =>
       simp only [go]
       rw [AIG.LawfulOperator.decl_eq (f := mkBEqCached), rih, lih]
-    | imp =>
-      simp only [go]
-      rw [AIG.LawfulOperator.decl_eq (f := mkImpCached), rih, lih]
 
 theorem ofBoolExprCached.go_isPrefix_aig {aig : AIG β} :
     IsPrefix aig.decls (go aig expr atomHandler).val.aig.decls := by

src/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean

@@ -297,7 +297,7 @@ theorem ofArray_eq (arr : Array (Literal (PosFin n)))
       dsimp; omega
     rw [List.getElem?_eq_getElem i_in_bounds, List.getElem?_eq_getElem i_in_bounds']
     simp only [List.get_eq_getElem, Nat.zero_add] at h
-    rw [← Array.getElem_eq_toList_getElem]
+    rw [← Array.getElem_eq_getElem_toList]
     simp [h]
   · have arr_data_length_le_i : arr.toList.length ≤ i := by
       dsimp; omega

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

@@ -503,7 +503,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
                 conv => rhs; rw [Array.size_mk]
                 exact hbound
               simp only [getElem!, id_eq_idx, Array.toList_length, idx_in_bounds2, ↓reduceDIte,
-                Fin.eta, Array.get_eq_getElem, Array.getElem_eq_toList_getElem, decidableGetElem?] at heq
+                Fin.eta, Array.get_eq_getElem, Array.getElem_eq_getElem_toList, decidableGetElem?] at heq
               rw [hidx, hl] at heq
               simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
               simp only [← heq] at l_ne_b
@@ -536,7 +536,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
                 conv => rhs; rw [Array.size_mk]
                 exact hbound
               simp only [getElem!, id_eq_idx, Array.toList_length, idx_in_bounds2, ↓reduceDIte,
-                Fin.eta, Array.get_eq_getElem, Array.getElem_eq_toList_getElem, decidableGetElem?] at heq
+                Fin.eta, Array.get_eq_getElem, Array.getElem_eq_getElem_toList, decidableGetElem?] at heq
               rw [hidx, hl] at heq
               simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
               have i_eq_l : i = l.1 := by rw [← heq]
@@ -596,7 +596,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
                 conv => rhs; rw [Array.size_mk]
                 exact hbound
               simp only [getElem!, id_eq_idx, Array.toList_length, idx_in_bounds2, ↓reduceDIte,
-                Fin.eta, Array.get_eq_getElem, Array.getElem_eq_toList_getElem, decidableGetElem?] at heq
+                Fin.eta, Array.get_eq_getElem, Array.getElem_eq_getElem_toList, decidableGetElem?] at heq
               rw [hidx] at heq
               simp only [Option.some.injEq] at heq
               rw [← heq] at hl

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

@@ -461,7 +461,7 @@ theorem existsRatHint_of_ratHintsExhaustive {n : Nat} (f : DefaultFormula n)
     constructor
     · rw [← Array.mem_toList]
       apply Array.getElem_mem_toList
-    · rw [← Array.getElem_eq_toList_getElem] at c'_in_f
+    · rw [← Array.getElem_eq_getElem_toList] at c'_in_f
       simp only [getElem!, Array.getElem_range, i_lt_f_clauses_size, dite_true,
         c'_in_f, DefaultClause.contains_iff, Array.get_eq_getElem, decidableGetElem?]
       simpa [Clause.toList] using negPivot_in_c'
@@ -472,8 +472,8 @@ theorem existsRatHint_of_ratHintsExhaustive {n : Nat} (f : DefaultFormula n)
     dsimp at *
     omega
   simp only [List.get_eq_getElem, Array.map_toList, Array.toList_length, List.getElem_map] at h'
-  rw [← Array.getElem_eq_toList_getElem] at h'
+  rw [← Array.getElem_eq_getElem_toList] at h'
-  rw [← Array.getElem_eq_toList_getElem] at c'_in_f
+  rw [← Array.getElem_eq_getElem_toList] at c'_in_f
   exists ⟨j.1, j_in_bounds⟩
   simp [getElem!, h', i_lt_f_clauses_size, dite_true, c'_in_f, decidableGetElem?]
 

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

@@ -1140,25 +1140,25 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n)
       specialize h3 ⟨j.1, j_in_bounds⟩ j_ne_k
       simp only [derivedLits_arr_def, Fin.getElem_fin] at li_eq_lj
       simp only [Fin.getElem_fin, derivedLits_arr_def, ne_eq, li, li_eq_lj] at h3
-      simp only [List.get_eq_getElem, Array.getElem_eq_toList_getElem, not_true_eq_false] at h3
+      simp only [List.get_eq_getElem, Array.getElem_eq_getElem_toList, not_true_eq_false] at h3
     · next k_ne_i =>
       have i_ne_k : ⟨i.1, i_in_bounds⟩ ≠ k := by intro i_eq_k; simp only [← i_eq_k, not_true] at k_ne_i
       specialize h3 ⟨i.1, i_in_bounds⟩ i_ne_k
       simp (config := { decide := true }) [Fin.getElem_fin, derivedLits_arr_def, ne_eq,
-        Array.getElem_eq_toList_getElem, li] at h3
+        Array.getElem_eq_getElem_toList, li] at h3
   · by_cases li.2 = true
     · next li_eq_true =>
       have i_ne_k2 : ⟨i.1, i_in_bounds⟩ ≠ k2 := by
         intro i_eq_k2
         rw [← i_eq_k2] at k2_eq_false
         simp only [List.get_eq_getElem] at k2_eq_false
-        simp [derivedLits_arr_def, Array.getElem_eq_toList_getElem, k2_eq_false, li] at li_eq_true
+        simp [derivedLits_arr_def, Array.getElem_eq_getElem_toList, k2_eq_false, li] at li_eq_true
       have j_ne_k2 : ⟨j.1, j_in_bounds⟩ ≠ k2 := by
         intro j_eq_k2
         rw [← j_eq_k2] at k2_eq_false
         simp only [List.get_eq_getElem] at k2_eq_false
-        simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_toList_getElem] at li_eq_lj
+        simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_getElem_toList] at li_eq_lj
-        simp [derivedLits_arr_def, Array.getElem_eq_toList_getElem, k2_eq_false, li_eq_lj, li] at li_eq_true
+        simp [derivedLits_arr_def, Array.getElem_eq_getElem_toList, k2_eq_false, li_eq_lj, li] at li_eq_true
       by_cases ⟨i.1, i_in_bounds⟩ = k1
       · next i_eq_k1 =>
         have j_ne_k1 : ⟨j.1, j_in_bounds⟩ ≠ k1 := by
@@ -1167,11 +1167,11 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n)
           simp only [Fin.mk.injEq] at i_eq_k1
           exact i_ne_j (Fin.eq_of_val_eq i_eq_k1)
         specialize h3 ⟨j.1, j_in_bounds⟩ j_ne_k1 j_ne_k2
-        simp [li, li_eq_lj, derivedLits_arr_def, Array.getElem_eq_toList_getElem] at h3
+        simp [li, li_eq_lj, derivedLits_arr_def, Array.getElem_eq_getElem_toList] at h3
       · next i_ne_k1 =>
         specialize h3 ⟨i.1, i_in_bounds⟩ i_ne_k1 i_ne_k2
         apply h3
-        simp (config := { decide := true }) only [Fin.getElem_fin, Array.getElem_eq_toList_getElem,
+        simp (config := { decide := true }) only [Fin.getElem_fin, Array.getElem_eq_getElem_toList,
           ne_eq, derivedLits_arr_def, li]
         rfl
     · next li_eq_false =>
@@ -1180,13 +1180,13 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n)
         intro i_eq_k1
         rw [← i_eq_k1] at k1_eq_true
         simp only [List.get_eq_getElem] at k1_eq_true
-        simp [derivedLits_arr_def, Array.getElem_eq_toList_getElem, k1_eq_true, li] at li_eq_false
+        simp [derivedLits_arr_def, Array.getElem_eq_getElem_toList, k1_eq_true, li] at li_eq_false
       have j_ne_k1 : ⟨j.1, j_in_bounds⟩ ≠ k1 := by
         intro j_eq_k1
         rw [← j_eq_k1] at k1_eq_true
         simp only [List.get_eq_getElem] at k1_eq_true
-        simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_toList_getElem] at li_eq_lj
+        simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_getElem_toList] at li_eq_lj
-        simp [derivedLits_arr_def, Array.getElem_eq_toList_getElem, k1_eq_true, li_eq_lj, li] at li_eq_false
+        simp [derivedLits_arr_def, Array.getElem_eq_getElem_toList, k1_eq_true, li_eq_lj, li] at li_eq_false
       by_cases ⟨i.1, i_in_bounds⟩ = k2
       · next i_eq_k2 =>
         have j_ne_k2 : ⟨j.1, j_in_bounds⟩ ≠ k2 := by
@@ -1195,10 +1195,10 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n)
           simp only [Fin.mk.injEq] at i_eq_k2
           exact i_ne_j (Fin.eq_of_val_eq i_eq_k2)
         specialize h3 ⟨j.1, j_in_bounds⟩ j_ne_k1 j_ne_k2
-        simp [li, li_eq_lj, derivedLits_arr_def, Array.getElem_eq_toList_getElem] at h3
+        simp [li, li_eq_lj, derivedLits_arr_def, Array.getElem_eq_getElem_toList] at h3
       · next i_ne_k2 =>
         specialize h3 ⟨i.1, i_in_bounds⟩ i_ne_k1 i_ne_k2
-        simp (config := { decide := true }) [Array.getElem_eq_toList_getElem, derivedLits_arr_def, li] at h3
+        simp (config := { decide := true }) [Array.getElem_eq_getElem_toList, derivedLits_arr_def, li] at h3
 
 theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormula n)
     (f_assignments_size : f.assignments.size = n)
@@ -1232,7 +1232,7 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu
     constructor
     · apply Nat.zero_le
     · constructor
-      · simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_toList_getElem, ← j_eq_i]
+      · simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_getElem_toList, ← j_eq_i]
         rfl
       · apply And.intro h1 ∘ And.intro h2
         intro k _ k_ne_j
@@ -1244,7 +1244,7 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu
           apply Fin.ne_of_val_ne
           simp only
           exact Fin.val_ne_of_ne k_ne_j
-        simp only [Fin.getElem_fin, Array.getElem_eq_toList_getElem, ne_eq, derivedLits_arr_def]
+        simp only [Fin.getElem_fin, Array.getElem_eq_getElem_toList, ne_eq, derivedLits_arr_def]
         exact h3 ⟨k.1, k_in_bounds⟩ k_ne_j
   · apply Or.inr ∘ Or.inr
     have j1_lt_derivedLits_arr_size : j1.1 < derivedLits_arr.size := by
@@ -1258,11 +1258,11 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu
             ⟨j2.1, j2_lt_derivedLits_arr_size⟩,
             i_gt_zero, Nat.zero_le j1.1, Nat.zero_le j2.1, ?_⟩
     constructor
-    · simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_toList_getElem, ← j1_eq_i]
+    · simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_getElem_toList, ← j1_eq_i]
       rw [← j1_eq_true]
       rfl
     · constructor
-      · simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_toList_getElem, ← j2_eq_i]
+      · simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_getElem_toList, ← j2_eq_i]
         rw [← j2_eq_false]
         rfl
       · apply And.intro h1 ∘ And.intro h2
@@ -1279,7 +1279,7 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu
           apply Fin.ne_of_val_ne
           simp only
           exact Fin.val_ne_of_ne k_ne_j2
-        simp only [Fin.getElem_fin, Array.getElem_eq_toList_getElem, ne_eq, derivedLits_arr_def]
+        simp only [Fin.getElem_fin, Array.getElem_eq_getElem_toList, ne_eq, derivedLits_arr_def]
         exact h3 ⟨k.1, k_in_bounds⟩ k_ne_j1 k_ne_j2
 
 theorem restoreAssignments_performRupCheck {n : Nat} (f : DefaultFormula n) (f_assignments_size : f.assignments.size = n)

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

@@ -61,6 +61,8 @@ attribute [bv_normalize] BitVec.getLsbD_zero_length
 attribute [bv_normalize] BitVec.getLsbD_concat_zero
 attribute [bv_normalize] BitVec.mul_one
 attribute [bv_normalize] BitVec.one_mul
+attribute [bv_normalize] BitVec.not_not
+
 
 end Constant
 
@@ -141,11 +143,6 @@ theorem BitVec.mul_zero (a : BitVec w) : a * 0#w = 0#w := by
 theorem BitVec.zero_mul (a : BitVec w) : 0#w * a = 0#w := by
   simp [bv_toNat]
 
-@[bv_normalize]
-theorem BitVec.not_not (a : BitVec w) : ~~~(~~~a) = a := by
-  ext
-  simp
-
 @[bv_normalize]
 theorem BitVec.shiftLeft_zero (n : BitVec w) : n <<< 0#w' = n := by
   ext i

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

@@ -13,16 +13,29 @@ This module contains the `Prop` simplifying part of the `bv_normalize` simp set.
 namespace Std.Tactic.BVDecide
 namespace Frontend.Normalize
 
-attribute [bv_normalize] not_true
+attribute [bv_normalize] ite_true
+attribute [bv_normalize] ite_false
+attribute [bv_normalize] dite_true
+attribute [bv_normalize] dite_false
 attribute [bv_normalize] and_true
 attribute [bv_normalize] true_and
+attribute [bv_normalize] and_false
+attribute [bv_normalize] false_and
 attribute [bv_normalize] or_true
 attribute [bv_normalize] true_or
-attribute [bv_normalize] eq_iff_iff
+attribute [bv_normalize] or_false
+attribute [bv_normalize] false_or
 attribute [bv_normalize] iff_true
 attribute [bv_normalize] true_iff
 attribute [bv_normalize] iff_false
 attribute [bv_normalize] false_iff
+attribute [bv_normalize] false_implies
+attribute [bv_normalize] imp_false
+attribute [bv_normalize] implies_true
+attribute [bv_normalize] true_implies
+attribute [bv_normalize] not_true
+attribute [bv_normalize] not_false_iff
+attribute [bv_normalize] eq_iff_iff
 
 end Frontend.Normalize
 end Std.Tactic.BVDecide

src/Std/Tactic/BVDecide/Reflect.lean

@@ -121,10 +121,6 @@ theorem and_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs)
     (lhs' && rhs') = (lhs && rhs) := by
   simp[*]
 
-theorem or_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
-    (lhs' || rhs') = (lhs || rhs) := by
-  simp[*]
-
 theorem xor_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
     (lhs' ^^ rhs') = (lhs ^^ rhs) := by
   simp[*]

src/lake/Lake/Config/Lang.lean

@@ -10,7 +10,10 @@ inductive ConfigLang
 | lean | toml
 deriving Repr, DecidableEq
 
-instance : Inhabited ConfigLang := ⟨.lean⟩
+/-- Lake's default configuration language. -/
+abbrev ConfigLang.default : ConfigLang := .toml
+
+instance : Inhabited ConfigLang := ⟨.default⟩
 
 def ConfigLang.ofString? : String → Option ConfigLang
 | "lean" => some .lean

src/lake/Lake/Load/Toml.lean

@@ -270,7 +270,7 @@ protected def DependencySrc.decodeToml (t : Table) (ref := Syntax.missing) : Exc
 instance : DecodeToml DependencySrc := ⟨fun v => do DependencySrc.decodeToml (← v.decodeTable) v.ref⟩
 
 protected def Dependency.decodeToml (t : Table) (ref := Syntax.missing) : Except (Array DecodeError) Dependency := ensureDecode do
-  let name  ← stringToLegalOrSimpleName <$> t.tryDecode `name ref
+  let name ← stringToLegalOrSimpleName <$> t.tryDecode `name ref
   let rev? ← t.tryDecode? `rev
   let src? : Option DependencySrc ← id do
     if let some dir ← t.tryDecode? `path then
@@ -316,6 +316,7 @@ def loadTomlConfig (dir relDir relConfigFile : FilePath) : LogIO Package := do
       let leanLibConfigs ← mkRBArray (·.name) <$> table.tryDecodeD `lean_lib #[]
       let leanExeConfigs ← mkRBArray (·.name) <$> table.tryDecodeD `lean_exe #[]
       let defaultTargets ← table.tryDecodeD `defaultTargets #[]
+      let defaultTargets := defaultTargets.map stringToLegalOrSimpleName
       let depConfigs ← table.tryDecodeD `require #[]
       return {
         dir, relDir, relConfigFile

src/lake/README.md

@@ -1,9 +1,9 @@
 # Lake
 
 Lake (Lean Make) is the new build system and package manager for Lean 4.
-With Lake, the package's configuration is written in Lean inside a dedicated `lakefile.lean` stored in the root of the package's directory.
+Lake configurations can be written in Lean or TOML and are conventionally stored in a `lakefile` in the root directory of package.
 
-Each `lakefile.lean` includes a `package` declaration (akin to `main`) which defines the package's basic configuration. It also typically includes build configurations for different targets (e.g., Lean libraries and binary executables) and Lean scripts to run on the command line (via `lake script run`).
+A Lake configuration file defines the package's basic configuration. It also typically includes build configurations for different targets (e.g., Lean libraries and binary executables) and Lean scripts to run on the command line (via `lake script run`).
 
 ***This README provides information about Lake relative to the current commit. If you are looking for documentation for the Lake version shipped with a given Lean release, you should look at the README of that version.***
 
@@ -63,7 +63,7 @@ Hello/         # library source files; accessible via `import Hello.*`
   ...          # additional files should be added here
 Hello.lean     # library root; imports standard modules from Hello
 Main.lean      # main file of the executable (contains `def main`)
-lakefile.lean  # Lake package configuration
+lakefile.toml  # Lake package configuration
 lean-toolchain # the Lean version used by the package
 .gitignore     # excludes system-specific files (e.g. `build`) from Git
 ```
@@ -90,23 +90,21 @@ def main : IO Unit :=
   IO.println s!"Hello, {hello}!"
 ```
 
-Lake also creates a basic `lakefile.lean` for the package along with a `lean-toolchain` file that contains the name of the Lean toolchain Lake belongs to, which tells [`elan`](https://github.com/leanprover/elan) to use that Lean toolchain for the package.
+Lake also creates a basic `lakefile.toml` for the package along with a `lean-toolchain` file that contains the name of the Lean toolchain Lake belongs to, which tells [`elan`](https://github.com/leanprover/elan) to use that Lean toolchain for the package.
 
 
-**lakefile.lean**
+**lakefile.toml**
-```lean
+```toml
-import Lake
+name = "hello"
-open Lake DSL
+version = "0.1.0"
+defaultTargets = ["hello"]
 
-package «hello» where
+[[lean_lib]]
-  -- add package configuration options here
+name = "Hello"
 
-lean_lib «Hello» where
+[[lean_exe]]
-  -- add library configuration options here
+name = "hello"
-
+root = "Main"
-@[default_target]
-lean_exe «hello» where
-  root := `Main
 ```
 
 The command `lake build` is used to build the package (and its [dependencies](#adding-dependencies), if it has them) into a native executable. The result will be placed in `.lake/build/bin`. The command `lake clean` deletes `build`.

src/lake/lakefile.toml

@@ -6,5 +6,5 @@ name = "Lake"
 
 [[lean_exe]]
 name = "lake"
-root = "Lake.Main"
+root = "LakeMain"
 supportInterpreter = true

src/lake/tests/depTree/test.sh

@@ -20,7 +20,7 @@ fi
 # https://github.com/leanprover/lake/issues/119
 
 # a@1/init
-$LAKE new a lib
+$LAKE new a lib.lean
 pushd a
 git checkout -b master
 git add .
@@ -31,7 +31,7 @@ git tag init
 popd
 
 # b@1: require a@master, manifest a@1
-$LAKE new b lib
+$LAKE new b lib.lean
 pushd b
 git checkout -b master
 cat >>lakefile.lean <<EOF
@@ -52,7 +52,7 @@ git commit -am 'second commit in a'
 popd
 
 # c@1: require a@master, manifest a@2
-$LAKE new c lib
+$LAKE new c lib.lean
 pushd c
 git checkout -b master
 cat >>lakefile.lean <<EOF
@@ -67,7 +67,7 @@ git commit -am 'first commit in c'
 popd
 
 # d@1: require b@master c@master => a, manifest a@1 b@1 c@1
-$LAKE new d lib
+$LAKE new d lib.lean
 pushd d
 git checkout -b master
 cat >>lakefile.lean <<EOF

src/lake/tests/init/test.sh

@@ -38,7 +38,7 @@ done
 
 # Test default (std) template
 
-$LAKE new hello
+$LAKE new hello .lean
 $LAKE -d hello exe hello
 test -f hello/.lake/build/lib/Hello.olean
 rm -rf hello
@@ -49,7 +49,7 @@ rm -rf hello
 
 # Test exe template
 
-$LAKE new hello exe
+$LAKE new hello exe.lean
 test -f hello/Main.lean
 $LAKE -d hello exe hello
 rm -rf hello
@@ -60,7 +60,7 @@ rm -rf hello
 
 # Test lib template
 
-$LAKE new hello lib
+$LAKE new hello lib.lean
 $LAKE -d hello build Hello
 test -f hello/.lake/build/lib/Hello.olean
 rm -rf hello
@@ -71,7 +71,7 @@ rm -rf hello
 
 # Test math template
 
-$LAKE new qed math || true # ignore toolchain download errors
+$LAKE new qed math.lean || true # ignore toolchain download errors
 # Remove the require, since we do not wish to download mathlib during tests
 sed_i '/^require.*/{N;d;}' qed/lakefile.lean
 $LAKE -d qed build Qed

src/util/shell.cpp

@@ -362,7 +362,7 @@ pair_ref<environment, object_ref> run_new_frontend(
     name const & main_module_name,
     uint32_t trust_level,
     optional<std::string> const & ilean_file_name,
-    uint8_t json
+    uint8_t json_output
 ) {
     object * oilean_file_name = mk_option_none();
     if (ilean_file_name) {