chore: update stage0

.github/workflows/pr-body.yml

@@ -1,7 +1,6 @@
 name: Check PR body for changelog convention
 
 on:
-  merge_group:
   pull_request:
     types: [opened, synchronize, reopened, edited, labeled, converted_to_draft, ready_for_review]
 
@@ -10,7 +9,6 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Check PR body
-        if: github.event_name == 'pull_request'
         uses: actions/github-script@v7
         with:
           script: |

src/Init/Core.lean

@@ -1922,12 +1922,12 @@ represents an element of `Squash α` the same as `α` itself
 `Squash.lift` will extract a value in any subsingleton `β` from a function on `α`,
 while `Nonempty.rec` can only do the same when `β` is a proposition.
 -/
-def Squash (α : Sort u) := Quot (fun (_ _ : α) => True)
+def Squash (α : Type u) := Quot (fun (_ _ : α) => True)
 
 /-- The canonical quotient map into `Squash α`. -/
-def Squash.mk {α : Sort u} (x : α) : Squash α := Quot.mk _ x
+def Squash.mk {α : Type u} (x : α) : Squash α := Quot.mk _ x
 
-theorem Squash.ind {α : Sort u} {motive : Squash α → Prop} (h : ∀ (a : α), motive (Squash.mk a)) : ∀ (q : Squash α), motive q :=
+theorem Squash.ind {α : Type u} {motive : Squash α → Prop} (h : ∀ (a : α), motive (Squash.mk a)) : ∀ (q : Squash α), motive q :=
   Quot.ind h
 
 /-- If `β` is a subsingleton, then a function `α → β` lifts to `Squash α → β`. -/

src/Init/Data/Array.lean

@@ -18,4 +18,3 @@ import Init.Data.Array.Bootstrap
 import Init.Data.Array.GetLit
 import Init.Data.Array.MapIdx
 import Init.Data.Array.Set
-import Init.Data.Array.Monadic

src/Init/Data/Array/Attach.lean

@@ -43,13 +43,6 @@ Unsafe implementation of `attachWith`, taking advantage of the fact that the rep
     l.attach.toList = l.toList.attachWith (· ∈ l) (by simp [mem_toList]) := by
   simp [attach]
 
-@[simp] theorem _root_.List.attachWith_mem_toArray {l : List α} :
-    l.attachWith (fun x => x ∈ l.toArray) (fun x h => by simpa using h) =
-      l.attach.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
-  simp only [List.attachWith, List.attach, List.map_pmap]
-  apply List.pmap_congr_left
-  simp
-
 /-! ## unattach
 
 `Array.unattach` is the (one-sided) inverse of `Array.attach`. It is a synonym for `Array.map Subtype.val`.
