chore: fix Array.modify lemmas

Closes #2710

.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,24 @@ 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]
+
+@[simp] theorem Functor.map_unit [Monad m] [LawfulMonad m] {a : m PUnit} : (fun _ => PUnit.unit) <$> a = a := by
+  simp [map]
 
 /--
 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
@@ -84,6 +84,11 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (ExceptT ε m) where
   pure_bind      := by intros; apply ext; simp [run_bind]
   bind_assoc     := by intros; apply ext; simp [run_bind]; apply bind_congr; intro a; cases a <;> simp
 
+@[simp] theorem map_throw [Monad m] [LawfulMonad m] {α β : Type _} (f : α → β) (e : ε) :
+    f <$> (throw e : ExceptT ε m α) = (throw e : ExceptT ε m β) := by
+  simp only [ExceptT.instMonad, ExceptT.map, ExceptT.mk, throw, throwThe, MonadExceptOf.throw,
+    pure_bind]
+
 end ExceptT
 
 /-! # Except -/
@@ -175,7 +180,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 +215,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 +229,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/Basic.lean

@@ -810,11 +810,27 @@ def split (as : Array α) (p : α → Bool) : Array α × Array α :=
   as.foldl (init := (#[], #[])) fun (as, bs) a =>
     if p a then (as.push a, bs) else (as, bs.push a)
 
-/-! ### Auxiliary functions used in metaprogramming.
+/-! ## Auxiliary functions used in metaprogramming.
 
 We do not intend to provide verification theorems for these functions.
 -/
 
+/-! ### eraseReps -/
+
+/--
+`O(|l|)`. Erase repeated adjacent elements. Keeps the first occurrence of each run.
+* `eraseReps #[1, 3, 2, 2, 2, 3, 5] = #[1, 3, 2, 3, 5]`
+-/
+def eraseReps {α} [BEq α] (as : Array α) : Array α :=
+  if h : 0 < as.size then
+    let ⟨last, r⟩ := as.foldl (init := (as[0], #[])) fun ⟨last, r⟩ a =>
+      if a == last then ⟨last, r⟩ else ⟨a, r.push last⟩
+    r.push last
+  else
+    #[]
+
+/-! ### allDiff -/
+
 private def allDiffAuxAux [BEq α] (as : Array α) (a : α) : forall (i : Nat), i < as.size → Bool
   | 0,   _ => true
   | i+1, h =>
@@ -832,6 +848,8 @@ decreasing_by simp_wf; decreasing_trivial_pre_omega
 def allDiff [BEq α] (as : Array α) : Bool :=
   allDiffAux as 0
 
+/-! ### getEvenElems -/
+
 @[inline] def getEvenElems (as : Array α) : Array α :=
   (·.2) <| as.foldl (init := (true, Array.empty)) fun (even, r) a =>
     if even then

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]
-  rw [List.getElem_append_right] <;> simp [getElem_eq_toList_getElem, Nat.zero_lt_one]
+  simp only [push, getElem_eq_getElem_toList, List.concat_eq_append]
+  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
@@ -57,9 +79,7 @@ open Array
 
 /-! ### Lemmas about `List.toArray`. -/
 
-@[simp] theorem toArray_size (as : List α) : as.toArray.size = as.length := by simp [size]
-
-@[simp] theorem toArrayAux_size {a : List α} {b : Array α} :
+@[simp] theorem size_toArrayAux {a : List α} {b : Array α} :
     (a.toArrayAux b).size = b.size + a.length := by
   simp [size]
 
@@ -67,14 +87,42 @@ open Array
 
 @[deprecated toArray_toList (since := "2024-09-09")]
 abbrev toArray_data := @toArray_toList
+
 @[simp] theorem getElem_toArray {a : List α} {i : Nat} (h : i < a.toArray.size) :
     a.toArray[i] = a[i]'(by simpa using h) := rfl
 
-@[simp] theorem 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 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
@@ -88,10 +136,10 @@ attribute [simp] uset
 @[deprecated toArray_toList (since := "2024-09-09")]
 abbrev toArray_data := @toArray_toList
 
-@[simp] theorem toList_length {l : Array α} : l.toList.length = l.size := rfl
+@[simp] theorem length_toList {l : Array α} : l.toList.length = l.size := rfl
 
-@[deprecated toList_length (since := "2024-09-09")]
-abbrev data_length := @toList_length
+@[deprecated length_toList (since := "2024-09-09")]
+abbrev data_length := @length_toList
 
 @[simp] theorem mkEmpty_eq (α n) : @mkEmpty α n = #[] := rfl
 
@@ -127,25 +175,25 @@ where
       mapM.map f arr i r = (arr.toList.drop i).foldlM (fun bs a => bs.push <$> f a) r := by
     unfold mapM.map; split
     · rw [← List.get_drop_eq_drop _ i ‹_›]
-      simp only [aux (i + 1), map_eq_pure_bind, toList_length, List.foldlM_cons, bind_assoc,
+      simp only [aux (i + 1), map_eq_pure_bind, length_toList, List.foldlM_cons, bind_assoc,
         pure_bind]
       rfl
     · rw [List.drop_of_length_le (Nat.ge_of_not_lt ‹_›)]; rfl
   termination_by arr.size - i
   decreasing_by decreasing_trivial_pre_omega
 
-@[simp] theorem map_toList (f : α → β) (arr : Array α) : (arr.map f).toList = arr.toList.map f := by
+@[simp] theorem toList_map (f : α → β) (arr : Array α) : (arr.map f).toList = arr.toList.map f := by
   rw [map, mapM_eq_foldlM]
   apply congrArg toList (foldl_eq_foldl_toList (fun bs a => push bs (f a)) #[] arr) |>.trans
   have H (l arr) : List.foldl (fun bs a => push bs (f a)) arr l = ⟨arr.toList ++ l.map f⟩ := by
     induction l generalizing arr <;> simp [*]
   simp [H]
 
-@[deprecated map_toList (since := "2024-09-09")]
-abbrev map_data := @map_toList
+@[deprecated toList_map (since := "2024-09-09")]
+abbrev map_data := @toList_map
 
 @[simp] theorem size_map (f : α → β) (arr : Array α) : (arr.map f).size = arr.size := by
-  simp only [← toList_length]
+  simp only [← length_toList]
   simp
 
 @[simp] theorem appendList_nil (arr : Array α) : arr ++ ([] : List α) = arr := Array.ext' (by simp)
@@ -153,6 +201,11 @@ abbrev map_data := @map_toList
 @[simp] theorem appendList_cons (arr : Array α) (a : α) (l : List α) :
     arr ++ (a :: l) = arr.push a ++ l := Array.ext' (by simp)
 
+@[simp] theorem toList_appendList (arr : Array α) (l : List α) :
+    (arr ++ l).toList = arr.toList ++ l := by
+  cases arr
+  simp
+
 theorem foldl_toList_eq_bind (l : List α) (acc : Array β)
     (F : Array β → α → Array β) (G : α → List β)
     (H : ∀ acc a, (F acc a).toList = acc.toList ++ G a) :
@@ -221,11 +274,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) :
@@ -244,14 +297,14 @@ theorem getElem_set (a : Array α) (i : Fin a.size) (v : α) (j : Nat)
 @[simp] theorem set!_is_setD : @set! = @setD := rfl
 
 @[simp] theorem size_setD (a : Array α) (index : Nat) (val : α) :
-  (Array.setD a index val).size = a.size := by
+    (Array.setD a index val).size = a.size := by
   if h : index < a.size  then
     simp [setD, h]
   else
     simp [setD, h]
 
 @[simp] theorem getElem_setD_eq (a : Array α) {i : Nat} (v : α) (h : _) :
-  (setD a i v)[i]'h = v := by
+    (setD a i v)[i]'h = v := by
   simp at h
   simp only [setD, h, dite_true, getElem_set, ite_true]
 
@@ -261,7 +314,7 @@ theorem getElem?_setD_eq (a : Array α) {i : Nat} (p : i < a.size) (v : α) : (a
 
 /-- Simplifies a normal form from `get!` -/
 @[simp] theorem getD_get?_setD (a : Array α) (i : Nat) (v d : α) :
-  Option.getD (setD a i v)[i]? d = if i < a.size then v else d := by
+    Option.getD (setD a i v)[i]? d = if i < a.size then v else d := by
   by_cases h : i < a.size <;>
     simp [setD, Nat.not_lt_of_le, h,  getD_get?]
 
@@ -315,7 +368,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 -/
 
@@ -356,7 +409,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
@@ -367,24 +420,27 @@ 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
 
+theorem getElem?_eq_toList_getElem? (a : Array α) (i : Nat) : a[i]? = a.toList[i]? := by
+  by_cases i < a.size <;> simp_all [getElem?_pos, getElem?_neg]
+
+@[deprecated getElem?_eq_toList_getElem? (since := "2024-09-30")]
 theorem getElem?_eq_toList_get? (a : Array α) (i : Nat) : a[i]? = a.toList.get? i := by
   by_cases i < a.size <;> simp_all [getElem?_pos, getElem?_neg, List.get?_eq_get, eq_comm]
 
-@[deprecated getElem?_eq_toList_get? (since := "2024-09-09")]
+set_option linter.deprecated false in
+@[deprecated getElem?_eq_toList_getElem? (since := "2024-09-09")]
 abbrev getElem?_eq_data_get? := @getElem?_eq_toList_get?
 
+set_option linter.deprecated false in
 theorem get?_eq_toList_get? (a : Array α) (i : Nat) : a.get? i = a.toList.get? i :=
   getElem?_eq_toList_get? ..
 
@@ -398,7 +454,7 @@ theorem get!_eq_get? [Inhabited α] (a : Array α) : a.get! n = (a.get? n).getD
   simp [back, back?]
 
 @[simp] theorem back?_push (a : Array α) : (a.push x).back? = some x := by
-  simp [back?, getElem?_eq_toList_get?]
+  simp [back?, getElem?_eq_toList_getElem?]
 
 theorem back_push [Inhabited α] (a : Array α) : (a.push x).back = x := by simp
 
@@ -434,7 +490,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]
@@ -453,10 +509,10 @@ 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
+    (setD a i v)[i] = v := by
   simp at h
   simp only [setD, h, dite_true, get_set, ite_true]
 
@@ -469,7 +525,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")]
@@ -482,7 +538,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]
 
@@ -555,14 +611,14 @@ 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
+@[simp] theorem toList_reverse (a : Array α) : a.reverse.toList = a.toList.reverse := by
   let rec go (as : Array α) (i j hj)
       (h : i + j + 1 = a.size) (h₂ : as.size = a.size)
-      (H : ∀ k, as.toList.get? k = if i ≤ k ∧ k ≤ j then a.toList.get? k else a.toList.reverse.get? k)
-      (k) : (reverse.loop as i ⟨j, hj⟩).toList.get? k = a.toList.reverse.get? k := by
+      (H : ∀ k, as.toList[k]? = if i ≤ k ∧ k ≤ j then a.toList[k]? else a.toList.reverse[k]?)
+      (k : Nat) : (reverse.loop as i ⟨j, hj⟩).toList[k]? = a.toList.reverse[k]? := by
     rw [reverse.loop]; dsimp; split <;> rename_i h₁
     · match j with | j+1 => ?_
       simp only [Nat.add_sub_cancel]
@@ -570,37 +626,66 @@ set_option linter.deprecated false in
       · rwa [Nat.add_right_comm i]
       · simp [size_swap, h₂]
       · intro k
-        rw [← getElem?_eq_toList_get?, get?_swap]
-        simp only [H, getElem_eq_toList_get, ← List.get?_eq_get, Nat.le_of_lt h₁,
-          getElem?_eq_toList_get?]
+        rw [← getElem?_eq_toList_getElem?, get?_swap]
+        simp only [H, getElem_eq_getElem_toList, ← List.getElem?_eq_getElem, Nat.le_of_lt h₁,
+          getElem?_eq_toList_getElem?]
         split <;> rename_i h₂
         · simp only [← h₂, Nat.not_le.2 (Nat.lt_succ_self _), Nat.le_refl, and_false]
-          exact (List.get?_reverse' (j+1) i (Eq.trans (by simp_arith) h)).symm
+          exact (List.getElem?_reverse' (j+1) i (Eq.trans (by simp_arith) h)).symm
         split <;> rename_i h₃
         · simp only [← h₃, Nat.not_le.2 (Nat.lt_succ_self _), Nat.le_refl, false_and]
-          exact (List.get?_reverse' i (j+1) (Eq.trans (by simp_arith) h)).symm
+          exact (List.getElem?_reverse' i (j+1) (Eq.trans (by simp_arith) h)).symm
         simp only [Nat.succ_le, Nat.lt_iff_le_and_ne.trans (and_iff_left h₃),
           Nat.lt_succ.symm.trans (Nat.lt_iff_le_and_ne.trans (and_iff_left (Ne.symm h₂)))]
     · rw [H]; split <;> rename_i h₂
       · cases Nat.le_antisymm (Nat.not_lt.1 h₁) (Nat.le_trans h₂.1 h₂.2)
         cases Nat.le_antisymm h₂.1 h₂.2
-        exact (List.get?_reverse' _ _ h).symm
+        exact (List.getElem?_reverse' _ _ h).symm
       · rfl
     termination_by j - i
   simp only [reverse]
   split
   · match a with | ⟨[]⟩ | ⟨[_]⟩ => rfl
   · have := Nat.sub_add_cancel (Nat.le_of_not_le ‹_›)
-    refine List.ext_get? <| go _ _ _ _ (by simp [this]) rfl fun k => ?_
+    refine List.ext_getElem? <| go _ _ _ _ (by simp [this]) rfl fun k => ?_
     split
     · rfl
     · rename_i h
       simp only [← show k < _ + 1 ↔ _ from Nat.lt_succ (n := a.size - 1), this, Nat.zero_le,
         true_and, Nat.not_lt] at h
-      rw [List.get?_eq_none.2 ‹_›, List.get?_eq_none.2 (a.toList.length_reverse ▸ ‹_›)]
+      rw [List.getElem?_eq_none_iff.2 ‹_›, List.getElem?_eq_none_iff.2 (a.toList.length_reverse ▸ ‹_›)]
+
+@[deprecated toList_reverse (since := "2024-09-30")]
+abbrev reverse_toList := @toList_reverse
 
 /-! ### foldl / foldr -/
 
+@[simp] theorem foldlM_loop_empty [Monad m] (f : β → α → m β) (init : β) (i j : Nat) :
+    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
@@ -637,7 +722,7 @@ theorem foldr_induction
 /-! ### map -/
 
 @[simp] theorem mem_map {f : α → β} {l : Array α} : b ∈ l.map f ↔ ∃ a, a ∈ l ∧ f a = b := by
-  simp only [mem_def, map_toList, List.mem_map]
+  simp only [mem_def, toList_map, List.mem_map]
 
 theorem mapM_eq_mapM_toList [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) :
     arr.mapM f = return mk (← arr.toList.mapM f) := by
@@ -645,7 +730,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
@@ -762,31 +847,31 @@ theorem mapIdx_spec (as : Array α) (f : Fin as.size → α → β)
   unfold modify modifyM Id.run
   split <;> simp
 
-theorem getElem_modify {as : Array α} {x i} (h : i < as.size) :
-    (as.modify x f)[i]'(by simp [h]) = if x = i then f as[i] else as[i] := by
+theorem getElem_modify {as : Array α} {x i} (h : i < (as.modify x f).size) :
+    (as.modify x f)[i] = if x = i then f (as[i]'(by simpa using h)) else as[i]'(by simpa using h) := by
   simp only [modify, modifyM, get_eq_getElem, Id.run, Id.pure_eq]
   split
-  · simp only [Id.bind_eq, get_set _ _ _ h]; split <;> simp [*]
-  · rw [if_neg (mt (by rintro rfl; exact h) ‹_›)]
+  · simp only [Id.bind_eq, get_set _ _ _ (by simpa using h)]; split <;> simp [*]
+  · rw [if_neg (mt (by rintro rfl; exact h) (by simp_all))]
 
-theorem getElem_modify_self {as : Array α} {i : Nat} (h : i < as.size) (f : α → α) :
-    (as.modify i f)[i]'(by simp [h]) = f as[i] := by
+theorem getElem_modify_self {as : Array α} {i : Nat} (f : α → α) (h : i < (as.modify i f).size) :
+    (as.modify i f)[i] = f (as[i]'(by simpa using h)) := by
   simp [getElem_modify h]
 
-theorem getElem_modify_of_ne {as : Array α} {i : Nat} (hj : j < as.size)
-    (f : α → α) (h : i ≠ j) :
-    (as.modify i f)[j]'(by rwa [size_modify]) = as[j] := by
+theorem getElem_modify_of_ne {as : Array α} {i : Nat} (h : i ≠ j)
+    (f : α → α) (hj : j < (as.modify i f).size) :
+    (as.modify i f)[j] = as[j]'(by simpa using hj) := by
   simp [getElem_modify hj, h]
 
 @[deprecated getElem_modify (since := "2024-08-08")]
-theorem get_modify {arr : Array α} {x i} (h : i < arr.size) :
-    (arr.modify x f).get ⟨i, by simp [h]⟩ =
-    if x = i then f (arr.get ⟨i, h⟩) else arr.get ⟨i, h⟩ := by
+theorem get_modify {arr : Array α} {x i} (h : i < (arr.modify x f).size) :
+    (arr.modify x f).get ⟨i, h⟩ =
+    if x = i then f (arr.get ⟨i, by simpa using h⟩) else arr.get ⟨i, by simpa using h⟩ := by
   simp [getElem_modify h]
 
 /-! ### filter -/
 
-@[simp] theorem 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]
@@ -797,23 +882,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")]
-abbrev filter_data := @filter_toList
+@[deprecated toList_filter (since := "2024-09-09")]
+abbrev filter_data := @toList_filter
 
 @[simp] theorem filter_filter (q) (l : Array α) :
     filter p (filter q l) = filter (fun a => p a && q a) l := by
   apply ext'
-  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]
@@ -826,12 +911,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")]
-abbrev filterMap_data := @filterMap_toList
+@[deprecated toList_filterMap (since := "2024-09-09")]
+abbrev filterMap_data := @toList_filterMap
 
 @[simp] theorem mem_filterMap {f : α → Option β} {l : Array α} {b : β} :
     b ∈ filterMap f l ↔ ∃ a, a ∈ l ∧ f a = some b := by
-  simp only [mem_def, filterMap_toList, List.mem_filterMap]
+  simp only [mem_def, toList_filterMap, List.mem_filterMap]
 
 /-! ### empty -/
 
@@ -854,16 +939,16 @@ 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]
-  have h' : i < (as.toList ++ bs.toList).length := by rwa [← toList_length, append_toList] at h
+  simp only [getElem_eq_getElem_toList]
+  have h' : i < (as.toList ++ bs.toList).length := by rwa [← length_toList, append_toList] at h
   conv => rhs; rw [← List.getElem_append_left (bs := bs.toList) (h' := h')]
   apply List.get_of_eq; rw [append_toList]
 
 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]
-  have h' : i < (as.toList ++ bs.toList).length := by rwa [← toList_length, append_toList] at h
+  simp only [getElem_eq_getElem_toList]
+  have h' : i < (as.toList ++ bs.toList).length := by rwa [← length_toList, append_toList] at h
   conv => rhs; rw [← List.getElem_append_right (h₁ := hle) (h₂ := h')]
   apply List.get_of_eq; rw [append_toList]
 
@@ -1010,6 +1095,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 ↔
@@ -1054,6 +1166,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]
@@ -1075,10 +1198,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]
@@ -1150,3 +1273,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/QSort.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Data.Array.Basic
+import Init.Data.Ord
 
 namespace Array
 -- TODO: remove the [Inhabited α] parameters as soon as we have the tactic framework for automating proof generation and using Array.fget
@@ -44,4 +45,11 @@ def qpartition (as : Array α) (lt : α → α → Bool) (lo hi : Nat) : Nat ×
     else as
   sort as low high
 
+set_option linter.unusedVariables.funArgs false in
+/--
+Sort an array using `compare` to compare elements.
+-/
+def qsortOrd [ord : Ord α] (xs : Array α) : Array α :=
+  xs.qsort fun x y => compare x y |>.isLT
+
 end Array

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
-modulo `2^n`.
+Multiplication for bit vectors. This can be interpreted as either signed or unsigned
+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,385 @@ 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 ..)
+
+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 [w]
+      · simp only [decide_eq_false_iff_not, Nat.not_lt] at 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]
-  rw [Nat.testBit_shiftLeft]
+  simp only [getLsbD, toNat_cons, Nat.testBit_or, Nat.testBit_shiftLeft, ge_iff_le]
   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/Float.lean

@@ -72,21 +72,35 @@ instance floatDecLt (a b : Float) : Decidable (a < b) := Float.decLt a b
 instance floatDecLe (a b : Float) : Decidable (a ≤ b) := Float.decLe a b
 
 @[extern "lean_float_to_string"] opaque Float.toString : Float → String
-
-/-- If the given float is positive, truncates the value to the nearest positive integer.
-If negative or larger than the maximum value for UInt8, returns 0. -/
+/-- If the given float is non-negative, truncates the value to the nearest non-negative integer.
+If negative or NaN, returns 0.
+If larger than the maximum value for UInt8 (including Inf), returns maximum value of UInt8
+(i.e. UInt8.size - 1).
+-/
 @[extern "lean_float_to_uint8"] opaque Float.toUInt8 : Float → UInt8
-/-- If the given float is positive, truncates the value to the nearest positive integer.
-If negative or larger than the maximum value for UInt16, returns 0. -/
+/-- If the given float is non-negative, truncates the value to the nearest non-negative integer.
+If negative or NaN, returns 0.
+If larger than the maximum value for UInt16 (including Inf), returns maximum value of UInt16
+(i.e. UInt16.size - 1).
+-/
 @[extern "lean_float_to_uint16"] opaque Float.toUInt16 : Float → UInt16
-/-- If the given float is positive, truncates the value to the nearest positive integer.
-If negative or larger than the maximum value for UInt32, returns 0. -/
+/-- If the given float is non-negative, truncates the value to the nearest non-negative integer.
+If negative or NaN, returns 0.
+If larger than the maximum value for UInt32 (including Inf), returns maximum value of UInt32
+(i.e. UInt32.size - 1).
+-/
 @[extern "lean_float_to_uint32"] opaque Float.toUInt32 : Float → UInt32
-/-- If the given float is positive, truncates the value to the nearest positive integer.
-If negative or larger than the maximum value for UInt64, returns 0. -/
+/-- If the given float is non-negative, truncates the value to the nearest non-negative integer.
+If negative or NaN, returns 0.
+If larger than the maximum value for UInt64 (including Inf), returns maximum value of UInt64
+(i.e. UInt64.size - 1).
+-/
 @[extern "lean_float_to_uint64"] opaque Float.toUInt64 : Float → UInt64
-/-- If the given float is positive, truncates the value to the nearest positive integer.
-If negative or larger than the maximum value for USize, returns 0. -/
+/-- If the given float is non-negative, truncates the value to the nearest non-negative integer.
+If negative or NaN, returns 0.
+If larger than the maximum value for USize (including Inf), returns maximum value of USize
+(i.e. USize.size - 1;  Note that this value is platform dependent).
+-/
 @[extern "lean_float_to_usize"] opaque Float.toUSize : Float → USize
 
 @[extern "lean_float_isnan"] opaque Float.isNaN : Float → Bool

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/Basic.lean

@@ -43,7 +43,7 @@ The operations are organized as follow:
 * Logic: `any`, `all`, `or`, and `and`.
 * Zippers: `zipWith`, `zip`, `zipWithAll`, and `unzip`.
 * Ranges and enumeration: `range`, `iota`, `enumFrom`, and `enum`.
-* Minima and maxima: `minimum?` and `maximum?`.
+* Minima and maxima: `min?` and `max?`.
 * Other functions: `intersperse`, `intercalate`, `eraseDups`, `eraseReps`, `span`, `groupBy`,
   `removeAll`
   (currently these functions are mostly only used in meta code,
@@ -1464,30 +1464,34 @@ def enum : List α → List (Nat × α) := enumFrom 0
 
 /-! ## Minima and maxima -/
 
-/-! ### minimum? -/
+/-! ### min? -/
 
 /--
 Returns the smallest element of the list, if it is not empty.
-* `[].minimum? = none`
-* `[4].minimum? = some 4`
-* `[1, 4, 2, 10, 6].minimum? = some 1`
+* `[].min? = none`
+* `[4].min? = some 4`
+* `[1, 4, 2, 10, 6].min? = some 1`
 -/
-def minimum? [Min α] : List α → Option α
+def min? [Min α] : List α → Option α
   | []    => none
   | a::as => some <| as.foldl min a
 
-/-! ### maximum? -/
+@[inherit_doc min?, deprecated min? (since := "2024-09-29")] abbrev minimum? := @min?
+
+/-! ### max? -/
 
 /--
 Returns the largest element of the list, if it is not empty.
-* `[].maximum? = none`
-* `[4].maximum? = some 4`
-* `[1, 4, 2, 10, 6].maximum? = some 10`
+* `[].max? = none`
+* `[4].max? = some 4`
+* `[1, 4, 2, 10, 6].max? = some 10`
 -/
-def maximum? [Max α] : List α → Option α
+def max? [Max α] : List α → Option α
   | []    => none
   | a::as => some <| as.foldl max a
 
+@[inherit_doc max?, deprecated max? (since := "2024-09-29")] abbrev maximum? := @max?
+
 /-! ## Other list operations
 
 The functions are currently mostly used in meta code,

src/Init/Data/List/Impl.lean

@@ -31,7 +31,7 @@ The following operations are still missing `@[csimp]` replacements:
 The following operations are not recursive to begin with
 (or are defined in terms of recursive primitives):
 `isEmpty`, `isSuffixOf`, `isSuffixOf?`, `rotateLeft`, `rotateRight`, `insert`, `zip`, `enum`,
-`minimum?`, `maximum?`, and `removeAll`.
+`min?`, `max?`, and `removeAll`.
 
 The following operations were already given `@[csimp]` replacements in `Init/Data/List/Basic.lean`:
 `length`, `map`, `filter`, `replicate`, `leftPad`, `unzip`, `range'`, `iota`, `intersperse`.

src/Init/Data/List/Lemmas.lean

@@ -55,7 +55,7 @@ See also
 * `Init.Data.List.Erase` for lemmas about `List.eraseP` and `List.erase`.
 * `Init.Data.List.Find` for lemmas about `List.find?`, `List.findSome?`, `List.findIdx`,
   `List.findIdx?`, and `List.indexOf`
-* `Init.Data.List.MinMax` for lemmas about `List.minimum?` and `List.maximum?`.
+* `Init.Data.List.MinMax` for lemmas about `List.min?` and `List.max?`.
 * `Init.Data.List.Pairwise` for lemmas about `List.Pairwise` and `List.Nodup`.
 * `Init.Data.List.Sublist` for lemmas about `List.Subset`, `List.Sublist`, `List.IsPrefix`,
   `List.IsSuffix`, and `List.IsInfix`.
@@ -203,6 +203,9 @@ theorem get?_eq_none : l.get? n = none ↔ length l ≤ n :=
 
 @[simp] theorem get_eq_getElem (l : List α) (i : Fin l.length) : l.get i = l[i.1]'i.2 := rfl
 
+theorem getElem?_eq_some {l : List α} : l[i]? = some a ↔ ∃ h : i < l.length, l[i]'h = a := by
+  simpa using get?_eq_some
+
 /--
 If one has `l.get i` in an expression (with `i : Fin l.length`) and `h : l = l'`,
 `rw [h]` will give a "motive it not type correct" error, as it cannot rewrite the
@@ -489,7 +492,7 @@ theorem getElem?_of_mem {a} {l : List α} (h : a ∈ l) : ∃ n : Nat, l[n]? = s
 theorem get?_of_mem {a} {l : List α} (h : a ∈ l) : ∃ n, l.get? n = some a :=
   let ⟨⟨n, _⟩, e⟩ := get_of_mem h; ⟨n, e ▸ get?_eq_get _⟩
 
-theorem getElem_mem : ∀ {l : List α} {n} (h : n < l.length), l[n]'h ∈ l
+@[simp] theorem getElem_mem : ∀ {l : List α} {n} (h : n < l.length), l[n]'h ∈ l
   | _ :: _, 0, _ => .head ..
   | _ :: l, _+1, _ => .tail _ (getElem_mem (l := l) ..)
 
@@ -878,6 +881,20 @@ theorem foldr_map' {α β : Type u} (g : α → β) (f : α → α → α) (f' :
   · simp
   · simp [*, h]
 
+theorem foldl_assoc {op : α → α → α} [ha : Std.Associative op] :
+    ∀ {l : List α} {a₁ a₂}, l.foldl op (op a₁ a₂) = op a₁ (l.foldl op a₂)
+  | [], a₁, a₂ => rfl
+  | a :: l, a₁, a₂ => by
+    simp only [foldl_cons, ha.assoc]
+    rw [foldl_assoc]
+
+theorem foldr_assoc {op : α → α → α} [ha : Std.Associative op] :
+    ∀ {l : List α} {a₁ a₂}, l.foldr op (op a₁ a₂) = op (l.foldr op a₁) a₂
+  | [], a₁, a₂ => rfl
+  | a :: l, a₁, a₂ => by
+    simp only [foldr_cons, ha.assoc]
+    rw [foldr_assoc]
+
 theorem foldl_hom (f : α₁ → α₂) (g₁ : α₁ → β → α₁) (g₂ : α₂ → β → α₂) (l : List β) (init : α₁)
     (H : ∀ x y, g₂ (f x) y = f (g₁ x y)) : l.foldl g₂ (f init) = f (l.foldl g₁ init) := by
   induction l generalizing init <;> simp [*, H]
@@ -1004,7 +1021,7 @@ theorem getLast_eq_getLastD (a l h) : @getLast α (a::l) h = getLastD l a := by
 theorem getLast!_cons [Inhabited α] : @getLast! α _ (a::l) = getLastD l a := by
   simp [getLast!, getLast_eq_getLastD]
 
-theorem getLast_mem : ∀ {l : List α} (h : l ≠ []), getLast l h ∈ l
+@[simp] theorem getLast_mem : ∀ {l : List α} (h : l ≠ []), getLast l h ∈ l
   | [], h => absurd rfl h
   | [_], _ => .head ..
   | _::a::l, _ => .tail _ <| getLast_mem (cons_ne_nil a l)
@@ -1102,7 +1119,7 @@ theorem head?_eq_some_iff {xs : List α} {a : α} : xs.head? = some a ↔ ∃ ys
 @[simp] theorem head?_isSome : l.head?.isSome ↔ l ≠ [] := by
   cases l <;> simp
 
-theorem head_mem : ∀ {l : List α} (h : l ≠ []), head l h ∈ l
+@[simp] theorem head_mem : ∀ {l : List α} (h : l ≠ []), head l h ∈ l
   | [], h => absurd rfl h
   | _::_, _ => .head ..
 
@@ -1654,6 +1671,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'
@@ -2387,11 +2409,21 @@ theorem map_eq_replicate_iff {l : List α} {f : α → β} {b : β} :
 @[simp] theorem map_const (l : List α) (b : β) : map (Function.const α b) l = replicate l.length b :=
   map_eq_replicate_iff.mpr fun _ _ => rfl
 
+@[simp] theorem map_const_fun (x : β) : map (Function.const α x) = (replicate ·.length x) := by
+  funext l
+  simp
+
 /-- Variant of `map_const` using a lambda rather than `Function.const`. -/
 -- This can not be a `@[simp]` lemma because it would fire on every `List.map`.
 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/MinMax.lean

@@ -7,7 +7,7 @@ prelude
 import Init.Data.List.Lemmas
 
 /-!
-# Lemmas about `List.minimum?` and `List.maximum?.
+# Lemmas about `List.min?` and `List.max?.
 -/
 
 namespace List
@@ -16,24 +16,24 @@ open Nat
 
 /-! ## Minima and maxima -/
 
-/-! ### minimum? -/
+/-! ### min? -/
 
-@[simp] theorem minimum?_nil [Min α] : ([] : List α).minimum? = none := rfl
+@[simp] theorem min?_nil [Min α] : ([] : List α).min? = none := rfl
 
--- We don't put `@[simp]` on `minimum?_cons`,
+-- We don't put `@[simp]` on `min?_cons`,
 -- because the definition in terms of `foldl` is not useful for proofs.
-theorem minimum?_cons [Min α] {xs : List α} : (x :: xs).minimum? = foldl min x xs := rfl
+theorem min?_cons [Min α] {xs : List α} : (x :: xs).min? = foldl min x xs := rfl
 
-@[simp] theorem minimum?_eq_none_iff {xs : List α} [Min α] : xs.minimum? = none ↔ xs = [] := by
-  cases xs <;> simp [minimum?]
+@[simp] theorem min?_eq_none_iff {xs : List α} [Min α] : xs.min? = none ↔ xs = [] := by
+  cases xs <;> simp [min?]
 
-theorem minimum?_mem [Min α] (min_eq_or : ∀ a b : α, min a b = a ∨ min a b = b) :
-    {xs : List α} → xs.minimum? = some a → a ∈ xs := by
+theorem min?_mem [Min α] (min_eq_or : ∀ a b : α, min a b = a ∨ min a b = b) :
+    {xs : List α} → xs.min? = some a → a ∈ xs := by
   intro xs
   match xs with
   | nil => simp
   | x :: xs =>
-    simp only [minimum?_cons, Option.some.injEq, List.mem_cons]
+    simp only [min?_cons, Option.some.injEq, List.mem_cons]
     intro eq
     induction xs generalizing x with
     | nil =>
@@ -49,12 +49,12 @@ theorem minimum?_mem [Min α] (min_eq_or : ∀ a b : α, min a b = a ∨ min a b
 
 -- See also `Init.Data.List.Nat.Basic` for specialisations of the next two results to `Nat`.
 
-theorem le_minimum?_iff [Min α] [LE α]
+theorem le_min?_iff [Min α] [LE α]
     (le_min_iff : ∀ a b c : α, a ≤ min b c ↔ a ≤ b ∧ a ≤ c) :
-    {xs : List α} → xs.minimum? = some a → ∀ {x}, x ≤ a ↔ ∀ b, b ∈ xs → x ≤ b
+    {xs : List α} → xs.min? = some a → ∀ {x}, x ≤ a ↔ ∀ b, b ∈ xs → x ≤ b
   | nil => by simp
   | cons x xs => by
-    rw [minimum?]
+    rw [min?]
     intro eq y
     simp only [Option.some.injEq] at eq
     induction xs generalizing x with
@@ -67,46 +67,46 @@ theorem le_minimum?_iff [Min α] [LE α]
 
 -- This could be refactored by designing appropriate typeclasses to replace `le_refl`, `min_eq_or`,
 -- and `le_min_iff`.
-theorem minimum?_eq_some_iff [Min α] [LE α] [anti : Antisymm ((· : α) ≤ ·)]
+theorem min?_eq_some_iff [Min α] [LE α] [anti : Antisymm ((· : α) ≤ ·)]
     (le_refl : ∀ a : α, a ≤ a)
     (min_eq_or : ∀ a b : α, min a b = a ∨ min a b = b)
     (le_min_iff : ∀ a b c : α, a ≤ min b c ↔ a ≤ b ∧ a ≤ c) {xs : List α} :
-    xs.minimum? = some a ↔ a ∈ xs ∧ ∀ b, b ∈ xs → a ≤ b := by
-  refine ⟨fun h => ⟨minimum?_mem min_eq_or h, (le_minimum?_iff le_min_iff h).1 (le_refl _)⟩, ?_⟩
+    xs.min? = some a ↔ a ∈ xs ∧ ∀ b, b ∈ xs → a ≤ b := by
+  refine ⟨fun h => ⟨min?_mem min_eq_or h, (le_min?_iff le_min_iff h).1 (le_refl _)⟩, ?_⟩
   intro ⟨h₁, h₂⟩
   cases xs with
   | nil => simp at h₁
   | cons x xs =>
     exact congrArg some <| anti.1
-      ((le_minimum?_iff le_min_iff (xs := x::xs) rfl).1 (le_refl _) _ h₁)
-      (h₂ _ (minimum?_mem min_eq_or (xs := x::xs) rfl))
+      ((le_min?_iff le_min_iff (xs := x::xs) rfl).1 (le_refl _) _ h₁)
+      (h₂ _ (min?_mem min_eq_or (xs := x::xs) rfl))
 
-theorem minimum?_replicate [Min α] {n : Nat} {a : α} (w : min a a = a) :
-    (replicate n a).minimum? = if n = 0 then none else some a := by
+theorem min?_replicate [Min α] {n : Nat} {a : α} (w : min a a = a) :
+    (replicate n a).min? = if n = 0 then none else some a := by
   induction n with
   | zero => rfl
-  | succ n ih => cases n <;> simp_all [replicate_succ, minimum?_cons]
+  | succ n ih => cases n <;> simp_all [replicate_succ, min?_cons]
 
-@[simp] theorem minimum?_replicate_of_pos [Min α] {n : Nat} {a : α} (w : min a a = a) (h : 0 < n) :
-    (replicate n a).minimum? = some a := by
-  simp [minimum?_replicate, Nat.ne_of_gt h, w]
+@[simp] theorem min?_replicate_of_pos [Min α] {n : Nat} {a : α} (w : min a a = a) (h : 0 < n) :
+    (replicate n a).min? = some a := by
+  simp [min?_replicate, Nat.ne_of_gt h, w]
 
-/-! ### maximum? -/
+/-! ### max? -/
 
-@[simp] theorem maximum?_nil [Max α] : ([] : List α).maximum? = none := rfl
+@[simp] theorem max?_nil [Max α] : ([] : List α).max? = none := rfl
 
--- We don't put `@[simp]` on `maximum?_cons`,
+-- We don't put `@[simp]` on `max?_cons`,
 -- because the definition in terms of `foldl` is not useful for proofs.
-theorem maximum?_cons [Max α] {xs : List α} : (x :: xs).maximum? = foldl max x xs := rfl
+theorem max?_cons [Max α] {xs : List α} : (x :: xs).max? = foldl max x xs := rfl
 
-@[simp] theorem maximum?_eq_none_iff {xs : List α} [Max α] : xs.maximum? = none ↔ xs = [] := by
-  cases xs <;> simp [maximum?]
+@[simp] theorem max?_eq_none_iff {xs : List α} [Max α] : xs.max? = none ↔ xs = [] := by
+  cases xs <;> simp [max?]
 
-theorem maximum?_mem [Max α] (min_eq_or : ∀ a b : α, max a b = a ∨ max a b = b) :
-    {xs : List α} → xs.maximum? = some a → a ∈ xs
+theorem max?_mem [Max α] (min_eq_or : ∀ a b : α, max a b = a ∨ max a b = b) :
+    {xs : List α} → xs.max? = some a → a ∈ xs
   | nil => by simp
   | cons x xs => by
-    rw [maximum?]; rintro ⟨⟩
+    rw [max?]; rintro ⟨⟩
     induction xs generalizing x with simp at *
     | cons y xs ih =>
       rcases ih (max x y) with h | h <;> simp [h]
@@ -114,40 +114,57 @@ theorem maximum?_mem [Max α] (min_eq_or : ∀ a b : α, max a b = a ∨ max a b
 
 -- See also `Init.Data.List.Nat.Basic` for specialisations of the next two results to `Nat`.
 
-theorem maximum?_le_iff [Max α] [LE α]
+theorem max?_le_iff [Max α] [LE α]
     (max_le_iff : ∀ a b c : α, max b c ≤ a ↔ b ≤ a ∧ c ≤ a) :
-    {xs : List α} → xs.maximum? = some a → ∀ {x}, a ≤ x ↔ ∀ b ∈ xs, b ≤ x
+    {xs : List α} → xs.max? = some a → ∀ {x}, a ≤ x ↔ ∀ b ∈ xs, b ≤ x
   | nil => by simp
   | cons x xs => by
-    rw [maximum?]; rintro ⟨⟩ y
+    rw [max?]; rintro ⟨⟩ y
     induction xs generalizing x with
     | nil => simp
     | cons y xs ih => simp [ih, max_le_iff, and_assoc]
 
 -- This could be refactored by designing appropriate typeclasses to replace `le_refl`, `max_eq_or`,
 -- and `le_min_iff`.
-theorem maximum?_eq_some_iff [Max α] [LE α] [anti : Antisymm ((· : α) ≤ ·)]
+theorem max?_eq_some_iff [Max α] [LE α] [anti : Antisymm ((· : α) ≤ ·)]
     (le_refl : ∀ a : α, a ≤ a)
     (max_eq_or : ∀ a b : α, max a b = a ∨ max a b = b)
     (max_le_iff : ∀ a b c : α, max b c ≤ a ↔ b ≤ a ∧ c ≤ a) {xs : List α} :
-    xs.maximum? = some a ↔ a ∈ xs ∧ ∀ b ∈ xs, b ≤ a := by
-  refine ⟨fun h => ⟨maximum?_mem max_eq_or h, (maximum?_le_iff max_le_iff h).1 (le_refl _)⟩, ?_⟩
+    xs.max? = some a ↔ a ∈ xs ∧ ∀ b ∈ xs, b ≤ a := by
+  refine ⟨fun h => ⟨max?_mem max_eq_or h, (max?_le_iff max_le_iff h).1 (le_refl _)⟩, ?_⟩
   intro ⟨h₁, h₂⟩
   cases xs with
   | nil => simp at h₁
   | cons x xs =>
     exact congrArg some <| anti.1
-      (h₂ _ (maximum?_mem max_eq_or (xs := x::xs) rfl))
-      ((maximum?_le_iff max_le_iff (xs := x::xs) rfl).1 (le_refl _) _ h₁)
+      (h₂ _ (max?_mem max_eq_or (xs := x::xs) rfl))
+      ((max?_le_iff max_le_iff (xs := x::xs) rfl).1 (le_refl _) _ h₁)
 
-theorem maximum?_replicate [Max α] {n : Nat} {a : α} (w : max a a = a) :
-    (replicate n a).maximum? = if n = 0 then none else some a := by
+theorem max?_replicate [Max α] {n : Nat} {a : α} (w : max a a = a) :
+    (replicate n a).max? = if n = 0 then none else some a := by
   induction n with
   | zero => rfl
-  | succ n ih => cases n <;> simp_all [replicate_succ, maximum?_cons]
+  | succ n ih => cases n <;> simp_all [replicate_succ, max?_cons]
 
-@[simp] theorem maximum?_replicate_of_pos [Max α] {n : Nat} {a : α} (w : max a a = a) (h : 0 < n) :
-    (replicate n a).maximum? = some a := by
-  simp [maximum?_replicate, Nat.ne_of_gt h, w]
+@[simp] theorem max?_replicate_of_pos [Max α] {n : Nat} {a : α} (w : max a a = a) (h : 0 < n) :
+    (replicate n a).max? = some a := by
+  simp [max?_replicate, Nat.ne_of_gt h, w]
+
+@[deprecated min?_nil (since := "2024-09-29")] abbrev minimum?_nil := @min?_nil
+@[deprecated min?_cons (since := "2024-09-29")] abbrev minimum?_cons := @min?_cons
+@[deprecated min?_eq_none_iff (since := "2024-09-29")] abbrev mininmum?_eq_none_iff := @min?_eq_none_iff
+@[deprecated min?_mem (since := "2024-09-29")] abbrev minimum?_mem := @min?_mem
+@[deprecated le_min?_iff (since := "2024-09-29")] abbrev le_minimum?_iff := @le_min?_iff
+@[deprecated min?_eq_some_iff (since := "2024-09-29")] abbrev minimum?_eq_some_iff := @min?_eq_some_iff
+@[deprecated min?_replicate (since := "2024-09-29")] abbrev minimum?_replicate := @min?_replicate
+@[deprecated min?_replicate_of_pos (since := "2024-09-29")] abbrev minimum?_replicate_of_pos := @min?_replicate_of_pos
+@[deprecated max?_nil (since := "2024-09-29")] abbrev maximum?_nil := @max?_nil
+@[deprecated max?_cons (since := "2024-09-29")] abbrev maximum?_cons := @max?_cons
+@[deprecated max?_eq_none_iff (since := "2024-09-29")] abbrev maximum?_eq_none_iff := @max?_eq_none_iff
+@[deprecated max?_mem (since := "2024-09-29")] abbrev maximum?_mem := @max?_mem
+@[deprecated max?_le_iff (since := "2024-09-29")] abbrev maximum?_le_iff := @max?_le_iff
+@[deprecated max?_eq_some_iff (since := "2024-09-29")] abbrev maximum?_eq_some_iff := @max?_eq_some_iff
+@[deprecated max?_replicate (since := "2024-09-29")] abbrev maximum?_replicate := @max?_replicate
+@[deprecated max?_replicate_of_pos (since := "2024-09-29")] abbrev maximum?_replicate_of_pos := @max?_replicate_of_pos
 
 end List

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/Nat/Basic.lean

@@ -86,26 +86,26 @@ theorem mem_eraseIdx_iff_getElem? {x : α} {l} {k} : x ∈ eraseIdx l k ↔ ∃
     obtain ⟨h', -⟩ := getElem?_eq_some_iff.1 h
     exact ⟨h', h⟩
 
-/-! ### minimum? -/
+/-! ### min? -/
 
--- A specialization of `minimum?_eq_some_iff` to Nat.
-theorem minimum?_eq_some_iff' {xs : List Nat} :
-    xs.minimum? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, a ≤ b) :=
-  minimum?_eq_some_iff
+-- A specialization of `min?_eq_some_iff` to Nat.
+theorem min?_eq_some_iff' {xs : List Nat} :
+    xs.min? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, a ≤ b) :=
+  min?_eq_some_iff
     (le_refl := Nat.le_refl)
-    (min_eq_or := fun _ _ => by omega)
-    (le_min_iff := fun _ _ _ => by omega)
+    (min_eq_or := fun _ _ => Nat.min_def .. ▸ by split <;> simp)
+    (le_min_iff := fun _ _ _ => Nat.le_min)
 
 -- This could be generalized,
 -- but will first require further work on order typeclasses in the core repository.
-theorem minimum?_cons' {a : Nat} {l : List Nat} :
-    (a :: l).minimum? = some (match l.minimum? with
+theorem min?_cons' {a : Nat} {l : List Nat} :
+    (a :: l).min? = some (match l.min? with
     | none => a
     | some m => min a m) := by
-  rw [minimum?_eq_some_iff']
+  rw [min?_eq_some_iff']
   split <;> rename_i h m
   · simp_all
-  · rw [minimum?_eq_some_iff'] at m
+  · rw [min?_eq_some_iff'] at m
     obtain ⟨m, le⟩ := m
     rw [Nat.min_def]
     constructor
@@ -122,11 +122,11 @@ theorem minimum?_cons' {a : Nat} {l : List Nat} :
 theorem foldl_min
     {α : Type _} [Min α] [Std.IdempotentOp (min : α → α → α)] [Std.Associative (min : α → α → α)]
     {l : List α} {a : α} :
-    l.foldl (init := a) min = min a (l.minimum?.getD a) := by
+    l.foldl (init := a) min = min a (l.min?.getD a) := by
   cases l with
   | nil => simp [Std.IdempotentOp.idempotent]
   | cons b l =>
-    simp only [minimum?]
+    simp only [min?]
     induction l generalizing a b with
     | nil => simp
     | cons c l ih => simp [ih, Std.Associative.assoc]
@@ -134,7 +134,7 @@ theorem foldl_min
 theorem foldl_min_right {α β : Type _}
     [Min β] [Std.IdempotentOp (min : β → β → β)] [Std.Associative (min : β → β → β)]
     {l : List α} {b : β} {f : α → β} :
-    (l.foldl (init := b) fun acc a => min acc (f a)) = min b ((l.map f).minimum?.getD b) := by
+    (l.foldl (init := b) fun acc a => min acc (f a)) = min b ((l.map f).min?.getD b) := by
   rw [← foldl_map, foldl_min]
 
 theorem foldl_min_le {l : List Nat} {a : Nat} : l.foldl (init := a) min ≤ a := by
@@ -148,12 +148,12 @@ theorem foldl_min_min_of_le {l : List Nat} {a b : Nat} (h : a ≤ b) :
     l.foldl (init := a) min ≤ b :=
   Nat.le_trans (foldl_min_le) h
 
-theorem minimum?_getD_le_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) :
-    l.minimum?.getD k ≤ a := by
+theorem min?_getD_le_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) :
+    l.min?.getD k ≤ a := by
   cases l with
   | nil => simp at h
   | cons b l =>
-    simp [minimum?_cons]
+    simp [min?_cons]
     simp at h
     rcases h with (rfl | h)
     · exact foldl_min_le
@@ -166,26 +166,26 @@ theorem minimum?_getD_le_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) :
         · exact foldl_min_min_of_le (Nat.min_le_right _ _)
         · exact ih _ h
 
-/-! ### maximum? -/
+/-! ### max? -/
 
--- A specialization of `maximum?_eq_some_iff` to Nat.
-theorem maximum?_eq_some_iff' {xs : List Nat} :
-    xs.maximum? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, b ≤ a) :=
-  maximum?_eq_some_iff
+-- A specialization of `max?_eq_some_iff` to Nat.
+theorem max?_eq_some_iff' {xs : List Nat} :
+    xs.max? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, b ≤ a) :=
+  max?_eq_some_iff
     (le_refl := Nat.le_refl)
-    (max_eq_or := fun _ _ => by omega)
-    (max_le_iff := fun _ _ _ => by omega)
+    (max_eq_or := fun _ _ => Nat.max_def .. ▸ by split <;> simp)
+    (max_le_iff := fun _ _ _ => Nat.max_le)
 
 -- This could be generalized,
 -- but will first require further work on order typeclasses in the core repository.
-theorem maximum?_cons' {a : Nat} {l : List Nat} :
-    (a :: l).maximum? = some (match l.maximum? with
+theorem max?_cons' {a : Nat} {l : List Nat} :
+    (a :: l).max? = some (match l.max? with
     | none => a
     | some m => max a m) := by
-  rw [maximum?_eq_some_iff']
+  rw [max?_eq_some_iff']
   split <;> rename_i h m
   · simp_all
-  · rw [maximum?_eq_some_iff'] at m
+  · rw [max?_eq_some_iff'] at m
     obtain ⟨m, le⟩ := m
     rw [Nat.max_def]
     constructor
@@ -202,11 +202,11 @@ theorem maximum?_cons' {a : Nat} {l : List Nat} :
 theorem foldl_max
     {α : Type _} [Max α] [Std.IdempotentOp (max : α → α → α)] [Std.Associative (max : α → α → α)]
     {l : List α} {a : α} :
-    l.foldl (init := a) max = max a (l.maximum?.getD a) := by
+    l.foldl (init := a) max = max a (l.max?.getD a) := by
   cases l with
   | nil => simp [Std.IdempotentOp.idempotent]
   | cons b l =>
-    simp only [maximum?]
+    simp only [max?]
     induction l generalizing a b with
     | nil => simp
     | cons c l ih => simp [ih, Std.Associative.assoc]
@@ -214,7 +214,7 @@ theorem foldl_max
 theorem foldl_max_right {α β : Type _}
     [Max β] [Std.IdempotentOp (max : β → β → β)] [Std.Associative (max : β → β → β)]
     {l : List α} {b : β} {f : α → β} :
-    (l.foldl (init := b) fun acc a => max acc (f a)) = max b ((l.map f).maximum?.getD b) := by
+    (l.foldl (init := b) fun acc a => max acc (f a)) = max b ((l.map f).max?.getD b) := by
   rw [← foldl_map, foldl_max]
 
 theorem le_foldl_max {l : List Nat} {a : Nat} : a ≤ l.foldl (init := a) max := by
@@ -228,12 +228,12 @@ theorem le_foldl_max_of_le {l : List Nat} {a b : Nat} (h : a ≤ b) :
     a ≤ l.foldl (init := b) max :=
   Nat.le_trans h (le_foldl_max)
 
-theorem le_maximum?_getD_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) :
-    a ≤ l.maximum?.getD k := by
+theorem le_max?_getD_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) :
+    a ≤ l.max?.getD k := by
   cases l with
   | nil => simp at h
   | cons b l =>
-    simp [maximum?_cons]
+    simp [max?_cons]
     simp at h
     rcases h with (rfl | h)
     · exact le_foldl_max
@@ -246,4 +246,11 @@ theorem le_maximum?_getD_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) :
         · exact le_foldl_max_of_le (Nat.le_max_right b a)
         · exact ih _ h
 
+@[deprecated min?_eq_some_iff' (since := "2024-09-29")] abbrev minimum?_eq_some_iff' := @min?_eq_some_iff'
+@[deprecated min?_cons' (since := "2024-09-29")] abbrev minimum?_cons' := @min?_cons'
+@[deprecated min?_getD_le_of_mem (since := "2024-09-29")] abbrev minimum?_getD_le_of_mem := @min?_getD_le_of_mem
+@[deprecated max?_eq_some_iff' (since := "2024-09-29")] abbrev maximum?_eq_some_iff' := @max?_eq_some_iff'
+@[deprecated max?_cons' (since := "2024-09-29")] abbrev maximum?_cons' := @max?_cons'
+@[deprecated le_max?_getD_of_mem (since := "2024-09-29")] abbrev le_maximum?_getD_of_mem := @le_max?_getD_of_mem
+
 end List

src/Init/Data/List/Nat/TakeDrop.lean

@@ -42,7 +42,7 @@ theorem getElem_take' (L : List α) {i j : Nat} (hi : i < L.length) (hj : i < j)
 
 /-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of
 length `> i`. Version designed to rewrite from the small list to the big list. -/
-theorem getElem_take (L : List α) {j i : Nat} {h : i < (L.take j).length} :
+@[simp] theorem getElem_take (L : List α) {j i : Nat} {h : i < (L.take j).length} :
     (L.take j)[i] =
     L[i]'(Nat.lt_of_lt_of_le h (length_take_le' _ _)) := by
   rw [length_take, Nat.lt_min] at h; rw [getElem_take' L _ h.1]
@@ -52,7 +52,7 @@ length `> i`. Version designed to rewrite from the big list to the small list. -
 @[deprecated getElem_take' (since := "2024-06-12")]
 theorem get_take (L : List α) {i j : Nat} (hi : i < L.length) (hj : i < j) :
     get L ⟨i, hi⟩ = get (L.take j) ⟨i, length_take .. ▸ Nat.lt_min.mpr ⟨hj, hi⟩⟩ := by
-  simp [getElem_take' _ hi hj]
+  simp
 
 /-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of
 length `> i`. Version designed to rewrite from the small list to the big list. -/

src/Init/Data/List/Perm.lean

@@ -248,6 +248,10 @@ theorem countP_eq_countP_filter_add (l : List α) (p q : α → Bool) :
 theorem Perm.count_eq [DecidableEq α] {l₁ l₂ : List α} (p : l₁ ~ l₂) (a) :
     count a l₁ = count a l₂ := p.countP_eq _
 
+/-
+This theorem is a variant of `Perm.foldl_eq` defined in Mathlib which uses typeclasses rather
+than the explicit `comm` argument.
+-/
 theorem Perm.foldl_eq' {f : β → α → β} {l₁ l₂ : List α} (p : l₁ ~ l₂)
     (comm : ∀ x ∈ l₁, ∀ y ∈ l₁, ∀ (z), f (f z x) y = f (f z y) x)
     (init) : foldl f init l₁ = foldl f init l₂ := by
@@ -264,6 +268,28 @@ theorem Perm.foldl_eq' {f : β → α → β} {l₁ l₂ : List α} (p : l₁ ~
     refine (IH₁ comm init).trans (IH₂ ?_ _)
     intros; apply comm <;> apply p₁.symm.subset <;> assumption
 
+/-
+This theorem is a variant of `Perm.foldr_eq` defined in Mathlib which uses typeclasses rather
+than the explicit `comm` argument.
+-/
+theorem Perm.foldr_eq' {f : α → β → β} {l₁ l₂ : List α} (p : l₁ ~ l₂)
+    (comm : ∀ x ∈ l₁, ∀ y ∈ l₁, ∀ (z), f y (f x z) = f x (f y z))
+    (init) : foldr f init l₁ = foldr f init l₂ := by
+  induction p using recOnSwap' generalizing init with
+  | nil => simp
+  | cons x _p IH =>
+    simp only [foldr]
+    congr 1
+    apply IH; intros; apply comm <;> exact .tail _ ‹_›
+  | swap' x y _p IH =>
+    simp only [foldr]
+    rw [comm x (.tail _ <| .head _) y (.head _)]
+    congr 2
+    apply IH; intros; apply comm <;> exact .tail _ (.tail _ ‹_›)
+  | trans p₁ _p₂ IH₁ IH₂ =>
+    refine (IH₁ comm init).trans (IH₂ ?_ _)
+    intros; apply comm <;> apply p₁.symm.subset <;> assumption
+
 theorem Perm.rec_heq {β : List α → Sort _} {f : ∀ a l, β l → β (a :: l)} {b : β []} {l l' : List α}
     (hl : l ~ l') (f_congr : ∀ {a l l' b b'}, l ~ l' → HEq b b' → HEq (f a l b) (f a l' b'))
     (f_swap : ∀ {a a' l b}, HEq (f a (a' :: l) (f a' l b)) (f a' (a :: l) (f a l b))) :

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/Data/Option.lean

@@ -8,3 +8,5 @@ import Init.Data.Option.Basic
 import Init.Data.Option.BasicAux
 import Init.Data.Option.Instances
 import Init.Data.Option.Lemmas
+import Init.Data.Option.Attach
+import Init.Data.Option.List

src/Init/Data/Option/Attach.lean

@@ -0,0 +1,178 @@
+/-
+Copyright (c) 2024 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Data.Option.Basic
+import Init.Data.Option.List
+import Init.Data.List.Attach
+import Init.BinderPredicates
+
+namespace Option
+
+/--
+Unsafe implementation of `attachWith`, taking advantage of the fact that the representation of
+`Option {x // P x}` is the same as the input `Option α`.
+-/
+@[inline] private unsafe def attachWithImpl
+    (o : Option α) (P : α → Prop) (_ : ∀ x ∈ o, P x) : Option {x // P x} := unsafeCast o
+
+/-- "Attach" a proof `P x` that holds for the element of `o`, if present,
+to produce a new option with the same element but in the type `{x // P x}`. -/
+@[implemented_by attachWithImpl] def attachWith
+    (xs : Option α) (P : α → Prop) (H : ∀ x ∈ xs, P x) : Option {x // P x} :=
+  match xs with
+  | none => none
+  | some x => some ⟨x, H x (mem_some_self x)⟩
+
+/-- "Attach" the proof that the element of `xs`, if present, is in `xs`
+to produce a new option with the same elements but in the type `{x // x ∈ xs}`. -/
+@[inline] def attach (xs : Option α) : Option {x // x ∈ xs} := xs.attachWith _ fun _ => id
+
+@[simp] theorem attach_none : (none : Option α).attach = none := rfl
+@[simp] theorem attachWith_none : (none : Option α).attachWith P H = none := rfl
+
+@[simp] theorem attach_some {x : α} :
+    (some x).attach = some ⟨x, rfl⟩ := rfl
+@[simp] theorem attachWith_some {x : α} {P : α → Prop} (h : ∀ (b : α), b ∈ some x → P b) :
+    (some x).attachWith P h = some ⟨x, by simpa using h⟩ := rfl
+
+theorem attach_congr {o₁ o₂ : Option α} (h : o₁ = o₂) :
+    o₁.attach = o₂.attach.map (fun x => ⟨x.1, h ▸ x.2⟩) := by
+  subst h
+  simp
+
+theorem attachWith_congr {o₁ o₂ : Option α} (w : o₁ = o₂) {P : α → Prop} {H : ∀ x ∈ o₁, P x} :
+    o₁.attachWith P H = o₂.attachWith P fun x h => H _ (w ▸ h) := by
+  subst w
+  simp
+
+theorem attach_map_coe (o : Option α) (f : α → β) :
+    (o.attach.map fun (i : {i // i ∈ o}) => f i) = o.map f := by
+  cases o <;> simp
+
+theorem attach_map_val (o : Option α) (f : α → β) :
+    (o.attach.map fun i => f i.val) = o.map f :=
+  attach_map_coe _ _
+
+@[simp]
+theorem attach_map_subtype_val (o : Option α) :
+    o.attach.map Subtype.val = o :=
+  (attach_map_coe _ _).trans (congrFun Option.map_id _)
+
+theorem attachWith_map_coe {p : α → Prop} (f : α → β) (o : Option α) (H : ∀ a ∈ o, p a) :
+    ((o.attachWith p H).map fun (i : { i // p i}) => f i.val) = o.map f := by
+  cases o <;> simp [H]
+
+theorem attachWith_map_val {p : α → Prop} (f : α → β) (o : Option α) (H : ∀ a ∈ o, p a) :
+    ((o.attachWith p H).map fun i => f i.val) = o.map f :=
+  attachWith_map_coe _ _ _
+
+@[simp]
+theorem attachWith_map_subtype_val {p : α → Prop} (o : Option α) (H : ∀ a ∈ o, p a) :
+    (o.attachWith p H).map Subtype.val = o :=
+  (attachWith_map_coe _ _ _).trans (congrFun Option.map_id _)
+
+@[simp] theorem mem_attach : ∀ (o : Option α) (x : {x // x ∈ o}), x ∈ o.attach
+  | none, ⟨x, h⟩ => by simp at h
+  | some a, ⟨x, h⟩ => by simpa using h
+
+@[simp] theorem isNone_attach (o : Option α) : o.attach.isNone = o.isNone := by
+  cases o <;> simp
+
+@[simp] theorem isNone_attachWith {p : α → Prop} (o : Option α) (H : ∀ a ∈ o, p a) :
+    (o.attachWith p H).isNone = o.isNone := by
+  cases o <;> simp
+
+@[simp] theorem isSome_attach (o : Option α) : o.attach.isSome = o.isSome := by
+  cases o <;> simp
+
+@[simp] theorem isSome_attachWith {p : α → Prop} (o : Option α) (H : ∀ a ∈ o, p a) :
+    (o.attachWith p H).isSome = o.isSome := by
+  cases o <;> simp
+
+@[simp] theorem attach_eq_none_iff (o : Option α) : o.attach = none ↔ o = none := by
+  cases o <;> simp
+
+@[simp] theorem attach_eq_some_iff {o : Option α} {x : {x // x ∈ o}} :
+    o.attach = some x ↔ o = some x.val := by
+  cases o <;> cases x <;> simp
+
+@[simp] theorem attachWith_eq_none_iff {p : α → Prop} (o : Option α) (H : ∀ a ∈ o, p a) :
+    o.attachWith p H = none ↔ o = none := by
+  cases o <;> simp
+
+@[simp] theorem attachWith_eq_some_iff {p : α → Prop} {o : Option α} (H : ∀ a ∈ o, p a) {x : {x // p x}} :
+    o.attachWith p H = some x ↔ o = some x.val := by
+  cases o <;> cases x <;> simp
+
+@[simp] theorem get_attach {o : Option α} (h : o.attach.isSome = true) :
+    o.attach.get h = ⟨o.get (by simpa using h), by simp⟩ := by
+  cases o
+  · simp at h
+  · simp [get_some]
+
+@[simp] theorem get_attachWith {p : α → Prop} {o : Option α} (H : ∀ a ∈ o, p a) (h : (o.attachWith p H).isSome) :
+    (o.attachWith p H).get h = ⟨o.get (by simpa using h), H _ (by simp)⟩ := by
+  cases o
+  · simp at h
+  · simp [get_some]
+
+@[simp] theorem toList_attach (o : Option α) :
+    o.attach.toList = o.toList.attach.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
+  cases o <;> simp
+
+theorem attach_map {o : Option α} (f : α → β) :
+    (o.map f).attach = o.attach.map (fun ⟨x, h⟩ => ⟨f x, mem_map_of_mem f h⟩) := by
+  cases o <;> simp
+
+theorem attachWith_map {o : Option α} (f : α → β) {P : β → Prop} {H : ∀ (b : β), b ∈ o.map f → P b} :
+    (o.map f).attachWith P H = (o.attachWith (P ∘ f) (fun a h => H _ (mem_map_of_mem f h))).map
+      fun ⟨x, h⟩ => ⟨f x, h⟩ := by
+  cases o <;> simp
+
+theorem map_attach {o : Option α} (f : { x // x ∈ o } → β) :
+    o.attach.map f = o.pmap (fun a (h : a ∈ o) => f ⟨a, h⟩) (fun a h => h) := by
+  cases o <;> simp
+
+theorem map_attachWith {o : Option α} {P : α → Prop} {H : ∀ (a : α), a ∈ o → P a}
+    (f : { x // P x } → β) :
+    (o.attachWith P H).map f =
+      o.pmap (fun a (h : a ∈ o ∧ P a) => f ⟨a, h.2⟩) (fun a h => ⟨h, H a h⟩) := by
+  cases o <;> simp
+
+theorem attach_bind {o : Option α} {f : α → Option β} :
+    (o.bind f).attach =
+      o.attach.bind fun ⟨x, h⟩ => (f x).attach.map fun ⟨y, h'⟩ => ⟨y, mem_bind_iff.mpr ⟨x, h, h'⟩⟩ := by
+  cases o <;> simp
+
+theorem bind_attach {o : Option α} {f : {x // x ∈ o} → Option β} :
+    o.attach.bind f = o.pbind fun a h => f ⟨a, h⟩ := by
+  cases o <;> simp
+
+theorem pbind_eq_bind_attach {o : Option α} {f : (a : α) → a ∈ o → Option β} :
+    o.pbind f = o.attach.bind fun ⟨x, h⟩ => f x h := by
+  cases o <;> simp
+
+theorem attach_filter {o : Option α} {p : α → Bool} :
+    (o.filter p).attach =
+      o.attach.bind fun ⟨x, h⟩ => if h' : p x then some ⟨x, by simp_all⟩ else none := by
+  cases o with
+  | none => simp
+  | some a =>
+    simp only [filter_some, attach_some]
+    ext
+    simp only [mem_def, attach_eq_some_iff, ite_none_right_eq_some, some.injEq, some_bind,
+      dite_none_right_eq_some]
+    constructor
+    · rintro ⟨h, w⟩
+      refine ⟨h, by ext; simpa using w⟩
+    · rintro ⟨h, rfl⟩
+      simp [h]
+
+theorem filter_attach {o : Option α} {p : {x // x ∈ o} → Bool} :
+    o.attach.filter p = o.pbind fun a h => if p ⟨a, h⟩ then some ⟨a, h⟩ else none := by
+  cases o <;> simp [filter_some]
+
+end Option

src/Init/Data/Option/Lemmas.lean

@@ -138,6 +138,10 @@ theorem bind_eq_none' {o : Option α} {f : α → Option β} :
     o.bind f = none ↔ ∀ b a, a ∈ o → b ∉ f a := by
   simp only [eq_none_iff_forall_not_mem, not_exists, not_and, mem_def, bind_eq_some]
 
+theorem mem_bind_iff {o : Option α} {f : α → Option β} :
+    b ∈ o.bind f ↔ ∃ a, a ∈ o ∧ b ∈ f a := by
+  cases o <;> simp
+
 theorem bind_comm {f : α → β → Option γ} (a : Option α) (b : Option β) :
     (a.bind fun x => b.bind (f x)) = b.bind fun y => a.bind fun x => f x y := by
   cases a <;> cases b <;> rfl
@@ -232,9 +236,27 @@ theorem isSome_filter_of_isSome (p : α → Bool) (o : Option α) (h : (o.filter
   cases o <;> simp at h ⊢
 
 @[simp] theorem filter_eq_none {p : α → Bool} :
-    Option.filter p o = none ↔ o = none ∨ ∀ a, a ∈ o → ¬ p a := by
+    o.filter p = none ↔ o = none ∨ ∀ a, a ∈ o → ¬ p a := by
   cases o <;> simp [filter_some]
 
+@[simp] theorem filter_eq_some {o : Option α} {p : α → Bool} :
+    o.filter p = some a ↔ a ∈ o ∧ p a := by
+  cases o with
+  | none => simp
+  | some a =>
+    simp [filter_some]
+    split <;> rename_i h
+    · simp only [some.injEq, iff_self_and]
+      rintro rfl
+      exact h
+    · simp only [reduceCtorEq, false_iff, not_and, Bool.not_eq_true]
+      rintro rfl
+      simpa using h
+
+theorem mem_filter_iff {p : α → Bool} {a : α} {o : Option α} :
+    a ∈ o.filter p ↔ a ∈ o ∧ p a := by
+  simp
+
 @[simp] theorem all_guard (p : α → Prop) [DecidablePred p] (a : α) :
     Option.all q (guard p a) = (!p a || q a) := by
   simp only [guard]
@@ -350,6 +372,8 @@ end choice
 
 @[simp] theorem toList_none (α : Type _) : (none : Option α).toList = [] := rfl
 
+-- See `Init.Data.Option.List` for lemmas about `toList`.
+
 @[simp] theorem or_some : (some a).or o = some a := rfl
 @[simp] theorem none_or : none.or o = o := rfl
 

src/Init/Data/Option/List.lean

@@ -0,0 +1,14 @@
+/-
+Copyright (c) 2024 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Data.List.Lemmas
+
+namespace Option
+
+@[simp] theorem mem_toList (a : α) (o : Option α) : a ∈ o.toList ↔ a ∈ o := by
+  cases o <;> simp [eq_comm]
+
+end Option

src/Init/Prelude.lean

@@ -2570,7 +2570,9 @@ structure Array (α : Type u) where
   /--
   Converts a `List α` into an `Array α`.
 
-  At runtime, this constructor is implemented by `List.toArray` and is O(n) in the length of the
+  You can also use the synonym `List.toArray` when dot notation is convenient.
+
+  At runtime, this constructor is implemented by `List.toArrayImpl` and is O(n) in the length of the
   list.
   -/
   mk ::

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
-example (h : False) : p := by contradiction
-```
+  ```lean
+  example (h : False) : p := by contradiction
+  ```
 - Injectivity of constructors
-```lean
-example (h : none = some true) : p := by contradiction  --
-```
+  ```lean
+  example (h : none = some true) : p := by contradiction  --
+  ```
 - Decidable false proposition
-```lean
-example (h : 2 + 2 = 3) : p := by contradiction
-```
+  ```lean
+  example (h : 2 + 2 = 3) : p := by contradiction
+  ```
 - Contradictory hypotheses
-```lean
-example (h : p) (h' : ¬ p) : q := by contradiction
-```
+  ```lean
+  example (h : p) (h' : ¬ p) : q := by contradiction
+  ```
 - Other simple contradictions such as
-```lean
-example (x : Nat) (h : x ≠ x) : p := by contradiction
-```
+  ```lean
+  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 is supposed to be an extensible tactic and users can add their own support
-for new reflexive relations.
-
-Remark: `rfl` is an extensible tactic. We later add `macro_rules` to try different
-reflexivity theorems (e.g., `Iff.rfl`).
+This tactic applies to a goal whose target has the form `x ~ x`,
+where `~` is equality, heterogeneous equality or any relation that
+has a reflexivity lemma tagged with the attribute @[refl].
 -/
-macro "rfl" : tactic => `(tactic| case' _ => fail "The rfl tactic failed. Possible reasons:
-- 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)
+syntax "rfl" : tactic
 
 /--
-This tactic applies to a goal whose target has the form `x ~ x`,
-where `~` is a reflexive relation other than `=`,
-that is, a relation which has a reflexive lemma tagged with the attribute @[refl].
+The same as `rfl`, but without trying `eq_refl` at the end.
 -/
 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 false
+            return arg
+      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
-  | _ => pure false
+  | Arg.stx stx@(Syntax.node _ ``Lean.Parser.Term.hole _) :: _ => pure stx
+  | _ => 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`,
-    and then execute the main loop.-/
+  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.
+  -/
   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`.
-    This method assume `fType` is a function type -/
+  Process a `fType` of the form `(x : A) → B x`.
+  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.
-        The idea is that this explicit argument can be inferred using the type of the named argument one.
-        Note that we also use this approach in the branch where there are no explicit arguments left.
-        This is important to make sure the system behaves in a uniform way.
-        Moreover, users rely on this behavior. For example, consider the example on issue #1851
+        We treat the explicit argument `argName` as implicit
+        if we have a named arguments that depends on it whose `suppressDeps` flag set to `true`.
+        The motivation for this is class projections (issue #1851).
+        In some cases, class projections can have explicit parameters. For example, in
         ```
         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`
-        Note that the argument `a` is explicit since there is no way to infer it from the expected
-        type or the type of other explicit arguments.
-        Recall that `f.val` is sugar for `Approx.val (self := f)`. In both `#check` commands above
-        the user assumed that `a` does not need to be provided since it can be inferred from the type
-        of `self`.
-        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`
+        the type of `Approx.val` is `{α : Type} → (a : α) → {X : Type} → [self : Approx a X] → X`.
+        Note that the parameter `a` is explicit since there is no way to infer it from the expected
+        type or from the types of other explicit parameters.
+        Being a parameter of the class, `a` is determined by the type of `self`.
+
+        Consider
+        ```
+        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 (← anyNamedArgDependsOnCurrent) then
-            addImplicitArg argName
-          else if (← read).ellipsis then
+        if (← read).ellipsis then
+          addImplicitArg argName
+        else if !(← get).namedArgs.isEmpty 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
-            addImplicitArg argName
-          else if (← fTypeHasOptAutoParams) then
+          if (← fTypeHasOptAutoParams) then
             addEtaArg argName
           else
             finalize
@@ -641,24 +668,30 @@ mutual
       finalize
 
   /--
-    Process a `fType` of the form `[x : A] → B x`.
-    This method assume `fType` is a function type -/
+  Process a `fType` of the form `[x : A] → B x`.
+  This method assume `fType` is a function type.
+  -/
   private partial def processInstImplicitArg (argName : Name) : M Expr := do
     if (← read).explicit then
-      if (← isNextArgHole) then
-        /- Recall that if '@' has been used, and the argument is '_', then we still use type class resolution -/
-        let arg ← mkFreshExprMVar (← getArgExpectedType) MetavarKind.synthetic
+      if let some stx ← nextArgHole? then
+        -- We still use typeclass resolution for `_` arguments.
+        -- 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
-    let idx := (← get).idx
-    if discrs.any Option.isNone then
-      for i in [idx:idx + xs.size], x in xs do
-        if let some tidx := (← read).elimInfo.targetsPos.indexOf? i then
-          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 fType.getAppFn == (← get).motive? do
+      throwError "Internal error, eliminator target type isn't an application of the motive"
+    let discrs := fType.getAppArgs
+    trace[Elab.app.elab_as_elim] "discrs: {discrs}"
+    let motiveVal ← mkMotive discrs 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) =>
-      if (← read).extraArgsPos.contains idx then
-        let arg ← elabArg (.stx stx) binderType
-        addArgAndContinue arg
-      else
-        addArgAndContinue (← postponeElabTerm stx binderType)
+    | .some (.stx stx) => 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
-    trace[Elab.app.elab_as_elim] "extraArgsPos: {extraArgsPos}"
-    ElabElim.main.run { elimInfo, expectedType, extraArgsPos } |>.run' {
+    ElabElim.main.run { elimInfo, expectedType } |>.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
-  and already elaborated expressions. It is used to elaborate applications. -/
+Auxiliary inductive datatype for combining unelaborated syntax
+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
-      mkSorry expectedType false
-    else
-      mkTacticMVar expectedType stx
+    mkTacticMVar expectedType stx .term
   | 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
@@ -732,7 +733,8 @@ private def addDefaults (lctx : LocalContext) (defaultAuxDecls : Array (Name ×
         throwError "invalid default value for field, it contains metavariables{indentExpr value}"
       /- The identity function is used as "marker". -/
       let value ← mkId value
-      discard <| mkAuxDefinition declName type value (zetaDelta := true)
+      -- No need to compile the definition, since it is only used during elaboration.
+      discard <| mkAuxDefinition declName type value (zetaDelta := true) (compile := false)
       setReducibleAttribute declName
 
 /--

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/Omega/Frontend.lean

@@ -277,6 +277,7 @@ where
       | _ => mkAtomLinearCombo e
     | (``Min.min, #[_, _, a, b]) => rewrite e (mkApp2 (.const ``Int.ofNat_min []) a b)
     | (``Max.max, #[_, _, a, b]) => rewrite e (mkApp2 (.const ``Int.ofNat_max []) a b)
+    | (``Int.toNat, #[n]) => rewrite e (mkApp (.const ``Int.toNat_eq_max []) n)
     | (``HShiftLeft.hShiftLeft, #[_, _, _, _, a, b]) =>
       rewrite e (mkApp2 (.const ``Int.ofNat_shiftLeft_eq []) a b)
     | (``HShiftRight.hShiftRight, #[_, _, _, _, a, b]) =>

src/Lean/Elab/Tactic/Omega/MinNatAbs.lean

@@ -29,12 +29,14 @@ The minimum non-zero entry in a list of natural numbers, or zero if all entries
 We completely characterize the function via
 `nonzeroMinimum_eq_zero_iff` and `nonzeroMinimum_eq_nonzero_iff` below.
 -/
-def nonzeroMinimum (xs : List Nat) : Nat := xs.filter (· ≠ 0) |>.minimum? |>.getD 0
+def nonzeroMinimum (xs : List Nat) : Nat := xs.filter (· ≠ 0) |>.min? |>.getD 0
 
 -- A specialization of `minimum?_eq_some_iff` to Nat.
-theorem minimum?_eq_some_iff' {xs : List Nat} :
-    xs.minimum? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, a ≤ b) :=
-  minimum?_eq_some_iff
+-- This is a duplicate `min?_eq_some_iff'` proved in `Init.Data.List.Nat.Basic`,
+-- and could be deduplicated but the import hierarchy is awkward.
+theorem min?_eq_some_iff'' {xs : List Nat} :
+    xs.min? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, a ≤ b) :=
+  min?_eq_some_iff
     (le_refl := Nat.le_refl)
     (min_eq_or := fun _ _ => Nat.min_def .. ▸ by split <;> simp)
     (le_min_iff := fun _ _ _ => Nat.le_min)
@@ -42,27 +44,27 @@ theorem minimum?_eq_some_iff' {xs : List Nat} :
 open Classical in
 @[simp] theorem nonzeroMinimum_eq_zero_iff {xs : List Nat} :
     xs.nonzeroMinimum = 0 ↔ ∀ x ∈ xs, x = 0 := by
-  simp [nonzeroMinimum, Option.getD_eq_iff, minimum?_eq_none_iff, minimum?_eq_some_iff',
+  simp [nonzeroMinimum, Option.getD_eq_iff, min?_eq_none_iff, min?_eq_some_iff'',
     filter_eq_nil_iff, mem_filter]
 
 theorem nonzeroMinimum_mem {xs : List Nat} (w : xs.nonzeroMinimum ≠ 0) :
     xs.nonzeroMinimum ∈ xs := by
   dsimp [nonzeroMinimum] at *
-  generalize h : (xs.filter (· ≠ 0) |>.minimum?) = m at *
+  generalize h : (xs.filter (· ≠ 0) |>.min?) = m at *
   match m, w with
-  | some (m+1), _ => simp_all [minimum?_eq_some_iff', mem_filter]
+  | some (m+1), _ => simp_all [min?_eq_some_iff'', mem_filter]
 
 theorem nonzeroMinimum_pos {xs : List Nat} (m : a ∈ xs) (h : a ≠ 0) : 0 < xs.nonzeroMinimum :=
   Nat.pos_iff_ne_zero.mpr fun w => h (nonzeroMinimum_eq_zero_iff.mp w _ m)
 
 theorem nonzeroMinimum_le {xs : List Nat} (m : a ∈ xs) (h : a ≠ 0) : xs.nonzeroMinimum ≤ a := by
-  have : (xs.filter (· ≠ 0) |>.minimum?) = some xs.nonzeroMinimum := by
+  have : (xs.filter (· ≠ 0) |>.min?) = some xs.nonzeroMinimum := by
     have w := nonzeroMinimum_pos m h
     dsimp [nonzeroMinimum] at *
-    generalize h : (xs.filter (· ≠ 0) |>.minimum?) = m? at *
+    generalize h : (xs.filter (· ≠ 0) |>.min?) = m? at *
     match m?, w with
     | some m?, _ => rfl
-  rw [minimum?_eq_some_iff'] at this
+  rw [min?_eq_some_iff''] at this
   apply this.2
   simp [List.mem_filter]
   exact ⟨m, h⟩
@@ -142,4 +144,4 @@ theorem minNatAbs_eq_nonzero_iff (xs : List Int) (w : z ≠ 0) :
 @[simp] theorem minNatAbs_nil : ([] : List Int).minNatAbs = 0 := rfl
 
 /-- The maximum absolute value in a list of integers. -/
-def maxNatAbs (xs : List Int) : Nat := xs.map Int.natAbs |>.maximum? |>.getD 0
+def maxNatAbs (xs : List Int) : Nat := xs.map Int.natAbs |>.max? |>.getD 0

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}"
-    throwTacticEx `apply_rfl goal explanation
+      return m!"the left-hand side{indentExpr lhs}\nis not definitionally equal to the right-hand side{indentExpr rhs}"
+    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/Meta/Tactic/Simp/Rewrite.lean

@@ -573,15 +573,33 @@ where
     catch _  =>
       return some mvarId
 
+/--
+Discharges assumptions of the form `∀ …, a = b` using `rfl`. This is particularly useful for higher
+order assumptions of the form `∀ …, e = ?g x y` to instaniate  a paramter `g` even if that does not
+appear on the lhs of the rule.
+-/
+def dischargeRfl (e : Expr) : SimpM (Option Expr) := do
+  forallTelescope e fun xs e => do
+    let some (t, a, b) := e.eq? | return .none
+    unless a.getAppFn.isMVar || b.getAppFn.isMVar do return .none
+    if (← withReducible <| isDefEq a b) then
+      trace[Meta.Tactic.simp.discharge] "Discharging with rfl: {e}"
+      let u ← getLevel t
+      let proof := mkApp2 (.const ``rfl [u]) t a
+      let proof ← mkLambdaFVars xs proof
+      return .some proof
+    return .none
+
+
 def dischargeDefault? (e : Expr) : SimpM (Option Expr) := do
   let e := e.cleanupAnnotations
   if isEqnThmHypothesis e then
-    if let some r ← dischargeUsingAssumption? e then
-      return some r
-    if let some r ← dischargeEqnThmHypothesis? e then
-      return some r
+    if let some r ← dischargeUsingAssumption? e then return some r
+    if let some r ← dischargeEqnThmHypothesis? e then return some r
   let r ← simp e
-  if r.expr.isTrue then
+  if let some p ← dischargeRfl r.expr then
+    return some (← mkEqMPR (← r.getProof) p)
+  else if r.expr.isTrue then
     return some (← mkOfEqTrue (← r.getProof))
   else
     return none

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/PrettyPrinter/Formatter.lean

@@ -360,7 +360,8 @@ def pushToken (info : SourceInfo) (tk : String) : FormatterM Unit := do
       modify fun st => { st with leadWord := if tk.trimLeft == tk then tk ++ st.leadWord else "" }
     else
       -- stopped after `tk` => add space
-      push $ tk ++ " "
+      pushLine
+      push tk
       modify fun st => { st with leadWord := if tk.trimLeft == tk then tk else "" }
   else
     -- already separated => use `tk` as is

src/Lean/Server/InfoUtils.lean

@@ -237,7 +237,7 @@ partial def InfoTree.hoverableInfoAt? (t : InfoTree) (hoverPos : String.Pos) (in
     let _ := @lexOrd
     let _ := @leOfOrd.{0}
     let _ := @maxOfLe
-    results.map (·.1) |>.maximum?
+    results.map (·.1) |>.max?
   let res? := results.find? (·.1 == maxPrio?) |>.map (·.2)
   if let some i := res? then
     if let .ofTermInfo ti := i.info then
@@ -380,7 +380,7 @@ partial def InfoTree.goalsAt? (text : FileMap) (t : InfoTree) (hoverPos : String
               priority := if hoverPos.byteIdx == tailPos.byteIdx + trailSize then 0 else 1
             }]
     return gs
-  let maxPrio? := gs.map (·.priority) |>.maximum?
+  let maxPrio? := gs.map (·.priority) |>.max?
   gs.filter (some ·.priority == maxPrio?)
 where
   hasNestedTactic (pos tailPos) : InfoTree → Bool

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/Model.lean

@@ -186,7 +186,7 @@ theorem toListModel_updateAllBuckets {m : Raw₀ α β} {f : AssocList α β →
     have := (hg (l := []) (l' := [])).length_eq
     rw [List.length_append, List.append_nil] at this
     omega
-  rw [updateAllBuckets, toListModel, Array.map_toList, List.bind_eq_foldl, List.foldl_map,
+  rw [updateAllBuckets, toListModel, Array.toList_map, List.bind_eq_foldl, List.foldl_map,
     toListModel, List.bind_eq_foldl]
   suffices ∀ (l : List (AssocList α β)) (l' : List ((a: α) × δ a)) (l'' : List ((a : α) × β a)),
       Perm (g l'') l' →

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/Sat/CNF/RelabelFin.lean

@@ -15,12 +15,12 @@ namespace CNF
 /--
 Obtain the literal with the largest identifier in `c`.
 -/
-def Clause.maxLiteral (c : Clause Nat) : Option Nat := (c.map (·.1)) |>.maximum?
+def Clause.maxLiteral (c : Clause Nat) : Option Nat := (c.map (·.1)) |>.max?
 
 theorem Clause.of_maxLiteral_eq_some (c : Clause Nat) (h : c.maxLiteral = some maxLit) :
     ∀ lit, Mem lit c → lit ≤ maxLit := by
   intro lit hlit
-  simp only [maxLiteral, List.maximum?_eq_some_iff', List.mem_map, forall_exists_index, and_imp,
+  simp only [maxLiteral, List.max?_eq_some_iff', List.mem_map, forall_exists_index, and_imp,
     forall_apply_eq_imp_iff₂] at h
   simp only [Mem] at hlit
   rcases h with ⟨_, hbar⟩
@@ -35,25 +35,25 @@ theorem Clause.maxLiteral_eq_some_of_mem (c : Clause Nat) (h : Mem l c) :
   cases h <;> rename_i h
   all_goals
     have h1 := List.ne_nil_of_mem h
-    have h2 := not_congr <| @List.maximum?_eq_none_iff _ (c.map (·.1)) _
+    have h2 := not_congr <| @List.max?_eq_none_iff _ (c.map (·.1)) _
     simp [← Option.ne_none_iff_exists', h1, h2, maxLiteral]
 
 theorem Clause.of_maxLiteral_eq_none (c : Clause Nat) (h : c.maxLiteral = none) :
     ∀ lit, ¬Mem lit c := by
   intro lit hlit
-  simp only [maxLiteral, List.maximum?_eq_none_iff, List.map_eq_nil_iff] at h
+  simp only [maxLiteral, List.max?_eq_none_iff, List.map_eq_nil_iff] at h
   simp only [h, not_mem_nil] at hlit
 
 /--
 Obtain the literal with the largest identifier in `f`.
 -/
 def maxLiteral (f : CNF Nat) : Option Nat :=
-  List.filterMap Clause.maxLiteral f |>.maximum?
+  List.filterMap Clause.maxLiteral f |>.max?
 
 theorem of_maxLiteral_eq_some' (f : CNF Nat) (h : f.maxLiteral = some maxLit) :
     ∀ clause, clause ∈ f → clause.maxLiteral = some localMax → localMax ≤ maxLit := by
   intro clause hclause1 hclause2
-  simp [maxLiteral, List.maximum?_eq_some_iff'] at h
+  simp [maxLiteral, List.max?_eq_some_iff'] at h
   rcases h with ⟨_, hclause3⟩
   apply hclause3 localMax clause hclause1 hclause2
 
@@ -70,7 +70,7 @@ theorem of_maxLiteral_eq_some (f : CNF Nat) (h : f.maxLiteral = some maxLit) :
 theorem of_maxLiteral_eq_none (f : CNF Nat) (h : f.maxLiteral = none) :
     ∀ lit, ¬Mem lit f := by
   intro lit hlit
-  simp only [maxLiteral, List.maximum?_eq_none_iff] at h
+  simp only [maxLiteral, List.max?_eq_none_iff] at h
   dsimp [Mem] at hlit
   rcases hlit with ⟨clause, ⟨hclause1, hclause2⟩⟩
   have := Clause.of_maxLiteral_eq_none clause (List.forall_none_of_filterMap_eq_nil h clause hclause1) lit

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

@@ -136,12 +136,10 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))
           exact ih.2 i b h
         | some (l, true) =>
           simp only [heq] at h
-          have i_in_bounds : i.1 < acc.size := by simp only [ih.1, i.2.2]
-          have l_in_bounds : l.1 < acc.size := by simp only [ih.1, l.2.2]
           rcases ih with ⟨hsize, ih⟩
           by_cases i = l.1
           · next i_eq_l =>
-            simp only [i_eq_l, Array.getElem_modify_self l_in_bounds] at h
+            simp only [i_eq_l, Array.getElem_modify_self] at h
             by_cases b
             · next b_eq_true =>
               rw [isUnit_iff, DefaultClause.toList] at heq
@@ -160,16 +158,14 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))
               rw [b_eq_false, Subtype.ext i_eq_l]
               exact ih h
           · next i_ne_l =>
-            simp only [Array.getElem_modify_of_ne i_in_bounds _ (Ne.symm i_ne_l)] at h
+            simp only [Array.getElem_modify_of_ne (Ne.symm i_ne_l)] at h
             exact ih i b h
         | some (l, false) =>
           simp only [heq] at h
-          have i_in_bounds : i.1 < acc.size := by simp only [ih.1, i.2.2]
-          have l_in_bounds : l.1 < acc.size := by simp only [ih.1, l.2.2]
           rcases ih with ⟨hsize, ih⟩
           by_cases i = l.1
           · next i_eq_l =>
-            simp only [i_eq_l, Array.getElem_modify_self l_in_bounds] at h
+            simp only [i_eq_l, Array.getElem_modify_self] at h
             by_cases b
             · next b_eq_true =>
               simp only [hasAssignment, b_eq_true, ite_true, hasPos_addNeg] at h
@@ -187,7 +183,7 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))
               rw [c_def] at cOpt_in_arr
               exact cOpt_in_arr
           · next i_ne_l =>
-            simp only [Array.getElem_modify_of_ne i_in_bounds _ (Ne.symm i_ne_l)] at h
+            simp only [Array.getElem_modify_of_ne (Ne.symm i_ne_l)] at h
             exact ih i b h
     rcases List.foldlRecOn arr.toList ofArray_fold_fn (mkArray n unassigned) hb hl with ⟨_h_size, h'⟩
     intro i b h
@@ -281,7 +277,6 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
     intro i b hb
     have hf := f_readyForRupAdd.2.2 i b
     have i_in_bounds : i.1 < f.assignments.size := by rw [f_readyForRupAdd.2.1]; exact i.2.2
-    have l_in_bounds : l.1 < f.assignments.size := by rw [f_readyForRupAdd.2.1]; exact l.2.2
     simp only at hb
     by_cases (i, b) = (l, true)
     · next ib_eq_c =>
@@ -292,7 +287,7 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
       apply DefaultClause.ext
       simp only [unit, hc]
     · next ib_ne_c =>
-      have hb' : hasAssignment b (f.assignments[i.1]'i_in_bounds) := by
+      have hb' : hasAssignment b f.assignments[i.1] := by
         by_cases l.1 = i.1
         · next l_eq_i =>
           have b_eq_false : b = false := by
@@ -302,10 +297,10 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
             · next b_eq_false =>
               simp only [Bool.not_eq_true] at b_eq_false
               exact b_eq_false
-          simp only [hasAssignment, b_eq_false, l_eq_i, Array.getElem_modify_self i_in_bounds, ite_false, hasNeg_addPos, reduceCtorEq] at hb
+          simp only [hasAssignment, b_eq_false, l_eq_i, Array.getElem_modify_self, ite_false, hasNeg_addPos, reduceCtorEq] at hb
           simp only [hasAssignment, b_eq_false, ite_false, hb, reduceCtorEq]
         · next l_ne_i =>
-          simp only [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i] at hb
+          simp only [Array.getElem_modify_of_ne l_ne_i] at hb
           exact hb
       specialize hf hb'
       simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
@@ -322,7 +317,6 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
     intro i b hb
     have hf := f_readyForRupAdd.2.2 i b
     have i_in_bounds : i.1 < f.assignments.size := by rw [f_readyForRupAdd.2.1]; exact i.2.2
-    have l_in_bounds : l.1 < f.assignments.size := by rw [f_readyForRupAdd.2.1]; exact l.2.2
     simp only at hb
     by_cases (i, b) = (l, false)
     · next ib_eq_c =>
@@ -333,7 +327,7 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
       apply DefaultClause.ext
       simp only [unit, hc]
     · next ib_ne_c =>
-      have hb' : hasAssignment b (f.assignments[i.1]'i_in_bounds) := by
+      have hb' : hasAssignment b f.assignments[i.1] := by
         by_cases l.1 = i.1
         · next l_eq_i =>
           have b_eq_false : b = true := by
@@ -341,10 +335,10 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
             · assumption
             · next b_eq_false =>
               simp only [b_eq_false, Subtype.ext l_eq_i, not_true] at ib_ne_c
-          simp only [hasAssignment, b_eq_false, l_eq_i, Array.getElem_modify_self i_in_bounds, ite_true, hasPos_addNeg] at hb
+          simp only [hasAssignment, b_eq_false, l_eq_i, Array.getElem_modify_self, ite_true, hasPos_addNeg] at hb
           simp only [hasAssignment, b_eq_false, ite_true, hb]
         · next l_ne_i =>
-          simp only [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i] at hb
+          simp only [Array.getElem_modify_of_ne l_ne_i] at hb
           exact hb
       specialize hf hb'
       simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
@@ -471,14 +465,14 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
       simp only [deleteOne, heq, hl] at hb
       by_cases l.1.1 = i.1
       · next l_eq_i =>
-        simp only [l_eq_i, Array.getElem_modify_self i_in_bounds] at hb
+        simp only [l_eq_i, Array.getElem_modify_self] at hb
         have l_ne_b : l.2 ≠ b := by
           intro l_eq_b
           rw [← l_eq_b] at hb
           have hb' := not_has_remove f.assignments[i.1] l.2
           simp [hb] at hb'
         replace l_ne_b := Bool.eq_not_of_ne l_ne_b
-        rw [l_ne_b] at hb
+        simp only [l_ne_b] at hb
         have hb := has_remove_irrelevant f.assignments[i.1] b hb
         specialize hf i b hb
         simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
@@ -502,8 +496,8 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
               have idx_in_bounds2 : idx < f.clauses.size := by
                 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
+              simp only [getElem!, id_eq_idx, Array.length_toList, idx_in_bounds2, ↓reduceDIte,
+                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
@@ -512,7 +506,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
           · exact hf
         · exact Or.inr hf
       · next l_ne_i =>
-        simp only [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i] at hb
+        simp only [Array.getElem_modify_of_ne l_ne_i] at hb
         specialize hf i b hb
         simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
           exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool] at hf
@@ -535,8 +529,8 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
               have idx_in_bounds2 : idx < f.clauses.size := by
                 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
+              simp only [getElem!, id_eq_idx, Array.length_toList, idx_in_bounds2, ↓reduceDIte,
+                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]
@@ -595,8 +589,8 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
               have idx_in_bounds2 : idx < f.clauses.size := by
                 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
+              simp only [getElem!, id_eq_idx, Array.length_toList, idx_in_bounds2, ↓reduceDIte,
+                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,19 +461,19 @@ 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'
   rcases List.get_of_mem h with ⟨j, h'⟩
   have j_in_bounds : j < ratHints.size := by
     have j_property := j.2
-    simp only [Array.map_toList, List.length_map] at j_property
+    simp only [Array.toList_map, List.length_map] at j_property
     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_toList_getElem] at c'_in_f
+  simp only [List.get_eq_getElem, Array.toList_map, Array.length_toList, List.getElem_map] at h'
+  rw [← Array.getElem_eq_getElem_toList] at h'
+  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

@@ -115,7 +115,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
         constructor
         · rfl
         · constructor
-          · rw [Array.getElem_modify_self l_in_bounds]
+          · rw [Array.getElem_modify_self]
             simp only [← i_eq_l, h1]
           · constructor
             · simp only [getElem!, l_in_bounds, ↓reduceDIte, Array.get_eq_getElem,
@@ -138,7 +138,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
       · next i_ne_l =>
         apply Or.inl
         simp only [insertUnit, h3, ite_false, reduceCtorEq]
-        rw [Array.getElem_modify_of_ne i_in_bounds _ (Ne.symm i_ne_l)]
+        rw [Array.getElem_modify_of_ne (Ne.symm i_ne_l)]
         constructor
         · exact h1
         · intro j
@@ -197,7 +197,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
               rfl
             · constructor
               · simp only [i_eq_l]
-                rw [Array.getElem_modify_self l_in_bounds]
+                rw [Array.getElem_modify_self]
                 simp only [addAssignment, hl, ← i_eq_l, h2, ite_true, ite_false]
                 apply addNeg_addPos_eq_both
               · constructor
@@ -234,7 +234,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
             · rw [Array.get_push_lt units l j.1 j.2, h1]
             · constructor
               · simp only [i_eq_l]
-                rw [Array.getElem_modify_self l_in_bounds]
+                rw [Array.getElem_modify_self]
                 simp only [addAssignment, hl, ← i_eq_l, h2, ite_true, ite_false]
                 apply addPos_addNeg_eq_both
               · constructor
@@ -277,7 +277,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
         constructor
         · rw [Array.get_push_lt units l j.1 j.2, h1]
         · constructor
-          · rw [Array.getElem_modify_of_ne i_in_bounds _ (Ne.symm i_ne_l), h2]
+          · rw [Array.getElem_modify_of_ne (Ne.symm i_ne_l), h2]
           · constructor
             · exact h3
             · intro k k_ne_j
@@ -319,9 +319,9 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
             by_cases i.1 = l.1.1
             · next i_eq_l =>
               simp only [i_eq_l]
-              rw [Array.getElem_modify_self l_in_bounds]
+              rw [Array.getElem_modify_self]
               simp only [← i_eq_l, h3, add_both_eq_both]
-            · next i_ne_l => rw [Array.getElem_modify_of_ne i_in_bounds _ (Ne.symm i_ne_l), h3]
+            · next i_ne_l => rw [Array.getElem_modify_of_ne (Ne.symm i_ne_l), h3]
         · constructor
           · exact h4
           · intro k k_ne_j1 k_ne_j2
@@ -535,7 +535,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme
       have i_in_bounds : i.1 < assignments.size := by
         rw [hsize]
         exact i.2
-      have h := Array.getElem_modify_of_ne i_in_bounds (removeAssignment units[idx.val].2) ih2
+      have h := Array.getElem_modify_of_ne ih2 (removeAssignment units[idx.val].2) (by simpa using i_in_bounds)
       simp only [Fin.getElem_fin] at h
       rw [h]
       exact ih1
@@ -546,8 +546,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme
       apply Or.inl
       constructor
       · simp only [clearUnit, idx_eq_j, Array.get_eq_getElem, ih1]
-        have i_in_bounds : i.1 < assignments.size := by rw [hsize]; exact i.2
-        rw [Array.getElem_modify_self i_in_bounds, ih2, remove_add_cancel]
+        rw [Array.getElem_modify_self, ih2, remove_add_cancel]
         exact ih3
       · intro k k_ge_idx_add_one
         have k_ge_idx : k.val ≥ idx.val := Nat.le_of_succ_le k_ge_idx_add_one
@@ -568,8 +567,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme
         · constructor
           · simp only [clearUnit, Array.get_eq_getElem]
             specialize ih4 idx (Nat.le_refl idx.1) idx_ne_j
-            have i_in_bounds : i.1 < assignments.size := by rw [hsize]; exact i.2
-            rw [Array.getElem_modify_of_ne i_in_bounds _ ih4]
+            rw [Array.getElem_modify_of_ne ih4]
             exact ih2
           · constructor
             · exact ih3
@@ -593,8 +591,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme
           exact ih2
         · constructor
           · simp only [clearUnit, idx_eq_j1, Array.get_eq_getElem, ih1]
-            have i_in_bounds : i.1 < assignments.size := hsize ▸ i.2
-            rw [Array.getElem_modify_self i_in_bounds, ih3, ih4]
+            rw [Array.getElem_modify_self, ih3, ih4]
             decide
           · constructor
             · simp [hasAssignment, hasNegAssignment, ih4]
@@ -630,8 +627,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme
             exact ih1
           · constructor
             · simp only [clearUnit, idx_eq_j2, Array.get_eq_getElem, ih2]
-              have i_in_bounds : i.1 < assignments.size := hsize ▸ i.2
-              rw [Array.getElem_modify_self i_in_bounds, ih3, ih4]
+              rw [Array.getElem_modify_self, ih3, ih4]
               decide
             · constructor
               · simp only [hasAssignment, hasNegAssignment, ih4, ite_false, not_false_eq_true]
@@ -687,10 +683,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme
                       simp only [Bool.not_eq_true] at h2
                       simp only [Fin.getElem_fin, ih2, ← h1, ← h2, ne_eq] at h3
                       exact h3 rfl
-                  have idx_unit_in_bounds : units[idx.1].1.1 < assignments.size := by
-                    rw [hsize]; exact units[idx.1].1.2.2
-                  have i_in_bounds : i.1 < assignments.size := hsize ▸ i.2
-                  rw [Array.getElem_modify_of_ne i_in_bounds _ idx_res_ne_i]
+                  rw [Array.getElem_modify_of_ne idx_res_ne_i]
                   exact ih3
                 · constructor
                   · exact ih4
@@ -796,7 +789,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
       constructor
       · simp only [List.get, l_eq_i]
       · constructor
-        · simp only [l_eq_i, Array.getElem_modify_self i_in_bounds, List.get, h1]
+        · simp only [l_eq_i, Array.getElem_modify_self, List.get, h1]
         · constructor
           · simp only [List.get, Bool.not_eq_true]
             simp only [getElem!, l_in_bounds, ↓reduceDIte, Array.get_eq_getElem,
@@ -826,7 +819,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
     · next l_ne_i =>
       apply Or.inl
       constructor
-      · rw [Array.getElem_modify_of_ne i_in_bounds (addAssignment l.2) l_ne_i]
+      · rw [Array.getElem_modify_of_ne l_ne_i]
         exact h1
       · intro l' l'_in_list
         simp only [List.find?, List.mem_cons] at l'_in_list
@@ -865,7 +858,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
             apply And.intro l_eq_true ∘ And.intro l'_eq_false
             constructor
             · simp only [l'] at l'_eq_false
-              simp only [l_eq_i, addAssignment, l_eq_true, ite_true, Array.getElem_modify_self i_in_bounds, h1,
+              simp only [l_eq_i, addAssignment, l_eq_true, ite_true, Array.getElem_modify_self, h1,
                 l'_eq_false, ite_false]
               apply addPos_addNeg_eq_both
             · constructor
@@ -914,7 +907,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
             apply And.intro l'_eq_true ∘ And.intro l_eq_false
             constructor
             · simp only [l'] at l'_eq_true
-              simp only [l_eq_i, addAssignment, l'_eq_true, ite_true, Array.getElem_modify_self i_in_bounds, h1,
+              simp only [l_eq_i, addAssignment, l'_eq_true, ite_true, Array.getElem_modify_self, h1,
                 l_eq_false, ite_false]
               apply addNeg_addPos_eq_both
             · constructor
@@ -950,7 +943,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
       constructor
       · exact j_eq_i
       · constructor
-        · rw [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i]
+        · rw [Array.getElem_modify_of_ne l_ne_i]
           exact h1
         · apply And.intro h2
           intro k k_ne_j_succ
@@ -1002,7 +995,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
       all_goals
         simp (config := {decide := true}) [getElem!, l_eq_i, i_in_bounds, h1, decidableGetElem?] at h
     constructor
-    · rw [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i]
+    · rw [Array.getElem_modify_of_ne l_ne_i]
       exact h1
     · constructor
       · exact h2
@@ -1140,25 +1133,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 [derivedLits_arr_def, Array.getElem_eq_toList_getElem, k2_eq_false, li_eq_lj, li] at li_eq_true
+        simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_getElem_toList] at li_eq_lj
+        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 +1160,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 +1173,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 [derivedLits_arr_def, Array.getElem_eq_toList_getElem, k1_eq_true, li_eq_lj, li] at li_eq_false
+        simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_getElem_toList] at li_eq_lj
+        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 +1188,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 +1225,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 +1237,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 +1251,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 +1272,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/LRAT/Internal/Formula/RupAddSound.lean

@@ -39,27 +39,26 @@ theorem contradiction_of_insertUnit_success {n : Nat} (assignments : Array Assig
     rcases insertUnit_success with foundContradiction_eq_true | assignments_l_ne_unassigned
     · simp only [insertUnit, hl, ite_false]
       rcases h foundContradiction_eq_true with ⟨i, h⟩
-      have i_in_bounds : i.1 < assignments.size := by rw [assignments_size]; exact i.2.2
       apply Exists.intro i
       by_cases l.1.1 = i.1
       · next l_eq_i =>
-        simp [l_eq_i, Array.getElem_modify_self i_in_bounds, h]
+        simp [l_eq_i, Array.getElem_modify_self, h]
         exact add_both_eq_both l.2
       · next l_ne_i =>
-        simp [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i]
+        simp [Array.getElem_modify_of_ne l_ne_i]
         exact h
     · apply Exists.intro l.1
-      simp only [insertUnit, hl, ite_false, Array.getElem_modify_self l_in_bounds, reduceCtorEq]
+      simp only [insertUnit, hl, ite_false, Array.getElem_modify_self, reduceCtorEq]
       simp only [getElem!, l_in_bounds, dite_true, decidableGetElem?] at assignments_l_ne_unassigned
       by_cases l.2
       · next l_eq_true =>
-        rw [l_eq_true]
+        simp only [l_eq_true]
         simp only [hasAssignment, l_eq_true, hasPosAssignment, getElem!, l_in_bounds, dite_true, ite_true,
           Bool.not_eq_true, decidableGetElem?] at hl
         split at hl <;> simp_all (config := { decide := true })
       · next l_eq_false =>
         simp only [Bool.not_eq_true] at l_eq_false
-        rw [l_eq_false]
+        simp only [l_eq_false]
         simp [hasAssignment, l_eq_false, hasNegAssignment, getElem!, l_in_bounds, decidableGetElem?] at hl
         split at hl <;> simp_all (config := { decide := true })
 
@@ -681,7 +680,7 @@ theorem confirmRupHint_preserves_motive {n : Nat} (f : DefaultFormula n) (rupHin
           by_cases l.1 = i.1
           · next l_eq_i =>
             simp only [getElem!, Array.size_modify, i_in_bounds, ↓ reduceDIte,
-              Array.get_eq_getElem, l_eq_i, Array.getElem_modify_self i_in_bounds (addAssignment b), decidableGetElem?]
+              Array.get_eq_getElem, l_eq_i, Array.getElem_modify_self (addAssignment b), decidableGetElem?]
             simp only [getElem!, i_in_bounds, dite_true, Array.get_eq_getElem, decidableGetElem?] at pacc
             by_cases pi : p i
             · simp only [pi, decide_False]
@@ -705,7 +704,7 @@ theorem confirmRupHint_preserves_motive {n : Nat} (f : DefaultFormula n) (rupHin
                 exact pacc
           · next l_ne_i =>
             simp only [getElem!, Array.size_modify, i_in_bounds,
-              Array.getElem_modify_of_ne i_in_bounds _ l_ne_i, dite_true,
+              Array.getElem_modify_of_ne l_ne_i, dite_true,
               Array.get_eq_getElem, decidableGetElem?]
             simp only [getElem!, i_in_bounds, dite_true, decidableGetElem?] at pacc
             exact pacc

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**
-```lean
-import Lake
-open Lake DSL
+**lakefile.toml**
+```toml
+name = "hello"
+version = "0.1.0"
+defaultTargets = ["hello"]
 
-package «hello» where
-  -- add package configuration options here
+[[lean_lib]]
+name = "Hello"
 
-lean_lib «Hello» where
-  -- add library configuration options here
-
-@[default_target]
-lean_exe «hello» where
-  root := `Main
+[[lean_exe]]
+name = "hello"
+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) {