@@ -90,7 +83,7 @@ def unattach {α : Type _} {p : α → Prop} (l : Array { x // p x }) := l.map (
 
 @[simp] theorem unattach_attach {l : Array α} : l.attach.unattach = l := by
   cases l
-  simp only [List.attach_toArray, List.unattach_toArray, List.unattach_attachWith]
+  simp
 
 @[simp] theorem unattach_attachWith {p : α → Prop} {l : Array α}
     {H : ∀ a ∈ l, p a} :

src/Init/Data/Array/Bootstrap.lean

@@ -15,26 +15,26 @@ This file contains some theorems about `Array` and `List` needed for `Init.Data.
 
 namespace Array
 
-theorem foldlM_toList.aux [Monad m]
+theorem foldlM_eq_foldlM_toList.aux [Monad m]
     (f : β → α → m β) (arr : Array α) (i j) (H : arr.size ≤ i + j) (b) :
     foldlM.loop f arr arr.size (Nat.le_refl _) i j b = (arr.toList.drop j).foldlM f b := by
   unfold foldlM.loop
   split; split
   · cases Nat.not_le_of_gt ‹_› (Nat.zero_add _ ▸ H)
   · rename_i i; rw [Nat.succ_add] at H
-    simp [foldlM_toList.aux f arr i (j+1) H]
+    simp [foldlM_eq_foldlM_toList.aux f arr i (j+1) H]
     rw (occs := .pos [2]) [← List.getElem_cons_drop_succ_eq_drop ‹_›]
     rfl
   · rw [List.drop_of_length_le (Nat.ge_of_not_lt ‹_›)]; rfl
 
-@[simp] theorem foldlM_toList [Monad m]
+theorem foldlM_eq_foldlM_toList [Monad m]
     (f : β → α → m β) (init : β) (arr : Array α) :
-    arr.toList.foldlM f init = arr.foldlM f init := by
-  simp [foldlM, foldlM_toList.aux]
+    arr.foldlM f init = arr.toList.foldlM f init := by
+  simp [foldlM, foldlM_eq_foldlM_toList.aux]
 
-@[simp] theorem foldl_toList (f : β → α → β) (init : β) (arr : Array α) :
-    arr.toList.foldl f init = arr.foldl f init :=
-  List.foldl_eq_foldlM .. ▸ foldlM_toList ..
+theorem foldl_eq_foldl_toList (f : β → α → β) (init : β) (arr : Array α) :
+    arr.foldl f init = arr.toList.foldl f init :=
+  List.foldl_eq_foldlM .. ▸ foldlM_eq_foldlM_toList ..
 
 theorem foldrM_eq_reverse_foldlM_toList.aux [Monad m]
     (f : α → β → m β) (arr : Array α) (init : β) (i h) :
@@ -51,23 +51,23 @@ theorem foldrM_eq_reverse_foldlM_toList [Monad m] (f : α → β → m β) (init
   match arr, this with | _, .inl rfl => rfl | arr, .inr h => ?_
   simp [foldrM, h, ← foldrM_eq_reverse_foldlM_toList.aux, List.take_length]
 
-@[simp] theorem foldrM_toList [Monad m]
+theorem foldrM_eq_foldrM_toList [Monad m]
     (f : α → β → m β) (init : β) (arr : Array α) :
-    arr.toList.foldrM f init = arr.foldrM f init := by
+    arr.foldrM f init = arr.toList.foldrM f init := by
   rw [foldrM_eq_reverse_foldlM_toList, List.foldlM_reverse]
 
-@[simp] theorem foldr_toList (f : α → β → β) (init : β) (arr : Array α) :
-    arr.toList.foldr f init = arr.foldr f init :=
-  List.foldr_eq_foldrM .. ▸ foldrM_toList ..
+theorem foldr_eq_foldr_toList (f : α → β → β) (init : β) (arr : Array α) :
+    arr.foldr f init = arr.toList.foldr f init :=
+  List.foldr_eq_foldrM .. ▸ foldrM_eq_foldrM_toList ..
 
 @[simp] theorem push_toList (arr : Array α) (a : α) : (arr.push a).toList = arr.toList ++ [a] := by
   simp [push, List.concat_eq_append]
 
 @[simp] theorem toListAppend_eq (arr : Array α) (l) : arr.toListAppend l = arr.toList ++ l := by
-  simp [toListAppend, ← foldr_toList]
+  simp [toListAppend, foldr_eq_foldr_toList]
 
 @[simp] theorem toListImpl_eq (arr : Array α) : arr.toListImpl = arr.toList := by
-  simp [toListImpl, ← foldr_toList]
+  simp [toListImpl, foldr_eq_foldr_toList]
 
 @[simp] theorem pop_toList (arr : Array α) : arr.pop.toList = arr.toList.dropLast := rfl
 
@@ -76,7 +76,7 @@ theorem foldrM_eq_reverse_foldlM_toList [Monad m] (f : α → β → m β) (init
 @[simp] theorem toList_append (arr arr' : Array α) :
     (arr ++ arr').toList = arr.toList ++ arr'.toList := by
   rw [← append_eq_append]; unfold Array.append
-  rw [← foldl_toList]
+  rw [foldl_eq_foldl_toList]
   induction arr'.toList generalizing arr <;> simp [*]
 
 @[simp] theorem toList_empty : (#[] : Array α).toList = [] := rfl
@@ -98,44 +98,20 @@ theorem foldrM_eq_reverse_foldlM_toList [Monad m] (f : α → β → m β) (init
   rw [← appendList_eq_append]; unfold Array.appendList
   induction l generalizing arr <;> simp [*]
 
-@[deprecated "Use the reverse direction of `foldrM_toList`." (since := "2024-11-13")]
-theorem foldrM_eq_foldrM_toList [Monad m]
-    (f : α → β → m β) (init : β) (arr : Array α) :
-    arr.foldrM f init = arr.toList.foldrM f init := by
-  simp
+@[deprecated foldlM_eq_foldlM_toList (since := "2024-09-09")]
+abbrev foldlM_eq_foldlM_data := @foldlM_eq_foldlM_toList
 
-@[deprecated "Use the reverse direction of `foldlM_toList`." (since := "2024-11-13")]
-theorem foldlM_eq_foldlM_toList [Monad m]
-    (f : β → α → m β) (init : β) (arr : Array α) :
-    arr.foldlM f init = arr.toList.foldlM f init:= by
-  simp
-
-@[deprecated "Use the reverse direction of `foldr_toList`." (since := "2024-11-13")]
-theorem foldr_eq_foldr_toList
-    (f : α → β → β) (init : β) (arr : Array α) :
-    arr.foldr f init = arr.toList.foldr f init := by
-  simp
-
-@[deprecated "Use the reverse direction of `foldl_toList`." (since := "2024-11-13")]
-theorem foldl_eq_foldl_toList
-    (f : β → α → β) (init : β) (arr : Array α) :
-    arr.foldl f init = arr.toList.foldl f init:= by
-  simp
-
-@[deprecated foldlM_toList (since := "2024-09-09")]
-abbrev foldlM_eq_foldlM_data := @foldlM_toList
-
-@[deprecated foldl_toList (since := "2024-09-09")]
-abbrev foldl_eq_foldl_data := @foldl_toList
+@[deprecated foldl_eq_foldl_toList (since := "2024-09-09")]
+abbrev foldl_eq_foldl_data := @foldl_eq_foldl_toList
 
 @[deprecated foldrM_eq_reverse_foldlM_toList (since := "2024-09-09")]
 abbrev foldrM_eq_reverse_foldlM_data := @foldrM_eq_reverse_foldlM_toList
 
-@[deprecated foldrM_toList (since := "2024-09-09")]
-abbrev foldrM_eq_foldrM_data := @foldrM_toList
+@[deprecated foldrM_eq_foldrM_toList (since := "2024-09-09")]
+abbrev foldrM_eq_foldrM_data := @foldrM_eq_foldrM_toList
 
-@[deprecated foldr_toList (since := "2024-09-09")]
-abbrev foldr_eq_foldr_data := @foldr_toList
+@[deprecated foldr_eq_foldr_toList (since := "2024-09-09")]
+abbrev foldr_eq_foldr_data := @foldr_eq_foldr_toList
 
 @[deprecated push_toList (since := "2024-09-09")]
 abbrev push_data := @push_toList

src/Init/Data/Array/Lemmas.lean

@@ -151,15 +151,15 @@ theorem foldrM_toArray [Monad m] (f : α → β → m β) (init : β) (l : List
 
 theorem foldlM_toArray [Monad m] (f : β → α → m β) (init : β) (l : List α) :
     l.toArray.foldlM f init = l.foldlM f init := by
-  rw [foldlM_toList]
+  rw [foldlM_eq_foldlM_toList]
 
 theorem foldr_toArray (f : α → β → β) (init : β) (l : List α) :
     l.toArray.foldr f init = l.foldr f init := by
-  rw [foldr_toList]
+  rw [foldr_eq_foldr_toList]
 
 theorem foldl_toArray (f : β → α → β) (init : β) (l : List α) :
     l.toArray.foldl f init = l.foldl f init := by
-  rw [foldl_toList]
+  rw [foldl_eq_foldl_toList]
 
 /-- Variant of `foldrM_toArray` with a side condition for the `start` argument. -/
 @[simp] theorem foldrM_toArray' [Monad m] (f : α → β → m β) (init : β) (l : List α)
@@ -174,21 +174,21 @@ theorem foldl_toArray (f : β → α → β) (init : β) (l : List α) :
     (h : stop = l.toArray.size) :
     l.toArray.foldlM f init 0 stop = l.foldlM f init := by
   subst h
-  rw [foldlM_toList]
+  rw [foldlM_eq_foldlM_toList]
 
 /-- Variant of `foldr_toArray` with a side condition for the `start` argument. -/
 @[simp] theorem foldr_toArray' (f : α → β → β) (init : β) (l : List α)
     (h : start = l.toArray.size) :
     l.toArray.foldr f init start 0 = l.foldr f init := by
   subst h
-  rw [foldr_toList]
+  rw [foldr_eq_foldr_toList]
 
 /-- Variant of `foldl_toArray` with a side condition for the `stop` argument. -/
 @[simp] theorem foldl_toArray' (f : β → α → β) (init : β) (l : List α)
     (h : stop = l.toArray.size) :
     l.toArray.foldl f init 0 stop = l.foldl f init := by
   subst h
-  rw [foldl_toList]
+  rw [foldl_eq_foldl_toList]
 
 @[simp] theorem append_toArray (l₁ l₂ : List α) :
     l₁.toArray ++ l₂.toArray = (l₁ ++ l₂).toArray := by
@@ -202,9 +202,6 @@ theorem foldl_toArray (f : β → α → β) (init : β) (l : List α) :
 @[simp] theorem foldl_push {l : List α} {as : Array α} : l.foldl Array.push as = as ++ l.toArray := by
   induction l generalizing as <;> simp [*]
 
-@[simp] theorem foldr_push {l : List α} {as : Array α} : l.foldr (fun a b => push b a) as = as ++ l.reverse.toArray := by
-  rw [foldr_eq_foldl_reverse, foldl_push]
-
 @[simp] theorem findSomeM?_toArray [Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α) :
     l.toArray.findSomeM? f = l.findSomeM? f := by
   rw [Array.findSomeM?]
@@ -365,8 +362,7 @@ namespace Array
 
 theorem foldrM_push [Monad m] (f : α → β → m β) (init : β) (arr : Array α) (a : α) :
     (arr.push a).foldrM f init = f a init >>= arr.foldrM f := by
-  simp only [foldrM_eq_reverse_foldlM_toList, push_toList, List.reverse_append, List.reverse_cons,
-    List.reverse_nil, List.nil_append, List.singleton_append, List.foldlM_cons, List.foldlM_reverse]
+  simp [foldrM_eq_reverse_foldlM_toList, -size_push]
 
 /--
 Variant of `foldrM_push` with `h : start = arr.size + 1`
@@ -392,11 +388,11 @@ rather than `(arr.push a).size` as the argument.
 @[inline] def toListRev (arr : Array α) : List α := arr.foldl (fun l t => t :: l) []
 
 @[simp] theorem toListRev_eq (arr : Array α) : arr.toListRev = arr.toList.reverse := by
-  rw [toListRev, ← foldl_toList, ← List.foldr_reverse, List.foldr_cons_nil]
+  rw [toListRev, foldl_eq_foldl_toList, ← List.foldr_reverse, List.foldr_cons_nil]
 
 theorem mapM_eq_foldlM [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) :
     arr.mapM f = arr.foldlM (fun bs a => bs.push <$> f a) #[] := by
-  rw [mapM, aux, ← foldlM_toList]; rfl
+  rw [mapM, aux, foldlM_eq_foldlM_toList]; rfl
 where
   aux (i r) :
       mapM.map f arr i r = (arr.toList.drop i).foldlM (fun bs a => bs.push <$> f a) r := by
@@ -411,7 +407,7 @@ where
 
 @[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_toList (fun bs a => push bs (f a)) #[] arr).symm |>.trans
+  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]
@@ -1027,7 +1023,7 @@ theorem foldr_congr {as bs : Array α} (h₀ : as = bs) {f g : α → β → β}
 
 theorem mapM_eq_mapM_toList [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) :
     arr.mapM f = List.toArray <$> (arr.toList.mapM f) := by
-  rw [mapM_eq_foldlM, ← foldlM_toList, ← List.foldrM_reverse]
+  rw [mapM_eq_foldlM, foldlM_eq_foldlM_toList, ← List.foldrM_reverse]
   conv => rhs; rw [← List.reverse_reverse arr.toList]
   induction arr.toList.reverse with
   | nil => simp
@@ -1152,7 +1148,7 @@ theorem getElem?_modify {as : Array α} {i : Nat} {f : α → α} {j : Nat} :
 @[simp] theorem toList_filter (p : α → Bool) (l : Array α) :
     (l.filter p).toList = l.toList.filter p := by
   dsimp only [filter]
-  rw [← foldl_toList]
+  rw [foldl_eq_foldl_toList]
   generalize l.toList = l
   suffices ∀ a, (List.foldl (fun r a => if p a = true then push r a else r) a l).toList =
       a.toList ++ List.filter p l by
@@ -1183,7 +1179,7 @@ theorem filter_congr {as bs : Array α} (h : as = bs)
 @[simp] theorem toList_filterMap (f : α → Option β) (l : Array α) :
     (l.filterMap f).toList = l.toList.filterMap f := by
   dsimp only [filterMap, filterMapM]
-  rw [← foldlM_toList]
+  rw [foldlM_eq_foldlM_toList]
   generalize l.toList = l
   have this : ∀ a : Array β, (Id.run (List.foldlM (m := Id) ?_ a l)).toList =
     a.toList ++ List.filterMap f l := ?_
@@ -1262,7 +1258,7 @@ theorem getElem?_append {as bs : Array α} {n : Nat} :
 @[simp] theorem toList_flatten {l : Array (Array α)} :
     l.flatten.toList = (l.toList.map toList).flatten := by
   dsimp [flatten]
-  simp only [← foldl_toList]
+  simp only [foldl_eq_foldl_toList]
   generalize l.toList = l
   have : ∀ a : Array α, (List.foldl ?_ a l).toList = a.toList ++ ?_ := ?_
   exact this #[]

src/Init/Data/Array/Monadic.lean

@@ -1,159 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kim Morrison
--/
-prelude
-import Init.Data.Array.Lemmas
-import Init.Data.Array.Attach
-import Init.Data.List.Monadic
-
-/-!
-# Lemmas about `Array.forIn'` and `Array.forIn`.
--/
-
-namespace Array
-
-open Nat
-
-/-! ## Monadic operations -/
-
-/-! ### mapM -/
-
-theorem mapM_eq_foldlM_push [Monad m] [LawfulMonad m] (f : α → m β) (l : Array α) :
-    mapM f l = l.foldlM (fun acc a => return (acc.push (← f a))) #[] := by
-  rcases l with ⟨l⟩
-  simp only [List.mapM_toArray, bind_pure_comp, size_toArray, List.foldlM_toArray']
-  rw [List.mapM_eq_reverse_foldlM_cons]
-  simp only [bind_pure_comp, Functor.map_map]
-  suffices ∀ (k), (fun a => a.reverse.toArray) <$> List.foldlM (fun acc a => (fun a => a :: acc) <$> f a) k l =
-      List.foldlM (fun acc a => acc.push <$> f a) k.reverse.toArray l by
-    exact this []
-  intro k
-  induction l generalizing k with
-  | nil => simp
-  | cons a as ih =>
-    simp [ih, List.foldlM_cons]
-
-/-! ### foldlM and foldrM -/
-
-theorem foldlM_map [Monad m] (f : β₁ → β₂) (g : α → β₂ → m α) (l : Array β₁) (init : α) :
-    (l.map f).foldlM g init = l.foldlM (fun x y => g x (f y)) init := by
-  cases l
-  rw [List.map_toArray] -- Why doesn't this fire via `simp`?
-  simp [List.foldlM_map]
-
-theorem foldrM_map [Monad m] [LawfulMonad m] (f : β₁ → β₂) (g : β₂ → α → m α) (l : Array β₁)
-    (init : α) : (l.map f).foldrM g init = l.foldrM (fun x y => g (f x) y) init := by
-  cases l
-  rw [List.map_toArray] -- Why doesn't this fire via `simp`?
-  simp [List.foldrM_map]
-
-theorem foldlM_filterMap [Monad m] [LawfulMonad m] (f : α → Option β) (g : γ → β → m γ) (l : Array α) (init : γ) :
-    (l.filterMap f).foldlM g init =
-      l.foldlM (fun x y => match f y with | some b => g x b | none => pure x) init := by
-  cases l
-  rw [List.filterMap_toArray] -- Why doesn't this fire via `simp`?
-  simp [List.foldlM_filterMap]
-  rfl
-
-theorem foldrM_filterMap [Monad m] [LawfulMonad m] (f : α → Option β) (g : β → γ → m γ) (l : Array α) (init : γ) :
-    (l.filterMap f).foldrM g init =
-      l.foldrM (fun x y => match f x with | some b => g b y | none => pure y) init := by
-  cases l
-  rw [List.filterMap_toArray] -- Why doesn't this fire via `simp`?
-  simp [List.foldrM_filterMap]
-  rfl
-
-theorem foldlM_filter [Monad m] [LawfulMonad m] (p : α → Bool) (g : β → α → m β) (l : Array α) (init : β) :
-    (l.filter p).foldlM g init =
-      l.foldlM (fun x y => if p y then g x y else pure x) init := by
-  cases l
-  rw [List.filter_toArray] -- Why doesn't this fire via `simp`?
-  simp [List.foldlM_filter]
-
-theorem foldrM_filter [Monad m] [LawfulMonad m] (p : α → Bool) (g : α → β → m β) (l : Array α) (init : β) :
-    (l.filter p).foldrM g init =
-      l.foldrM (fun x y => if p x then g x y else pure y) init := by
-  cases l
-  rw [List.filter_toArray] -- Why doesn't this fire via `simp`?
-  simp [List.foldrM_filter]
-
-/-! ### forIn' -/
-
-/--
-We can express a for loop over an array as a fold,
-in which whenever we reach `.done b` we keep that value through the rest of the fold.
--/
-theorem forIn'_eq_foldlM [Monad m] [LawfulMonad m]
-    (l : Array α) (f : (a : α) → a ∈ l → β → m (ForInStep β)) (init : β) :
-    forIn' l init f = ForInStep.value <$>
-      l.attach.foldlM (fun b ⟨a, m⟩ => match b with
-        | .yield b => f a m b
-        | .done b => pure (.done b)) (ForInStep.yield init) := by
-  cases l
-  rw [List.attach_toArray] -- Why doesn't this fire via `simp`?
-  simp only [List.forIn'_toArray, List.forIn'_eq_foldlM, List.attachWith_mem_toArray, size_toArray,
-    List.length_map, List.length_attach, List.foldlM_toArray', List.foldlM_map]
-  congr
-
-/-- We can express a for loop over an array which always yields as a fold. -/
-@[simp] theorem forIn'_yield_eq_foldlM [Monad m] [LawfulMonad m]
-    (l : Array α) (f : (a : α) → a ∈ l → β → m γ) (g : (a : α) → a ∈ l → β → γ → β) (init : β) :
-    forIn' l init (fun a m b => (fun c => .yield (g a m b c)) <$> f a m b) =
-      l.attach.foldlM (fun b ⟨a, m⟩ => g a m b <$> f a m b) init := by
-  cases l
-  rw [List.attach_toArray] -- Why doesn't this fire via `simp`?
-  simp [List.foldlM_map]
-
-theorem forIn'_pure_yield_eq_foldl [Monad m] [LawfulMonad m]
-    (l : Array α) (f : (a : α) → a ∈ l → β → β) (init : β) :
-    forIn' l init (fun a m b => pure (.yield (f a m b))) =
-      pure (f := m) (l.attach.foldl (fun b ⟨a, h⟩ => f a h b) init) := by
-  cases l
-  simp [List.forIn'_pure_yield_eq_foldl, List.foldl_map]
-
-@[simp] theorem forIn'_yield_eq_foldl
-    (l : Array α) (f : (a : α) → a ∈ l → β → β) (init : β) :
-    forIn' (m := Id) l init (fun a m b => .yield (f a m b)) =
-      l.attach.foldl (fun b ⟨a, h⟩ => f a h b) init := by
-  cases l
-  simp [List.foldl_map]
-
-/--
-We can express a for loop over an array as a fold,
-in which whenever we reach `.done b` we keep that value through the rest of the fold.
--/
-theorem forIn_eq_foldlM [Monad m] [LawfulMonad m]
-    (f : α → β → m (ForInStep β)) (init : β) (l : Array α) :
-    forIn l init f = ForInStep.value <$>
-      l.foldlM (fun b a => match b with
-        | .yield b => f a b
-        | .done b => pure (.done b)) (ForInStep.yield init) := by
-  cases l
-  simp only [List.forIn_toArray, List.forIn_eq_foldlM, size_toArray, List.foldlM_toArray']
-  congr
-
-/-- We can express a for loop over an array which always yields as a fold. -/
-@[simp] theorem forIn_yield_eq_foldlM [Monad m] [LawfulMonad m]
-    (l : Array α) (f : α → β → m γ) (g : α → β → γ → β) (init : β) :
-    forIn l init (fun a b => (fun c => .yield (g a b c)) <$> f a b) =
-      l.foldlM (fun b a => g a b <$> f a b) init := by
-  cases l
-  simp [List.foldlM_map]
-
-theorem forIn_pure_yield_eq_foldl [Monad m] [LawfulMonad m]
-    (l : Array α) (f : α → β → β) (init : β) :
-    forIn l init (fun a b => pure (.yield (f a b))) =
-      pure (f := m) (l.foldl (fun b a => f a b) init) := by
-  cases l
-  simp [List.forIn_pure_yield_eq_foldl, List.foldl_map]
-
-@[simp] theorem forIn_yield_eq_foldl
-    (l : Array α) (f : α → β → β) (init : β) :
-    forIn (m := Id) l init (fun a b => .yield (f a b)) =
-      l.foldl (fun b a => f a b) init := by
-  cases l
-  simp [List.foldl_map]
-
-end Array

src/Init/Data/Array/Subarray.lean

@@ -15,6 +15,15 @@ structure Subarray (α : Type u)  where
   start_le_stop : start ≤ stop
   stop_le_array_size : stop ≤ array.size
 
+@[deprecated Subarray.array (since := "2024-04-13")]
+abbrev Subarray.as (s : Subarray α) : Array α := s.array
+
+@[deprecated Subarray.start_le_stop (since := "2024-04-13")]
+theorem Subarray.h₁ (s : Subarray α) : s.start ≤ s.stop := s.start_le_stop
+
+@[deprecated Subarray.stop_le_array_size (since := "2024-04-13")]
+theorem Subarray.h₂ (s : Subarray α) : s.stop ≤ s.array.size := s.stop_le_array_size
+
 namespace Subarray
 
 def size (s : Subarray α) : Nat :=

src/Init/Data/BitVec/Basic.lean

@@ -29,6 +29,9 @@ section Nat
 
 instance natCastInst : NatCast (BitVec w) := ⟨BitVec.ofNat w⟩
 
+@[deprecated isLt (since := "2024-03-12")]
+theorem toNat_lt (x : BitVec n) : x.toNat < 2^n := x.isLt
+
 /-- Theorem for normalizing the bit vector literal representation. -/
 -- TODO: This needs more usage data to assess which direction the simp should go.
 @[simp, bv_toNat] theorem ofNat_eq_ofNat : @OfNat.ofNat (BitVec n) i _ = .ofNat n i := rfl

src/Init/Data/Fin/Lemmas.lean

@@ -642,7 +642,7 @@ theorem pred_add_one (i : Fin (n + 2)) (h : (i : Nat) < n + 1) :
   ext
   simp
 
-@[simp] theorem subNat_one_succ (i : Fin (n + 1)) (h : 1 ≤ (i : Nat)) : (subNat 1 i h).succ = i := by
+@[simp] theorem subNat_one_succ (i : Fin (n + 1)) (h : 1 ≤ ↑i) : (subNat 1 i h).succ = i := by
   ext
   simp
   omega

src/Init/Data/List/Impl.lean

@@ -91,7 +91,7 @@ The following operations are given `@[csimp]` replacements below:
 @[specialize] def foldrTR (f : α → β → β) (init : β) (l : List α) : β := l.toArray.foldr f init
 
 @[csimp] theorem foldr_eq_foldrTR : @foldr = @foldrTR := by
-  funext α β f init l; simp [foldrTR, ← Array.foldr_toList, -Array.size_toArray]
+  funext α β f init l; simp [foldrTR, Array.foldr_eq_foldr_toList, -Array.size_toArray]
 
 /-! ### flatMap  -/
 
@@ -331,7 +331,7 @@ def enumFromTR (n : Nat) (l : List α) : List (Nat × α) :=
     | a::as, n => by
       rw [← show _ + as.length = n + (a::as).length from Nat.succ_add .., foldr, go as]
       simp [enumFrom, f]
-  rw [← Array.foldr_toList]
+  rw [Array.foldr_eq_foldr_toList]
   simp [go]
 
 /-! ## Other list operations -/

src/Init/Data/Nat/Linear.lean

@@ -52,23 +52,25 @@ def Poly.denote (ctx : Context) (p : Poly) : Nat :=
   | [] => 0
   | (k, v) :: p => Nat.add (Nat.mul k (v.denote ctx)) (denote ctx p)
 
-def Poly.insert (k : Nat) (v : Var) (p : Poly) : Poly :=
+def Poly.insertSorted (k : Nat) (v : Var) (p : Poly) : Poly :=
   match p with
   | [] => [(k, v)]
-  | (k', v') :: p =>
-    bif Nat.blt v v' then
-      (k, v) :: (k', v') :: p
-    else bif Nat.beq v v' then
-      (k + k', v') :: p
-    else
-      (k', v') :: insert k v p
+  | (k', v') :: p => bif Nat.blt v v' then (k, v) :: (k', v') :: p else (k', v') :: insertSorted k v p
 
-def Poly.norm (p : Poly) : Poly := go p []
-where
-  go (p : Poly) (r : Poly) : Poly :=
+def Poly.sort (p : Poly) : Poly :=
+  let rec go (p : Poly) (r : Poly) : Poly :=
     match p with
     | [] => r
-    | (k, v) :: p => go p (r.insert k v)
+    | (k, v) :: p => go p (r.insertSorted k v)
+  go p []
+
+def Poly.fuse (p : Poly) : Poly :=
+  match p with
+  | []  => []
+  | (k, v) :: p =>
+    match fuse p with
+    | [] => [(k, v)]
+    | (k', v') :: p' => bif v == v' then (Nat.add k k', v)::p' else (k, v) :: (k', v') :: p'
 
 def Poly.mul (k : Nat) (p : Poly) : Poly :=
   bif k == 0 then
@@ -144,17 +146,15 @@ def Poly.combineAux (fuel : Nat) (p₁ p₂ : Poly) : Poly :=
 def Poly.combine (p₁ p₂ : Poly) : Poly :=
   combineAux hugeFuel p₁ p₂
 
-def Expr.toPoly (e : Expr) :=
-  go 1 e []
-where
-  -- Implementation note: This assembles the result using difference lists
-  -- to avoid `++` on lists.
-  go (coeff : Nat) : Expr → (Poly → Poly)
-    | Expr.num k    => bif k == 0 then id else ((coeff * k, fixedVar) :: ·)
-    | Expr.var i    => ((coeff, i) :: ·)
-    | Expr.add a b  => go coeff a ∘ go coeff b
-    | Expr.mulL k a
-    | Expr.mulR a k => bif k == 0 then id else go (coeff * k) a
+def Expr.toPoly : Expr → Poly
+  | Expr.num k    => bif k == 0 then [] else [ (k, fixedVar) ]
+  | Expr.var i    => [(1, i)]
+  | Expr.add a b  => a.toPoly ++ b.toPoly
+  | Expr.mulL k a => a.toPoly.mul k
+  | Expr.mulR a k => a.toPoly.mul k
+
+def Poly.norm (p : Poly) : Poly :=
+  p.sort.fuse
 
 def Expr.toNormPoly (e : Expr) : Poly :=
   e.toPoly.norm
@@ -201,7 +201,7 @@ def PolyCnstr.denote (ctx : Context) (c : PolyCnstr) : Prop :=
     Poly.denote_le ctx (c.lhs, c.rhs)
 
 def PolyCnstr.norm (c : PolyCnstr) : PolyCnstr :=
-  let (lhs, rhs) := Poly.cancel c.lhs.norm c.rhs.norm
+  let (lhs, rhs) := Poly.cancel c.lhs.sort.fuse c.rhs.sort.fuse
   { eq := c.eq, lhs, rhs }
 
 def PolyCnstr.isUnsat (c : PolyCnstr) : Bool :=
@@ -268,32 +268,24 @@ def PolyCnstr.toExpr (c : PolyCnstr) : ExprCnstr :=
   { c with lhs := c.lhs.toExpr, rhs := c.rhs.toExpr }
 
 attribute [local simp] Nat.add_comm Nat.add_assoc Nat.add_left_comm Nat.right_distrib Nat.left_distrib Nat.mul_assoc Nat.mul_comm
-attribute [local simp] Poly.denote Expr.denote Poly.insert Poly.norm Poly.norm.go Poly.cancelAux
+attribute [local simp] Poly.denote Expr.denote Poly.insertSorted Poly.sort Poly.sort.go Poly.fuse Poly.cancelAux
 attribute [local simp] Poly.mul Poly.mul.go
 
-theorem Poly.denote_insert (ctx : Context) (k : Nat) (v : Var) (p : Poly) :
-    (p.insert k v).denote ctx = p.denote ctx + k * v.denote ctx := by
+theorem Poly.denote_insertSorted (ctx : Context) (k : Nat) (v : Var) (p : Poly) : (p.insertSorted k v).denote ctx = p.denote ctx + k * v.denote ctx := by
   match p with
   | [] => simp
-  | (k', v') :: p =>
-    by_cases h₁ : Nat.blt v v'
-    · simp [h₁]
-    · by_cases h₂ : Nat.beq v v'
-      · simp only [insert, h₁, h₂, cond_false, cond_true]
-        simp [Nat.eq_of_beq_eq_true h₂]
-      · simp only [insert, h₁, h₂, cond_false, cond_true]
-        simp [denote_insert]
+  | (k', v') :: p => by_cases h : Nat.blt v v' <;> simp [h, denote_insertSorted]
 
-attribute [local simp] Poly.denote_insert
+attribute [local simp] Poly.denote_insertSorted
 
-theorem Poly.denote_norm_go (ctx : Context) (p : Poly) (r : Poly) : (norm.go p r).denote ctx = p.denote ctx + r.denote ctx := by
+theorem Poly.denote_sort_go (ctx : Context) (p : Poly) (r : Poly) : (sort.go p r).denote ctx = p.denote ctx + r.denote ctx := by
   match p with
   | [] => simp
-  | (k, v):: p => simp [denote_norm_go]
+  | (k, v):: p => simp [denote_sort_go]
 
-attribute [local simp] Poly.denote_norm_go
+attribute [local simp] Poly.denote_sort_go
 
-theorem Poly.denote_sort (ctx : Context) (m : Poly) : m.norm.denote ctx = m.denote ctx := by
+theorem Poly.denote_sort (ctx : Context) (m : Poly) : m.sort.denote ctx = m.denote ctx := by
   simp
 
 attribute [local simp] Poly.denote_sort
@@ -324,6 +316,18 @@ theorem Poly.denote_reverse (ctx : Context) (p : Poly) : denote ctx (List.revers
 
 attribute [local simp] Poly.denote_reverse
 
+theorem Poly.denote_fuse (ctx : Context) (p : Poly) : p.fuse.denote ctx = p.denote ctx := by
+  match p with
+  | [] => rfl
+  | (k, v) :: p =>
+    have ih := denote_fuse ctx p
+    simp
+    split
+    case _ h => simp [← ih, h]
+    case _ k' v' p' h => by_cases he : v == v' <;> simp [he, ← ih, h]; rw [eq_of_beq he]
+
+attribute [local simp] Poly.denote_fuse
+
 theorem Poly.denote_mul (ctx : Context) (k : Nat) (p : Poly) : (p.mul k).denote ctx = k * p.denote ctx := by
   simp
   by_cases h : k == 0 <;> simp [h]; simp [eq_of_beq h]
@@ -512,25 +516,13 @@ theorem Poly.denote_combine (ctx : Context) (p₁ p₂ : Poly) : (p₁.combine p
 
 attribute [local simp] Poly.denote_combine
 
-theorem Expr.denote_toPoly_go (ctx : Context) (e : Expr) :
-  (toPoly.go k e p).denote ctx = k * e.denote ctx + p.denote ctx := by
-  induction k, e using Expr.toPoly.go.induct generalizing p with
-  | case1 k k' =>
-    simp only [toPoly.go]
-    by_cases h : k' == 0
-    · simp [h, eq_of_beq h]
-    · simp [h, Var.denote]
-  | case2 k i => simp [toPoly.go]
-  | case3 k a b iha ihb => simp [toPoly.go, iha, ihb]
-  | case4 k k' a ih
-  | case5 k a k' ih =>
-    simp only [toPoly.go, denote, mul_eq]
-    by_cases h : k' == 0
-    · simp [h, eq_of_beq h]
-    · simp [h, cond_false, ih, Nat.mul_assoc]
-
 theorem Expr.denote_toPoly (ctx : Context) (e : Expr) : e.toPoly.denote ctx = e.denote ctx := by
-  simp [toPoly, Expr.denote_toPoly_go]
+  induction e with
+  | num k => by_cases h : k == 0 <;> simp [toPoly, h, Var.denote]; simp [eq_of_beq h]
+  | var i => simp [toPoly]
+  | add a b iha ihb => simp [toPoly, iha, ihb]
+  | mulL k a ih => simp [toPoly, ih, -Poly.mul]
+  | mulR k a ih => simp [toPoly, ih, -Poly.mul]
 
 attribute [local simp] Expr.denote_toPoly
 
@@ -562,8 +554,8 @@ theorem ExprCnstr.denote_toPoly (ctx : Context) (c : ExprCnstr) : c.toPoly.denot
   cases c; rename_i eq lhs rhs
   simp [ExprCnstr.denote, PolyCnstr.denote, ExprCnstr.toPoly];
   by_cases h : eq = true <;> simp [h]
-  · simp [Poly.denote_eq]
-  · simp [Poly.denote_le]
+  · simp [Poly.denote_eq, Expr.toPoly]
+  · simp [Poly.denote_le, Expr.toPoly]
 
 attribute [local simp] ExprCnstr.denote_toPoly
 

src/Init/Data/Option/Basic.lean

@@ -16,6 +16,10 @@ def getM [Alternative m] : Option α → m α
   | none     => failure
   | some a   => pure a
 
+@[deprecated getM (since := "2024-04-17")]
+-- `[Monad m]` is not needed here.
+def toMonad [Monad m] [Alternative m] : Option α → m α := getM
+
 /-- Returns `true` on `some x` and `false` on `none`. -/
 @[inline] def isSome : Option α → Bool
   | some _ => true
@@ -24,6 +28,8 @@ def getM [Alternative m] : Option α → m α
 @[simp] theorem isSome_none : @isSome α none = false := rfl
 @[simp] theorem isSome_some : isSome (some a) = true := rfl
 
+@[deprecated isSome (since := "2024-04-17"), inline] def toBool : Option α → Bool := isSome
+
 /-- Returns `true` on `none` and `false` on `some x`. -/
 @[inline] def isNone : Option α → Bool
   | some _ => false

src/Init/Data/SInt/Basic.lean

@@ -148,9 +148,6 @@ instance : ShiftLeft Int8   := ⟨Int8.shiftLeft⟩
 instance : ShiftRight Int8  := ⟨Int8.shiftRight⟩
 instance : DecidableEq Int8 := Int8.decEq
 
-@[extern "lean_bool_to_int8"]
-def Bool.toInt8 (b : Bool) : Int8 := if b then 1 else 0
-
 @[extern "lean_int8_dec_lt"]
 def Int8.decLt (a b : Int8) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
@@ -252,9 +249,6 @@ instance : ShiftLeft Int16   := ⟨Int16.shiftLeft⟩
 instance : ShiftRight Int16  := ⟨Int16.shiftRight⟩
 instance : DecidableEq Int16 := Int16.decEq
 
-@[extern "lean_bool_to_int16"]
-def Bool.toInt16 (b : Bool) : Int16 := if b then 1 else 0
-
 @[extern "lean_int16_dec_lt"]
 def Int16.decLt (a b : Int16) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
@@ -360,9 +354,6 @@ instance : ShiftLeft Int32   := ⟨Int32.shiftLeft⟩
 instance : ShiftRight Int32  := ⟨Int32.shiftRight⟩
 instance : DecidableEq Int32 := Int32.decEq
 
-@[extern "lean_bool_to_int32"]
-def Bool.toInt32 (b : Bool) : Int32 := if b then 1 else 0
-
 @[extern "lean_int32_dec_lt"]
 def Int32.decLt (a b : Int32) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
@@ -472,9 +463,6 @@ instance : ShiftLeft Int64   := ⟨Int64.shiftLeft⟩
 instance : ShiftRight Int64  := ⟨Int64.shiftRight⟩
 instance : DecidableEq Int64 := Int64.decEq
 
-@[extern "lean_bool_to_int64"]
-def Bool.toInt64 (b : Bool) : Int64 := if b then 1 else 0
-
 @[extern "lean_int64_dec_lt"]
 def Int64.decLt (a b : Int64) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
@@ -586,9 +574,6 @@ instance : ShiftLeft ISize   := ⟨ISize.shiftLeft⟩
 instance : ShiftRight ISize  := ⟨ISize.shiftRight⟩
 instance : DecidableEq ISize := ISize.decEq
 
-@[extern "lean_bool_to_isize"]
-def Bool.toISize (b : Bool) : ISize := if b then 1 else 0
-
 @[extern "lean_isize_dec_lt"]
 def ISize.decLt (a b : ISize) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))

src/Init/Data/String/Basic.lean

@@ -514,6 +514,9 @@ instance : Inhabited String := ⟨""⟩
 
 instance : Append String := ⟨String.append⟩
 
+@[deprecated push (since := "2024-04-06")]
+def str : String → Char → String := push
+
 @[inline] def pushn (s : String) (c : Char) (n : Nat) : String :=
   n.repeat (fun s => s.push c) s
 

src/Init/Data/UInt/Basic.lean

@@ -56,9 +56,6 @@ instance : Xor UInt8       := ⟨UInt8.xor⟩
 instance : ShiftLeft UInt8  := ⟨UInt8.shiftLeft⟩
 instance : ShiftRight UInt8 := ⟨UInt8.shiftRight⟩
 
-@[extern "lean_bool_to_uint8"]
-def Bool.toUInt8 (b : Bool) : UInt8 := if b then 1 else 0
-
 @[extern "lean_uint8_dec_lt"]
 def UInt8.decLt (a b : UInt8) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))
@@ -119,9 +116,6 @@ instance : Xor UInt16       := ⟨UInt16.xor⟩
 instance : ShiftLeft UInt16  := ⟨UInt16.shiftLeft⟩
 instance : ShiftRight UInt16 := ⟨UInt16.shiftRight⟩
 
-@[extern "lean_bool_to_uint16"]
-def Bool.toUInt16 (b : Bool) : UInt16 := if b then 1 else 0
-
 set_option bootstrap.genMatcherCode false in
 @[extern "lean_uint16_dec_lt"]
 def UInt16.decLt (a b : UInt16) : Decidable (a < b) :=
@@ -180,9 +174,6 @@ instance : Xor UInt32       := ⟨UInt32.xor⟩
 instance : ShiftLeft UInt32  := ⟨UInt32.shiftLeft⟩
 instance : ShiftRight UInt32 := ⟨UInt32.shiftRight⟩
 
-@[extern "lean_bool_to_uint32"]
-def Bool.toUInt32 (b : Bool) : UInt32 := if b then 1 else 0
-
 @[extern "lean_uint64_add"]
 def UInt64.add (a b : UInt64) : UInt64 := ⟨a.toBitVec + b.toBitVec⟩
 @[extern "lean_uint64_sub"]
@@ -287,8 +278,5 @@ instance : Xor USize        := ⟨USize.xor⟩
 instance : ShiftLeft USize  := ⟨USize.shiftLeft⟩
 instance : ShiftRight USize := ⟨USize.shiftRight⟩
 
-@[extern "lean_bool_to_usize"]
-def Bool.toUSize (b : Bool) : USize := if b then 1 else 0
-
 instance : Max USize := maxOfLe
 instance : Min USize := minOfLe

src/Init/Tactics.lean

@@ -466,7 +466,7 @@ hypotheses or the goal. It can have one of the forms:
 * `at h₁ h₂ ⊢`: target the hypotheses `h₁` and `h₂`, and the goal
 * `at *`: target all hypotheses and the goal
 -/
-syntax location := withPosition(ppGroup(" at" (locationWildcard <|> locationHyp)))
+syntax location := withPosition(" at" (locationWildcard <|> locationHyp))
 
 /--
 * `change tgt'` will change the goal from `tgt` to `tgt'`,

src/Lean/Data/NameMap.lean

@@ -33,16 +33,6 @@ def find? (m : NameMap α) (n : Name) : Option α := RBMap.find? m n
 instance : ForIn m (NameMap α) (Name × α) :=
   inferInstanceAs (ForIn _ (RBMap ..) ..)
 
-/-- `filter f m` returns the `NameMap` consisting of all
-"`key`/`val`"-pairs in `m` where `f key val` returns `true`. -/
-def filter (f : Name → α → Bool) (m : NameMap α) : NameMap α := RBMap.filter f m
-
-/-- `filterMap f m` filters an `NameMap` and simultaneously modifies the filtered values.
-
-It takes a function `f : Name → α → Option β` and applies `f name` to the value with key `name`.
-The resulting entries with non-`none` value are collected to form the output `NameMap`. -/
-def filterMap (f : Name → α → Option β) (m : NameMap α) : NameMap β := RBMap.filterMap f m
-
 end NameMap
 
 def NameSet := RBTree Name Name.quickCmp
@@ -63,9 +53,6 @@ def append (s t : NameSet) : NameSet :=
 instance : Append NameSet where
   append := NameSet.append
 
-/-- `filter f s` returns the `NameSet` consisting of all `x` in `s` where `f x` returns `true`. -/
-def filter (f : Name → Bool) (s : NameSet) : NameSet := RBTree.filter f s
-
 end NameSet
 
 def NameSSet := SSet Name
@@ -86,9 +73,6 @@ instance : EmptyCollection NameHashSet := ⟨empty⟩
 instance : Inhabited NameHashSet := ⟨{}⟩
 def insert (s : NameHashSet) (n : Name) := Std.HashSet.insert s n
 def contains (s : NameHashSet) (n : Name) : Bool := Std.HashSet.contains s n
-
-/-- `filter f s` returns the `NameHashSet` consisting of all `x` in `s` where `f x` returns `true`. -/
-def filter (f : Name → Bool) (s : NameHashSet) : NameHashSet := Std.HashSet.filter f s
 end NameHashSet
 
 def MacroScopesView.isPrefixOf (v₁ v₂ : MacroScopesView) : Bool :=

src/Lean/Data/RBMap.lean

@@ -404,24 +404,6 @@ def intersectBy {γ : Type v₁} {δ : Type v₂} (mergeFn : α → β → γ
       | some b₂ => acc.insert a <| mergeFn a b₁ b₂
       | none => acc
 
-/--
-`filter f m` returns the `RBMap` consisting of all
-"`key`/`val`"-pairs in `m` where `f key val` returns `true`.
--/
-def filter (f : α → β → Bool) (m : RBMap α β cmp) : RBMap α β cmp :=
-  m.fold (fun r k v => if f k v then r.insert k v else r) {}
-
-/--
-`filterMap f m` filters an `RBMap` and simultaneously modifies the filtered values.
-
-It takes a function `f : α → β → Option γ` and applies `f k v` to the value with key `k`.
-The resulting entries with non-`none` value are collected to form the output `RBMap`.
--/
-def filterMap (f : α → β → Option γ) (m : RBMap α β cmp) : RBMap α γ cmp :=
-  m.fold (fun r k v => match f k v with
-    | none => r
-    | some b => r.insert k b) {}
-
 end RBMap
 
 def rbmapOf {α : Type u} {β : Type v} (l : List (α × β)) (cmp : α → α → Ordering) : RBMap α β cmp :=

src/Lean/Data/RBTree.lean

@@ -114,13 +114,6 @@ def union (t₁ t₂ : RBTree α cmp) : RBTree α cmp :=
 def diff (t₁ t₂ : RBTree α cmp) : RBTree α cmp :=
   t₂.fold .erase t₁
 
-/--
-`filter f m` returns the `RBTree` consisting of all
-`x` in `m` where `f x` returns `true`.
--/
-def filter (f : α → Bool) (m : RBTree α cmp) : RBTree α cmp :=
-  RBMap.filter (fun a _ => f a) m
-
 end RBTree
 
 def rbtreeOf {α : Type u} (l : List α) (cmp : α → α → Ordering) : RBTree α cmp :=

src/Lean/Elab/Command.lean

@@ -214,7 +214,7 @@ private def addTraceAsMessagesCore (ctx : Context) (log : MessageLog) (traceStat
   let mut log := log
   let traces' := traces.toArray.qsort fun ((a, _), _) ((b, _), _) => a < b
   for ((pos, endPos), traceMsg) in traces' do
-    let data := .tagged `trace <| .joinSep traceMsg.toList "\n"
+    let data := .tagged `_traceMsg <| .joinSep traceMsg.toList "\n"
     log := log.add <| mkMessageCore ctx.fileName ctx.fileMap data .information pos endPos
   return log
 

src/Lean/Elab/PreDefinition/Nonrec/Eqns.lean

@@ -50,9 +50,7 @@ private partial def mkProof (declName : Name) (type : Expr) : MetaM Expr := do
         go mvarId
       else if let some mvarId ← whnfReducibleLHS? mvarId then
         go mvarId
-      else
-        let ctx ← Simp.mkContext (config := { dsimp := false })
-        match (← simpTargetStar mvarId ctx (simprocs := {})).1 with
+      else match (← simpTargetStar mvarId { config.dsimp := false } (simprocs := {})).1 with
         | TacticResultCNM.closed => return ()
         | TacticResultCNM.modified mvarId => go mvarId
         | TacticResultCNM.noChange =>

src/Lean/Elab/PreDefinition/Structural/Eqns.lean

@@ -45,9 +45,7 @@ where
       go mvarId
     else if let some mvarId ← simpIf? mvarId then
       go mvarId
-    else
-      let ctx ← Simp.mkContext
-      match (← simpTargetStar mvarId ctx (simprocs := {})).1 with
+    else match (← simpTargetStar mvarId {} (simprocs := {})).1 with
       | TacticResultCNM.closed => return ()
       | TacticResultCNM.modified mvarId => go mvarId
       | TacticResultCNM.noChange =>

src/Lean/Elab/PreDefinition/WF/Eqns.lean

@@ -57,9 +57,7 @@ private partial def mkProof (declName : Name) (type : Expr) : MetaM Expr := do
         go mvarId
       else if let some mvarId ← whnfReducibleLHS? mvarId then
         go mvarId
-      else
-        let ctx ← Simp.mkContext (config := { dsimp := false })
-        match (← simpTargetStar mvarId ctx (simprocs := {})).1 with
+      else match (← simpTargetStar mvarId { config.dsimp := false } (simprocs := {})).1 with
         | TacticResultCNM.closed => return ()
         | TacticResultCNM.modified mvarId => go mvarId
         | TacticResultCNM.noChange =>

src/Lean/Elab/PreDefinition/WF/Fix.lean

@@ -227,7 +227,7 @@ def mkFix (preDef : PreDefinition) (prefixArgs : Array Expr) (argsPacker : ArgsP
     -- decreasing goals when the function has only one non fixed argument.
     -- This renaming is irrelevant if the function has multiple non fixed arguments. See `process*` functions above.
     let lctx := (← getLCtx).setUserName x.fvarId! varName
-    withLCtx' lctx do
+    withTheReader Meta.Context (fun ctx => { ctx with lctx }) do
       let F   := xs[1]!
       let val := preDef.value.beta (prefixArgs.push x)
       let val ← processSumCasesOn x F val fun x F val => do

src/Lean/Elab/PreDefinition/WF/GuessLex.lean

@@ -166,7 +166,7 @@ def mayOmitSizeOf (is_mutual : Bool) (args : Array Expr) (x : Expr) : MetaM Bool
 def withUserNames {α} (xs : Array Expr) (ns : Array Name) (k : MetaM α) : MetaM α := do
   let mut lctx ←  getLCtx
   for x in xs, n in ns do lctx := lctx.setUserName x.fvarId! n
-  withLCtx' lctx k
+  withTheReader Meta.Context (fun ctx => { ctx with lctx }) k
 
 /-- Create one measure for each (eligible) parameter of the given predefintion.  -/
 def simpleMeasures (preDefs : Array PreDefinition) (fixedPrefixSize : Nat)

src/Lean/Elab/StructInst.lean

@@ -900,16 +900,8 @@ partial def tryToSynthesizeDefault (structs : Array Struct) (allStructNames : Ar
           | none   =>
             let mvarDecl ← getMVarDecl mvarId
             let val ← ensureHasType mvarDecl.type val
-            /-
-            We must use `checkedAssign` here to ensure we do not create a cyclic
-            assignment. See #3150.
-            This can happen when there are holes in the the fields the default value
-            depends on.
-            Possible improvement: create a new `_` instead of returning `false` when
-            `checkedAssign` fails. Reason: the field will not be needed after the
-            other `_` are resolved by the user.
-            -/
-            mvarId.checkedAssign val
+            mvarId.assign val
+            return true
       | _ => loop (i+1) dist
     else
       return false

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

@@ -198,10 +198,11 @@ def rewriteRulesPass (maxSteps : Nat) : Pass where
     let sevalThms ← getSEvalTheorems
     let sevalSimprocs ← Simp.getSEvalSimprocs
 
-    let simpCtx ← Simp.mkContext
-      (config := { failIfUnchanged := false, zetaDelta := true, maxSteps })
-      (simpTheorems := #[bvThms, sevalThms])
-      (congrTheorems := (← getSimpCongrTheorems))
+    let simpCtx : Simp.Context := {
+      config := { failIfUnchanged := false, zetaDelta := true, maxSteps }
+      simpTheorems := #[bvThms, sevalThms]
+      congrTheorems := (← getSimpCongrTheorems)
+    }
 
     let hyps ← goal.getNondepPropHyps
     let ⟨result?, _⟩ ← simpGoal goal
@@ -282,10 +283,11 @@ def embeddedConstraintPass (maxSteps : Nat) : Pass where
 
       let goal ← goal.tryClearMany duplicates
 
-      let simpCtx ← Simp.mkContext
-        (config := { failIfUnchanged := false, maxSteps })
-        (simpTheorems := relevantHyps)
-        (congrTheorems := (← getSimpCongrTheorems))
+      let simpCtx : Simp.Context := {
+        config := { failIfUnchanged := false, maxSteps }
+        simpTheorems := relevantHyps
+        congrTheorems := (← getSimpCongrTheorems)
+      }
 
       let ⟨result?, _⟩ ← simpGoal goal (ctx := simpCtx) (fvarIdsToSimp := ← goal.getNondepPropHyps)
       let some (_, newGoal) := result? | return none

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

@@ -12,10 +12,11 @@ namespace Lean.Elab.Tactic.Conv
 open Meta
 
 private def getContext : MetaM Simp.Context := do
-  Simp.mkContext
-    (simpTheorems  := {})
-    (congrTheorems := (← getSimpCongrTheorems))
-    (config        := Simp.neutralConfig)
+  return {
+    simpTheorems  := {}
+    congrTheorems := (← getSimpCongrTheorems)
+    config        := Simp.neutralConfig
+  }
 
 partial def matchPattern? (pattern : AbstractMVarsResult) (e : Expr) : MetaM (Option (Expr × Array Expr)) :=
   withNewMCtxDepth do
@@ -125,7 +126,7 @@ private def pre (pattern : AbstractMVarsResult) (state : IO.Ref PatternMatchStat
         pure (.occs #[] 0 ids.toList)
       | _ => throwUnsupportedSyntax
     let state ← IO.mkRef occs
-    let ctx := (← getContext).setMemoize (occs matches .all _)
+    let ctx := { ← getContext with config.memoize := occs matches .all _ }
     let (result, _) ← Simp.main lhs ctx (methods := { pre := pre patternA state })
     let subgoals ← match ← state.get with
     | .all #[] | .occs _ 0 _ =>

src/Lean/Elab/Tactic/NormCast.lean

@@ -28,10 +28,8 @@ def proveEqUsing (s : SimpTheorems) (a b : Expr) : MetaM (Option Simp.Result) :=
     unless ← isDefEq a'.expr b'.expr do return none
     a'.mkEqTrans (← b'.mkEqSymm b)
   withReducible do
-    let ctx ← Simp.mkContext
-        (simpTheorems := #[s])
-        (congrTheorems := ← Meta.getSimpCongrTheorems)
-    (go (← Simp.mkDefaultMethods).toMethodsRef ctx).run' {}
+    (go (← Simp.mkDefaultMethods).toMethodsRef
+      { simpTheorems := #[s], congrTheorems := ← Meta.getSimpCongrTheorems }).run' {}
 
 /-- Proves `a = b` by simplifying using move and squash lemmas. -/
 def proveEqUsingDown (a b : Expr) : MetaM (Option Simp.Result) := do
@@ -193,25 +191,19 @@ def derive (e : Expr) : MetaM Simp.Result := do
   -- step 1: pre-processing of numerals
   let r ← withTrace "pre-processing numerals" do
     let post e := return Simp.Step.done (← try numeralToCoe e catch _ => pure {expr := e})
-    let ctx ← Simp.mkContext (config := config) (congrTheorems := congrTheorems)
-    r.mkEqTrans (← Simp.main r.expr ctx (methods := { post })).1
+    r.mkEqTrans (← Simp.main r.expr { config, congrTheorems } (methods := { post })).1
 
   -- step 2: casts are moved upwards and eliminated
   let r ← withTrace "moving upward, splitting and eliminating" do
     let post := upwardAndElim (← normCastExt.up.getTheorems)
-    let ctx ← Simp.mkContext (config := config) (congrTheorems := congrTheorems)
-    r.mkEqTrans (← Simp.main r.expr ctx (methods := { post })).1
+    r.mkEqTrans (← Simp.main r.expr { config, congrTheorems } (methods := { post })).1
 
   let simprocs ← ({} : Simp.SimprocsArray).add `reduceCtorEq false
 
   -- step 3: casts are squashed
   let r ← withTrace "squashing" do
     let simpTheorems := #[← normCastExt.squash.getTheorems]
-    let ctx ← Simp.mkContext
-      (config := config)
-      (simpTheorems := simpTheorems)
-      (congrTheorems := congrTheorems)
-    r.mkEqTrans (← simp r.expr ctx simprocs).1
+    r.mkEqTrans (← simp r.expr { simpTheorems, config, congrTheorems } simprocs).1
 
   return r
 
@@ -271,7 +263,7 @@ def evalConvNormCast : Tactic :=
 def evalPushCast : Tactic := fun stx => do
   let { ctx, simprocs, dischargeWrapper } ← withMainContext do
     mkSimpContext (simpTheorems := pushCastExt.getTheorems) stx (eraseLocal := false)
-  let ctx := ctx.setFailIfUnchanged false
+  let ctx := { ctx with config := { ctx.config with failIfUnchanged := false } }
   dischargeWrapper.with fun discharge? =>
     discard <| simpLocation ctx simprocs discharge? (expandOptLocation stx[5])
 

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

@@ -6,6 +6,7 @@ Authors: Kim Morrison
 prelude
 import Lean.Elab.Tactic.Omega.Core
 import Lean.Elab.Tactic.FalseOrByContra
+import Lean.Meta.Tactic.Cases
 import Lean.Elab.Tactic.Config
 
 /-!
@@ -519,6 +520,23 @@ partial def processFacts (p : MetaProblem) : OmegaM (MetaProblem × Nat) := do
 
 end MetaProblem
 
+/--
+Given `p : P ∨ Q` (or any inductive type with two one-argument constructors),
+split the goal into two subgoals:
+one containing the hypothesis `h : P` and another containing `h : Q`.
+-/
+def cases₂ (mvarId : MVarId) (p : Expr) (hName : Name := `h) :
+    MetaM ((MVarId × FVarId) × (MVarId × FVarId)) := do
+  let mvarId ← mvarId.assert `hByCases (← inferType p) p
+  let (fvarId, mvarId) ← mvarId.intro1
+  let #[s₁, s₂] ← mvarId.cases fvarId #[{ varNames := [hName] }, { varNames := [hName] }] |
+    throwError "'cases' tactic failed, unexpected number of subgoals"
+  let #[Expr.fvar f₁ ..] ← pure s₁.fields
+    | throwError "'cases' tactic failed, unexpected new hypothesis"
+  let #[Expr.fvar f₂ ..] ← pure s₂.fields
+    | throwError "'cases' tactic failed, unexpected new hypothesis"
+  return ((s₁.mvarId, f₁), (s₂.mvarId, f₂))
+
 /--
 Helpful error message when omega cannot find a solution
 -/
@@ -610,36 +628,33 @@ mutual
 Split a disjunction in a `MetaProblem`, and if we find a new usable fact
 call `omegaImpl` in both branches.
 -/
-partial def splitDisjunction (m : MetaProblem) : OmegaM Expr := do
+partial def splitDisjunction (m : MetaProblem) (g : MVarId) : OmegaM Unit := g.withContext do
   match m.disjunctions with
     | [] => throwError "omega could not prove the goal:\n{← formatErrorMessage m.problem}"
-    | h :: t => do
-      let hType ← whnfD (← inferType h)
-      trace[omega] "Case splitting on {hType}"
-      let_expr Or hType₁ hType₂ := hType | throwError "Unexpected disjunction {hType}"
-      let p?₁ ← withoutModifyingState do withLocalDeclD `h₁ hType₁ fun h₁ => do
-        withTraceNode `omega (msg := fun _ => do pure m!"Assuming fact:{indentExpr hType₁}") do
-        let m₁ := { m with facts := [h₁], disjunctions := t }
-        let (m₁, n) ← m₁.processFacts
+    | h :: t =>
+      trace[omega] "Case splitting on {← inferType h}"
+      let ctx ← getMCtx
+      let (⟨g₁, h₁⟩, ⟨g₂, h₂⟩) ← cases₂ g h
+      trace[omega] "Adding facts:\n{← g₁.withContext <| inferType (.fvar h₁)}"
+      let m₁ := { m with facts := [.fvar h₁], disjunctions := t }
+      let r ← withoutModifyingState do
+        let (m₁, n) ← g₁.withContext m₁.processFacts
         if 0 < n then
-          let p₁ ← omegaImpl m₁
-          let p₁ ← mkLambdaFVars #[h₁] p₁
-          return some p₁
+          omegaImpl m₁ g₁
+          pure true
         else
-          return none
-      if let some p₁ := p?₁ then
-         withLocalDeclD `h₂ hType₂ fun h₂ => do
-          withTraceNode `omega (msg := fun _ => do pure m!"Assuming fact:{indentExpr hType₂}") do
-          let m₂ := { m with facts := [h₂], disjunctions := t }
-          let p₂ ← omegaImpl m₂
-          let p₂ ← mkLambdaFVars #[h₂] p₂
-          return mkApp6 (mkConst ``Or.elim) hType₁ hType₂ (mkConst ``False) h p₁ p₂
+          pure false
+      if r then
+        trace[omega] "Adding facts:\n{← g₂.withContext <| inferType (.fvar h₂)}"
+        let m₂ := { m with facts := [.fvar h₂], disjunctions := t }
+        omegaImpl m₂ g₂
       else
         trace[omega] "No new facts found."
-        splitDisjunction { m with disjunctions := t }
+        setMCtx ctx
+        splitDisjunction { m with disjunctions := t } g
 
 /-- Implementation of the `omega` algorithm, and handling disjunctions. -/
-partial def omegaImpl (m : MetaProblem) : OmegaM Expr := do
+partial def omegaImpl (m : MetaProblem) (g : MVarId) : OmegaM Unit := g.withContext do
   let (m, _) ← m.processFacts
   guard m.facts.isEmpty
   let p := m.problem
@@ -648,12 +663,12 @@ partial def omegaImpl (m : MetaProblem) : OmegaM Expr := do
   trace[omega] "After elimination:\nAtoms: {← atomsList}\n{p'}"
   match p'.possible, p'.proveFalse?, p'.proveFalse?_spec with
   | true, _, _ =>
-    splitDisjunction m
+    splitDisjunction m g
   | false, .some prf, _ =>
     trace[omega] "Justification:\n{p'.explanation?.get}"
     let prf ← instantiateMVars (← prf)
     trace[omega] "omega found a contradiction, proving {← inferType prf}"
-    return prf
+    g.assign prf
 
 end
 
@@ -662,9 +677,7 @@ Given a collection of facts, try prove `False` using the omega algorithm,
 and close the goal using that.
 -/
 def omega (facts : List Expr) (g : MVarId) (cfg : OmegaConfig := {}) : MetaM Unit :=
-  g.withContext do
-    let prf ← OmegaM.run (omegaImpl { facts }) cfg
-    g.assign prf
+  OmegaM.run (omegaImpl { facts } g) cfg
 
 open Lean Elab Tactic Parser.Tactic
 

src/Lean/Elab/Tactic/Simp.lean

@@ -234,7 +234,7 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simp.SimprocsAr
             logException ex
           else
             throw ex
-      return { ctx := ctx.setSimpTheorems (thmsArray.set! 0 thms), simprocs, starArg }
+      return { ctx := { ctx with simpTheorems := thmsArray.set! 0 thms }, simprocs, starArg }
     -- If recovery is disabled, then we want simp argument elaboration failures to be exceptions.
     -- This affects `addSimpTheorem`.
     if (← read).recover then
@@ -311,11 +311,10 @@ def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (kind := SimpKind.simp)
     simpTheorems
   let simprocs ← if simpOnly then pure {} else Simp.getSimprocs
   let congrTheorems ← getSimpCongrTheorems
-  let ctx ← Simp.mkContext
-     (config := (← elabSimpConfig stx[1] (kind := kind)))
-     (simpTheorems := #[simpTheorems])
-     congrTheorems
-  let r ← elabSimpArgs stx[4] (eraseLocal := eraseLocal) (kind := kind) (simprocs := #[simprocs]) ctx
+  let r ← elabSimpArgs stx[4] (eraseLocal := eraseLocal) (kind := kind) (simprocs := #[simprocs]) {
+    config      := (← elabSimpConfig stx[1] (kind := kind))
+    simpTheorems := #[simpTheorems], congrTheorems
+  }
   if !r.starArg || ignoreStarArg then
     return { r with dischargeWrapper }
   else
@@ -330,7 +329,7 @@ def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (kind := SimpKind.simp)
     for h in hs do
       unless simpTheorems.isErased (.fvar h) do
         simpTheorems ← simpTheorems.addTheorem (.fvar h) (← h.getDecl).toExpr
-    let ctx := ctx.setSimpTheorems simpTheorems
+    let ctx := { ctx with simpTheorems }
     return { ctx, simprocs, dischargeWrapper }
 
 register_builtin_option tactic.simp.trace : Bool := {

src/Lean/Elab/Tactic/Simpa.lean

@@ -36,9 +36,9 @@ deriving instance Repr for UseImplicitLambdaResult
     let stx ← `(tactic| simp $cfg:optConfig $(disch)? $[only%$only]? $[[$args,*]]?)
     let { ctx, simprocs, dischargeWrapper } ←
       withMainContext <| mkSimpContext stx (eraseLocal := false)
-    let ctx := if unfold.isSome then ctx.setAutoUnfold else ctx
+    let ctx := if unfold.isSome then { ctx with config.autoUnfold := true } else ctx
     -- TODO: have `simpa` fail if it doesn't use `simp`.
-    let ctx := ctx.setFailIfUnchanged false
+    let ctx := { ctx with config := { ctx.config with failIfUnchanged := false } }
     dischargeWrapper.with fun discharge? => do
       let (some (_, g), stats) ← simpGoal (← getMainGoal) ctx (simprocs := simprocs)
           (simplifyTarget := true) (discharge? := discharge?)

src/Lean/Message.lean

@@ -116,7 +116,7 @@ variable (p : Name → Bool) in
 /-- Returns true when the message contains a `MessageData.tagged tag ..` constructor where `p tag`
 is true.
 
-This does not descend into lazily generated subtrees (`.ofLazy`); message tags
+This does not descend into lazily generated subtress (`.ofLazy`); message tags
 of interest (like those added by `logLinter`) are expected to be near the root
 of the `MessageData`, and not hidden inside `.ofLazy`.
 -/
@@ -130,19 +130,6 @@ partial def hasTag : MessageData → Bool
   | trace data msg msgs     => p data.cls || hasTag msg || msgs.any hasTag
   | _                       => false
 
-/--
-Returns the top-level tag of the message.
-If none, returns `Name.anonymous`.
-
-This does not descend into message subtrees (e.g., `.compose`, `.ofLazy`).
-The message kind is expected to describe the whole message.
--/
-def kind : MessageData → Name
-  | withContext _ msg       => kind msg
-  | withNamingContext _ msg => kind msg
-  | tagged n _              => n
-  | _                       => .anonymous
-
 /-- An empty message. -/
 def nil : MessageData :=
   ofFormat Format.nil
@@ -328,7 +315,7 @@ structure BaseMessage (α : Type u) where
   endPos        : Option Position := none
   /-- If `true`, report range as given; see `msgToInteractiveDiagnostic`. -/
   keepFullRange : Bool := false
-  severity      : MessageSeverity := .error
+  severity      : MessageSeverity := MessageSeverity.error
   caption       : String          := ""
   /-- The content of the message. -/
   data          : α
@@ -341,10 +328,7 @@ abbrev Message := BaseMessage MessageData
 /-- A `SerialMessage` is a `Message` whose `MessageData` has been eagerly
 serialized and is thus appropriate for use in pure contexts where the effectful
 `MessageData.toString` cannot be used. -/
-structure SerialMessage extends BaseMessage String where
-  /-- The message kind (i.e., the top-level tag). -/
-  kind          : Name
-  deriving ToJson, FromJson
+abbrev SerialMessage := BaseMessage String
 
 namespace SerialMessage
 
@@ -370,12 +354,8 @@ end SerialMessage
 
 namespace Message
 
-@[inherit_doc MessageData.kind] abbrev kind (msg : Message) :=
-  msg.data.kind
-
-/-- Serializes the message, converting its data into a string and saving its kind. -/
 @[inline] def serialize (msg : Message) : IO SerialMessage := do
-  return {msg with kind := msg.kind, data := ← msg.data.toString}
+  return {msg with data := ← msg.data.toString}
 
 protected def toString (msg : Message) (includeEndPos := false) : IO String := do
   -- Remark: The inline here avoids a new message allocation when `msg` is shared

src/Lean/Meta/Basic.lean

@@ -332,7 +332,7 @@ register_builtin_option maxSynthPendingDepth : Nat := {
   Contextual information for the `MetaM` monad.
 -/
 structure Context where
-  private config    : Config               := {}
+  config            : Config               := {}
   /-- Local context -/
   lctx              : LocalContext         := {}
   /-- Local instances in `lctx`. -/
@@ -943,15 +943,6 @@ def elimMVarDeps (xs : Array Expr) (e : Expr) (preserveOrder : Bool := false) :
 @[inline] def withConfig (f : Config → Config) : n α → n α :=
   mapMetaM <| withReader (fun ctx => { ctx with config := f ctx.config })
 
-@[inline] def withCanUnfoldPred (p : Config → ConstantInfo → CoreM Bool) : n α → n α :=
-  mapMetaM <| withReader (fun ctx => { ctx with canUnfold? := p })
-
-@[inline] def withIncSynthPending : n α → n α :=
-  mapMetaM <| withReader (fun ctx => { ctx with synthPendingDepth := ctx.synthPendingDepth + 1 })
-
-@[inline] def withInTypeClassResolution : n α → n α :=
-  mapMetaM <| withReader (fun ctx => { ctx with inTypeClassResolution := true })
-
 /--
 Executes `x` tracking zetaDelta reductions `Config.trackZetaDelta := true`
 -/
@@ -1431,14 +1422,6 @@ def withLocalDecl (name : Name) (bi : BinderInfo) (type : Expr) (k : Expr → n
 def withLocalDeclD (name : Name) (type : Expr) (k : Expr → n α) : n α :=
   withLocalDecl name BinderInfo.default type k
 
-/--
-Similar to `withLocalDecl`, but it does **not** check whether the new variable is a local instance or not.
--/
-def withLocalDeclNoLocalInstanceUpdate (name : Name) (bi : BinderInfo) (type : Expr) (x : Expr → MetaM α) : MetaM α := do
-  let fvarId ← mkFreshFVarId
-  withReader (fun ctx => { ctx with lctx := ctx.lctx.mkLocalDecl fvarId name type bi }) do
-    x (mkFVar fvarId)
-
 /-- Append an array of free variables `xs` to the local context and execute `k xs`.
 `declInfos` takes the form of an array consisting of:
 - the name of the variable
@@ -1555,11 +1538,11 @@ def withReplaceFVarId {α} (fvarId : FVarId) (e : Expr) : MetaM α → MetaM α
     localInstances := ctx.localInstances.erase fvarId }
 
 /--
-`withNewMCtxDepth k` executes `k` with a higher metavariable context depth,
-where metavariables created outside the `withNewMCtxDepth` (with a lower depth) cannot be assigned.
-If `allowLevelAssignments` is set to true, then the level metavariable depth
-is not increased, and level metavariables from the outer scope can be
-assigned.  (This is used by TC synthesis.)
+  `withNewMCtxDepth k` executes `k` with a higher metavariable context depth,
+  where metavariables created outside the `withNewMCtxDepth` (with a lower depth) cannot be assigned.
+  If `allowLevelAssignments` is set to true, then the level metavariable depth
+  is not increased, and level metavariables from the outer scope can be
+  assigned.  (This is used by TC synthesis.)
 -/
 def withNewMCtxDepth (k : n α) (allowLevelAssignments := false) : n α :=
   mapMetaM (withNewMCtxDepthImp allowLevelAssignments) k
@@ -1569,20 +1552,13 @@ private def withLocalContextImp (lctx : LocalContext) (localInsts : LocalInstanc
     x
 
 /--
-`withLCtx lctx localInsts k` replaces the local context and local instances, and then executes `k`.
-The local context and instances are restored after executing `k`.
-This method assumes that the local instances in `localInsts` are in the local context `lctx`.
+  `withLCtx lctx localInsts k` replaces the local context and local instances, and then executes `k`.
+  The local context and instances are restored after executing `k`.
+  This method assumes that the local instances in `localInsts` are in the local context `lctx`.
 -/
 def withLCtx (lctx : LocalContext) (localInsts : LocalInstances) : n α → n α :=
   mapMetaM <| withLocalContextImp lctx localInsts
 
-/--
-Simpler version of `withLCtx` which just updates the local context. It is the resposability of the
-caller ensure the local instances are also properly updated.
--/
-def withLCtx' (lctx : LocalContext) : n α → n α :=
-  mapMetaM <| withReader (fun ctx => { ctx with lctx })
-
 /--
 Runs `k` in a local environment with the `fvarIds` erased.
 -/

src/Lean/Meta/Coe.lean

@@ -157,11 +157,9 @@ def coerceMonadLift? (e expectedType : Expr) : MetaM (Option Expr) := do
   let eType ← instantiateMVars (← inferType e)
   let some (n, β) ← isTypeApp? expectedType | return none
   let some (m, α) ← isTypeApp? eType | return none
-  -- Need to save and restore the state in case `m` and `n` are defeq but not monads to prevent this procedure from having side effects.
-  let saved ← saveState
   if (← isDefEq m n) then
-    let some monadInst ← isMonad? n | restoreState saved; return none
-    try expandCoe (← mkAppOptM ``Lean.Internal.coeM #[m, α, β, none, monadInst, e]) catch _ => restoreState saved; return none
+    let some monadInst ← isMonad? n | return none
+    try expandCoe (← mkAppOptM ``Lean.Internal.coeM #[m, α, β, none, monadInst, e]) catch _ => return none
   else if autoLift.get (← getOptions) then
     try
       -- Construct lift from `m` to `n`

src/Lean/Meta/DiscrTree.lean

@@ -553,8 +553,8 @@ private def getKeyArgs (e : Expr) (isMatch root : Bool) (config : WhnfCoreConfig
     if isMatch then
       return (.other, #[])
     else do
-      let cfg ← getConfig
-      if cfg.isDefEqStuckEx then
+      let ctx ← read
+      if ctx.config.isDefEqStuckEx then
         /-
           When the configuration flag `isDefEqStuckEx` is set to true,
           we want `isDefEq` to throw an exception whenever it tries to assign

src/Lean/Meta/ExprDefEq.lean

@@ -364,7 +364,7 @@ private partial def isDefEqBindingAux (lctx : LocalContext) (fvars : Array Expr)
   | Expr.forallE n d₁ b₁ _, Expr.forallE _ d₂ b₂ _ => process n d₁ d₂ b₁ b₂
   | Expr.lam     n d₁ b₁ _, Expr.lam     _ d₂ b₂ _ => process n d₁ d₂ b₁ b₂
   | _,                      _                      =>
-    withLCtx' lctx do
+    withReader (fun ctx => { ctx with lctx := lctx }) do
       isDefEqBindingDomain fvars ds₂ do
         Meta.isExprDefEqAux (e₁.instantiateRev fvars) (e₂.instantiateRev fvars)
 
@@ -758,8 +758,8 @@ mutual
     if mvarDecl.depth != (← getMCtx).depth || mvarDecl.kind.isSyntheticOpaque then
       traceM `Meta.isDefEq.assign.readOnlyMVarWithBiggerLCtx <| addAssignmentInfo (mkMVar mvarId)
       throwCheckAssignmentFailure
-    let cfg ← getConfig
-    unless cfg.ctxApprox && ctx.mvarDecl.lctx.isSubPrefixOf mvarDecl.lctx do
+    let ctxMeta ← readThe Meta.Context
+    unless ctxMeta.config.ctxApprox && ctx.mvarDecl.lctx.isSubPrefixOf mvarDecl.lctx do
       traceM `Meta.isDefEq.assign.readOnlyMVarWithBiggerLCtx <| addAssignmentInfo (mkMVar mvarId)
       throwCheckAssignmentFailure
     /- Create an auxiliary metavariable with a smaller context and "checked" type.
@@ -814,8 +814,8 @@ mutual
 
   partial def checkApp (e : Expr) : CheckAssignmentM Expr :=
     e.withApp fun f args => do
-      let cfg ← getConfig
-      if f.isMVar && cfg.ctxApprox && args.all Expr.isFVar then
+      let ctxMeta ← readThe Meta.Context
+      if f.isMVar && ctxMeta.config.ctxApprox && args.all Expr.isFVar then
         let f ← check f
         catchInternalId outOfScopeExceptionId
           (do
@@ -1794,8 +1794,8 @@ private partial def isDefEqQuickOther (t s : Expr) : MetaM LBool := do
         | LBool.true => return LBool.true
         | LBool.false => return LBool.false
         | _ =>
-          let cfg ← getConfig
-          if cfg.isDefEqStuckEx then do
+          let ctx ← read
+          if ctx.config.isDefEqStuckEx then do
             trace[Meta.isDefEq.stuck] "{t} =?= {s}"
             Meta.throwIsDefEqStuck
           else
@@ -1834,7 +1834,7 @@ end
       let e ← instantiateMVars e
       successK e
     else
-      if (← getConfig).isDefEqStuckEx then
+      if (← read).config.isDefEqStuckEx then
         /-
         When `isDefEqStuckEx := true` and `mvar` was created in a previous level,
         we should throw an exception. See issue #2736 for a situation where this can happen.

src/Lean/Meta/GetUnfoldableConst.lean

@@ -22,11 +22,10 @@ private def canUnfoldDefault (cfg : Config) (info : ConstantInfo) : CoreM Bool :
 
 def canUnfold (info : ConstantInfo) : MetaM Bool := do
   let ctx ← read
-  let cfg ← getConfig
   if let some f := ctx.canUnfold? then
-    f cfg info
+    f ctx.config info
   else
-    canUnfoldDefault cfg info
+    canUnfoldDefault ctx.config info
 
 /--
 Look up a constant name, returning the `ConstantInfo`

src/Lean/Meta/InferType.lean

@@ -382,6 +382,11 @@ def isType (e : Expr) : MetaM Bool := do
     | .sort .. => return true
     | _        => return false
 
+@[inline] private def withLocalDecl' {α} (name : Name) (bi : BinderInfo) (type : Expr) (x : Expr → MetaM α) : MetaM α := do
+  let fvarId ← mkFreshFVarId
+  withReader (fun ctx => { ctx with lctx := ctx.lctx.mkLocalDecl fvarId name type bi }) do
+    x (mkFVar fvarId)
+
 def typeFormerTypeLevelQuick : Expr → Option Level
   | .forallE _ _ b _ => typeFormerTypeLevelQuick b
   | .sort l => some l
@@ -398,7 +403,7 @@ where
   go (type : Expr) (xs : Array Expr) : MetaM (Option Level) := do
     match type with
     | .sort l => return some l
-    | .forallE n d b c => withLocalDeclNoLocalInstanceUpdate n c (d.instantiateRev xs) fun x => go b (xs.push x)
+    | .forallE n d b c => withLocalDecl' n c (d.instantiateRev xs) fun x => go b (xs.push x)
     | _ =>
       let type ← whnfD (type.instantiateRev xs)
       match type with

src/Lean/Meta/LazyDiscrTree.lean

@@ -222,8 +222,8 @@ private def getKeyArgs (e : Expr) (isMatch root : Bool) (config : WhnfCoreConfig
     if isMatch then
       return (.other, #[])
     else do
-      let cfg ← getConfig
-      if cfg.isDefEqStuckEx then
+      let ctx ← read
+      if ctx.config.isDefEqStuckEx then
         /-
           When the configuration flag `isDefEqStuckEx` is set to true,
           we want `isDefEq` to throw an exception whenever it tries to assign

src/Lean/Meta/LevelDefEq.lean

@@ -149,8 +149,8 @@ mutual
             if r != LBool.undef then
               return r == LBool.true
             else if !(← hasAssignableLevelMVar lhs <||> hasAssignableLevelMVar rhs) then
-              let cfg ← getConfig
-              if cfg.isDefEqStuckEx && (lhs.isMVar || rhs.isMVar) then do
+              let ctx ← read
+              if ctx.config.isDefEqStuckEx && (lhs.isMVar || rhs.isMVar) then do
                 trace[Meta.isLevelDefEq.stuck] "{lhs} =?= {rhs}"
                 Meta.throwIsDefEqStuck
               else

src/Lean/Meta/Match/MatcherApp/Transform.lean

@@ -162,7 +162,7 @@ def refineThrough? (matcherApp : MatcherApp) (e : Expr) :
 private def withUserNamesImpl {α} (fvars : Array Expr) (names : Array Name) (k : MetaM α) : MetaM α := do
   let lctx := (Array.zip fvars names).foldl (init := ← (getLCtx)) fun lctx (fvar, name) =>
     lctx.setUserName fvar.fvarId! name
-  withLCtx' lctx k
+  withTheReader Meta.Context (fun ctx => { ctx with lctx }) k
 
 /--
 Sets the user name of the FVars in the local context according to the given array of names.

src/Lean/Meta/SynthInstance.lean

@@ -782,7 +782,7 @@ def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (
     (return m!"{exceptOptionEmoji ·} {← instantiateMVars type}") do
   withConfig (fun config => { config with isDefEqStuckEx := true, transparency := TransparencyMode.instances,
                                           foApprox := true, ctxApprox := true, constApprox := false, univApprox := false }) do
-  withInTypeClassResolution do
+  withReader (fun ctx => { ctx with inTypeClassResolution := true }) do
     let localInsts ← getLocalInstances
     let type ← instantiateMVars type
     let type ← preprocess type
@@ -839,7 +839,7 @@ private def synthPendingImp (mvarId : MVarId) : MetaM Bool := withIncRecDepth <|
         recordSynthPendingFailure mvarDecl.type
         return false
       else
-        withIncSynthPending do
+        withReader (fun ctx => { ctx with synthPendingDepth := ctx.synthPendingDepth + 1 }) do
           trace[Meta.synthPending] "synthPending {mkMVar mvarId}"
           let val? ← catchInternalId isDefEqStuckExceptionId (synthInstance? mvarDecl.type (maxResultSize? := none)) (fun _ => pure none)
           match val? with

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

@@ -188,10 +188,12 @@ def post (e : Expr) : SimpM Simp.Step := do
   | e, _ => return Simp.Step.done { expr := e }
 
 def rewriteUnnormalized (mvarId : MVarId) : MetaM MVarId := do
-  let simpCtx ← Simp.mkContext
-      (simpTheorems  := {})
-      (congrTheorems := (← getSimpCongrTheorems))
-      (config        := Simp.neutralConfig)
+  let simpCtx :=
+    {
+      simpTheorems  := {}
+      congrTheorems := (← getSimpCongrTheorems)
+      config        := Simp.neutralConfig
+    }
   let tgt ← instantiateMVars (← mvarId.getType)
   let (res, _) ← Simp.main tgt simpCtx (methods := { post })
   applySimpResultToTarget mvarId tgt res
@@ -205,10 +207,12 @@ def rewriteUnnormalizedRefl (goal : MVarId) : MetaM Unit := do
 
 def acNfHypMeta (goal : MVarId) (fvarId : FVarId) : MetaM (Option MVarId) := do
   goal.withContext do
-    let simpCtx ← Simp.mkContext
-      (simpTheorems  := {})
-      (congrTheorems := (← getSimpCongrTheorems))
-      (config        := Simp.neutralConfig)
+    let simpCtx :=
+    {
+      simpTheorems  := {}
+      congrTheorems := (← getSimpCongrTheorems)
+      config        := Simp.neutralConfig
+    }
     let tgt ← instantiateMVars (← fvarId.getType)
     let (res, _) ← Simp.main tgt simpCtx (methods := { post })
     return (← applySimpResultToLocalDecl goal fvarId res false).map (·.snd)

src/Lean/Meta/Tactic/Acyclic.lean

@@ -38,10 +38,7 @@ where
       let sizeOfEq ← mkLT sizeOf_lhs sizeOf_rhs
       let hlt ← mkFreshExprSyntheticOpaqueMVar sizeOfEq
       -- TODO: we only need the `sizeOf` simp theorems
-      let ctx ← Simp.mkContext
-         (config := { arith := true })
-         (simpTheorems := #[ (← getSimpTheorems) ])
-      match (← simpTarget hlt.mvarId! ctx {}).1 with
+      match (← simpTarget hlt.mvarId! { config.arith := true, simpTheorems := #[ (← getSimpTheorems) ] } {}).1 with
       | some _ => return false
       | none   =>
         let heq ← mkCongrArg sizeOf_lhs.appFn! (← mkEqSymm h)

src/Lean/Meta/Tactic/Apply.lean

@@ -254,6 +254,10 @@ Apply `And.intro` as much as possible to goal `mvarId`.
 abbrev splitAnd (mvarId : MVarId) : MetaM (List MVarId) :=
   splitAndCore mvarId
 
+@[deprecated splitAnd (since := "2024-03-17")]
+def _root_.Lean.Meta.splitAnd (mvarId : MVarId) : MetaM (List MVarId) :=
+  mvarId.splitAnd
+
 def exfalso (mvarId : MVarId) : MetaM MVarId :=
   mvarId.withContext do
     mvarId.checkNotAssigned `exfalso

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

@@ -38,10 +38,11 @@ abbrev PreM := ReaderT Context $ StateRefT State GrindM
 def PreM.run (x : PreM α) : GrindM α := do
   let thms ← grindNormExt.getTheorems
   let simprocs := #[(← grindNormSimprocExt.getSimprocs)]
-  let simp ← Simp.mkContext
-    (config := { arith := true })
-    (simpTheorems := #[thms])
-    (congrTheorems := (← getSimpCongrTheorems))
+  let simp : Simp.Context := {
+    config := { arith := true }
+    simpTheorems := #[thms]
+    congrTheorems := (← getSimpCongrTheorems)
+  }
   x { simp, simprocs } |>.run' {}
 
 def simp (_goal : Goal) (e : Expr) : PreM Simp.Result := do

src/Lean/Meta/Tactic/Intro.lean

@@ -17,7 +17,7 @@ namespace Lean.Meta
     match i, type with
     | 0, type =>
       let type := type.instantiateRevRange j fvars.size fvars
-      withLCtx' lctx do
+      withReader (fun ctx => { ctx with lctx := lctx }) do
         withNewLocalInstances fvars j do
           let tag     ← mvarId.getTag
           let type := type.headBeta
@@ -57,7 +57,7 @@ namespace Lean.Meta
         loop i lctx fvars j s body
       else
         let type := type.instantiateRevRange j fvars.size fvars
-        withLCtx' lctx do
+        withReader (fun ctx => { ctx with lctx := lctx }) do
           withNewLocalInstances fvars j do
             /- We used to use just `whnf`, but it produces counterintuitive behavior if
               - `type` is a metavariable `?m` such that `?m := let x := v; b`, or

src/Lean/Meta/Tactic/Rewrites.lean

@@ -60,6 +60,9 @@ private def addImport (name : Name) (constInfo : ConstantInfo) :
         pure a
       | _ => return #[]
 
+/-- Configuration for `DiscrTree`. -/
+def discrTreeConfig : WhnfCoreConfig := {}
+
 /-- Select `=` and `↔` local hypotheses. -/
 def localHypotheses (except : List FVarId := []) : MetaM (Array (Expr × Bool × Nat)) := do
   let r ← getLocalHyps

src/Lean/Meta/Tactic/Simp/Attr.lean

@@ -73,10 +73,7 @@ def getSimpTheorems : CoreM SimpTheorems :=
 def getSEvalTheorems : CoreM SimpTheorems :=
   sevalSimpExtension.getTheorems
 
-def Simp.Context.mkDefault : MetaM Context := do
-  mkContext
-    (config := {})
-    (simpTheorems := #[(← Meta.getSimpTheorems)])
-    (congrTheorems := (← Meta.getSimpCongrTheorems))
+def Simp.Context.mkDefault : MetaM Context :=
+  return { config := {}, simpTheorems := #[(← Meta.getSimpTheorems)], congrTheorems := (← Meta.getSimpCongrTheorems) }
 
 end Lean.Meta

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

@@ -20,6 +20,18 @@ builtin_initialize congrHypothesisExceptionId : InternalExceptionId ←
 def throwCongrHypothesisFailed : MetaM α :=
   throw <| Exception.internal congrHypothesisExceptionId
 
+/--
+  Helper method for bootstrapping purposes. It disables `arith` if support theorems have not been defined yet.
+-/
+def Config.updateArith (c : Config) : CoreM Config := do
+  if c.arith then
+    if (← getEnv).contains ``Nat.Linear.ExprCnstr.eq_of_toNormPoly_eq then
+      return c
+    else
+      return { c with arith := false }
+  else
+    return c
+
 /-- Return true if `e` is of the form `ofNat n` where `n` is a kernel Nat literal -/
 def isOfNatNatLit (e : Expr) : Bool :=
   e.isAppOf ``OfNat.ofNat && e.getAppNumArgs >= 3 && (e.getArg! 1).isRawNatLit
@@ -244,7 +256,7 @@ def withNewLemmas {α} (xs : Array Expr) (f : SimpM α) : SimpM α := do
           s ← s.addTheorem (.fvar x.fvarId!) x
           updated := true
       if updated then
-        withSimpTheorems s f
+        withTheReader Context (fun ctx => { ctx with simpTheorems := s }) f
       else
         f
   else if (← getMethods).wellBehavedDischarge then
@@ -451,7 +463,7 @@ private partial def dsimpImpl (e : Expr) : SimpM Expr := do
   let m ← getMethods
   let pre := m.dpre >> doNotVisitOfNat >> doNotVisitOfScientific >> doNotVisitCharLit
   let post := m.dpost >> dsimpReduce
-  withInDSimp do
+  withTheReader Simp.Context (fun ctx => { ctx with inDSimp := true }) do
   transform (usedLetOnly := cfg.zeta) e (pre := pre) (post := post)
 
 def visitFn (e : Expr) : SimpM Result := do
@@ -646,12 +658,11 @@ where
     trace[Meta.Tactic.simp.heads] "{repr e.toHeadIndex}"
     simpLoop e
 
--- TODO: delete
 @[inline] def withSimpContext (ctx : Context) (x : MetaM α) : MetaM α :=
   withConfig (fun c => { c with etaStruct := ctx.config.etaStruct }) <| withReducible x
 
 def main (e : Expr) (ctx : Context) (stats : Stats := {}) (methods : Methods := {}) : MetaM (Result × Stats) := do
-  let ctx ← ctx.setLctxInitIndices
+  let ctx := { ctx with config := (← ctx.config.updateArith), lctxInitIndices := (← getLCtx).numIndices }
   withSimpContext ctx do
     let (r, s) ← go e methods.toMethodsRef ctx |>.run { stats with }
     trace[Meta.Tactic.simp.numSteps] "{s.numSteps}"
@@ -799,7 +810,7 @@ def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray :=
     for fvarId in fvarIdsToSimp do
       let localDecl ← fvarId.getDecl
       let type ← instantiateMVars localDecl.type
-      let ctx := ctx.setSimpTheorems <| ctx.simpTheorems.eraseTheorem (.fvar localDecl.fvarId)
+      let ctx := { ctx with simpTheorems := ctx.simpTheorems.eraseTheorem (.fvar localDecl.fvarId) }
       let (r, stats') ← simp type ctx simprocs discharge? stats
       stats := stats'
       match r.proof? with
@@ -833,7 +844,7 @@ def simpTargetStar (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsAr
     let localDecl ← h.getDecl
     let proof  := localDecl.toExpr
     let simpTheorems ← ctx.simpTheorems.addTheorem (.fvar h) proof
-    ctx := ctx.setSimpTheorems simpTheorems
+    ctx := { ctx with simpTheorems }
   match (← simpTarget mvarId ctx simprocs discharge? (stats := stats)) with
   | (none, stats) => return (TacticResultCNM.closed, stats)
   | (some mvarId', stats') =>

src/Lean/Meta/Tactic/Simp/Rewrite.lean

@@ -41,7 +41,7 @@ def discharge?' (thmId : Origin) (x : Expr) (type : Expr) : SimpM Bool := do
     let ctx ← getContext
     if ctx.dischargeDepth >= ctx.maxDischargeDepth then
       return .maxDepth
-    else withIncDischargeDepth do
+    else withTheReader Context (fun ctx => { ctx with dischargeDepth := ctx.dischargeDepth + 1 }) do
       -- We save the state, so that `UsedTheorems` does not accumulate
       -- `simp` lemmas used during unsuccessful discharging.
       -- We use `withPreservedCache` to ensure the cache is restored after `discharge?`
@@ -446,13 +446,10 @@ def mkSEvalMethods : CoreM Methods := do
     wellBehavedDischarge := true
   }
 
-def mkSEvalContext : MetaM Context := do
+def mkSEvalContext : CoreM Context := do
   let s ← getSEvalTheorems
   let c ← Meta.getSimpCongrTheorems
-  mkContext
-    (simpTheorems := #[s])
-    (congrTheorems := c)
-    (config := { ground := true })
+  return { simpTheorems := #[s], congrTheorems := c, config := { ground := true } }
 
 /--
 Invoke ground/symbolic evaluator from `simp`.
@@ -555,7 +552,7 @@ private def dischargeUsingAssumption? (e : Expr) : SimpM (Option Expr) := do
 partial def dischargeEqnThmHypothesis? (e : Expr) : MetaM (Option Expr) := do
   assert! isEqnThmHypothesis e
   let mvar ← mkFreshExprSyntheticOpaqueMVar e
-  withCanUnfoldPred canUnfoldAtMatcher do
+  withReader (fun ctx => { ctx with canUnfold? := canUnfoldAtMatcher }) do
     if let .none ← go? mvar.mvarId! then
       instantiateMVars mvar
     else

src/Lean/Meta/Tactic/Simp/SimpAll.lean

@@ -43,7 +43,7 @@ private def initEntries : M Unit := do
       let localDecl ← h.getDecl
       let proof  := localDecl.toExpr
       simpThms ← simpThms.addTheorem (.fvar h) proof
-      modify fun s => { s with ctx := s.ctx.setSimpTheorems simpThms }
+      modify fun s => { s with ctx.simpTheorems := simpThms }
       if hsNonDeps.contains h then
         -- We only simplify nondependent hypotheses
         let type ← instantiateMVars localDecl.type
@@ -62,7 +62,7 @@ private partial def loop : M Bool := do
     let ctx := (← get).ctx
     -- We disable the current entry to prevent it to be simplified to `True`
     let simpThmsWithoutEntry := (← getSimpTheorems).eraseTheorem entry.id
-    let ctx := ctx.setSimpTheorems simpThmsWithoutEntry
+    let ctx := { ctx with simpTheorems := simpThmsWithoutEntry }
     let (r, stats) ← simpStep (← get).mvarId entry.proof entry.type ctx simprocs (stats := { (← get) with })
     modify fun s => { s with usedTheorems := stats.usedTheorems, diag := stats.diag }
     match r with
@@ -98,7 +98,7 @@ private partial def loop : M Bool := do
         simpThmsNew ← simpThmsNew.addTheorem (.other idNew) (← mkExpectedTypeHint proofNew typeNew)
         modify fun s => { s with
           modified         := true
-          ctx              := ctx.setSimpTheorems simpThmsNew
+          ctx.simpTheorems := simpThmsNew
           entries[i]       := { entry with type := typeNew, proof := proofNew, id := .other idNew }
         }
   -- simplify target

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

@@ -52,7 +52,6 @@ abbrev Cache := SExprMap Result
 abbrev CongrCache := ExprMap (Option CongrTheorem)
 
 structure Context where
-  private mk ::
   config           : Config := {}
   /-- `maxDischargeDepth` from `config` as an `UInt32`. -/
   maxDischargeDepth : UInt32 := UInt32.ofNatTruncate config.maxDischargeDepth
@@ -104,41 +103,6 @@ structure Context where
   inDSimp : Bool := false
   deriving Inhabited
 
-/--
-Helper method for bootstrapping purposes.
-It disables `arith` if support theorems have not been defined yet.
--/
-private def updateArith (c : Config) : CoreM Config := do
-  if c.arith then
-    if (← getEnv).contains ``Nat.Linear.ExprCnstr.eq_of_toNormPoly_eq then
-      return c
-    else
-      return { c with arith := false }
-  else
-    return c
-
-def mkContext (config : Config := {}) (simpTheorems : SimpTheoremsArray := {}) (congrTheorems : SimpCongrTheorems := {}) : MetaM Context := do
-  let config ← updateArith config
-  return { config, simpTheorems, congrTheorems }
-
-def Context.setConfig (context : Context) (config : Config) : Context :=
-  { context with config }
-
-def Context.setSimpTheorems (c : Context) (simpTheorems : SimpTheoremsArray) : Context :=
-  { c with simpTheorems }
-
-def Context.setLctxInitIndices (c : Context) : MetaM Context :=
-  return { c with lctxInitIndices := (← getLCtx).numIndices }
-
-def Context.setAutoUnfold (c : Context) : Context :=
-  { c with config.autoUnfold := true }
-
-def Context.setFailIfUnchanged (c : Context) (flag : Bool) : Context :=
-  { c with config.failIfUnchanged := flag }
-
-def Context.setMemoize (c : Context) (flag : Bool) : Context :=
-  { c with config.memoize := flag }
-
 def Context.isDeclToUnfold (ctx : Context) (declName : Name) : Bool :=
   ctx.simpTheorems.isDeclToUnfold declName
 
@@ -194,15 +158,6 @@ instance : Nonempty MethodsRef := MethodsRefPointed.property
 
 abbrev SimpM := ReaderT MethodsRef $ ReaderT Context $ StateRefT State MetaM
 
-@[inline] def withIncDischargeDepth : SimpM α → SimpM α :=
-  withTheReader Context (fun ctx => { ctx with dischargeDepth := ctx.dischargeDepth + 1 })
-
-@[inline] def withSimpTheorems (s : SimpTheoremsArray) : SimpM α → SimpM α :=
-  withTheReader Context (fun ctx => { ctx with simpTheorems := s })
-
-@[inline] def withInDSimp : SimpM α → SimpM α :=
-  withTheReader Context (fun ctx => { ctx with inDSimp := true })
-
 @[extern "lean_simp"]
 opaque simp (e : Expr) : SimpM Result
 

src/Lean/Meta/Tactic/Split.lean

@@ -13,11 +13,12 @@ import Lean.Meta.Tactic.Generalize
 namespace Lean.Meta
 namespace Split
 
-def getSimpMatchContext : MetaM Simp.Context := do
-   Simp.mkContext
-      (simpTheorems   := {})
-      (congrTheorems := (← getSimpCongrTheorems))
-      (config        := { Simp.neutralConfig with dsimp := false })
+def getSimpMatchContext : MetaM Simp.Context :=
+   return {
+      simpTheorems   := {}
+      congrTheorems := (← getSimpCongrTheorems)
+      config        := { Simp.neutralConfig with dsimp := false }
+   }
 
 def simpMatch (e : Expr) : MetaM Simp.Result := do
   let discharge? ← SplitIf.mkDischarge?

src/Lean/Meta/Tactic/SplitIf.lean

@@ -19,10 +19,11 @@ def getSimpContext : MetaM Simp.Context := do
   s ← s.addConst ``if_neg
   s ← s.addConst ``dif_pos
   s ← s.addConst ``dif_neg
-  Simp.mkContext
-    (simpTheorems  := #[s])
-    (congrTheorems := (← getSimpCongrTheorems))
-    (config        := { Simp.neutralConfig with dsimp := false })
+  return {
+    simpTheorems  := #[s]
+    congrTheorems := (← getSimpCongrTheorems)
+    config        := { Simp.neutralConfig with dsimp := false }
+  }
 
 /--
   Default `discharge?` function for `simpIf` methods.

src/Lean/Meta/Tactic/Unfold.lean

@@ -10,10 +10,11 @@ import Lean.Meta.Tactic.Simp.Main
 
 namespace Lean.Meta
 
-private def getSimpUnfoldContext : MetaM Simp.Context := do
-   Simp.mkContext
-      (congrTheorems := (← getSimpCongrTheorems))
-      (config        := Simp.neutralConfig)
+private def getSimpUnfoldContext : MetaM Simp.Context :=
+   return {
+      congrTheorems := (← getSimpCongrTheorems)
+      config        := Simp.neutralConfig
+   }
 
 def unfold (e : Expr) (declName : Name) : MetaM Simp.Result := do
   if let some unfoldThm ← getUnfoldEqnFor? declName  then

src/Lean/Meta/UnificationHint.lean

@@ -96,7 +96,7 @@ builtin_initialize
 
 def tryUnificationHints (t s : Expr) : MetaM Bool := do
   trace[Meta.isDefEq.hint] "{t} =?= {s}"
-  unless (← getConfig).unificationHints do
+  unless (← read).config.unificationHints do
     return false
   if t.isMVar then
     return false

src/Lean/Meta/WHNF.lean

@@ -529,7 +529,7 @@ private def whnfMatcher (e : Expr) : MetaM Expr := do
      TODO: consider other solutions; investigate whether the solution above produces counterintuitive behavior.  -/
   if (← getTransparency) matches .instances | .reducible then
     -- Also unfold some default-reducible constants; see `canUnfoldAtMatcher`
-    withTransparency .instances <| withCanUnfoldPred canUnfoldAtMatcher do
+    withTransparency .instances <| withReader (fun ctx => { ctx with canUnfold? := canUnfoldAtMatcher }) do
       whnf e
   else
     -- Do NOT use `canUnfoldAtMatcher` here as it does not affect all/default reducibility and inhibits caching (#2564).

src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean

@@ -205,7 +205,7 @@ def replaceLPsWithVars (e : Expr) : MetaM Expr := do
     | l => if !l.hasParam then some l else none
 
 def isDefEqAssigning (t s : Expr) : MetaM Bool := do
-  withConfig (fun cfg => { cfg with assignSyntheticOpaque := true }) do
+  withReader (fun ctx => { ctx with config := { ctx.config with assignSyntheticOpaque := true }}) $
     Meta.isDefEq t s
 
 def checkpointDefEq (t s : Expr) : MetaM Bool := do
@@ -624,7 +624,7 @@ open TopDownAnalyze SubExpr
 def topDownAnalyze (e : Expr) : MetaM OptionsPerPos := do
   let s₀ ← get
   withTraceNode `pp.analyze (fun _ => return e) do
-    withConfig Elab.Term.setElabConfig do
+    withReader (fun ctx => { ctx with config := Elab.Term.setElabConfig ctx.config }) do
       let ϕ : AnalyzeM OptionsPerPos := do withNewMCtxDepth analyze; pure (← get).annotations
       try
         let knowsType := getPPAnalyzeKnowsType (← getOptions)

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

@@ -38,7 +38,7 @@ theorem toListModel_mkArray_nil {c} :
 @[simp]
 theorem computeSize_eq {buckets : Array (AssocList α β)} :
     computeSize buckets = (toListModel buckets).length := by
-  rw [computeSize, toListModel, List.flatMap_eq_foldl, Array.foldl_toList]
+  rw [computeSize, toListModel, List.flatMap_eq_foldl, Array.foldl_eq_foldl_toList]
   suffices ∀ (l : List (AssocList α β)) (l' : List ((a : α) × β a)),
       l.foldl (fun d b => d + b.toList.length) l'.length =
         (l.foldl (fun acc a => acc ++ a.toList) l').length
@@ -61,13 +61,13 @@ theorem isEmpty_eq_isEmpty [BEq α] [Hashable α] {m : Raw α β} (h : Raw.WFImp
 
 theorem fold_eq {l : Raw α β} {f : γ → (a : α) → β a → γ} {init : γ} :
     l.fold f init = l.buckets.foldl (fun acc l => l.foldl f acc) init := by
-  simp only [Raw.fold, Raw.foldM, ← Array.foldlM_toList, Array.foldl_toList,
+  simp only [Raw.fold, Raw.foldM, Array.foldlM_eq_foldlM_toList, Array.foldl_eq_foldl_toList,
     ← List.foldl_eq_foldlM, Id.run, AssocList.foldl]
 
 theorem fold_cons_apply {l : Raw α β} {acc : List γ} (f : (a : α) → β a → γ) :
     l.fold (fun acc k v => f k v :: acc) acc =
       ((toListModel l.buckets).reverse.map (fun p => f p.1 p.2)) ++ acc := by
-  rw [fold_eq, ← Array.foldl_toList, toListModel]
+  rw [fold_eq, Array.foldl_eq_foldl_toList, toListModel]
   generalize l.buckets.toList = l
   induction l generalizing acc with
   | nil => simp

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

@@ -61,7 +61,7 @@ theorem CNF.Clause.mem_lrat_of_mem (clause : CNF.Clause (PosFin n)) (h1 : l ∈
   | nil => cases h1
   | cons hd tl ih =>
     unfold DefaultClause.ofArray at h2
-    rw [← Array.foldr_toList, List.toArray_toList] at h2
+    rw [Array.foldr_eq_foldr_toList, List.toArray_toList] at h2
     dsimp only [List.foldr] at h2
     split at h2
     · cases h2
@@ -77,7 +77,7 @@ theorem CNF.Clause.mem_lrat_of_mem (clause : CNF.Clause (PosFin n)) (h1 : l ∈
             · assumption
             · next heq _ _ =>
               unfold DefaultClause.ofArray
-              rw [← Array.foldr_toList, List.toArray_toList]
+              rw [Array.foldr_eq_foldr_toList, List.toArray_toList]
               exact heq
         · cases h1
           · simp only [← Option.some.inj h2]
@@ -89,7 +89,7 @@ theorem CNF.Clause.mem_lrat_of_mem (clause : CNF.Clause (PosFin n)) (h1 : l ∈
             apply ih
             assumption
             unfold DefaultClause.ofArray
-            rw [← Array.foldr_toList, List.toArray_toList]
+            rw [Array.foldr_eq_foldr_toList, List.toArray_toList]
             exact heq
 
 theorem CNF.Clause.convertLRAT_sat_of_sat (clause : CNF.Clause (PosFin n))

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

@@ -106,7 +106,7 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))
   constructor
   · simp only [ofArray]
   · have hsize : (ofArray arr).assignments.size = n := by
-      simp only [ofArray, ← Array.foldl_toList]
+      simp only [ofArray, Array.foldl_eq_foldl_toList]
       have hb : (mkArray n unassigned).size = n := by simp only [Array.size_mkArray]
       have hl (acc : Array Assignment) (ih : acc.size = n) (cOpt : Option (DefaultClause n)) (_cOpt_in_arr : cOpt ∈ arr.toList) :
         (ofArray_fold_fn acc cOpt).size = n := by rw [size_ofArray_fold_fn acc cOpt, ih]
@@ -187,7 +187,7 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))
             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
-    simp only [ofArray, ← Array.foldl_toList] at h
+    simp only [ofArray, Array.foldl_eq_foldl_toList] at h
     exact h' i b h
 
 theorem readyForRatAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))) :
@@ -605,7 +605,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
 theorem readyForRupAdd_delete {n : Nat} (f : DefaultFormula n) (arr : Array Nat) :
     ReadyForRupAdd f → ReadyForRupAdd (delete f arr) := by
   intro h
-  rw [delete, ← Array.foldl_toList]
+  rw [delete, Array.foldl_eq_foldl_toList]
   constructor
   · have hb : f.rupUnits = #[] := h.1
     have hl (acc : DefaultFormula n) (ih : acc.rupUnits = #[]) (id : Nat) (_id_in_arr : id ∈ arr.toList) :
@@ -625,7 +625,7 @@ theorem readyForRatAdd_delete {n : Nat} (f : DefaultFormula n) (arr : Array Nat)
     ReadyForRatAdd f → ReadyForRatAdd (delete f arr) := by
   intro h
   constructor
-  · rw [delete, ← Array.foldl_toList]
+  · rw [delete, Array.foldl_eq_foldl_toList]
     have hb : f.ratUnits = #[] := h.1
     have hl (acc : DefaultFormula n) (ih : acc.ratUnits = #[]) (id : Nat) (_id_in_arr : id ∈ arr.toList) :
       (deleteOne acc id).ratUnits = #[] := by rw [deleteOne_preserves_ratUnits, ih]
@@ -659,7 +659,7 @@ theorem deleteOne_subset (f : DefaultFormula n) (id : Nat) (c : DefaultClause n)
 
 theorem delete_subset (f : DefaultFormula n) (arr : Array Nat) (c : DefaultClause n) :
     c ∈ toList (delete f arr) → c ∈ toList f := by
-  simp only [delete, ← Array.foldl_toList]
+  simp only [delete, Array.foldl_eq_foldl_toList]
   have hb : c ∈ toList f → c ∈ toList f := id
   have hl (f' : DefaultFormula n) (ih : c ∈ toList f' → c ∈ toList f) (id : Nat) (_ : id ∈ arr.toList) :
     c ∈ toList (deleteOne f' id) → c ∈ toList f := by intro h; exact ih <| deleteOne_subset f' id c h

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

@@ -739,7 +739,7 @@ theorem size_assignemnts_confirmRupHint {n : Nat} (clauses : Array (Option (Defa
 theorem size_assignments_performRupCheck {n : Nat} (f : DefaultFormula n) (rupHints : Array Nat) :
     (performRupCheck f rupHints).1.assignments.size = f.assignments.size := by
   simp only [performRupCheck]
-  rw [← Array.foldl_toList]
+  rw [Array.foldl_eq_foldl_toList]
   have hb : (f.assignments, ([] : CNF.Clause (PosFin n)), false, false).1.size = f.assignments.size := rfl
   have hl (acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool) (hsize : acc.1.size = f.assignments.size)
     (id : Nat) (_ : id ∈ rupHints.toList) : (confirmRupHint f.clauses acc id).1.size = f.assignments.size := by
@@ -1288,7 +1288,7 @@ theorem restoreAssignments_performRupCheck {n : Nat} (f : DefaultFormula n) (f_a
   have derivedLits_satisfies_invariant := derivedLitsInvariant_performRupCheck f f_assignments_size rupHints f'_assignments_size
   simp only at derivedLits_satisfies_invariant
   generalize (performRupCheck f rupHints).2.1 = derivedLits at *
-  rw [← f'_def, Array.foldl_toList]
+  rw [← f'_def, ← Array.foldl_eq_foldl_toList]
   let derivedLits_arr : Array (Literal (PosFin n)) := {toList := derivedLits}
   have derivedLits_arr_def : derivedLits_arr = {toList := derivedLits} := rfl
   have derivedLits_arr_nodup := nodup_derivedLits f f_assignments_size rupHints f'_assignments_size derivedLits
@@ -1301,7 +1301,7 @@ theorem restoreAssignments_performRupCheck {n : Nat} (f : DefaultFormula n) (f_a
     clear_insert_inductive_case f f_assignments_size derivedLits_arr derivedLits_arr_nodup idx assignments ih
   rcases Array.foldl_induction motive h_base h_inductive with ⟨h_size, h⟩
   apply Array.ext
-  · rw [← Array.foldl_toList, size_clearUnit_foldl f'.assignments clearUnit size_clearUnit derivedLits,
+  · rw [Array.foldl_eq_foldl_toList, size_clearUnit_foldl f'.assignments clearUnit size_clearUnit derivedLits,
       f'_assignments_size, f_assignments_size]
   · intro i hi1 hi2
     rw [f_assignments_size] at hi2

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

@@ -544,7 +544,7 @@ theorem reduce_postcondition {n : Nat} (c : DefaultClause n) (assignment : Array
     (∀ l : Literal (PosFin n), reduce c assignment = reducedToUnit l → ∀ (p : (PosFin n) → Bool), p ⊨ assignment → p ⊨ c → p ⊨ l) := by
   let c_arr := c.clause.toArray
   have c_clause_rw : c.clause = c_arr.toList := by simp [c_arr]
-  rw [reduce, c_clause_rw, Array.foldl_toList]
+  rw [reduce, c_clause_rw, ← Array.foldl_eq_foldl_toList]
   let motive := ReducePostconditionInductionMotive c_arr assignment
   have h_base : motive 0 reducedToEmpty := by
     have : ∀ (a : PosFin n) (b : Bool), (reducedToEmpty = reducedToUnit (a, b)) = False := by intros; simp

src/include/lean/lean.h

@@ -1617,16 +1617,7 @@ static inline uint8_t lean_int_dec_nonneg(b_lean_obj_arg a) {
 
 /* Bool */
 
-static inline uint8_t lean_bool_to_uint8(uint8_t a) { return a; }
-static inline uint16_t lean_bool_to_uint16(uint8_t a) { return (uint16_t)a; }
-static inline uint32_t lean_bool_to_uint32(uint8_t a) { return (uint32_t)a; }
-static inline uint64_t lean_bool_to_uint64(uint8_t a) { return (uint64_t)a; }
-static inline size_t lean_bool_to_usize(uint8_t a) { return (size_t)a; }
-static inline uint8_t lean_bool_to_int8(uint8_t a) { return (uint8_t)(int8_t)a; }
-static inline uint16_t lean_bool_to_int16(uint8_t a) { return (uint16_t)(int16_t)a; }
-static inline uint32_t lean_bool_to_int32(uint8_t a) { return (uint32_t)(int32_t)a; }
-static inline uint64_t lean_bool_to_int64(uint8_t a) { return (uint64_t)(int64_t)a; }
-static inline size_t lean_bool_to_isize(uint8_t a) { return (size_t)(ptrdiff_t)a; }
+static inline uint64_t lean_bool_to_uint64(uint8_t a) { return ((uint64_t)a); }
 
 
 /* UInt8 */

src/lake/Lake/CLI/Init.lean

@@ -24,14 +24,12 @@ s!"/{defaultLakeDir}
 "
 
 def basicFileContents :=
-s!"def hello := \"world\"
-"
+  s!"def hello := \"world\""
 
 def libRootFileContents (libName : String) (libRoot : Name) :=
 s!"-- This module serves as the root of the `{libName}` library.
 -- Import modules here that should be built as part of the library.
-import {libRoot}.Basic
-"
+import {libRoot}.Basic"
 
 def mainFileName : FilePath :=
   s!"{defaultExeRoot}.lean"

src/lake/Lake/CLI/Main.lean

@@ -515,7 +515,7 @@ protected def translateConfig : CliM PUnit := do
   if outFile?.isNone then
     IO.FS.rename pkg.configFile (pkg.configFile.addExtension "bak")
 
-def ReservoirConfig.currentSchemaVersion : StdVer := {major := 1}
+def ReservoirConfig.currentSchemaVersion : StdVer := v!"1.0.0"
 
 structure ReservoirConfig where
   name : String

src/lake/Lake/CLI/Translate/Lean.lean

@@ -119,7 +119,7 @@ def PackageConfig.mkSyntax (cfg : PackageConfig)
     |> addDeclFieldD `testDriverArgs cfg.testDriverArgs #[]
     |> addDeclFieldD `lintDriver lintDriver ""
     |> addDeclFieldD `lintDriverArgs cfg.lintDriverArgs #[]
-    |> addDeclFieldD `version cfg.version {}
+    |> addDeclFieldD `version cfg.version v!"0.0.0"
     |> addDeclField? `versionTags (quoteVerTags? cfg.versionTags)
     |> addDeclFieldD `description cfg.description ""
     |> addDeclFieldD `keywords cfg.keywords #[]

src/lake/Lake/CLI/Translate/Toml.lean

@@ -76,7 +76,7 @@ protected def PackageConfig.toToml (cfg : PackageConfig) (t : Table := {}) : Tab
   |>.smartInsert `releaseRepo (cfg.releaseRepo <|> cfg.releaseRepo?)
   |>.insertD `buildArchive (cfg.buildArchive?.getD cfg.buildArchive) (defaultBuildArchive cfg.name)
   |>.insertD `preferReleaseBuild cfg.preferReleaseBuild false
-  |>.insertD `version cfg.version {}
+  |>.insertD `version cfg.version v!"0.0.0"
   |> smartInsertVerTags cfg.versionTags
   |>.smartInsert `keywords cfg.description
   |>.smartInsert `keywords cfg.keywords

src/lake/Lake/Config/Package.lean

@@ -275,7 +275,7 @@ structure PackageConfig extends WorkspaceConfig, LeanConfig where
 
   Packages without a defined version default to `0.0.0`.
   -/
-  version : StdVer := {}
+  version : StdVer := v!"0.0.0"
 
   /--
   Git tags of this package's repository that should be treated as versions.

src/lake/Lake/Load/Manifest.lean

@@ -49,7 +49,7 @@ That is, Lake ignores the `-` suffix.
 - `"1.0.0"`: Switches to a semantic versioning scheme
 - `"1.1.0"`: Add optional `scope` package entry field
 -/
-@[inline] def Manifest.version : StdVer := {major := 1, minor := 1}
+@[inline] def Manifest.version : StdVer := v!"1.1.0"
 
 /-- Manifest version `0.6.0` package entry. For backwards compatibility. -/
 inductive PackageEntryV6
@@ -201,14 +201,14 @@ protected def fromJson? (json : Json) : Except String Manifest := do
   if ver.major > 1 then
     throw s!"manifest version '{ver}' is of a higher major version than this \
       Lake's '{Manifest.version}'; you may need to update your 'lean-toolchain'"
-  else if ver < {minor := 5} then
+  else if ver < v!"0.5.0" then
     throw s!"incompatible manifest version '{ver}'"
   else
     let name ← obj.getD "name" Name.anonymous
     let lakeDir ← obj.getD "lakeDir" defaultLakeDir
     let packagesDir? ← obj.get? "packagesDir"
     let packages ←
-      if ver < {minor := 7} then
+      if ver < v!"0.7.0" then
         (·.map PackageEntry.ofV6) <$> obj.getD "packages" #[]
       else
         obj.getD "packages" #[]

src/lake/Lake/Load/Toml.lean

@@ -207,7 +207,7 @@ protected def PackageConfig.decodeToml (t : Table) (ref := Syntax.missing) : Exc
   let testDriverArgs ← t.tryDecodeD `testDriverArgs #[]
   let lintDriver ← t.tryDecodeD `lintDriver ""
   let lintDriverArgs ← t.tryDecodeD `lintDriverArgs #[]
-  let version : StdVer ← t.tryDecodeD `version {}
+  let version : StdVer ← t.tryDecodeD `version v!"0.0.0"
   let versionTags ← optDecodeD defaultVersionTags (t.find? `versionTags)
     <| StrPat.decodeToml (presets := versionTagPresets)
   let description ← t.tryDecodeD `description ""

tests/bench/simp_arith1.lean

@@ -1,29 +0,0 @@
-import Lean
-
-open Lean Meta Elab in
-elab "largeGoal%" : term =>
-  let n := 30 -- number of variables
-  let r := 3 -- number of repetitions
-  let mkAdd := mkApp2 (mkConst ``Nat.add)
-  let mkMul := mkApp2 (mkConst ``Nat.mul)
-  let decls := Array.ofFn fun (i : Fin n) =>
-    ((`x).appendIndexAfter i, (fun _ => pure (mkConst ``Nat)))
-  withLocalDeclsD decls fun xs => do
-    let mut e₁ : Expr := mkNatLit 42
-    let mut e₂ : Expr := mkNatLit 23
-    for _ in [:r] do
-      for i in [:xs.size] do
-        e₁ := mkAdd (mkMul (mkNatLit i) e₁) xs[i]!
-        e₂ := mkAdd xs[i]! (mkMul e₂ (mkNatLit (xs.size - i)))
-    let goal ← mkEq e₁ e₂
-    let goal := mkNot goal
-    let goal ← mkForallFVars xs goal
-    return goal
-
-set_option maxRecDepth 10000
-
--- manually verified: most time spent in type-checking
--- set_option trace.profiler true
-example : largeGoal% := by
-  intros
-  simp_arith only

tests/bench/speedcenter.exec.velcom.yaml

@@ -316,12 +316,6 @@
   run_config:
     <<: *time
     cmd: lean reduceMatch.lean
-- attributes:
-    description: simp_arith1
-    tags: [fast, suite]
-  run_config:
-    <<: *time
-    cmd: lean simp_arith1.lean
 - attributes:
     description: nat_repr
     tags: [fast, suite]

tests/lean/1018unknowMVarIssue.lean.expected.out

@@ -56,8 +56,8 @@ a : α
           • Fam2.any : Fam2 α α @ ⟨9, 4⟩†-⟨9, 12⟩†
             • α : Type @ ⟨9, 4⟩†-⟨9, 12⟩†
           • a (isBinder := true) : α @ ⟨8, 2⟩†-⟨10, 19⟩†
-          • FVarAlias a: _uniq.585 -> _uniq.312
-          • FVarAlias α: _uniq.584 -> _uniq.310
+          • FVarAlias a: _uniq.632 -> _uniq.312
+          • FVarAlias α: _uniq.631 -> _uniq.310
           • ?m x α a : α @ ⟨9, 18⟩-⟨9, 19⟩ @ Lean.Elab.Term.elabHole
           • [.] Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
           • Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
@@ -71,8 +71,8 @@ a : α
           • Fam2.nat n : Fam2 Nat Nat @ ⟨10, 4⟩†-⟨10, 14⟩
             • n (isBinder := true) : Nat @ ⟨10, 13⟩-⟨10, 14⟩
           • a (isBinder := true) : Nat @ ⟨8, 2⟩†-⟨10, 19⟩†
-          • FVarAlias a: _uniq.616 -> _uniq.312
-          • FVarAlias n: _uniq.615 -> _uniq.310
+          • FVarAlias a: _uniq.663 -> _uniq.312
+          • FVarAlias n: _uniq.662 -> _uniq.310
           • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabIdent
             • [.] n : some Nat @ ⟨10, 18⟩-⟨10, 19⟩
             • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩

tests/lean/1081.lean.expected.out

@@ -1,12 +1,12 @@
 1081.lean:7:2-7:5: error: type mismatch
   rfl
 has type
-  ?m = ?m : Prop
+  f 0 y = f 0 y : Prop
 but is expected to have type
   f 0 y = y : Prop
 1081.lean:23:4-23:7: error: type mismatch
   rfl
 has type
-  ?m = ?m : Prop
+  insert a ⟨0, ⋯⟩ v = insert a ⟨0, ⋯⟩ v : Prop
 but is expected to have type
   insert a ⟨0, ⋯⟩ v = cons a v : Prop

tests/lean/1433.lean.expected.out

@@ -1,6 +1,6 @@
 1433.lean:11:49-11:52: error: type mismatch
   rfl
 has type
-  ?m = ?m : Prop
+  dividend % divisor = dividend % divisor : Prop
 but is expected to have type
   dividend % divisor = wrongRem : Prop

tests/lean/755.lean

@@ -1,5 +1,3 @@
-set_option pp.mvars false
-
 def Additive (α : Type) := α
 
 instance [OfNat α 1] : OfNat (Additive α) (nat_lit 0) := ⟨(1 : α)⟩

tests/lean/755.lean.expected.out

@@ -1,24 +1,24 @@
-755.lean:7:44-7:47: error: type mismatch
+755.lean:5:44-5:47: error: type mismatch
   rfl
 has type
-  ?_ = ?_ : Prop
+  0 = @OfNat.ofNat Nat 0 (instOfNatNat 0) : Prop
 but is expected to have type
-  0 = 0 : Prop
-755.lean:26:2-26:5: error: type mismatch
+  0 = @OfNat.ofNat (Additive Nat) 0 instOfNatAdditiveOfOfNatNat : Prop
+755.lean:24:2-24:5: error: type mismatch
   rfl
 has type
-  ?_ = ?_ : Prop
+  2 * 3 = @HMul.hMul Nat Nat Nat instHMul 2 3 : Prop
 but is expected to have type
-  2 * 3 = 2 * 3 : Prop
-755.lean:29:2-29:5: error: type mismatch
+  2 * 3 = @HMul.hMul (Foo Nat) (Foo Nat) (Foo Nat) instHMulFooOfHAdd 2 3 : Prop
+755.lean:27:2-27:5: error: type mismatch
   rfl
 has type
-  ?_ = ?_ : Prop
+  2 + 3 = @HAdd.hAdd Nat Nat Nat instHAdd 2 3 : Prop
 but is expected to have type
-  2 + 3 = 2 + 3 : Prop
-755.lean:32:2-32:5: error: type mismatch
+  2 + 3 = @HAdd.hAdd (Foo Nat) (Foo Nat) (Foo Nat) instHAddFoo 2 3 : Prop
+755.lean:30:2-30:5: error: type mismatch
   rfl
 has type
-  ?_ = ?_ : Prop
+  2 - 3 = @HSub.hSub Nat Nat Nat instHSub 2 3 : Prop
 but is expected to have type
-  2 - 3 = 2 - 3 : Prop
+  2 - 3 = @HSub.hSub (Foo Nat) (Foo Nat) (Foo Nat) instHSubFooOfHAdd 2 3 : Prop

tests/lean/bool2int.lean

@@ -1,20 +0,0 @@
-#eval Bool.toUInt8 false = 0
-#eval Bool.toUInt8 true = 1
-#eval Bool.toUInt16 false = 0
-#eval Bool.toUInt16 true = 1
-#eval Bool.toUInt32 false = 0
-#eval Bool.toUInt32 true = 1
-#eval Bool.toUInt64 false = 0
-#eval Bool.toUInt64 true = 1
-#eval Bool.toUSize false = 0
-#eval Bool.toUSize true = 1
-#eval Bool.toInt8 false = 0
-#eval Bool.toInt8 true = 1
-#eval Bool.toInt16 false = 0
-#eval Bool.toInt16 true = 1
-#eval Bool.toInt32 false = 0
-#eval Bool.toInt32 true = 1
-#eval Bool.toInt64 false = 0
-#eval Bool.toInt64 true = 1
-#eval Bool.toISize false = 0
-#eval Bool.toISize true = 1

tests/lean/bool2int.lean.expected.out

@@ -1,20 +0,0 @@
-true
-true
-true
-true
-true
-true
-true
-true
-true
-true
-true
-true
-true
-true
-true
-true
-true
-true
-true
-true

tests/lean/calcErrors.lean.expected.out

@@ -1,7 +1,7 @@
 calcErrors.lean:7:30-7:33: error: type mismatch
   rfl
 has type
-  ?m = ?m : Prop
+  b + b = b + b : Prop
 but is expected to have type
   b + b = 0 + c + b : Prop
 calcErrors.lean:13:8-13:29: error: invalid 'calc' step, left-hand side is

tests/lean/coeM.lean

@@ -4,8 +4,6 @@
 The functions inserted for the coercions are supposed to be inlined immediately during elaboration.
 -/
 
-set_option pp.mvars false
-
 variable (p : Nat → Prop) (m : IO (Subtype p))
 
 /-!
@@ -17,18 +15,3 @@ variable (p : Nat → Prop) (m : IO (Subtype p))
 `Lean.Internal.coeM`
 -/
 #check (m : IO Nat)
-
-/-!
-Making sure the monad lift coercion elaborator does not have side effects.
-
-It used to be responsible for hinting that the LHSs of equalities were defeq, like in the following example.
-It was checking that `Eq (some true)` and `Eq _` were defeq monads. The defeq check caused `_` to be solved as `some true`.
--/
-/--
-error: invalid dotted identifier notation, expected type is not of the form (... → C ...) where C is a constant
-  ?_
--/
-#guard_msgs in
-example : some true = (some true).map id := by
-  refine show _ = .some true from ?_
-  rfl

tests/lean/etaStructIssue.lean.expected.out

@@ -1,6 +1,6 @@
 etaStructIssue.lean:20:2-20:5: error: type mismatch
   rfl
 has type
-  ?m = ?m : Prop
+  mkNat e x₁ = mkNat e x₁ : Prop
 but is expected to have type
   mkNat e x₁ = mkNat e.mk x₂ : Prop

tests/lean/interactive/builtinCodeactions.lean

@@ -1,7 +0,0 @@
-/-- Must not introduce line break between `at` and `h` -/
-example {a b c d : Nat} (h : a = b)
-    (AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA : b = c)
-    (aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa : c = d) :
-    a = b := by
-  simp? [AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA, aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa] at h
-  --^ codeAction

tests/lean/interactive/builtinCodeactions.lean.expected.out

@@ -1,13 +0,0 @@
-{"title":
- "Try this: simp only [AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA,\n    aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa] at h",
- "kind": "quickfix",
- "isPreferred": true,
- "edit":
- {"documentChanges":
-  [{"textDocument": {"version": 1, "uri": "file:///builtinCodeactions.lean"},
-    "edits":
-    [{"range":
-      {"start": {"line": 5, "character": 2},
-       "end": {"line": 5, "character": 97}},
-      "newText":
-      "simp only [AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA,\n    aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa] at h"}]}]}}

tests/lean/isDefEqOffsetBug.lean.expected.out

@@ -1,6 +1,6 @@
 isDefEqOffsetBug.lean:19:2-19:5: error: type mismatch
   rfl
 has type
-  ?m = ?m : Prop
+  0 + 0 = 0 + 0 : Prop
 but is expected to have type
   0 + 0 = 0 : Prop

tests/lean/mulcommErrorMessage.lean.expected.out

@@ -8,10 +8,16 @@ the following variables have been introduced by the implicit lambda feature
   a✝ : Bool
   b✝ : Bool
 you can disable implicit lambdas using `@` or writing a lambda expression with `{}` or `[]` binder annotations.
+mulcommErrorMessage.lean:11:22-11:25: error: type mismatch
+  rfl
+has type
+  true = true : Prop
+but is expected to have type
+  true = false : Prop
 mulcommErrorMessage.lean:12:22-12:25: error: type mismatch
   rfl
 has type
-  ?m = ?m : Prop
+  false = false : Prop
 but is expected to have type
   false = true : Prop
 mulcommErrorMessage.lean:16:3-17:47: error: type mismatch

tests/lean/phashmap_inst_coherence.lean.expected.out

@@ -5,4 +5,4 @@ argument
 has type
   @PersistentHashMap Nat Nat instBEqOfDecidableEq instHashableNat : Type
 but is expected to have type
-  @PersistentHashMap Nat Nat ?m natDiffHash : Type
+  @PersistentHashMap Nat Nat instBEqOfDecidableEq natDiffHash : Type

tests/lean/run/1017.lean

@@ -25,7 +25,7 @@ def isFinite : Prop :=
 
 instance hasNextWF : WellFoundedRelation {s : ρ // isFinite s} where
   rel := λ s1 s2 => hasNext s2.val s1.val
-  wf := ⟨λ ⟨s,h⟩ => ⟨Subtype.mk s h, by
+  wf := ⟨λ ⟨s,h⟩ => ⟨⟨s,h⟩, by
     simp only [Subtype.forall]
     cases h; case intro w h =>
     induction w generalizing s

tests/lean/run/3150.lean

@@ -1,24 +0,0 @@
-class One (α : Type) where
-  one : α
-
-variable (R A : Type) [One R] [One A]
-
-class OneHom where
-  toFun : R → A
-  map_one : toFun One.one = One.one
-
-structure Subone where
-  mem : R → Prop
-  one_mem : mem One.one
-
-structure Subalgebra [OneHom R A] extends Subone A : Type where
-  algebraMap_mem : ∀ r : R, mem (OneHom.toFun r)
-  one_mem := OneHom.map_one (R := R) (A := A) ▸ algebraMap_mem One.one
-
-/--
-error: fields missing: 'one_mem'
--/
-#guard_msgs in
-example [OneHom R A] : Subalgebra R A where
-  mem := _
-  algebraMap_mem := _

tests/lean/run/4405.lean

@@ -4,13 +4,13 @@ set_option pp.mvars false
 
 /--
 error: application type mismatch
-  ⟨Nat.lt_irrefl (?_ n), Fin.is_lt ?_⟩
+  ⟨Nat.lt_irrefl ↑(?_ n), Fin.is_lt (?_ n)⟩
 argument
-  Fin.is_lt ?_
+  Fin.is_lt (?_ n)
 has type
-  ↑?_ < ?_ : Prop
+  ↑(?_ n) < ?_ n : Prop
 but is expected to have type
-  ?_ n < ?_ n : Prop
+  ↑(?_ n) < ↑(?_ n) : Prop
 -/
 #guard_msgs in
 def foo := fun n => (not_and_self_iff _).mp ⟨Nat.lt_irrefl _, Fin.is_lt _⟩

tests/lean/run/4413.lean

@@ -1,5 +1,3 @@
-set_option pp.mvars false
-
 structure Note where
   pitch : UInt64
   start : Nat
@@ -18,13 +16,13 @@ theorem Note.self_containsNote_lowerSemitone_self (n : Note) :
 error: type mismatch
   rfl
 has type
-  ?_ = ?_ : Prop
+  n = n : Prop
 but is expected to have type
   n = n - 1 : Prop
 -/
 #guard_msgs in
 set_option maxRecDepth 100 in
-set_option maxHeartbeats 200 in
+set_option maxHeartbeats 100 in
 example (n : UInt64) : n = n - 1 :=
   rfl
 

tests/lean/run/PPTopDownAnalyze.lean

@@ -328,11 +328,9 @@ set_option pp.analyze.explicitHoles false in
 #testDelab ∀ {α : Sort u} {β : α → Sort v} {f₁ f₂ : (x : α) → β x}, (∀ (x : α), f₁ x = f₂ _) → f₁ = f₂
   expecting ∀ {α : Sort u} {β : α → Sort v} {f₁ f₂ : (x : α) → β x}, (∀ (x : α), f₁ x = f₂ x) → f₁ = f₂
 
-/- TODO(kmill) 2024-11-10 fix the following test
 set_option pp.analyze.trustSubtypeMk true in
 #testDelab fun (n : Nat) (val : List Nat) (property : List.length val = n) => List.length { val := val, property := property : { x : List Nat // List.length x = n } }.val = n
   expecting fun n val property => (Subtype.val (p := fun x => x.length = n) (⟨val, property⟩ : { x : List Nat // x.length = n })).length = n
--/
 
 #testDelabN Nat.brecOn
 #testDelabN Nat.below

tests/lean/run/messageKind.lean

@@ -1,26 +0,0 @@
-import Lean.Elab.Command
-
-open Lean Elab Command
-
-elab tk:"#guard_msg_kind " kind:ident " in " cmd:command : command => do
-  let initMsgs ← modifyGet fun st => (st.messages, {st with messages := {}})
-  elabCommandTopLevel cmd
-  let msgs ← modifyGet fun st => (st.messages, {st with messages := initMsgs})
-  let kind := kind.getId
-  for msg in msgs.toList do
-    if msg.kind != kind then
-      logErrorAt tk s!"expected {kind}, got {msg.kind}"
-
-/- Test inferring kind from a tag. -/
-#guard_msg_kind custom in
-run_cmd do logInfo <| .tagged `custom ""
-
-/- Test trace message kind. -/
-#guard_msg_kind trace in
-set_option trace.Elab.step true in
-def trace := ()
-
-/- Test linter kind. -/
-#guard_msg_kind linter.unusedVariables in
-#guard_msgs (info) in -- hack to avoid re-triggering the linter
-def unused (x : Unit) := ()

tests/lean/run/scopedLocalReducibility.lean

@@ -1,11 +1,10 @@
 @[irreducible] def f (x : Nat) := x + 1
 set_option allowUnsafeReducibility true
-set_option pp.mvars false
 /--
 error: type mismatch
   rfl
 has type
-  ?_ = ?_ : Prop
+  f x = f x : Prop
 but is expected to have type
   f x = x + 1 : Prop
 -/
@@ -23,7 +22,7 @@ end
 error: type mismatch
   rfl
 has type
-  ?_ = ?_ : Prop
+  f x = f x : Prop
 but is expected to have type
   f x = x + 1 : Prop
 -/
@@ -39,7 +38,7 @@ end Boo
 error: type mismatch
   rfl
 has type
-  ?_ = ?_ : Prop
+  f x = f x : Prop
 but is expected to have type
   f x = x + 1 : Prop
 -/
@@ -55,7 +54,7 @@ example : f x = x + 1 :=
 error: type mismatch
   rfl
 has type
-  ?_ = ?_ : Prop
+  f x = f x : Prop
 but is expected to have type
   f x = x + 1 : Prop
 -/

tests/lean/run/sealCommand.lean

@@ -1,5 +1,3 @@
-set_option pp.mvars false
-
 def f (x : Nat) := x + 1
 
 example : f x = x + 1 := rfl
@@ -8,7 +6,7 @@ example : f x = x + 1 := rfl
 error: type mismatch
   rfl
 has type
-  ?_ = ?_ : Prop
+  f x = f x : Prop
 but is expected to have type
   f x = x + 1 : Prop
 -/
@@ -24,7 +22,7 @@ seal f
 error: type mismatch
   rfl
 has type
-  ?_ = ?_ : Prop
+  f x = f x : Prop
 but is expected to have type
   f x = x + 1 : Prop
 -/

tests/lean/run/wfirred.lean

@@ -2,8 +2,6 @@
 Tests that definitions by well-founded recursion are irreducible.
 -/
 
-set_option pp.mvars false
-
 def foo : Nat → Nat
   | 0 => 0
   | n+1 => foo n
@@ -13,7 +11,7 @@ termination_by n => n
 error: type mismatch
   rfl
 has type
-  ?_ = ?_ : Prop
+  foo 0 = foo 0 : Prop
 but is expected to have type
   foo 0 = 0 : Prop
 -/
@@ -24,7 +22,7 @@ example : foo 0 = 0 := rfl
 error: type mismatch
   rfl
 has type
-  ?_ = ?_ : Prop
+  foo (n + 1) = foo (n + 1) : Prop
 but is expected to have type
   foo (n + 1) = foo n : Prop
 -/
@@ -72,7 +70,7 @@ end Unsealed
 error: type mismatch
   rfl
 has type
-  ?_ = ?_ : Prop
+  foo 0 = foo 0 : Prop
 but is expected to have type
   foo 0 = 0 : Prop
 -/
@@ -91,7 +89,7 @@ termination_by n => n
 error: type mismatch
   rfl
 has type
-  ?_ = ?_ : Prop
+  foo = foo : Prop
 but is expected to have type
   foo = bar : Prop
 -/
@@ -116,7 +114,7 @@ seal baz in
 error: type mismatch
   rfl
 has type
-  ?_ = ?_ : Prop
+  baz 0 = baz 0 : Prop
 but is expected to have type
   baz 0 = 0 : Prop
 -/
@@ -138,7 +136,7 @@ seal quux in
 error: type mismatch
   rfl
 has type
-  ?_ = ?_ : Prop
+  quux 0 = quux 0 : Prop
 but is expected to have type
   quux 0 = 0 : Prop
 -/