fix: grind sort internalization

This PR ensures sorts are internalized by `grind`.

script/AnalyzeGrindAnnotations.lean

@@ -90,7 +90,7 @@ def analyzeEMatchTheorems (c : Config := {}) : MetaM Unit := do
 
 /-- Macro for analyzing E-match theorems with unlimited heartbeats -/
 macro "#analyzeEMatchTheorems" : command => `(
-  set_option maxHeartbeats 2_000_000 in
+  set_option maxHeartbeats 0 in
   run_meta analyzeEMatchTheorems
 )
 
@@ -101,55 +101,32 @@ set_option trace.grind.ematch.instance true
 
 -- 1. grind immediately sees `(#[] : Array α) = ([] : List α).toArray` but probably this should be hidden.
 -- 2. `Vector.toArray_empty` keys on `Array.mk []` rather than `#v[].toArray`
--- I guess we could add `(#[].extract _ _).extract _ _` as a global stop pattern,
--- or add `#[].extract _ _` as a forbidden subterm for `Array.extract_extract`.
+-- I guess we could add `(#[].extract _ _).extract _ _` as a stop pattern.
 run_meta analyzeEMatchTheorem ``Array.extract_empty {}
 
--- * Neither `Option.bind_some` nor `Option.bind_fun_some` fire, because the terms appear inside
---   lambdas. So we get crazy things like:
---   `fun x => ((some x).bind some).bind fun x => (some x).bind fun x => (some x).bind some`
--- * We could consider replacing `filterMap_filterMap` with
---   `filterMap g (filterMap f xs) = filterMap (f >=> g) xs`
---   to avoid the lambda that `grind` struggles with, but this would require more API around the fish.
--- * Alternatively, we could investigating splitting equivalence classes into "active" and "passive"
---   buckets, and e.g. when instantianting `filterMap_some : Array.filterMap some xs = xs`,
---   leave `Array.filterMap some xs` in the "passive" bucket.
---   We would use this for merging classes, but not instantiating.
+-- Neither `Option.bind_some` nor `Option.bind_fun_some` fire, because the terms appear inside
+-- lambdas. So we get crazy things like:
+-- `fun x => ((some x).bind some).bind fun x => (some x).bind fun x => (some x).bind some`
+-- We could consider replacing `filterMap_some` with
+-- `filterMap g (filterMap f xs) = filterMap (f >=> g) xs`
+-- to avoid the lambda that `grind` struggles with, but this would require more API around the fish.
 run_meta analyzeEMatchTheorem ``Array.filterMap_some {}
 
--- * It seems crazy to me that as soon as we have `0 >>> n = 0`, we instantiate based on the
---   pattern `0 >>> n >>> m` by substituting `0` into `0 >>> n` to produce the `0 >>> n >>> n`.
--- * We should add `0 >>> n` as a forbidden subterm for `Int.shiftRight_add`.
-run_meta analyzeEMatchTheorem ``Int.zero_shiftRight {}
-
--- * `eq_empty_of_append_eq_empty` was firing too often, before being removed in https://github.com/leanprover/lean4/pull/10162
---   Ideally we could instantiate this if we find `xs ++ ys` and `[]` in the same equivalence class,
---   not just as soon as we see `xs ++ ys`.
--- * `eq_nil_of_map_eq_nil` is similar.
--- * ban all the variants of `#[] ++ (_ ++ _)` for `Array.append_assoc`?
+-- Not entirely certain what is wrong here, but certainly
+-- `eq_empty_of_append_eq_empty` is firing too often.
+-- Ideally we could instantiate this is we fine `xs ++ ys` in the same equivalence class,
+-- note just as soon as we see `xs ++ ys`.
+-- I've tried removing this in https://github.com/leanprover/lean4/pull/10162
 run_meta analyzeEMatchTheorem ``Array.range'_succ {}
 
--- * also ban `a :: ([] ++ l)` etc for `List.cons_append`
--- * just ban `[] ++ l` for *everything* except `List.nil_append`?
---   effectively, just add this as a normalization rule?
+-- Perhaps the same story here.
 run_meta analyzeEMatchTheorem ``Array.range_succ {}
 
--- * forbid `modifyHead f (modifyHead g [])`
--- * actually just making sure that *only* modifyHead_nil acts on `modifyHead g []`
-run_meta analyzeEMatchTheorem ``List.eraseIdx_modifyHead_zero {}
+-- `zip_map_left` and `zip_map_right` are bad grind lemmas,
+-- checking if they can be removed in https://github.com/leanprover/lean4/pull/10163
+run_meta analyzeEMatchTheorem ``Array.zip_map {}
 
--- * forbid `(List.flatMap (List.reverse ∘ f) l).reverse` for `reverse_flatMap`
--- * forbid `List.flatMap (List.reverse ∘ f) l.reverse` for `flatMap_reverse`
-run_meta analyzeEMatchTheorem ``List.flatMap_reverse {}
-
--- * forbid `List.countP p (List.filter p l)` for `countP_eq_length_filter`
--- * this one is just crazy; so over-eager instantiation of unhelpful lemmas
--- I'm changing `countP_eq_length_filter` from `_=_` to `=` in https://github.com/leanprover/lean4/pull/10532
-run_meta analyzeEMatchTheorem ``List.getLast_filter {}
-
--- Another one: `modify_nil` is the only thing we should ever use on `[].modify i f`
-run_meta analyzeEMatchTheorem ``List.modify_nil {}
-
--- `count_eq_length_filter` (and related lemmas) shouldn't fire on lists that are already filters?
--- similarly for `List.filter_subset`?
-run_meta analyzeEMatchTheorem ``List.replicate_sublist_iff {}
+-- It seems crazy to me that as soon as we have `0 >>> n = 0`, we instantiate based on the
+-- pattern `0 >>> n >>> m` by substituting `0` into `0 >>> n` to produce the `0 >>> n >>> n`.
+-- I don't think any forbidden subterms can help us here. I don't know what to do. :-(
+run_meta analyzeEMatchTheorem ``Int.zero_shiftRight {}

src/Init/Data/Array/Attach.lean

@@ -95,16 +95,16 @@ well-founded recursion mechanism to prove that the function terminates.
   intro a m h₁ h₂
   congr
 
-@[simp] theorem pmap_empty {P : α → Prop} (f : ∀ a, P a → β) : pmap f #[] (by simp) = #[] := rfl
+@[simp, grind =] theorem pmap_empty {P : α → Prop} (f : ∀ a, P a → β) : pmap f #[] (by simp) = #[] := rfl
 
-@[simp] theorem pmap_push {P : α → Prop} (f : ∀ a, P a → β) (a : α) (xs : Array α) (h : ∀ b ∈ xs.push a, P b) :
+@[simp, grind =] theorem pmap_push {P : α → Prop} (f : ∀ a, P a → β) (a : α) (xs : Array α) (h : ∀ b ∈ xs.push a, P b) :
     pmap f (xs.push a) h =
       (pmap f xs (fun a m => by simp at h; exact h a (.inl m))).push (f a (h a (by simp))) := by
   simp [pmap]
 
-@[simp] theorem attach_empty : (#[] : Array α).attach = #[] := rfl
+@[simp, grind =] theorem attach_empty : (#[] : Array α).attach = #[] := rfl
 
-@[simp] theorem attachWith_empty {P : α → Prop} (H : ∀ x ∈ #[], P x) : (#[] : Array α).attachWith P H = #[] := rfl
+@[simp, grind =] theorem attachWith_empty {P : α → Prop} (H : ∀ x ∈ #[], P x) : (#[] : Array α).attachWith P H = #[] := rfl
 
 @[simp] theorem _root_.List.attachWith_mem_toArray {l : List α} :
     l.attachWith (fun x => x ∈ l.toArray) (fun x h => by simpa using h) =
@@ -125,11 +125,13 @@ theorem pmap_congr_left {p q : α → Prop} {f : ∀ a, p a → β} {g : ∀ a,
   simp only [List.pmap_toArray, mk.injEq]
   rw [List.pmap_congr_left _ h]
 
+@[grind =]
 theorem map_pmap {p : α → Prop} {g : β → γ} {f : ∀ a, p a → β} {xs : Array α} (H) :
     map g (pmap f xs H) = pmap (fun a h => g (f a h)) xs H := by
   cases xs
   simp [List.map_pmap]
 
+@[grind =]
 theorem pmap_map {p : β → Prop} {g : ∀ b, p b → γ} {f : α → β} {xs : Array α} (H) :
     pmap g (map f xs) H = pmap (fun a h => g (f a) h) xs fun _ h => H _ (mem_map_of_mem h) := by
   cases xs
@@ -145,14 +147,14 @@ theorem attachWith_congr {xs ys : Array α} (w : xs = ys) {P : α → Prop} {H :
   subst w
   simp
 
-@[simp] theorem attach_push {a : α} {xs : Array α} :
+@[simp, grind =] theorem attach_push {a : α} {xs : Array α} :
     (xs.push a).attach =
       (xs.attach.map (fun ⟨x, h⟩ => ⟨x, mem_push_of_mem a h⟩)).push ⟨a, by simp⟩ := by
   cases xs
   rw [attach_congr (List.push_toArray _ _)]
   simp [Function.comp_def]
 
-@[simp] theorem attachWith_push {a : α} {xs : Array α} {P : α → Prop} {H : ∀ x ∈ xs.push a, P x} :
+@[simp, grind =] theorem attachWith_push {a : α} {xs : Array α} {P : α → Prop} {H : ∀ x ∈ xs.push a, P x} :
     (xs.push a).attachWith P H =
       (xs.attachWith P (fun x h => by simp at H; exact H x (.inl h))).push ⟨a, H a (by simp)⟩ := by
   cases xs
@@ -174,6 +176,9 @@ theorem attach_map_val (xs : Array α) (f : α → β) :
   cases xs
   simp
 
+@[deprecated attach_map_val (since := "2025-02-17")]
+abbrev attach_map_coe := @attach_map_val
+
 -- The argument `xs : Array α` is explicit to allow rewriting from right to left.
 theorem attach_map_subtype_val (xs : Array α) : xs.attach.map Subtype.val = xs := by
   cases xs; simp
@@ -182,6 +187,9 @@ theorem attachWith_map_val {p : α → Prop} {f : α → β} {xs : Array α} (H
     ((xs.attachWith p H).map fun (i : { i // p i}) => f i) = xs.map f := by
   cases xs; simp
 
+@[deprecated attachWith_map_val (since := "2025-02-17")]
+abbrev attachWith_map_coe := @attachWith_map_val
+
 theorem attachWith_map_subtype_val {p : α → Prop} {xs : Array α} (H : ∀ a ∈ xs, p a) :
     (xs.attachWith p H).map Subtype.val = xs := by
   cases xs; simp
@@ -286,23 +294,25 @@ theorem getElem_attach {xs : Array α} {i : Nat} (h : i < xs.attach.size) :
     xs.attach[i] = ⟨xs[i]'(by simpa using h), getElem_mem (by simpa using h)⟩ :=
   getElem_attachWith h
 
-@[simp] theorem pmap_attach {xs : Array α} {p : {x // x ∈ xs} → Prop} {f : ∀ a, p a → β} (H) :
+@[simp, grind =] theorem pmap_attach {xs : Array α} {p : {x // x ∈ xs} → Prop} {f : ∀ a, p a → β} (H) :
     pmap f xs.attach H =
       xs.pmap (P := fun a => ∃ h : a ∈ xs, p ⟨a, h⟩)
         (fun a h => f ⟨a, h.1⟩ h.2) (fun a h => ⟨h, H ⟨a, h⟩ (by simp)⟩) := by
   ext <;> simp
 
-@[simp] theorem pmap_attachWith {xs : Array α} {p : {x // q x} → Prop} {f : ∀ a, p a → β} (H₁ H₂) :
+@[simp, grind =] theorem pmap_attachWith {xs : Array α} {p : {x // q x} → Prop} {f : ∀ a, p a → β} (H₁ H₂) :
     pmap f (xs.attachWith q H₁) H₂ =
       xs.pmap (P := fun a => ∃ h : q a, p ⟨a, h⟩)
         (fun a h => f ⟨a, h.1⟩ h.2) (fun a h => ⟨H₁ _ h, H₂ ⟨a, H₁ _ h⟩ (by simpa)⟩) := by
   ext <;> simp
 
+@[grind =]
 theorem foldl_pmap {xs : Array α} {P : α → Prop} {f : (a : α) → P a → β}
     (H : ∀ (a : α), a ∈ xs → P a) (g : γ → β → γ) (x : γ) :
     (xs.pmap f H).foldl g x = xs.attach.foldl (fun acc a => g acc (f a.1 (H _ a.2))) x := by
   rw [pmap_eq_map_attach, foldl_map]
 
+@[grind =]
 theorem foldr_pmap {xs : Array α} {P : α → Prop} {f : (a : α) → P a → β}
     (H : ∀ (a : α), a ∈ xs → P a) (g : β → γ → γ) (x : γ) :
     (xs.pmap f H).foldr g x = xs.attach.foldr (fun a acc => g (f a.1 (H _ a.2)) acc) x := by
@@ -360,18 +370,20 @@ theorem foldr_attach {xs : Array α} {f : α → β → β} {b : β} :
   ext
   simpa using fun a => List.mem_of_getElem? a
 
+@[grind =]
 theorem attach_map {xs : Array α} {f : α → β} :
     (xs.map f).attach = xs.attach.map (fun ⟨x, h⟩ => ⟨f x, mem_map_of_mem h⟩) := by
   cases xs
   ext <;> simp
 
+@[grind =]
 theorem attachWith_map {xs : Array α} {f : α → β} {P : β → Prop} (H : ∀ (b : β), b ∈ xs.map f → P b) :
     (xs.map f).attachWith P H = (xs.attachWith (P ∘ f) (fun _ h => H _ (mem_map_of_mem h))).map
       fun ⟨x, h⟩ => ⟨f x, h⟩ := by
   cases xs
   simp [List.attachWith_map]
 
-@[simp] theorem map_attachWith {xs : Array α} {P : α → Prop} {H : ∀ (a : α), a ∈ xs → P a}
+@[simp, grind =] theorem map_attachWith {xs : Array α} {P : α → Prop} {H : ∀ (a : α), a ∈ xs → P a}
     {f : { x // P x } → β} :
     (xs.attachWith P H).map f = xs.attach.map fun ⟨x, h⟩ => f ⟨x, H _ h⟩ := by
   cases xs <;> simp_all
@@ -389,6 +401,9 @@ theorem map_attach_eq_pmap {xs : Array α} {f : { x // x ∈ xs } → β} :
   cases xs
   ext <;> simp
 
+@[deprecated map_attach_eq_pmap (since := "2025-02-09")]
+abbrev map_attach := @map_attach_eq_pmap
+
 @[grind =]
 theorem attach_filterMap {xs : Array α} {f : α → Option β} :
     (xs.filterMap f).attach = xs.attach.filterMap
@@ -424,6 +439,7 @@ theorem filter_attachWith {q : α → Prop} {xs : Array α} {p : {x // q x} →
   cases xs
   simp [Function.comp_def, List.filter_map]
 
+@[grind =]
 theorem pmap_pmap {p : α → Prop} {q : β → Prop} {g : ∀ a, p a → β} {f : ∀ b, q b → γ} {xs} (H₁ H₂) :
     pmap f (pmap g xs H₁) H₂ =
       pmap (α := { x // x ∈ xs }) (fun a h => f (g a h) (H₂ (g a h) (mem_pmap_of_mem a.2))) xs.attach
@@ -431,7 +447,7 @@ theorem pmap_pmap {p : α → Prop} {q : β → Prop} {g : ∀ a, p a → β} {f
   cases xs
   simp [List.pmap_pmap, List.pmap_map]
 
-@[simp] theorem pmap_append {p : ι → Prop} {f : ∀ a : ι, p a → α} {xs ys : Array ι}
+@[simp, grind =] theorem pmap_append {p : ι → Prop} {f : ∀ a : ι, p a → α} {xs ys : Array ι}
     (h : ∀ a ∈ xs ++ ys, p a) :
     (xs ++ ys).pmap f h =
       (xs.pmap f fun a ha => h a (mem_append_left ys ha)) ++
@@ -446,7 +462,7 @@ theorem pmap_append' {p : α → Prop} {f : ∀ a : α, p a → β} {xs ys : Arr
       xs.pmap f h₁ ++ ys.pmap f h₂ :=
   pmap_append _
 
-@[simp] theorem attach_append {xs ys : Array α} :
+@[simp, grind =] theorem attach_append {xs ys : Array α} :
     (xs ++ ys).attach = xs.attach.map (fun ⟨x, h⟩ => ⟨x, mem_append_left ys h⟩) ++
       ys.attach.map fun ⟨x, h⟩ => ⟨x, mem_append_right xs h⟩ := by
   cases xs
@@ -454,59 +470,62 @@ theorem pmap_append' {p : α → Prop} {f : ∀ a : α, p a → β} {xs ys : Arr
   rw [attach_congr (List.append_toArray _ _)]
   simp [List.attach_append, Function.comp_def]
 
-@[simp] theorem attachWith_append {P : α → Prop} {xs ys : Array α}
+@[simp, grind =] theorem attachWith_append {P : α → Prop} {xs ys : Array α}
     {H : ∀ (a : α), a ∈ xs ++ ys → P a} :
     (xs ++ ys).attachWith P H = xs.attachWith P (fun a h => H a (mem_append_left ys h)) ++
       ys.attachWith P (fun a h => H a (mem_append_right xs h)) := by
   simp [attachWith]
 
-@[simp] theorem pmap_reverse {P : α → Prop} {f : (a : α) → P a → β} {xs : Array α}
+@[simp, grind =] theorem pmap_reverse {P : α → Prop} {f : (a : α) → P a → β} {xs : Array α}
     (H : ∀ (a : α), a ∈ xs.reverse → P a) :
     xs.reverse.pmap f H = (xs.pmap f (fun a h => H a (by simpa using h))).reverse := by
   induction xs <;> simp_all
 
+@[grind =]
 theorem reverse_pmap {P : α → Prop} {f : (a : α) → P a → β} {xs : Array α}
     (H : ∀ (a : α), a ∈ xs → P a) :
     (xs.pmap f H).reverse = xs.reverse.pmap f (fun a h => H a (by simpa using h)) := by
   rw [pmap_reverse]
 
-@[simp] theorem attachWith_reverse {P : α → Prop} {xs : Array α}
+@[simp, grind =] theorem attachWith_reverse {P : α → Prop} {xs : Array α}
     {H : ∀ (a : α), a ∈ xs.reverse → P a} :
     xs.reverse.attachWith P H =
       (xs.attachWith P (fun a h => H a (by simpa using h))).reverse := by
   cases xs
   simp
 
+@[grind =]
 theorem reverse_attachWith {P : α → Prop} {xs : Array α}
     {H : ∀ (a : α), a ∈ xs → P a} :
     (xs.attachWith P H).reverse = (xs.reverse.attachWith P (fun a h => H a (by simpa using h))) := by
   cases xs
   simp
 
-@[simp] theorem attach_reverse {xs : Array α} :
+@[simp, grind =] theorem attach_reverse {xs : Array α} :
     xs.reverse.attach = xs.attach.reverse.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
   cases xs
   rw [attach_congr List.reverse_toArray]
   simp
 
+@[grind =]
 theorem reverse_attach {xs : Array α} :
     xs.attach.reverse = xs.reverse.attach.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
   cases xs
   simp
 
-@[simp] theorem back?_pmap {P : α → Prop} {f : (a : α) → P a → β} {xs : Array α}
+@[simp, grind =] theorem back?_pmap {P : α → Prop} {f : (a : α) → P a → β} {xs : Array α}
     (H : ∀ (a : α), a ∈ xs → P a) :
     (xs.pmap f H).back? = xs.attach.back?.map fun ⟨a, m⟩ => f a (H a m) := by
   cases xs
   simp
 
-@[simp] theorem back?_attachWith {P : α → Prop} {xs : Array α}
+@[simp, grind =] theorem back?_attachWith {P : α → Prop} {xs : Array α}
     {H : ∀ (a : α), a ∈ xs → P a} :
     (xs.attachWith P H).back? = xs.back?.pbind (fun a h => some ⟨a, H _ (mem_of_back? h)⟩) := by
   cases xs
   simp
 
-@[simp]
+@[simp, grind =]
 theorem back?_attach {xs : Array α} :
     xs.attach.back? = xs.back?.pbind fun a h => some ⟨a, mem_of_back? h⟩ := by
   cases xs

src/Init/Data/Array/Basic.lean

@@ -129,11 +129,20 @@ end Array
 
 namespace List
 
+@[deprecated Array.toArray_toList (since := "2025-02-17")]
+abbrev toArray_toList := @Array.toArray_toList
+
 -- This does not need to be a simp lemma, as already after the `whnfR` the right hand side is `as`.
 theorem toList_toArray {as : List α} : as.toArray.toList = as := rfl
 
+@[deprecated toList_toArray (since := "2025-02-17")]
+abbrev _root_.Array.toList_toArray := @List.toList_toArray
+
 @[simp, grind =] theorem size_toArray {as : List α} : as.toArray.size = as.length := by simp [Array.size]
 
+@[deprecated size_toArray (since := "2025-02-17")]
+abbrev _root_.Array.size_toArray := @List.size_toArray
+
 @[simp, grind =] theorem getElem_toArray {xs : List α} {i : Nat} (h : i < xs.toArray.size) :
     xs.toArray[i] = xs[i]'(by simpa using h) := rfl
 
@@ -403,6 +412,10 @@ that requires a proof the array is non-empty.
 def back? (xs : Array α) : Option α :=
   xs[xs.size - 1]?
 
+@[deprecated "Use `a[i]?` instead." (since := "2025-02-12"), expose]
+def get? (xs : Array α) (i : Nat) : Option α :=
+  if h : i < xs.size then some xs[i] else none
+
 /--
 Swaps a new element with the element at the given index.
 
@@ -1799,6 +1812,7 @@ Examples:
 * `#["apple", "pear", "orange"].eraseIdxIfInBounds 3 = #["apple", "pear", "orange"]`
 * `#["apple", "pear", "orange"].eraseIdxIfInBounds 5 = #["apple", "pear", "orange"]`
 -/
+@[grind]
 def eraseIdxIfInBounds (xs : Array α) (i : Nat) : Array α :=
   if h : i < xs.size then xs.eraseIdx i h else xs
 

src/Init/Data/Array/Bootstrap.lean

@@ -24,6 +24,29 @@ set_option linter.indexVariables true -- Enforce naming conventions for index va
 
 namespace Array
 
+/--
+Use the indexing notation `a[i]` instead.
+
+Access an element from an array without needing a runtime bounds checks,
+using a `Nat` index and a proof that it is in bounds.
+
+This function does not use `get_elem_tactic` to automatically find the proof that
+the index is in bounds. This is because the tactic itself needs to look up values in
+arrays.
+-/
+@[deprecated "Use indexing notation `as[i]` instead" (since := "2025-02-17")]
+def get {α : Type u} (xs : @& Array α) (i : @& Nat) (h : LT.lt i xs.size) : α :=
+  xs.toList.get ⟨i, h⟩
+
+/--
+Use the indexing notation `a[i]!` instead.
+
+Access an element from an array, or panic if the index is out of bounds.
+-/
+@[deprecated "Use indexing notation `as[i]!` instead" (since := "2025-02-17"), expose]
+def get! {α : Type u} [Inhabited α] (xs : @& Array α) (i : @& Nat) : α :=
+  Array.getD xs i default
+
 theorem foldlM_toList.aux [Monad m]
     {f : β → α → m β} {xs : Array α} {i j} (H : xs.size ≤ i + j) {b} :
     foldlM.loop f xs xs.size (Nat.le_refl _) i j b = (xs.toList.drop j).foldlM f b := by
@@ -85,6 +108,9 @@ abbrev push_toList := @toList_push
 
 @[simp, grind =] theorem toList_pop {xs : Array α} : xs.pop.toList = xs.toList.dropLast := rfl
 
+@[deprecated toList_pop (since := "2025-02-17")]
+abbrev pop_toList := @Array.toList_pop
+
 @[simp] theorem append_eq_append {xs ys : Array α} : xs.append ys = xs ++ ys := rfl
 
 @[simp, grind =] theorem toList_append {xs ys : Array α} :

src/Init/Data/Array/Erase.lean

@@ -324,13 +324,6 @@ abbrev erase_mkArray_ne := @erase_replicate_ne
 
 end erase
 
-/-! ### eraseIdxIfInBounds -/
-
-@[grind =]
-theorem eraseIdxIfInBounds_eq {xs : Array α} {i : Nat} :
-    xs.eraseIdxIfInBounds i = if h : i < xs.size then xs.eraseIdx i else xs := by
-  simp [eraseIdxIfInBounds]
-
 /-! ### eraseIdx -/
 
 theorem eraseIdx_eq_eraseIdxIfInBounds {xs : Array α} {i : Nat} (h : i < xs.size) :

src/Init/Data/Array/Find.lean

@@ -278,6 +278,9 @@ theorem find?_flatten_eq_none_iff {xss : Array (Array α)} {p : α → Bool} :
     xss.flatten.find? p = none ↔ ∀ ys ∈ xss, ∀ x ∈ ys, !p x := by
   simp
 
+@[deprecated find?_flatten_eq_none_iff (since := "2025-02-03")]
+abbrev find?_flatten_eq_none := @find?_flatten_eq_none_iff
+
 /--
 If `find? p` returns `some a` from `xs.flatten`, then `p a` holds, and
 some array in `xs` contains `a`, and no earlier element of that array satisfies `p`.
@@ -303,6 +306,9 @@ theorem find?_flatten_eq_some_iff {xss : Array (Array α)} {p : α → Bool} {a
       ⟨zs.toList, bs.toList.map Array.toList, by simpa using h⟩,
         by simpa using h₁, by simpa using h₂⟩
 
+@[deprecated find?_flatten_eq_some_iff (since := "2025-02-03")]
+abbrev find?_flatten_eq_some := @find?_flatten_eq_some_iff
+
 @[simp, grind =] theorem find?_flatMap {xs : Array α} {f : α → Array β} {p : β → Bool} :
     (xs.flatMap f).find? p = xs.findSome? (fun x => (f x).find? p) := by
   cases xs
@@ -312,11 +318,17 @@ theorem find?_flatMap_eq_none_iff {xs : Array α} {f : α → Array β} {p : β
     (xs.flatMap f).find? p = none ↔ ∀ x ∈ xs, ∀ y ∈ f x, !p y := by
   simp
 
+@[deprecated find?_flatMap_eq_none_iff (since := "2025-02-03")]
+abbrev find?_flatMap_eq_none := @find?_flatMap_eq_none_iff
+
 @[grind =]
 theorem find?_replicate :
     find? p (replicate n a) = if n = 0 then none else if p a then some a else none := by
   simp [← List.toArray_replicate, List.find?_replicate]
 
+@[deprecated find?_replicate (since := "2025-03-18")]
+abbrev find?_mkArray := @find?_replicate
+
 @[simp] theorem find?_replicate_of_size_pos (h : 0 < n) :
     find? p (replicate n a) = if p a then some a else none := by
   simp [find?_replicate, Nat.ne_of_gt h]
@@ -334,19 +346,34 @@ abbrev find?_mkArray_of_pos := @find?_replicate_of_pos
 @[simp] theorem find?_replicate_of_neg (h : ¬ p a) : find? p (replicate n a) = none := by
   simp [find?_replicate, h]
 
+@[deprecated find?_replicate_of_neg (since := "2025-03-18")]
+abbrev find?_mkArray_of_neg := @find?_replicate_of_neg
+
 -- This isn't a `@[simp]` lemma since there is already a lemma for `l.find? p = none` for any `l`.
 theorem find?_replicate_eq_none_iff {n : Nat} {a : α} {p : α → Bool} :
     (replicate n a).find? p = none ↔ n = 0 ∨ !p a := by
   simp [← List.toArray_replicate, Classical.or_iff_not_imp_left]
 
+@[deprecated find?_replicate_eq_none_iff (since := "2025-03-18")]
+abbrev find?_mkArray_eq_none_iff := @find?_replicate_eq_none_iff
+
 @[simp] theorem find?_replicate_eq_some_iff {n : Nat} {a b : α} {p : α → Bool} :
     (replicate n a).find? p = some b ↔ n ≠ 0 ∧ p a ∧ a = b := by
   simp [← List.toArray_replicate]
 
+@[deprecated find?_replicate_eq_some_iff (since := "2025-03-18")]
+abbrev find?_mkArray_eq_some_iff := @find?_replicate_eq_some_iff
+
+@[deprecated find?_replicate_eq_some_iff (since := "2025-02-03")]
+abbrev find?_mkArray_eq_some := @find?_replicate_eq_some_iff
+
 @[simp] theorem get_find?_replicate {n : Nat} {a : α} {p : α → Bool} (h) :
     ((replicate n a).find? p).get h = a := by
   simp [← List.toArray_replicate]
 
+@[deprecated get_find?_replicate (since := "2025-03-18")]
+abbrev get_find?_mkArray := @get_find?_replicate
+
 @[grind =]
 theorem find?_pmap {P : α → Prop} {f : (a : α) → P a → β} {xs : Array α}
     (H : ∀ (a : α), a ∈ xs → P a) {p : β → Bool} :

src/Init/Data/Array/Lemmas.lean

@@ -80,6 +80,9 @@ theorem ne_empty_of_size_pos (h : 0 < xs.size) : xs ≠ #[] := by
 @[simp] theorem size_eq_zero_iff : xs.size = 0 ↔ xs = #[] :=
   ⟨eq_empty_of_size_eq_zero, fun h => h ▸ rfl⟩
 
+@[deprecated size_eq_zero_iff (since := "2025-02-24")]
+abbrev size_eq_zero := @size_eq_zero_iff
+
 theorem eq_empty_iff_size_eq_zero : xs = #[] ↔ xs.size = 0 :=
   size_eq_zero_iff.symm
 
@@ -104,10 +107,17 @@ theorem exists_mem_of_size_eq_add_one {xs : Array α} (h : xs.size = n + 1) :
 theorem size_pos_iff {xs : Array α} : 0 < xs.size ↔ xs ≠ #[] :=
   Nat.pos_iff_ne_zero.trans (not_congr size_eq_zero_iff)
 
+@[deprecated size_pos_iff (since := "2025-02-24")]
+abbrev size_pos := @size_pos_iff
+
 theorem size_eq_one_iff {xs : Array α} : xs.size = 1 ↔ ∃ a, xs = #[a] := by
   cases xs
   simpa using List.length_eq_one_iff
 
+@[deprecated size_eq_one_iff (since := "2025-02-24")]
+abbrev size_eq_one := @size_eq_one_iff
+
+
 /-! ## L[i] and L[i]? -/
 
 theorem getElem?_eq_none_iff {xs : Array α} : xs[i]? = none ↔ xs.size ≤ i := by
@@ -361,7 +371,6 @@ abbrev getElem?_mkArray := @getElem?_replicate
 
 /-! ### mem -/
 
-@[grind ←]
 theorem not_mem_empty (a : α) : ¬ a ∈ #[] := by simp
 
 @[simp, grind =] theorem mem_push {xs : Array α} {x y : α} : x ∈ xs.push y ↔ x ∈ xs ∨ x = y := by
@@ -533,12 +542,18 @@ theorem isEmpty_eq_false_iff_exists_mem {xs : Array α} :
 @[simp] theorem isEmpty_iff {xs : Array α} : xs.isEmpty ↔ xs = #[] := by
   cases xs <;> simp
 
+@[deprecated isEmpty_iff (since := "2025-02-17")]
+abbrev isEmpty_eq_true := @isEmpty_iff
+
 @[grind →]
 theorem empty_of_isEmpty {xs : Array α} (h : xs.isEmpty) : xs = #[] := Array.isEmpty_iff.mp h
 
 @[simp] theorem isEmpty_eq_false_iff {xs : Array α} : xs.isEmpty = false ↔ xs ≠ #[] := by
   cases xs <;> simp
 
+@[deprecated isEmpty_eq_false_iff (since := "2025-02-17")]
+abbrev isEmpty_eq_false := @isEmpty_eq_false_iff
+
 theorem isEmpty_iff_size_eq_zero {xs : Array α} : xs.isEmpty ↔ xs.size = 0 := by
   rw [isEmpty_iff, size_eq_zero_iff]
 
@@ -2981,6 +2996,11 @@ theorem _root_.List.toArray_drop {l : List α} {k : Nat} :
     (l.drop k).toArray = l.toArray.extract k := by
   rw [List.drop_eq_extract, List.extract_toArray, List.size_toArray]
 
+@[deprecated extract_size (since := "2025-02-27")]
+theorem take_size {xs : Array α} : xs.take xs.size = xs := by
+  cases xs
+  simp
+
 /-! ### shrink -/
 
 @[simp] private theorem size_shrink_loop {xs : Array α} {n : Nat} : (shrink.loop n xs).size = xs.size - n := by
@@ -3566,6 +3586,8 @@ theorem foldr_eq_foldl_reverse {xs : Array α} {f : α → β → β} {b} :
   subst w
   rw [foldr_eq_foldl_reverse, foldl_push_eq_append rfl, map_reverse]
 
+@[deprecated foldr_push_eq_append (since := "2025-02-09")] abbrev foldr_flip_push_eq_append := @foldr_push_eq_append
+
 theorem foldl_assoc {op : α → α → α} [ha : Std.Associative op] {xs : Array α} {a₁ a₂} :
      xs.foldl op (op a₁ a₂) = op a₁ (xs.foldl op a₂) := by
   rcases xs with ⟨l⟩
@@ -4690,3 +4712,44 @@ namespace List
       simp_all
 
 end List
+
+/-! ### Deprecations -/
+namespace Array
+
+set_option linter.deprecated false in
+@[deprecated "`get?` is deprecated" (since := "2025-02-12"), simp]
+theorem get?_eq_getElem? (xs : Array α) (i : Nat) : xs.get? i = xs[i]? := rfl
+
+@[deprecated getD_eq_getD_getElem? (since := "2025-02-12")] abbrev getD_eq_get? := @getD_eq_getD_getElem?
+
+set_option linter.deprecated false in
+@[deprecated getElem!_eq_getD (since := "2025-02-12")]
+theorem get!_eq_getD [Inhabited α] (xs : Array α) : xs.get! n = xs.getD n default := rfl
+
+set_option linter.deprecated false in
+@[deprecated "Use `a[i]!` instead of `a.get! i`." (since := "2025-02-12")]
+theorem get!_eq_getD_getElem? [Inhabited α] (xs : Array α) (i : Nat) :
+    xs.get! i = xs[i]?.getD default := by
+  by_cases p : i < xs.size <;>
+  simp [get!, getD_eq_getD_getElem?, p]
+
+set_option linter.deprecated false in
+@[deprecated get!_eq_getD_getElem? (since := "2025-02-12")] abbrev get!_eq_getElem? := @get!_eq_getD_getElem?
+
+set_option linter.deprecated false in
+@[deprecated "`Array.get?` is deprecated, use `a[i]?` instead." (since := "2025-02-12")]
+theorem get?_eq_get?_toList (xs : Array α) (i : Nat) : xs.get? i = xs.toList.get? i := by
+  simp [← getElem?_toList]
+
+set_option linter.deprecated false in
+@[deprecated get!_eq_getD_getElem? (since := "2025-02-12")] abbrev get!_eq_get? := @get!_eq_getD_getElem?
+
+/-! ### set -/
+
+@[deprecated getElem?_set_self (since := "2025-02-27")] abbrev get?_set_eq := @getElem?_set_self
+@[deprecated getElem?_set_ne (since := "2025-02-27")] abbrev get?_set_ne := @getElem?_set_ne
+@[deprecated getElem?_set (since := "2025-02-27")] abbrev get?_set := @getElem?_set
+@[deprecated get_set (since := "2025-02-27")] abbrev get_set := @getElem_set
+@[deprecated get_set_ne (since := "2025-02-27")] abbrev get_set_ne := @getElem_set_ne
+
+end Array

src/Init/Data/Array/Lex/Basic.lean

@@ -9,8 +9,8 @@ prelude
 public import Init.Core
 import Init.Data.Array.Basic
 import Init.Data.Nat.Lemmas
-public import Init.Data.Range.Polymorphic.Iterators
-public import Init.Data.Range.Polymorphic.Nat
+import Init.Data.Range.Polymorphic.Iterators
+import Init.Data.Range.Polymorphic.Nat
 import Init.Data.Iterators.Consumers
 
 public section

src/Init/Data/Array/Subarray.lean

@@ -7,7 +7,6 @@ module
 
 prelude
 public import Init.GetElem
-public import Init.Data.Array.Basic
 import Init.Data.Array.GetLit
 public import Init.Data.Slice.Basic
 

src/Init/Data/BitVec/Basic.lean

@@ -29,6 +29,10 @@ set_option linter.missingDocs true
 
 namespace BitVec
 
+@[inline, deprecated BitVec.ofNatLT (since := "2025-02-13"), inherit_doc BitVec.ofNatLT]
+protected def ofNatLt {n : Nat} (i : Nat) (p : i < 2 ^ n) : BitVec n :=
+  BitVec.ofNatLT i p
+
 section Nat
 
 /--

src/Init/Data/BitVec/Lemmas.lean

@@ -74,6 +74,10 @@ theorem some_eq_getElem?_iff {l : BitVec w} : some a = l[n]? ↔ ∃ h : n < w,
 theorem getElem_of_getElem? {l : BitVec w} : l[n]? = some a → ∃ h : n < w, l[n] = a :=
   getElem?_eq_some_iff.mp
 
+set_option linter.missingDocs false in
+@[deprecated getElem?_eq_some_iff (since := "2025-02-17")]
+abbrev getElem?_eq_some := @getElem?_eq_some_iff
+
 theorem getElem?_eq_none_iff {l : BitVec w} : l[n]? = none ↔ w ≤ n := by
   simp
 
@@ -346,14 +350,25 @@ theorem ofBool_eq_iff_eq : ∀ {b b' : Bool}, BitVec.ofBool b = BitVec.ofBool b'
 @[simp] theorem ofBool_xor_ofBool : ofBool b ^^^ ofBool b' = ofBool (b ^^ b') := by
   cases b <;> cases b' <;> rfl
 
+@[deprecated toNat_ofNatLT (since := "2025-02-13")]
+theorem toNat_ofNatLt (x : Nat) (p : x < 2^w) : (x#'p).toNat = x := rfl
+
 @[simp, grind =] theorem getLsbD_ofNatLT {n : Nat} (x : Nat) (lt : x < 2^n) (i : Nat) :
   getLsbD (x#'lt) i = x.testBit i := by
   simp [getLsbD, BitVec.ofNatLT]
 
+@[deprecated getLsbD_ofNatLT (since := "2025-02-13")]
+theorem getLsbD_ofNatLt {n : Nat} (x : Nat) (lt : x < 2^n) (i : Nat) :
+  getLsbD (x#'lt) i = x.testBit i := getLsbD_ofNatLT x lt i
+
 @[simp, grind =] theorem getMsbD_ofNatLT {n x i : Nat} (h : x < 2^n) :
     getMsbD (x#'h) i = (decide (i < n) && x.testBit (n - 1 - i)) := by
   simp [getMsbD, getLsbD]
 
+@[deprecated getMsbD_ofNatLT (since := "2025-02-13")]
+theorem getMsbD_ofNatLt {n x i : Nat} (h : x < 2^n) :
+    getMsbD (x#'h) i = (decide (i < n) && x.testBit (n - 1 - i)) := getMsbD_ofNatLT h
+
 @[grind =]
 theorem ofNatLT_eq_ofNat {w : Nat} {n : Nat} (hn) : BitVec.ofNatLT n hn = BitVec.ofNat w n :=
   eq_of_toNat_eq (by simp [Nat.mod_eq_of_lt hn])
@@ -6346,4 +6361,15 @@ theorem two_pow_ctz_le_toNat_of_ne_zero {x : BitVec w} (hx : x ≠ 0#w) :
   have hclz := getLsbD_true_ctz_of_ne_zero (x := x) hx
   exact Nat.ge_two_pow_of_testBit hclz
 
+/-! ### Deprecations -/
+
+set_option linter.missingDocs false
+
+@[deprecated toFin_uShiftRight (since := "2025-02-18")]
+abbrev toFin_uShiftRight := @toFin_ushiftRight
+
+
+
+
+
 end BitVec

src/Init/Data/ByteArray/Lemmas.lean

@@ -11,13 +11,6 @@ public import Init.Data.Array.Extract
 
 public section
 
--- At present the preferred normal form for empty byte arrays is `ByteArray.empty`
-@[simp]
-theorem emptyc_eq_empty : (∅ : ByteArray) = ByteArray.empty := rfl
-
-@[simp]
-theorem emptyWithCapacity_eq_empty : ByteArray.emptyWithCapacity 0 = ByteArray.empty := rfl
-
 @[simp]
 theorem ByteArray.data_empty : ByteArray.empty.data = #[] := rfl
 

src/Init/Data/Int/DivMod/Bootstrap.lean

@@ -206,6 +206,9 @@ theorem ediv_nonneg_iff_of_pos {a b : Int} (h : 0 < b) : 0 ≤ a / b ↔ 0 ≤ a
   | Int.ofNat (b+1), _ =>
     rcases a with ⟨a⟩ <;> simp [Int.ediv, -natCast_ediv]
 
+@[deprecated ediv_nonneg_iff_of_pos (since := "2025-02-28")]
+abbrev div_nonneg_iff_of_pos := @ediv_nonneg_iff_of_pos
+
 /-! ### emod -/
 
 theorem emod_nonneg : ∀ (a : Int) {b : Int}, b ≠ 0 → 0 ≤ a % b

src/Init/Data/Int/Order.lean

@@ -1347,6 +1347,8 @@ theorem neg_of_sign_eq_neg_one : ∀ {a : Int}, sign a = -1 → a < 0
   | 0 => Int.mul_zero _
   | -[_+1] => Int.mul_neg_one _
 
+@[deprecated mul_sign_self (since := "2025-02-24")] abbrev mul_sign := @mul_sign_self
+
 @[simp] theorem sign_mul_self (i : Int) : sign i * i = natAbs i := by
   rw [Int.mul_comm, mul_sign_self]
 

src/Init/Data/Int/Pow.lean

@@ -50,9 +50,14 @@ protected theorem pow_ne_zero {n : Int} {m : Nat} : n ≠ 0 → n ^ m ≠ 0 := b
 
 instance {n : Int} {m : Nat} [NeZero n] : NeZero (n ^ m) := ⟨Int.pow_ne_zero (NeZero.ne _)⟩
 
--- This can't be removed until the next update-stage0
+@[deprecated Nat.pow_le_pow_left (since := "2025-02-17")]
+abbrev pow_le_pow_of_le_left := @Nat.pow_le_pow_left
+
+@[deprecated Nat.pow_le_pow_right (since := "2025-02-17")]
+abbrev pow_le_pow_of_le_right := @Nat.pow_le_pow_right
+
 @[deprecated Nat.pow_pos (since := "2025-02-17")]
-abbrev _root_.Nat.pos_pow_of_pos := @Nat.pow_pos
+abbrev pos_pow_of_pos := @Nat.pow_pos
 
 @[simp, norm_cast]
 protected theorem natCast_pow (b n : Nat) : ((b^n : Nat) : Int) = (b : Int) ^ n := by

src/Init/Data/List/Attach.lean

@@ -95,12 +95,14 @@ theorem pmap_congr_left {p q : α → Prop} {f : ∀ a, p a → β} {g : ∀ a,
   | cons x l ih =>
     rw [pmap, pmap, h _ mem_cons_self, ih fun a ha => h a (mem_cons_of_mem _ ha)]
 
+@[grind =]
 theorem map_pmap {p : α → Prop} {g : β → γ} {f : ∀ a, p a → β} {l : List α} (H) :
     map g (pmap f l H) = pmap (fun a h => g (f a h)) l H := by
   induction l
   · rfl
   · simp only [*, pmap, map]
 
+@[grind =]
 theorem pmap_map {p : β → Prop} {g : ∀ b, p b → γ} {f : α → β} {l : List α} (H) :
     pmap g (map f l) H = pmap (fun a h => g (f a) h) l fun _ h => H _ (mem_map_of_mem h) := by
   induction l
@@ -147,6 +149,9 @@ theorem attach_map_val {l : List α} {f : α → β} :
     (l.attach.map fun (i : {i // i ∈ l}) => f i) = l.map f := by
   rw [attach, attachWith, map_pmap]; exact pmap_eq_map _
 
+@[deprecated attach_map_val (since := "2025-02-17")]
+abbrev attach_map_coe := @attach_map_val
+
 -- The argument `l : List α` is explicit to allow rewriting from right to left.
 theorem attach_map_subtype_val (l : List α) : l.attach.map Subtype.val = l :=
   attach_map_val.trans (List.map_id _)
@@ -155,6 +160,9 @@ theorem attachWith_map_val {p : α → Prop} {f : α → β} {l : List α} (H :
     ((l.attachWith p H).map fun (i : { i // p i}) => f i) = l.map f := by
   rw [attachWith, map_pmap]; exact pmap_eq_map _
 
+@[deprecated attachWith_map_val (since := "2025-02-17")]
+abbrev attachWith_map_coe := @attachWith_map_val
+
 theorem attachWith_map_subtype_val {p : α → Prop} {l : List α} (H : ∀ a ∈ l, p a) :
     (l.attachWith p H).map Subtype.val = l :=
   (attachWith_map_val _).trans (List.map_id _)
@@ -246,6 +254,13 @@ theorem getElem?_pmap {p : α → Prop} {f : ∀ a, p a → β} {l : List α} (h
     · simp
     · simp only [pmap, getElem?_cons_succ, hl]
 
+set_option linter.deprecated false in
+@[deprecated List.getElem?_pmap (since := "2025-02-12")]
+theorem get?_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h : ∀ a ∈ l, p a) (n : Nat) :
+    get? (pmap f l h) n = Option.pmap f (get? l n) fun x H => h x (mem_of_get? H) := by
+  simp only [get?_eq_getElem?]
+  simp [getElem?_pmap]
+
 -- The argument `f` is explicit to allow rewriting from right to left.
 @[simp, grind =]
 theorem getElem_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h : ∀ a ∈ l, p a) {i : Nat}
@@ -262,6 +277,15 @@ theorem getElem_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h
     · simp
     · simp [hl]
 
+@[deprecated getElem_pmap (since := "2025-02-13")]
+theorem get_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h : ∀ a ∈ l, p a) {n : Nat}
+    (hn : n < (pmap f l h).length) :
+    get (pmap f l h) ⟨n, hn⟩ =
+      f (get l ⟨n, @length_pmap _ _ p f l h ▸ hn⟩)
+        (h _ (getElem_mem (@length_pmap _ _ p f l h ▸ hn))) := by
+  simp only [get_eq_getElem]
+  simp [getElem_pmap]
+
 @[simp, grind =]
 theorem getElem?_attachWith {xs : List α} {i : Nat} {P : α → Prop} {H : ∀ a ∈ xs, P a} :
     (xs.attachWith P H)[i]? = xs[i]?.pmap Subtype.mk (fun _ a => H _ (mem_of_getElem? a)) :=
@@ -283,13 +307,13 @@ theorem getElem_attach {xs : List α} {i : Nat} (h : i < xs.attach.length) :
     xs.attach[i] = ⟨xs[i]'(by simpa using h), getElem_mem (by simpa using h)⟩ :=
   getElem_attachWith h
 
-@[simp] theorem pmap_attach {l : List α} {p : {x // x ∈ l} → Prop} {f : ∀ a, p a → β} (H) :
+@[simp, grind =] theorem pmap_attach {l : List α} {p : {x // x ∈ l} → Prop} {f : ∀ a, p a → β} (H) :
     pmap f l.attach H =
       l.pmap (P := fun a => ∃ h : a ∈ l, p ⟨a, h⟩)
         (fun a h => f ⟨a, h.1⟩ h.2) (fun a h => ⟨h, H ⟨a, h⟩ (by simp)⟩) := by
   apply ext_getElem <;> simp
 
-@[simp] theorem pmap_attachWith {l : List α} {p : {x // q x} → Prop} {f : ∀ a, p a → β} (H₁ H₂) :
+@[simp, grind =] theorem pmap_attachWith {l : List α} {p : {x // q x} → Prop} {f : ∀ a, p a → β} (H₁ H₂) :
     pmap f (l.attachWith q H₁) H₂ =
       l.pmap (P := fun a => ∃ h : q a, p ⟨a, h⟩)
         (fun a h => f ⟨a, h.1⟩ h.2) (fun a h => ⟨H₁ _ h, H₂ ⟨a, H₁ _ h⟩ (by simpa)⟩) := by
@@ -347,24 +371,26 @@ theorem getElem_attach {xs : List α} {i : Nat} (h : i < xs.attach.length) :
     xs.attach.tail = xs.tail.attach.map (fun ⟨x, h⟩ => ⟨x, mem_of_mem_tail h⟩) := by
   cases xs <;> simp
 
+@[grind =]
 theorem foldl_pmap {l : List α} {P : α → Prop} {f : (a : α) → P a → β}
     (H : ∀ (a : α), a ∈ l → P a) (g : γ → β → γ) (x : γ) :
     (l.pmap f H).foldl g x = l.attach.foldl (fun acc a => g acc (f a.1 (H _ a.2))) x := by
   rw [pmap_eq_map_attach, foldl_map]
 
+@[grind =]
 theorem foldr_pmap {l : List α} {P : α → Prop} {f : (a : α) → P a → β}
     (H : ∀ (a : α), a ∈ l → P a) (g : β → γ → γ) (x : γ) :
     (l.pmap f H).foldr g x = l.attach.foldr (fun a acc => g (f a.1 (H _ a.2)) acc) x := by
   rw [pmap_eq_map_attach, foldr_map]
 
-@[simp] theorem foldl_attachWith
+@[simp, grind =] theorem foldl_attachWith
     {l : List α} {q : α → Prop} (H : ∀ a, a ∈ l → q a) {f : β → { x // q x } → β} {b} :
     (l.attachWith q H).foldl f b = l.attach.foldl (fun b ⟨a, h⟩ => f b ⟨a, H _ h⟩) b := by
   induction l generalizing b with
   | nil => simp
   | cons a l ih => simp [ih, foldl_map]
 
-@[simp] theorem foldr_attachWith
+@[simp, grind =] theorem foldr_attachWith
     {l : List α} {q : α → Prop} (H : ∀ a, a ∈ l → q a) {f : { x // q x } → β → β} {b} :
     (l.attachWith q H).foldr f b = l.attach.foldr (fun a acc => f ⟨a.1, H _ a.2⟩ acc) b := by
   induction l generalizing b with
@@ -403,16 +429,18 @@ theorem foldr_attach {l : List α} {f : α → β → β} {b : β} :
   | nil => simp
   | cons a l ih => rw [foldr_cons, attach_cons, foldr_cons, foldr_map, ih]
 
+@[grind =]
 theorem attach_map {l : List α} {f : α → β} :
     (l.map f).attach = l.attach.map (fun ⟨x, h⟩ => ⟨f x, mem_map_of_mem h⟩) := by
   induction l <;> simp [*]
 
+@[grind =]
 theorem attachWith_map {l : List α} {f : α → β} {P : β → Prop} (H : ∀ (b : β), b ∈ l.map f → P b) :
     (l.map f).attachWith P H = (l.attachWith (P ∘ f) (fun _ h => H _ (mem_map_of_mem h))).map
       fun ⟨x, h⟩ => ⟨f x, h⟩ := by
   induction l <;> simp [*]
 
-@[simp] theorem map_attachWith {l : List α} {P : α → Prop} {H : ∀ (a : α), a ∈ l → P a}
+@[simp, grind =] theorem map_attachWith {l : List α} {P : α → Prop} {H : ∀ (a : α), a ∈ l → P a}
     {f : { x // P x } → β} :
     (l.attachWith P H).map f = l.attach.map fun ⟨x, h⟩ => f ⟨x, H _ h⟩ := by
   induction l <;> simp_all
@@ -438,6 +466,10 @@ theorem map_attach_eq_pmap {l : List α} {f : { x // x ∈ l } → β} :
     apply pmap_congr_left
     simp
 
+@[deprecated map_attach_eq_pmap (since := "2025-02-09")]
+abbrev map_attach := @map_attach_eq_pmap
+
+@[grind =]
 theorem attach_filterMap {l : List α} {f : α → Option β} :
     (l.filterMap f).attach = l.attach.filterMap
       fun ⟨x, h⟩ => (f x).pbind (fun b m => some ⟨b, mem_filterMap.mpr ⟨x, h, m⟩⟩) := by
@@ -468,6 +500,7 @@ theorem attach_filterMap {l : List α} {f : α → Option β} :
       ext
       simp
 
+@[grind =]
 theorem attach_filter {l : List α} (p : α → Bool) :
     (l.filter p).attach = l.attach.filterMap
       fun x => if w : p x.1 then some ⟨x.1, mem_filter.mpr ⟨x.2, w⟩⟩ else none := by
@@ -479,7 +512,7 @@ theorem attach_filter {l : List α} (p : α → Bool) :
 
 -- We are still missing here `attachWith_filterMap` and `attachWith_filter`.
 
-@[simp]
+@[simp, grind =]
 theorem filterMap_attachWith {q : α → Prop} {l : List α} {f : {x // q x} → Option β} (H) :
     (l.attachWith q H).filterMap f = l.attach.filterMap (fun ⟨x, h⟩ => f ⟨x, H _ h⟩) := by
   induction l with
@@ -488,7 +521,7 @@ theorem filterMap_attachWith {q : α → Prop} {l : List α} {f : {x // q x} →
     simp only [attachWith_cons, filterMap_cons]
     split <;> simp_all [Function.comp_def]
 
-@[simp]
+@[simp, grind =]
 theorem filter_attachWith {q : α → Prop} {l : List α} {p : {x // q x} → Bool} (H) :
     (l.attachWith q H).filter p =
       (l.attach.filter (fun ⟨x, h⟩ => p ⟨x, H _ h⟩)).map (fun ⟨x, h⟩ => ⟨x, H _ h⟩) := by
@@ -498,13 +531,14 @@ theorem filter_attachWith {q : α → Prop} {l : List α} {p : {x // q x} → Bo
     simp only [attachWith_cons, filter_cons]
     split <;> simp_all [Function.comp_def, filter_map]
 
+@[grind =]
 theorem pmap_pmap {p : α → Prop} {q : β → Prop} {g : ∀ a, p a → β} {f : ∀ b, q b → γ} {l} (H₁ H₂) :
     pmap f (pmap g l H₁) H₂ =
       pmap (α := { x // x ∈ l }) (fun a h => f (g a h) (H₂ (g a h) (mem_pmap_of_mem a.2))) l.attach
         (fun a _ => H₁ a a.2) := by
   simp [pmap_eq_map_attach, attach_map]
 
-@[simp] theorem pmap_append {p : ι → Prop} {f : ∀ a : ι, p a → α} {l₁ l₂ : List ι}
+@[simp, grind =] theorem pmap_append {p : ι → Prop} {f : ∀ a : ι, p a → α} {l₁ l₂ : List ι}
     (h : ∀ a ∈ l₁ ++ l₂, p a) :
     (l₁ ++ l₂).pmap f h =
       (l₁.pmap f fun a ha => h a (mem_append_left l₂ ha)) ++
@@ -521,47 +555,50 @@ theorem pmap_append' {p : α → Prop} {f : ∀ a : α, p a → β} {l₁ l₂ :
       l₁.pmap f h₁ ++ l₂.pmap f h₂ :=
   pmap_append _
 
-@[simp] theorem attach_append {xs ys : List α} :
+@[simp, grind =] theorem attach_append {xs ys : List α} :
     (xs ++ ys).attach = xs.attach.map (fun ⟨x, h⟩ => ⟨x, mem_append_left ys h⟩) ++
       ys.attach.map fun ⟨x, h⟩ => ⟨x, mem_append_right xs h⟩ := by
   simp only [attach, attachWith, map_pmap, pmap_append]
   congr 1 <;>
   exact pmap_congr_left _ fun _ _ _ _ => rfl
 
-@[simp] theorem attachWith_append {P : α → Prop} {xs ys : List α}
+@[simp, grind =] theorem attachWith_append {P : α → Prop} {xs ys : List α}
     {H : ∀ (a : α), a ∈ xs ++ ys → P a} :
     (xs ++ ys).attachWith P H = xs.attachWith P (fun a h => H a (mem_append_left ys h)) ++
       ys.attachWith P (fun a h => H a (mem_append_right xs h)) := by
   simp only [attachWith, pmap_append]
 
-@[simp] theorem pmap_reverse {P : α → Prop} {f : (a : α) → P a → β} {xs : List α}
+@[simp, grind =] theorem pmap_reverse {P : α → Prop} {f : (a : α) → P a → β} {xs : List α}
     (H : ∀ (a : α), a ∈ xs.reverse → P a) :
     xs.reverse.pmap f H = (xs.pmap f (fun a h => H a (by simpa using h))).reverse := by
   induction xs <;> simp_all
 
+@[grind =]
 theorem reverse_pmap {P : α → Prop} {f : (a : α) → P a → β} {xs : List α}
     (H : ∀ (a : α), a ∈ xs → P a) :
     (xs.pmap f H).reverse = xs.reverse.pmap f (fun a h => H a (by simpa using h)) := by
   rw [pmap_reverse]
 
-@[simp] theorem attachWith_reverse {P : α → Prop} {xs : List α}
+@[simp, grind =] theorem attachWith_reverse {P : α → Prop} {xs : List α}
     {H : ∀ (a : α), a ∈ xs.reverse → P a} :
     xs.reverse.attachWith P H =
       (xs.attachWith P (fun a h => H a (by simpa using h))).reverse :=
   pmap_reverse ..
 
+@[grind =]
 theorem reverse_attachWith {P : α → Prop} {xs : List α}
     {H : ∀ (a : α), a ∈ xs → P a} :
     (xs.attachWith P H).reverse = (xs.reverse.attachWith P (fun a h => H a (by simpa using h))) :=
   reverse_pmap ..
 
-@[simp] theorem attach_reverse {xs : List α} :
+@[simp, grind =] theorem attach_reverse {xs : List α} :
     xs.reverse.attach = xs.attach.reverse.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
   simp only [attach, attachWith, reverse_pmap, map_pmap]
   apply pmap_congr_left
   intros
   rfl
 
+@[grind =]
 theorem reverse_attach {xs : List α} :
     xs.attach.reverse = xs.reverse.attach.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
   simp only [attach, attachWith, reverse_pmap, map_pmap]
@@ -615,7 +652,7 @@ theorem countP_attachWith {p : α → Prop} {q : α → Bool} {l : List α} (H :
     (l.attachWith p H).countP (fun a : {x // p x} => q a) = l.countP q := by
   simp only [← Function.comp_apply (g := Subtype.val), ← countP_map, attachWith_map_subtype_val]
 
-@[simp, grind =]
+@[simp]
 theorem count_attach [BEq α] {l : List α} {a : {x // x ∈ l}} :
     l.attach.count a = l.count ↑a :=
   Eq.trans (countP_congr fun _ _ => by simp) <| countP_attach

src/Init/Data/List/Basic.lean

@@ -289,6 +289,16 @@ theorem cons_lex_nil [BEq α] {a} {as : List α} : lex (a :: as) [] lt = false :
 @[simp] theorem lex_nil [BEq α] {as : List α} : lex as [] lt = false := by
   cases as <;> simp [nil_lex_nil, cons_lex_nil]
 
+@[deprecated nil_lex_nil (since := "2025-02-10")]
+theorem lex_nil_nil [BEq α] : lex ([] : List α) [] lt = false := rfl
+@[deprecated nil_lex_cons (since := "2025-02-10")]
+theorem lex_nil_cons [BEq α] {b} {bs : List α} : lex [] (b :: bs) lt = true := rfl
+@[deprecated cons_lex_nil (since := "2025-02-10")]
+theorem lex_cons_nil [BEq α] {a} {as : List α} : lex (a :: as) [] lt = false := rfl
+@[deprecated cons_lex_cons (since := "2025-02-10")]
+theorem lex_cons_cons [BEq α] {a b} {as bs : List α} :
+    lex (a :: as) (b :: bs) lt = (lt a b || (a == b && lex as bs lt)) := rfl
+
 /-! ## Alternative getters -/
 
 /-! ### getLast -/

src/Init/Data/List/BasicAux.lean

@@ -21,6 +21,65 @@ namespace List
 
 /-! ## Alternative getters -/
 
+/-! ### get? -/
+
+/--
+Returns the `i`-th element in the list (zero-based).
+
+If the index is out of bounds (`i ≥ as.length`), this function returns `none`.
+Also see `get`, `getD` and `get!`.
+-/
+@[deprecated "Use `a[i]?` instead." (since := "2025-02-12"), expose]
+def get? : (as : List α) → (i : Nat) → Option α
+  | a::_,  0   => some a
+  | _::as, n+1 => get? as n
+  | _,     _   => none
+
+set_option linter.deprecated false in
+@[deprecated "Use `a[i]?` instead." (since := "2025-02-12"), simp]
+theorem get?_nil : @get? α [] n = none := rfl
+set_option linter.deprecated false in
+@[deprecated "Use `a[i]?` instead." (since := "2025-02-12"), simp]
+theorem get?_cons_zero : @get? α (a::l) 0 = some a := rfl
+set_option linter.deprecated false in
+@[deprecated "Use `a[i]?` instead." (since := "2025-02-12"), simp]
+theorem get?_cons_succ : @get? α (a::l) (n+1) = get? l n := rfl
+
+set_option linter.deprecated false in
+@[deprecated "Use `List.ext_getElem?`." (since := "2025-02-12")]
+theorem ext_get? : ∀ {l₁ l₂ : List α}, (∀ n, l₁.get? n = l₂.get? n) → l₁ = l₂
+  | [], [], _ => rfl
+  | _ :: _, [], h => nomatch h 0
+  | [], _ :: _, h => nomatch h 0
+  | a :: l₁, a' :: l₂, h => by
+    have h0 : some a = some a' := h 0
+    injection h0 with aa; simp only [aa, ext_get? fun n => h (n+1)]
+
+/-! ### get! -/
+
+/--
+Returns the `i`-th element in the list (zero-based).
+
+If the index is out of bounds (`i ≥ as.length`), this function panics when executed, and returns
+`default`. See `get?` and `getD` for safer alternatives.
+-/
+@[deprecated "Use `a[i]!` instead." (since := "2025-02-12"), expose]
+def get! [Inhabited α] : (as : List α) → (i : Nat) → α
+  | a::_,  0   => a
+  | _::as, n+1 => get! as n
+  | _,     _   => panic! "invalid index"
+
+set_option linter.deprecated false in
+@[deprecated "Use `a[i]!` instead." (since := "2025-02-12")]
+theorem get!_nil [Inhabited α] (n : Nat) : [].get! n = (default : α) := rfl
+set_option linter.deprecated false in
+@[deprecated "Use `a[i]!` instead." (since := "2025-02-12")]
+theorem get!_cons_succ [Inhabited α] (l : List α) (a : α) (n : Nat) :
+    (a::l).get! (n+1) = get! l n := rfl
+set_option linter.deprecated false in
+@[deprecated "Use `a[i]!` instead." (since := "2025-02-12")]
+theorem get!_cons_zero [Inhabited α] (l : List α) (a : α) : (a::l).get! 0 = a := rfl
+
 /-! ### getD -/
 
 /--
@@ -222,6 +281,17 @@ theorem getElem_append_right {as bs : List α} {i : Nat} (h₁ : as.length ≤ i
     cases i with simp [Nat.succ_sub_succ] <;> simp at h₁
     | succ i => apply ih; simp [h₁]
 
+@[deprecated "Deprecated without replacement." (since := "2025-02-13")]
+theorem get_last {as : List α} {i : Fin (length (as ++ [a]))} (h : ¬ i.1 < as.length) : (as ++ [a] : List _).get i = a := by
+  cases i; rename_i i h'
+  induction as generalizing i with
+  | nil => cases i with
+    | zero => simp [List.get]
+    | succ => simp +arith at h'
+  | cons a as ih =>
+    cases i with simp at h
+    | succ i => apply ih; simp [h]
+
 theorem sizeOf_lt_of_mem [SizeOf α] {as : List α} (h : a ∈ as) : sizeOf a < sizeOf as := by
   induction h with
   | head => simp +arith

src/Init/Data/List/Find.lean

@@ -360,6 +360,9 @@ theorem find?_flatten_eq_none_iff {xs : List (List α)} {p : α → Bool} :
     xs.flatten.find? p = none ↔ ∀ ys ∈ xs, ∀ x ∈ ys, !p x := by
   simp
 
+@[deprecated find?_flatten_eq_none_iff (since := "2025-02-03")]
+abbrev find?_flatten_eq_none := @find?_flatten_eq_none_iff
+
 /--
 If `find? p` returns `some a` from `xs.flatten`, then `p a` holds, and
 some list in `xs` contains `a`, and no earlier element of that list satisfies `p`.
@@ -400,6 +403,9 @@ theorem find?_flatten_eq_some_iff {xs : List (List α)} {p : α → Bool} {a :
     · exact h₁ l ml a m
     · exact h₂ a m
 
+@[deprecated find?_flatten_eq_some_iff (since := "2025-02-03")]
+abbrev find?_flatten_eq_some := @find?_flatten_eq_some_iff
+
 @[simp, grind =] theorem find?_flatMap {xs : List α} {f : α → List β} {p : β → Bool} :
     (xs.flatMap f).find? p = xs.findSome? (fun x => (f x).find? p) := by
   simp [flatMap_def, findSome?_map]; rfl
@@ -428,10 +434,16 @@ theorem find?_replicate_eq_none_iff {n : Nat} {a : α} {p : α → Bool} :
     (replicate n a).find? p = none ↔ n = 0 ∨ !p a := by
   simp [Classical.or_iff_not_imp_left]
 
+@[deprecated find?_replicate_eq_none_iff (since := "2025-02-03")]
+abbrev find?_replicate_eq_none := @find?_replicate_eq_none_iff
+
 @[simp] theorem find?_replicate_eq_some_iff {n : Nat} {a b : α} {p : α → Bool} :
     (replicate n a).find? p = some b ↔ n ≠ 0 ∧ p a ∧ a = b := by
   cases n <;> simp
 
+@[deprecated find?_replicate_eq_some_iff (since := "2025-02-03")]
+abbrev find?_replicate_eq_some := @find?_replicate_eq_some_iff
+
 @[simp] theorem get_find?_replicate {n : Nat} {a : α} {p : α → Bool} (h) : ((replicate n a).find? p).get h = a := by
   cases n with
   | zero => simp at h
@@ -824,6 +836,9 @@ theorem of_findIdx?_eq_some {xs : List α} {p : α → Bool} (w : xs.findIdx? p
     simp_all only [findIdx?_cons]
     split at w <;> cases i <;> simp_all
 
+@[deprecated of_findIdx?_eq_some (since := "2025-02-02")]
+abbrev findIdx?_of_eq_some := @of_findIdx?_eq_some
+
 theorem of_findIdx?_eq_none {xs : List α} {p : α → Bool} (w : xs.findIdx? p = none) :
     ∀ i : Nat, match xs[i]? with | some a => ¬ p a | none => true := by
   intro i
@@ -839,6 +854,9 @@ theorem of_findIdx?_eq_none {xs : List α} {p : α → Bool} (w : xs.findIdx? p
       apply ih
       split at w <;> simp_all
 
+@[deprecated of_findIdx?_eq_none (since := "2025-02-02")]
+abbrev findIdx?_of_eq_none := @of_findIdx?_eq_none
+
 @[simp, grind _=_] theorem findIdx?_map {f : β → α} {l : List β} : findIdx? p (l.map f) = l.findIdx? (p ∘ f) := by
   induction l with
   | nil => simp

src/Init/Data/List/Lemmas.lean

@@ -107,6 +107,9 @@ theorem ne_nil_of_length_pos (_ : 0 < length l) : l ≠ [] := fun _ => nomatch l
 @[simp] theorem length_eq_zero_iff : length l = 0 ↔ l = [] :=
   ⟨eq_nil_of_length_eq_zero, fun h => h ▸ rfl⟩
 
+@[deprecated length_eq_zero_iff (since := "2025-02-24")]
+abbrev length_eq_zero := @length_eq_zero_iff
+
 theorem eq_nil_iff_length_eq_zero : l = [] ↔ length l = 0 :=
   length_eq_zero_iff.symm
 
@@ -139,12 +142,18 @@ theorem exists_cons_of_length_eq_add_one :
 theorem length_pos_iff {l : List α} : 0 < length l ↔ l ≠ [] :=
   Nat.pos_iff_ne_zero.trans (not_congr length_eq_zero_iff)
 
+@[deprecated length_pos_iff (since := "2025-02-24")]
+abbrev length_pos := @length_pos_iff
+
 theorem ne_nil_iff_length_pos {l : List α} : l ≠ [] ↔ 0 < length l :=
   length_pos_iff.symm
 
 theorem length_eq_one_iff {l : List α} : length l = 1 ↔ ∃ a, l = [a] :=
   ⟨fun h => match l, h with | [_], _ => ⟨_, rfl⟩, fun ⟨_, h⟩ => by simp [h]⟩
 
+@[deprecated length_eq_one_iff (since := "2025-02-24")]
+abbrev length_eq_one := @length_eq_one_iff
+
 /-! ### cons -/
 
 -- The arguments here are intentionally explicit.
@@ -189,6 +198,38 @@ We simplify `l.get i` to `l[i.1]'i.2` and `l.get? i` to `l[i]?`.
 @[simp, grind =]
 theorem get_eq_getElem {l : List α} {i : Fin l.length} : l.get i = l[i.1]'i.2 := rfl
 
+set_option linter.deprecated false in
+@[deprecated "Use `a[i]?` instead." (since := "2025-02-12")]
+theorem get?_eq_none : ∀ {l : List α} {n}, length l ≤ n → l.get? n = none
+  | [], _, _ => rfl
+  | _ :: l, _+1, h => get?_eq_none (l := l) <| Nat.le_of_succ_le_succ h
+
+set_option linter.deprecated false in
+@[deprecated "Use `a[i]?` instead." (since := "2025-02-12")]
+theorem get?_eq_get : ∀ {l : List α} {n} (h : n < l.length), l.get? n = some (get l ⟨n, h⟩)
+  | _ :: _, 0, _ => rfl
+  | _ :: l, _+1, _ => get?_eq_get (l := l) _
+
+set_option linter.deprecated false in
+@[deprecated "Use `a[i]?` instead." (since := "2025-02-12")]
+theorem get?_eq_some_iff : l.get? n = some a ↔ ∃ h, get l ⟨n, h⟩ = a :=
+  ⟨fun e =>
+    have : n < length l := Nat.gt_of_not_le fun hn => by cases get?_eq_none hn ▸ e
+    ⟨this, by rwa [get?_eq_get this, Option.some.injEq] at e⟩,
+  fun ⟨_, e⟩ => e ▸ get?_eq_get _⟩
+
+set_option linter.deprecated false in
+@[deprecated "Use `a[i]?` instead." (since := "2025-02-12")]
+theorem get?_eq_none_iff : l.get? n = none ↔ length l ≤ n :=
+  ⟨fun e => Nat.ge_of_not_lt (fun h' => by cases e ▸ get?_eq_some_iff.2 ⟨h', rfl⟩), get?_eq_none⟩
+
+set_option linter.deprecated false in
+@[deprecated "Use `a[i]?` instead." (since := "2025-02-12"), simp]
+theorem get?_eq_getElem? {l : List α} {i : Nat} : l.get? i = l[i]? := by
+  simp only [getElem?_def]; split
+  · exact (get?_eq_get ‹_›)
+  · exact (get?_eq_none_iff.2 <| Nat.not_lt.1 ‹_›)
+
 /-! ### getElem!
 
 We simplify `l[i]!` to `(l[i]?).getD default`.
@@ -332,9 +373,26 @@ theorem getD_eq_getElem?_getD {l : List α} {i : Nat} {a : α} : getD l i a = (l
 theorem getD_cons_zero : getD (x :: xs) 0 d = x := by simp
 theorem getD_cons_succ : getD (x :: xs) (n + 1) d = getD xs n d := by simp
 
+/-! ### get!
+
+We simplify `l.get! i` to `l[i]!`.
+-/
+
+set_option linter.deprecated false in
+@[deprecated "Use `a[i]!` instead." (since := "2025-02-12")]
+theorem get!_eq_getD [Inhabited α] : ∀ (l : List α) i, l.get! i = l.getD i default
+  | [], _      => rfl
+  | _a::_, 0   => by simp [get!]
+  | _a::l, n+1 => by simpa using get!_eq_getD l n
+
+set_option linter.deprecated false in
+@[deprecated "Use `a[i]!` instead." (since := "2025-02-12"), simp]
+theorem get!_eq_getElem! [Inhabited α] (l : List α) (i) : l.get! i = l[i]! := by
+  simp [get!_eq_getD]
+
 /-! ### mem -/
 
-@[simp, grind ←] theorem not_mem_nil {a : α} : ¬ a ∈ [] := nofun
+@[simp] theorem not_mem_nil {a : α} : ¬ a ∈ [] := nofun
 
 @[simp, grind =] theorem mem_cons : a ∈ b :: l ↔ a = b ∨ a ∈ l :=
   ⟨fun h => by cases h <;> simp [Membership.mem, *],
@@ -523,9 +581,15 @@ theorem elem_eq_mem [BEq α] [LawfulBEq α] (a : α) (as : List α) :
 @[grind →]
 theorem nil_of_isEmpty {l : List α} (h : l.isEmpty) : l = [] := List.isEmpty_iff.mp h
 
+@[deprecated isEmpty_iff (since := "2025-02-17")]
+abbrev isEmpty_eq_true := @isEmpty_iff
+
 @[simp] theorem isEmpty_eq_false_iff {l : List α} : l.isEmpty = false ↔ l ≠ [] := by
   cases l <;> simp
 
+@[deprecated isEmpty_eq_false_iff (since := "2025-02-17")]
+abbrev isEmpty_eq_false := @isEmpty_eq_false_iff
+
 theorem isEmpty_eq_false_iff_exists_mem {xs : List α} :
     xs.isEmpty = false ↔ ∃ x, x ∈ xs := by
   cases xs <;> simp
@@ -2817,6 +2881,9 @@ theorem getLast_eq_head_reverse {l : List α} (h : l ≠ []) :
     l.getLast h = l.reverse.head (by simp_all) := by
   rw [← head_reverse]
 
+@[deprecated getLast_eq_iff_getLast?_eq_some (since := "2025-02-17")]
+abbrev getLast_eq_iff_getLast_eq_some := @getLast_eq_iff_getLast?_eq_some
+
 @[simp] theorem getLast?_eq_none_iff {xs : List α} : xs.getLast? = none ↔ xs = [] := by
   rw [getLast?_eq_head?_reverse, head?_eq_none_iff, reverse_eq_nil_iff]
 
@@ -3620,6 +3687,10 @@ theorem get_cons_succ' {as : List α} {i : Fin as.length} :
 theorem get_mk_zero : ∀ {l : List α} (h : 0 < l.length), l.get ⟨0, h⟩ = l.head (length_pos_iff.mp h)
   | _::_, _ => rfl
 
+set_option linter.deprecated false in
+@[deprecated "Use `a[0]?` instead." (since := "2025-02-12")]
+theorem get?_zero (l : List α) : l.get? 0 = l.head? := by cases l <;> rfl
+
 /--
 If one has `l.get i` in an expression (with `i : Fin l.length`) and `h : l = l'`,
 `rw [h]` will give a "motive is not type correct" error, as it cannot rewrite the
@@ -3629,6 +3700,18 @@ such a rewrite, with `rw [get_of_eq h]`.
 theorem get_of_eq {l l' : List α} (h : l = l') (i : Fin l.length) :
     get l i = get l' ⟨i, h ▸ i.2⟩ := by cases h; rfl
 
+set_option linter.deprecated false in
+@[deprecated "Use `a[i]?` instead." (since := "2025-02-12")]
+theorem get!_of_get? [Inhabited α] : ∀ {l : List α} {n}, get? l n = some a → get! l n = a
+  | _a::_, 0, rfl => rfl
+  | _::l, _+1, e => get!_of_get? (l := l) e
+
+set_option linter.deprecated false in
+@[deprecated "Use `a[i]!` instead." (since := "2025-02-12")]
+theorem get!_len_le [Inhabited α] : ∀ {l : List α} {n}, length l ≤ n → l.get! n = (default : α)
+  | [], _, _ => rfl
+  | _ :: l, _+1, h => get!_len_le (l := l) <| Nat.le_of_succ_le_succ h
+
 theorem getElem!_nil [Inhabited α] {n : Nat} : ([] : List α)[n]! = default := rfl
 
 theorem getElem!_cons_zero [Inhabited α] {l : List α} : (a::l)[0]! = a := by
@@ -3654,11 +3737,30 @@ theorem get_of_mem {a} {l : List α} (h : a ∈ l) : ∃ n, get l n = a := by
   obtain ⟨n, h, e⟩ := getElem_of_mem h
   exact ⟨⟨n, h⟩, e⟩
 
+set_option linter.deprecated false in
+@[deprecated getElem?_of_mem (since := "2025-02-12")]
+theorem get?_of_mem {a} {l : List α} (h : a ∈ l) : ∃ n, l.get? n = some a :=
+  let ⟨⟨n, _⟩, e⟩ := get_of_mem h; ⟨n, e ▸ get?_eq_get _⟩
+
 theorem get_mem : ∀ (l : List α) n, get l n ∈ l
   | _ :: _, ⟨0, _⟩ => .head ..
   | _ :: l, ⟨_+1, _⟩ => .tail _ (get_mem l ..)
 
+set_option linter.deprecated false in
+@[deprecated mem_of_getElem? (since := "2025-02-12")]
+theorem mem_of_get? {l : List α} {n a} (e : l.get? n = some a) : a ∈ l :=
+  let ⟨_, e⟩ := get?_eq_some_iff.1 e; e ▸ get_mem ..
+
 theorem mem_iff_get {a} {l : List α} : a ∈ l ↔ ∃ n, get l n = a :=
   ⟨get_of_mem, fun ⟨_, e⟩ => e ▸ get_mem ..⟩
 
+set_option linter.deprecated false in
+@[deprecated mem_iff_getElem? (since := "2025-02-12")]
+theorem mem_iff_get? {a} {l : List α} : a ∈ l ↔ ∃ n, l.get? n = some a := by
+  simp [getElem?_eq_some_iff, Fin.exists_iff, mem_iff_get]
+
+/-! ### Deprecations -/
+
+
+
 end List

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

@@ -105,6 +105,9 @@ theorem length_leftpad {n : Nat} {a : α} {l : List α} :
     (leftpad n a l).length = max n l.length := by
   simp only [leftpad, length_append, length_replicate, Nat.sub_add_eq_max]
 
+@[deprecated length_leftpad (since := "2025-02-24")]
+abbrev leftpad_length := @length_leftpad
+
 theorem length_rightpad {n : Nat} {a : α} {l : List α} :
     (rightpad n a l).length = max n l.length := by
   simp [rightpad]

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

@@ -196,6 +196,9 @@ theorem getElem_insertIdx_of_gt {l : List α} {x : α} {i j : Nat} (hn : i < j)
         | zero => omega
         | succ j => simp
 
+@[deprecated getElem_insertIdx_of_gt (since := "2025-02-04")]
+abbrev getElem_insertIdx_of_ge := @getElem_insertIdx_of_gt
+
 @[grind =]
 theorem getElem_insertIdx {l : List α} {x : α} {i j : Nat} (h : j < (l.insertIdx i x).length) :
     (l.insertIdx i x)[j] =
@@ -258,6 +261,9 @@ theorem getElem?_insertIdx_of_gt {l : List α} {x : α} {i j : Nat} (h : i < j)
     (l.insertIdx i x)[j]? = l[j - 1]? := by
   rw [getElem?_insertIdx, if_neg (by omega), if_neg (by omega)]
 
+@[deprecated getElem?_insertIdx_of_gt (since := "2025-02-04")]
+abbrev getElem?_insertIdx_of_ge := @getElem?_insertIdx_of_gt
+
 end InsertIdx
 
 end List

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

@@ -117,6 +117,9 @@ theorem take_set_of_le {a : α} {i j : Nat} {l : List α} (h : j ≤ i) :
     next h' => rw [getElem?_set_ne (by omega)]
     · rfl
 
+@[deprecated take_set_of_le (since := "2025-02-04")]
+abbrev take_set_of_lt := @take_set_of_le
+
 @[simp, grind =] theorem take_replicate {a : α} : ∀ {i n : Nat}, take i (replicate n a) = replicate (min i n) a
   | n, 0 => by simp
   | 0, m => by simp
@@ -162,6 +165,9 @@ theorem take_eq_take_iff :
   | x :: xs, 0, j + 1 => by simp [succ_min_succ]
   | x :: xs, i + 1, j + 1 => by simp [succ_min_succ, take_eq_take_iff]
 
+@[deprecated take_eq_take_iff (since := "2025-02-16")]
+abbrev take_eq_take := @take_eq_take_iff
+
 @[grind =]
 theorem take_add {l : List α} {i j : Nat} : l.take (i + j) = l.take i ++ (l.drop i).take j := by
   suffices take (i + j) (take i l ++ drop i l) = take i l ++ take j (drop i l) by

src/Init/Data/List/TakeDrop.lean

@@ -165,6 +165,9 @@ theorem take_set {l : List α} {i j : Nat} {a : α} :
     | nil => simp
     | cons hd tl => cases j <;> simp_all
 
+@[deprecated take_set (since := "2025-02-17")]
+abbrev set_take := @take_set
+
 theorem drop_set {l : List α} {i j : Nat} {a : α} :
     (l.set j a).drop i = if j < i then l.drop i else (l.drop i).set (j - i) a := by
   induction i generalizing l j with

src/Init/Data/Nat/Basic.lean

@@ -791,6 +791,18 @@ protected theorem pow_le_pow_right {n : Nat} (hx : n > 0) {i : Nat} : ∀ {j}, i
     | Or.inr h =>
       h.symm ▸ Nat.le_refl _
 
+set_option linter.missingDocs false in
+@[deprecated Nat.pow_le_pow_left (since := "2025-02-17")]
+abbrev pow_le_pow_of_le_left := @Nat.pow_le_pow_left
+
+set_option linter.missingDocs false in
+@[deprecated Nat.pow_le_pow_right (since := "2025-02-17")]
+abbrev pow_le_pow_of_le_right := @Nat.pow_le_pow_right
+
+set_option linter.missingDocs false in
+@[deprecated Nat.pow_pos (since := "2025-02-17")]
+abbrev pos_pow_of_pos := @Nat.pow_pos
+
 @[simp] theorem zero_pow_of_pos (n : Nat) (h : 0 < n) : 0 ^ n = 0 := by
   cases n with
   | zero => cases h
@@ -870,6 +882,9 @@ protected theorem ne_zero_of_lt (h : b < a) : a ≠ 0 := by
   exact absurd h (Nat.not_lt_zero _)
   apply Nat.noConfusion
 
+@[deprecated Nat.ne_zero_of_lt (since := "2025-02-06")]
+theorem not_eq_zero_of_lt (h : b < a) : a ≠ 0 := Nat.ne_zero_of_lt h
+
 theorem pred_lt_of_lt {n m : Nat} (h : m < n) : pred n < n :=
   pred_lt (Nat.ne_zero_of_lt h)
 

src/Init/Data/Option/Attach.lean

@@ -75,7 +75,10 @@ theorem attach_map_val (o : Option α) (f : α → β) :
     (o.attach.map fun (i : {i // o = some i}) => f i) = o.map f := by
   cases o <;> simp
 
-@[simp] theorem attach_map_subtype_val (o : Option α) :
+@[deprecated attach_map_val (since := "2025-02-17")]
+abbrev attach_map_coe := @attach_map_val
+
+@[simp, grind =]theorem attach_map_subtype_val (o : Option α) :
     o.attach.map Subtype.val = o :=
   (attach_map_val _ _).trans (congrFun Option.map_id _)
 
@@ -83,7 +86,10 @@ theorem attachWith_map_val {p : α → Prop} (f : α → β) (o : Option α) (H
     ((o.attachWith p H).map fun (i : { i // p i}) => f i.val) = o.map f := by
   cases o <;> simp
 
-@[simp] theorem attachWith_map_subtype_val {p : α → Prop} (o : Option α) (H : ∀ a, o = some a → p a) :
+@[deprecated attachWith_map_val (since := "2025-02-17")]
+abbrev attachWith_map_coe := @attachWith_map_val
+
+@[simp, grind =] theorem attachWith_map_subtype_val {p : α → Prop} (o : Option α) (H : ∀ a, o = some a → p a) :
     (o.attachWith p H).map Subtype.val = o :=
   (attachWith_map_val _ _ _).trans (congrFun Option.map_id _)
 
@@ -168,23 +174,23 @@ theorem toArray_attachWith {p : α → Prop} {o : Option α} {h} :
     o.toList.attach = (o.attach.map fun ⟨a, h⟩ => ⟨a, by simpa using h⟩).toList := by
   cases o <;> simp [toList]
 
-@[grind =]
-theorem attach_map {o : Option α} (f : α → β) :
+@[grind =] theorem attach_map {o : Option α} (f : α → β) :
     (o.map f).attach = o.attach.map (fun ⟨x, h⟩ => ⟨f x, map_eq_some_iff.2 ⟨_, h, rfl⟩⟩) := by
   cases o <;> simp
 
-@[grind =]
-theorem attachWith_map {o : Option α} (f : α → β) {P : β → Prop} {H : ∀ (b : β), o.map f = some b → P b} :
+@[grind =] theorem attachWith_map {o : Option α} (f : α → β) {P : β → Prop} {H : ∀ (b : β), o.map f = some b → P b} :
     (o.map f).attachWith P H = (o.attachWith (P ∘ f) (fun _ h => H _ (map_eq_some_iff.2 ⟨_, h, rfl⟩))).map
       fun ⟨x, h⟩ => ⟨f x, h⟩ := by
   cases o <;> simp
 
-@[grind =]
-theorem map_attach_eq_pmap {o : Option α} (f : { x // o = some x } → β) :
+@[grind =] theorem map_attach_eq_pmap {o : Option α} (f : { x // o = some x } → β) :
     o.attach.map f = o.pmap (fun a (h : o = some a) => f ⟨a, h⟩) (fun _ h => h) := by
   cases o <;> simp
 
-@[simp] theorem map_attachWith {l : Option α} {P : α → Prop} {H : ∀ (a : α), l = some a → P a}
+@[deprecated map_attach_eq_pmap (since := "2025-02-09")]
+abbrev map_attach := @map_attach_eq_pmap
+
+@[simp, grind =] theorem map_attachWith {l : Option α} {P : α → Prop} {H : ∀ (a : α), l = some a → P a}
     (f : { x // P x } → β) :
     (l.attachWith P H).map f = l.attach.map fun ⟨x, h⟩ => f ⟨x, H _ h⟩ := by
   cases l <;> simp_all
@@ -200,12 +206,12 @@ theorem map_attach_eq_attachWith {o : Option α} {p : α → Prop} (f : ∀ a, o
     o.attach.map (fun x => ⟨x.1, f x.1 x.2⟩) = o.attachWith p f := by
   cases o <;> simp_all
 
-theorem attach_bind {o : Option α} {f : α → Option β} :
+@[grind =] theorem attach_bind {o : Option α} {f : α → Option β} :
     (o.bind f).attach =
       o.attach.bind fun ⟨x, h⟩ => (f x).attach.map fun ⟨y, h'⟩ => ⟨y, bind_eq_some_iff.2 ⟨_, h, h'⟩⟩ := by
   cases o <;> simp
 
-theorem bind_attach {o : Option α} {f : {x // o = some x} → Option β} :
+@[grind =] theorem bind_attach {o : Option α} {f : {x // o = some x} → Option β} :
     o.attach.bind f = o.pbind fun a h => f ⟨a, h⟩ := by
   cases o <;> simp
 
@@ -213,7 +219,7 @@ theorem pbind_eq_bind_attach {o : Option α} {f : (a : α) → o = some a → Op
     o.pbind f = o.attach.bind fun ⟨x, h⟩ => f x h := by
   cases o <;> simp
 
-theorem attach_filter {o : Option α} {p : α → Bool} :
+@[grind =] theorem attach_filter {o : Option α} {p : α → Bool} :
     (o.filter p).attach =
       o.attach.bind fun ⟨x, h⟩ => if h' : p x then some ⟨x, by simp_all⟩ else none := by
   cases o with
@@ -229,12 +235,12 @@ theorem attach_filter {o : Option α} {p : α → Bool} :
     · rintro ⟨h, rfl⟩
       simp [h]
 
-theorem filter_attachWith {P : α → Prop} {o : Option α} {h : ∀ x, o = some x → P x} {q : α → Bool} :
+@[grind =] theorem filter_attachWith {P : α → Prop} {o : Option α} {h : ∀ x, o = some x → P x} {q : α → Bool} :
     (o.attachWith P h).filter q =
       (o.filter q).attachWith P (fun _ h' => h _ (eq_some_of_filter_eq_some h')) := by
   cases o <;> simp [filter_some] <;> split <;> simp
 
-theorem filter_attach {o : Option α} {p : {x // o = some x} → Bool} :
+@[grind =] theorem filter_attach {o : Option α} {p : {x // o = some x} → Bool} :
     o.attach.filter p = o.pbind fun a h => if p ⟨a, h⟩ then some ⟨a, h⟩ else none := by
   cases o <;> simp [filter_some]
 
@@ -278,7 +284,7 @@ theorem toArray_pmap {p : α → Prop} {o : Option α} {f : (a : α) → p a →
     (o.pmap f h).toArray = o.attach.toArray.map (fun x => f x.1 (h _ x.2)) := by
   cases o <;> simp
 
-theorem attach_pfilter {o : Option α} {p : (a : α) → o = some a → Bool} :
+@[grind =] theorem attach_pfilter {o : Option α} {p : (a : α) → o = some a → Bool} :
     (o.pfilter p).attach =
       o.attach.pbind fun x h => if h' : p x (by simp_all) then
         some ⟨x.1, by simpa [pfilter_eq_some_iff] using ⟨_, h'⟩⟩ else none := by

src/Init/Data/SInt/Basic.lean

@@ -96,7 +96,8 @@ theorem Int8.toBitVec.inj : {x y : Int8} → x.toBitVec = y.toBitVec → x = y
 
 /-- Obtains the `Int8` that is 2's complement equivalent to the `UInt8`. -/
 @[inline] def UInt8.toInt8 (i : UInt8) : Int8 := Int8.ofUInt8 i
-
+@[inline, deprecated UInt8.toInt8 (since := "2025-02-13"), inherit_doc UInt8.toInt8]
+def Int8.mk (i : UInt8) : Int8 := UInt8.toInt8 i
 /--
 Converts an arbitrary-precision integer to an 8-bit integer, wrapping on overflow or underflow.
 
@@ -158,7 +159,8 @@ Converts an 8-bit signed integer to a natural number, mapping all negative numbe
 Use `Int8.toBitVec` to obtain the two's complement representation.
 -/
 @[inline] def Int8.toNatClampNeg (i : Int8) : Nat := i.toInt.toNat
-
+@[inline, deprecated Int8.toNatClampNeg (since := "2025-02-13"), inherit_doc Int8.toNatClampNeg]
+def Int8.toNat (i : Int8) : Nat := i.toInt.toNat
 /-- Obtains the `Int8` whose 2's complement representation is the given `BitVec 8`. -/
 @[inline] def Int8.ofBitVec (b : BitVec 8) : Int8 := ⟨⟨b⟩⟩
 /--
@@ -447,7 +449,8 @@ theorem Int16.toBitVec.inj : {x y : Int16} → x.toBitVec = y.toBitVec → x = y
 
 /-- Obtains the `Int16` that is 2's complement equivalent to the `UInt16`. -/
 @[inline] def UInt16.toInt16 (i : UInt16) : Int16 := Int16.ofUInt16 i
-
+@[inline, deprecated UInt16.toInt16 (since := "2025-02-13"), inherit_doc UInt16.toInt16]
+def Int16.mk (i : UInt16) : Int16 := UInt16.toInt16 i
 /--
 Converts an arbitrary-precision integer to a 16-bit signed integer, wrapping on overflow or underflow.
 
@@ -511,7 +514,8 @@ Converts a 16-bit signed integer to a natural number, mapping all negative numbe
 Use `Int16.toBitVec` to obtain the two's complement representation.
 -/
 @[inline] def Int16.toNatClampNeg (i : Int16) : Nat := i.toInt.toNat
-
+@[inline, deprecated Int16.toNatClampNeg (since := "2025-02-13"), inherit_doc Int16.toNatClampNeg]
+def Int16.toNat (i : Int16) : Nat := i.toInt.toNat
 /-- Obtains the `Int16` whose 2's complement representation is the given `BitVec 16`. -/
 @[inline] def Int16.ofBitVec (b : BitVec 16) : Int16 := ⟨⟨b⟩⟩
 /--
@@ -816,7 +820,8 @@ theorem Int32.toBitVec.inj : {x y : Int32} → x.toBitVec = y.toBitVec → x = y
 
 /-- Obtains the `Int32` that is 2's complement equivalent to the `UInt32`. -/
 @[inline] def UInt32.toInt32 (i : UInt32) : Int32 := Int32.ofUInt32 i
-
+@[inline, deprecated UInt32.toInt32 (since := "2025-02-13"), inherit_doc UInt32.toInt32]
+def Int32.mk (i : UInt32) : Int32 := UInt32.toInt32 i
 /--
 Converts an arbitrary-precision integer to a 32-bit integer, wrapping on overflow or underflow.
 
@@ -881,7 +886,8 @@ Converts a 32-bit signed integer to a natural number, mapping all negative numbe
 Use `Int32.toBitVec` to obtain the two's complement representation.
 -/
 @[inline] def Int32.toNatClampNeg (i : Int32) : Nat := i.toInt.toNat
-
+@[inline, deprecated Int32.toNatClampNeg (since := "2025-02-13"), inherit_doc Int32.toNatClampNeg]
+def Int32.toNat (i : Int32) : Nat := i.toInt.toNat
 /-- Obtains the `Int32` whose 2's complement representation is the given `BitVec 32`. -/
 @[inline] def Int32.ofBitVec (b : BitVec 32) : Int32 := ⟨⟨b⟩⟩
 /--
@@ -1201,7 +1207,8 @@ theorem Int64.toBitVec.inj : {x y : Int64} → x.toBitVec = y.toBitVec → x = y
 
 /-- Obtains the `Int64` that is 2's complement equivalent to the `UInt64`. -/
 @[inline] def UInt64.toInt64 (i : UInt64) : Int64 := Int64.ofUInt64 i
-
+@[inline, deprecated UInt64.toInt64 (since := "2025-02-13"), inherit_doc UInt64.toInt64]
+def Int64.mk (i : UInt64) : Int64 := UInt64.toInt64 i
 /--
 Converts an arbitrary-precision integer to a 64-bit integer, wrapping on overflow or underflow.
 
@@ -1271,7 +1278,8 @@ Converts a 64-bit signed integer to a natural number, mapping all negative numbe
 Use `Int64.toBitVec` to obtain the two's complement representation.
 -/
 @[inline] def Int64.toNatClampNeg (i : Int64) : Nat := i.toInt.toNat
-
+@[inline, deprecated Int64.toNatClampNeg (since := "2025-02-13"), inherit_doc Int64.toNatClampNeg]
+def Int64.toNat (i : Int64) : Nat := i.toInt.toNat
 /-- Obtains the `Int64` whose 2's complement representation is the given `BitVec 64`. -/
 @[inline] def Int64.ofBitVec (b : BitVec 64) : Int64 := ⟨⟨b⟩⟩
 /--
@@ -1605,7 +1613,8 @@ theorem ISize.toBitVec.inj : {x y : ISize} → x.toBitVec = y.toBitVec → x = y
 
 /-- Obtains the `ISize` that is 2's complement equivalent to the `USize`. -/
 @[inline] def USize.toISize (i : USize) : ISize := ISize.ofUSize i
-
+@[inline, deprecated USize.toISize (since := "2025-02-13"), inherit_doc USize.toISize]
+def ISize.mk (i : USize) : ISize := USize.toISize i
 /--
 Converts an arbitrary-precision integer to a word-sized signed integer, wrapping around on over- or
 underflow.
@@ -1638,7 +1647,8 @@ Converts a word-sized signed integer to a natural number, mapping all negative n
 Use `ISize.toBitVec` to obtain the two's complement representation.
 -/
 @[inline] def ISize.toNatClampNeg (i : ISize) : Nat := i.toInt.toNat
-
+@[inline, deprecated ISize.toNatClampNeg (since := "2025-02-13"), inherit_doc ISize.toNatClampNeg]
+def ISize.toNat (i : ISize) : Nat := i.toInt.toNat
 /-- Obtains the `ISize` whose 2's complement representation is the given `BitVec`. -/
 @[inline] def ISize.ofBitVec (b : BitVec System.Platform.numBits) : ISize := ⟨⟨b⟩⟩
 /--

src/Init/Data/String/Extra.lean

@@ -104,7 +104,8 @@ where
 
 /--
 Decodes an array of bytes that encode a string as [UTF-8](https://en.wikipedia.org/wiki/UTF-8) into
-the corresponding string.
+the corresponding string. Invalid UTF-8 characters in the byte array result in `(default : Char)`,
+or `'A'`, in the string.
 -/
 @[extern "lean_string_from_utf8_unchecked"]
 def fromUTF8 (a : @& ByteArray) (h : validateUTF8 a) : String :=

src/Init/Data/ToString/Name.lean

@@ -7,7 +7,7 @@ module
 
 prelude
 public import Init.Meta
-public import Init.Data.String.Extra
+import Init.Data.String.Extra
 
 /-!
 Here we give the. implementation of `Name.toString`. There is also a private implementation in

src/Init/Data/UInt/Basic.lean

@@ -21,7 +21,12 @@ open Nat
 
 /-- Converts a `Fin UInt8.size` into the corresponding `UInt8`. -/
 @[inline] def UInt8.ofFin (a : Fin UInt8.size) : UInt8 := ⟨⟨a⟩⟩
-
+@[deprecated UInt8.ofBitVec (since := "2025-02-12"), inherit_doc UInt8.ofBitVec]
+def UInt8.mk (bitVec : BitVec 8) : UInt8 :=
+  UInt8.ofBitVec bitVec
+@[inline, deprecated UInt8.ofNatLT (since := "2025-02-13"), inherit_doc UInt8.ofNatLT]
+def UInt8.ofNatCore (n : Nat) (h : n < UInt8.size) : UInt8 :=
+  UInt8.ofNatLT n h
 
 /-- Converts an `Int` to a `UInt8` by taking the (non-negative remainder of the division by `2 ^ 8`. -/
 def UInt8.ofInt (x : Int) : UInt8 := ofNat (x % 2 ^ 8).toNat
@@ -185,6 +190,12 @@ instance : Min UInt8 := minOfLe
 
 /-- Converts a `Fin UInt16.size` into the corresponding `UInt16`. -/
 @[inline] def UInt16.ofFin (a : Fin UInt16.size) : UInt16 := ⟨⟨a⟩⟩
+@[deprecated UInt16.ofBitVec (since := "2025-02-12"), inherit_doc UInt16.ofBitVec]
+def UInt16.mk (bitVec : BitVec 16) : UInt16 :=
+  UInt16.ofBitVec bitVec
+@[inline, deprecated UInt16.ofNatLT (since := "2025-02-13"), inherit_doc UInt16.ofNatLT]
+def UInt16.ofNatCore (n : Nat) (h : n < UInt16.size) : UInt16 :=
+  UInt16.ofNatLT n h
 
 /-- Converts an `Int` to a `UInt16` by taking the (non-negative remainder of the division by `2 ^ 16`. -/
 def UInt16.ofInt (x : Int) : UInt16 := ofNat (x % 2 ^ 16).toNat
@@ -395,6 +406,12 @@ instance : Min UInt16 := minOfLe
 
 /-- Converts a `Fin UInt32.size` into the corresponding `UInt32`. -/
 @[inline] def UInt32.ofFin (a : Fin UInt32.size) : UInt32 := ⟨⟨a⟩⟩
+@[deprecated UInt32.ofBitVec (since := "2025-02-12"), inherit_doc UInt32.ofBitVec]
+def UInt32.mk (bitVec : BitVec 32) : UInt32 :=
+  UInt32.ofBitVec bitVec
+@[inline, deprecated UInt32.ofNatLT (since := "2025-02-13"), inherit_doc UInt32.ofNatLT]
+def UInt32.ofNatCore (n : Nat) (h : n < UInt32.size) : UInt32 :=
+  UInt32.ofNatLT n h
 
 /-- Converts an `Int` to a `UInt32` by taking the (non-negative remainder of the division by `2 ^ 32`. -/
 def UInt32.ofInt (x : Int) : UInt32 := ofNat (x % 2 ^ 32).toNat
@@ -568,6 +585,12 @@ def Bool.toUInt32 (b : Bool) : UInt32 := if b then 1 else 0
 
 /-- Converts a `Fin UInt64.size` into the corresponding `UInt64`. -/
 @[inline] def UInt64.ofFin (a : Fin UInt64.size) : UInt64 := ⟨⟨a⟩⟩
+@[deprecated UInt64.ofBitVec (since := "2025-02-12"), inherit_doc UInt64.ofBitVec]
+def UInt64.mk (bitVec : BitVec 64) : UInt64 :=
+  UInt64.ofBitVec bitVec
+@[inline, deprecated UInt64.ofNatLT (since := "2025-02-13"), inherit_doc UInt64.ofNatLT]
+def UInt64.ofNatCore (n : Nat) (h : n < UInt64.size) : UInt64 :=
+  UInt64.ofNatLT n h
 
 /-- Converts an `Int` to a `UInt64` by taking the (non-negative remainder of the division by `2 ^ 64`. -/
 def UInt64.ofInt (x : Int) : UInt64 := ofNat (x % 2 ^ 64).toNat
@@ -776,6 +799,12 @@ instance : Min UInt64 := minOfLe
 
 /-- Converts a `Fin USize.size` into the corresponding `USize`. -/
 @[inline] def USize.ofFin (a : Fin USize.size) : USize := ⟨⟨a⟩⟩
+@[deprecated USize.ofBitVec (since := "2025-02-12"), inherit_doc USize.ofBitVec]
+def USize.mk (bitVec : BitVec System.Platform.numBits) : USize :=
+  USize.ofBitVec bitVec
+@[inline, deprecated USize.ofNatLT (since := "2025-02-13"), inherit_doc USize.ofNatLT]
+def USize.ofNatCore (n : Nat) (h : n < USize.size) : USize :=
+  USize.ofNatLT n h
 
 /-- Converts an `Int` to a `USize` by taking the (non-negative remainder of the division by `2 ^ numBits`. -/
 def USize.ofInt (x : Int) : USize := ofNat (x % 2 ^ System.Platform.numBits).toNat
@@ -783,6 +812,14 @@ def USize.ofInt (x : Int) : USize := ofNat (x % 2 ^ System.Platform.numBits).toN
 @[simp] theorem USize.le_size : 2 ^ 32 ≤ USize.size := by cases USize.size_eq <;> simp_all
 @[simp] theorem USize.size_le : USize.size ≤ 2 ^ 64 := by cases USize.size_eq <;> simp_all
 
+@[deprecated USize.size_le (since := "2025-02-24")]
+theorem usize_size_le : USize.size ≤ 18446744073709551616 :=
+  USize.size_le
+
+@[deprecated USize.le_size (since := "2025-02-24")]
+theorem le_usize_size : 4294967296 ≤ USize.size :=
+  USize.le_size
+
 /--
 Multiplies two word-sized unsigned integers, wrapping around on overflow.  Usually accessed via the
 `*` operator.

src/Init/Data/UInt/BasicAux.lean

@@ -26,6 +26,8 @@ open Nat
 
 /-- Converts a `UInt8` into the corresponding `Fin UInt8.size`. -/
 def UInt8.toFin (x : UInt8) : Fin UInt8.size := x.toBitVec.toFin
+@[deprecated UInt8.toFin (since := "2025-02-12"), inherit_doc UInt8.toFin]
+def UInt8.val (x : UInt8) : Fin UInt8.size := x.toFin
 
 /--
 Converts a natural number to an 8-bit unsigned integer, returning the largest representable value if
@@ -65,6 +67,8 @@ instance UInt8.instOfNat : OfNat UInt8 n := ⟨UInt8.ofNat n⟩
 
 /-- Converts a `UInt16` into the corresponding `Fin UInt16.size`. -/
 def UInt16.toFin (x : UInt16) : Fin UInt16.size := x.toBitVec.toFin
+@[deprecated UInt16.toFin (since := "2025-02-12"), inherit_doc UInt16.toFin]
+def UInt16.val (x : UInt16) : Fin UInt16.size := x.toFin
 
 /--
 Converts a natural number to a 16-bit unsigned integer, wrapping on overflow.
@@ -130,6 +134,8 @@ instance UInt16.instOfNat : OfNat UInt16 n := ⟨UInt16.ofNat n⟩
 
 /-- Converts a `UInt32` into the corresponding `Fin UInt32.size`. -/
 def UInt32.toFin (x : UInt32) : Fin UInt32.size := x.toBitVec.toFin
+@[deprecated UInt32.toFin (since := "2025-02-12"), inherit_doc UInt32.toFin]
+def UInt32.val (x : UInt32) : Fin UInt32.size := x.toFin
 
 /--
 Converts a natural number to a 32-bit unsigned integer, wrapping on overflow.
@@ -143,7 +149,8 @@ Examples:
 -/
 @[extern "lean_uint32_of_nat"]
 def UInt32.ofNat (n : @& Nat) : UInt32 := ⟨BitVec.ofNat 32 n⟩
-
+@[inline, deprecated UInt32.ofNatLT (since := "2025-02-13"), inherit_doc UInt32.ofNatLT]
+def UInt32.ofNat' (n : Nat) (h : n < UInt32.size) : UInt32 := UInt32.ofNatLT n h
 /--
 Converts a natural number to a 32-bit unsigned integer, returning the largest representable value if
 the number is too large.
@@ -203,14 +210,23 @@ theorem UInt32.ofNatLT_lt_of_lt {n m : Nat} (h1 : n < UInt32.size) (h2 : m < UIn
   simp only [(· < ·), BitVec.toNat, ofNatLT, BitVec.ofNatLT, ofNat, BitVec.ofNat,
     Fin.Internal.ofNat_eq_ofNat, Fin.ofNat, Nat.mod_eq_of_lt h2, imp_self]
 
+@[deprecated UInt32.ofNatLT_lt_of_lt (since := "2025-02-13")]
+theorem UInt32.ofNat'_lt_of_lt {n m : Nat} (h1 : n < UInt32.size) (h2 : m < UInt32.size) :
+     n < m → UInt32.ofNatLT n h1 < UInt32.ofNat m := UInt32.ofNatLT_lt_of_lt h1 h2
+
 theorem UInt32.lt_ofNatLT_of_lt {n m : Nat} (h1 : n < UInt32.size) (h2 : m < UInt32.size) :
      m < n → UInt32.ofNat m < UInt32.ofNatLT n h1 := by
   simp only [(· < ·), BitVec.toNat, ofNatLT, BitVec.ofNatLT, ofNat, BitVec.ofNat, Fin.Internal.ofNat_eq_ofNat,
     Fin.ofNat, Nat.mod_eq_of_lt h2, imp_self]
 
+@[deprecated UInt32.lt_ofNatLT_of_lt (since := "2025-02-13")]
+theorem UInt32.lt_ofNat'_of_lt {n m : Nat} (h1 : n < UInt32.size) (h2 : m < UInt32.size) :
+     m < n → UInt32.ofNat m < UInt32.ofNatLT n h1 := UInt32.lt_ofNatLT_of_lt h1 h2
+
 /-- Converts a `UInt64` into the corresponding `Fin UInt64.size`. -/
 def UInt64.toFin (x : UInt64) : Fin UInt64.size := x.toBitVec.toFin
-
+@[deprecated UInt64.toFin (since := "2025-02-12"), inherit_doc UInt64.toFin]
+def UInt64.val (x : UInt64) : Fin UInt64.size := x.toFin
 /--
 Converts a natural number to a 64-bit unsigned integer, wrapping on overflow.
 
@@ -299,9 +315,18 @@ def UInt32.toUInt64 (a : UInt32) : UInt64 := ⟨⟨a.toNat, Nat.lt_trans a.toBit
 
 instance UInt64.instOfNat : OfNat UInt64 n := ⟨UInt64.ofNat n⟩
 
+@[deprecated USize.size_eq (since := "2025-02-24")]
+theorem usize_size_eq : USize.size = 4294967296 ∨ USize.size = 18446744073709551616 :=
+  USize.size_eq
+
+@[deprecated USize.size_pos (since := "2025-02-24")]
+theorem usize_size_pos : 0 < USize.size :=
+  USize.size_pos
+
 /-- Converts a `USize` into the corresponding `Fin USize.size`. -/
 def USize.toFin (x : USize) : Fin USize.size := x.toBitVec.toFin
-
+@[deprecated USize.toFin (since := "2025-02-12"), inherit_doc USize.toFin]
+def USize.val (x : USize) : Fin USize.size := x.toFin
 /--
 Converts an arbitrary-precision natural number to an unsigned word-sized integer, wrapping around on
 overflow.

src/Init/Data/UInt/Lemmas.lean

@@ -42,6 +42,9 @@ macro "declare_uint_theorems" typeName:ident bits:term:arg : command => do
 
   @[simp] theorem toNat_ofBitVec : (ofBitVec a).toNat = a.toNat := (rfl)
 
+  @[deprecated toNat_ofBitVec (since := "2025-02-12")]
+  theorem toNat_mk : (ofBitVec a).toNat = a.toNat := (rfl)
+
   @[simp] theorem toNat_ofNat' {n : Nat} : (ofNat n).toNat = n % 2 ^ $bits := BitVec.toNat_ofNat ..
 
   -- Not `simp` because we have simprocs which will avoid the modulo.
@@ -49,14 +52,34 @@ macro "declare_uint_theorems" typeName:ident bits:term:arg : command => do
 
   @[simp] theorem toNat_ofNatLT {n : Nat} {h : n < size} : (ofNatLT n h).toNat = n := BitVec.toNat_ofNatLT ..
 
+  @[deprecated toNat_ofNatLT (since := "2025-02-13")]
+  theorem toNat_ofNatCore {n : Nat} {h : n < size} : (ofNatLT n h).toNat = n := BitVec.toNat_ofNatLT ..
+
   @[simp] theorem toFin_val (x : $typeName) : x.toFin.val = x.toNat := (rfl)
+  @[deprecated toFin_val (since := "2025-02-12")]
+  theorem val_val_eq_toNat (x : $typeName) : x.toFin.val = x.toNat := (rfl)
 
   @[simp] theorem toNat_toBitVec (x : $typeName) : x.toBitVec.toNat = x.toNat := (rfl)
   @[simp] theorem toFin_toBitVec (x : $typeName) : x.toBitVec.toFin = x.toFin := (rfl)
 
+  @[deprecated toNat_toBitVec (since := "2025-02-21")]
+  theorem toNat_toBitVec_eq_toNat (x : $typeName) : x.toBitVec.toNat = x.toNat := (rfl)
+
   @[simp] theorem ofBitVec_toBitVec : ∀ (a : $typeName), ofBitVec a.toBitVec = a
     | ⟨_, _⟩ => rfl
 
+  @[deprecated ofBitVec_toBitVec (since := "2025-02-21")]
+  theorem ofBitVec_toBitVec_eq : ∀ (a : $typeName), ofBitVec a.toBitVec = a :=
+    ofBitVec_toBitVec
+
+  @[deprecated ofBitVec_toBitVec_eq (since := "2025-02-12")]
+  theorem mk_toBitVec_eq : ∀ (a : $typeName), ofBitVec a.toBitVec = a
+    | ⟨_, _⟩ => rfl
+
+  @[deprecated "Use `toNat_toBitVec` and `toNat_ofNat_of_lt`." (since := "2025-03-05")]
+  theorem toBitVec_eq_of_lt {a : Nat} : a < size → (ofNat a).toBitVec.toNat = a :=
+    Nat.mod_eq_of_lt
+
   theorem toBitVec_ofNat' (n : Nat) : (ofNat n).toBitVec = BitVec.ofNat _ n := (rfl)
 
   theorem toNat_ofNat_of_lt' {n : Nat} (h : n < size) : (ofNat n).toNat = n := by
@@ -117,10 +140,17 @@ macro "declare_uint_theorems" typeName:ident bits:term:arg : command => do
   protected theorem eq_of_toFin_eq {a b : $typeName} (h : a.toFin = b.toFin) : a = b := by
     rcases a with ⟨⟨_⟩⟩; rcases b with ⟨⟨_⟩⟩; simp_all [toFin]
   open $typeName (eq_of_toFin_eq) in
+  @[deprecated eq_of_toFin_eq (since := "2025-02-12")]
+  protected theorem eq_of_val_eq {a b : $typeName} (h : a.toFin = b.toFin) : a = b :=
+    eq_of_toFin_eq h
 
   open $typeName (eq_of_toFin_eq) in
   protected theorem toFin_inj {a b : $typeName} : a.toFin = b.toFin ↔ a = b :=
     Iff.intro eq_of_toFin_eq (congrArg toFin)
+  open $typeName (toFin_inj) in
+  @[deprecated toFin_inj (since := "2025-02-12")]
+  protected theorem val_inj {a b : $typeName} : a.toFin = b.toFin ↔ a = b :=
+    toFin_inj
 
   open $typeName (eq_of_toBitVec_eq) in
   protected theorem toBitVec_ne_of_ne {a b : $typeName} (h : a ≠ b) : a.toBitVec ≠ b.toBitVec :=
@@ -206,6 +236,8 @@ instance : LawfulOrderLT $typeName where
 
   @[simp]
   theorem toFin_ofNat (n : Nat) : toFin (no_index (OfNat.ofNat n)) = OfNat.ofNat n := (rfl)
+  @[deprecated toFin_ofNat (since := "2025-02-12")]
+  theorem val_ofNat (n : Nat) : toFin (no_index (OfNat.ofNat n)) = OfNat.ofNat n := (rfl)
 
   @[simp, int_toBitVec]
   theorem toBitVec_ofNat (n : Nat) : toBitVec (no_index (OfNat.ofNat n)) = BitVec.ofNat _ n := (rfl)
@@ -213,6 +245,9 @@ instance : LawfulOrderLT $typeName where
   @[simp]
   theorem ofBitVec_ofNat (n : Nat) : ofBitVec (BitVec.ofNat _ n) = OfNat.ofNat n := (rfl)
 
+  @[deprecated ofBitVec_ofNat (since := "2025-02-12")]
+  theorem mk_ofNat (n : Nat) : ofBitVec (BitVec.ofNat _ n) = OfNat.ofNat n := (rfl)
+
   @[simp, int_toBitVec] protected theorem toBitVec_add {a b : $typeName} : (a + b).toBitVec = a.toBitVec + b.toBitVec := (rfl)
   @[simp, int_toBitVec] protected theorem toBitVec_sub {a b : $typeName} : (a - b).toBitVec = a.toBitVec - b.toBitVec := (rfl)
   @[simp, int_toBitVec] protected theorem toBitVec_mul {a b : $typeName} : (a * b).toBitVec = a.toBitVec * b.toBitVec := (rfl)

src/Init/Data/Vector/Attach.lean

@@ -97,16 +97,16 @@ Unsafe implementation of `attachWith`, taking advantage of the fact that the rep
   intro a m h₁ h₂
   congr
 
-@[simp] theorem pmap_empty {P : α → Prop} {f : ∀ a, P a → β} : pmap f #v[] (by simp) = #v[] := rfl
+@[simp, grind =] theorem pmap_empty {P : α → Prop} {f : ∀ a, P a → β} : pmap f #v[] (by simp) = #v[] := rfl
 
-@[simp] theorem pmap_push {P : α → Prop} {f : ∀ a, P a → β} {a : α} {xs : Vector α n} {h : ∀ b ∈ xs.push a, P b} :
+@[simp, grind =] theorem pmap_push {P : α → Prop} {f : ∀ a, P a → β} {a : α} {xs : Vector α n} {h : ∀ b ∈ xs.push a, P b} :
     pmap f (xs.push a) h =
       (pmap f xs (fun a m => by simp at h; exact h a (.inl m))).push (f a (h a (by simp))) := by
   simp [pmap]
 
-@[simp] theorem attach_empty : (#v[] : Vector α 0).attach = #v[] := rfl
+@[simp, grind =] theorem attach_empty : (#v[] : Vector α 0).attach = #v[] := rfl
 
-@[simp] theorem attachWith_empty {P : α → Prop} (H : ∀ x ∈ #v[], P x) : (#v[] : Vector α 0).attachWith P H = #v[] := rfl
+@[simp, grind =] theorem attachWith_empty {P : α → Prop} (H : ∀ x ∈ #v[], P x) : (#v[] : Vector α 0).attachWith P H = #v[] := rfl
 
 @[simp]
 theorem pmap_eq_map {p : α → Prop} {f : α → β} {xs : Vector α n} (H) :
@@ -120,11 +120,13 @@ theorem pmap_congr_left {p q : α → Prop} {f : ∀ a, p a → β} {g : ∀ a,
   apply Array.pmap_congr_left
   simpa using h
 
+@[grind =]
 theorem map_pmap {p : α → Prop} {g : β → γ} {f : ∀ a, p a → β} {xs : Vector α n} (H) :
     map g (pmap f xs H) = pmap (fun a h => g (f a h)) xs H := by
   rcases xs with ⟨xs, rfl⟩
   simp [Array.map_pmap]
 
+@[grind =]
 theorem pmap_map {p : β → Prop} {g : ∀ b, p b → γ} {f : α → β} {xs : Vector α n} (H) :
     pmap g (map f xs) H = pmap (fun a h => g (f a) h) xs fun _ h => H _ (mem_map_of_mem h) := by
   rcases xs with ⟨xs, rfl⟩
@@ -140,13 +142,13 @@ theorem attachWith_congr {xs ys : Vector α n} (w : xs = ys) {P : α → Prop} {
   subst w
   simp
 
-@[simp] theorem attach_push {a : α} {xs : Vector α n} :
+@[simp, grind =] theorem attach_push {a : α} {xs : Vector α n} :
     (xs.push a).attach =
       (xs.attach.map (fun ⟨x, h⟩ => ⟨x, mem_push_of_mem a h⟩)).push ⟨a, by simp⟩ := by
   rcases xs with ⟨xs, rfl⟩
   simp [Array.map_attach_eq_pmap]
 
-@[simp] theorem attachWith_push {a : α} {xs : Vector α n} {P : α → Prop} {H : ∀ x ∈ xs.push a, P x} :
+@[simp, grind =] theorem attachWith_push {a : α} {xs : Vector α n} {P : α → Prop} {H : ∀ x ∈ xs.push a, P x} :
     (xs.push a).attachWith P H =
       (xs.attachWith P (fun x h => by simp at H; exact H x (.inl h))).push ⟨a, H a (by simp)⟩ := by
   rcases xs with ⟨xs, rfl⟩
@@ -170,6 +172,9 @@ theorem attach_map_val (xs : Vector α n) (f : α → β) :
   rcases xs with ⟨xs, rfl⟩
   simp
 
+@[deprecated attach_map_val (since := "2025-02-17")]
+abbrev attach_map_coe := @attach_map_val
+
 -- The argument `xs : Vector α n` is explicit to allow rewriting from right to left.
 theorem attach_map_subtype_val (xs : Vector α n) : xs.attach.map Subtype.val = xs := by
   rcases xs with ⟨xs, rfl⟩
@@ -180,6 +185,9 @@ theorem attachWith_map_val {p : α → Prop} {f : α → β} {xs : Vector α n}
   rcases xs with ⟨xs, rfl⟩
   simp
 
+@[deprecated attachWith_map_val (since := "2025-02-17")]
+abbrev attachWith_map_coe := @attachWith_map_val
+
 theorem attachWith_map_subtype_val {p : α → Prop} {xs : Vector α n} (H : ∀ a ∈ xs, p a) :
     (xs.attachWith p H).map Subtype.val = xs := by
   rcases xs with ⟨xs, rfl⟩
@@ -250,24 +258,26 @@ theorem getElem_attach {xs : Vector α n} {i : Nat} (h : i < n) :
     xs.attach[i] = ⟨xs[i]'(by simpa using h), getElem_mem (by simpa using h)⟩ :=
   getElem_attachWith h
 
-@[simp] theorem pmap_attach {xs : Vector α n} {p : {x // x ∈ xs} → Prop} {f : ∀ a, p a → β} (H) :
+@[simp, grind =] theorem pmap_attach {xs : Vector α n} {p : {x // x ∈ xs} → Prop} {f : ∀ a, p a → β} (H) :
     pmap f xs.attach H =
       xs.pmap (P := fun a => ∃ h : a ∈ xs, p ⟨a, h⟩)
         (fun a h => f ⟨a, h.1⟩ h.2) (fun a h => ⟨h, H ⟨a, h⟩ (by simp)⟩) := by
   rcases xs with ⟨xs, rfl⟩
   ext <;> simp
 
-@[simp] theorem pmap_attachWith {xs : Vector α n} {p : {x // q x} → Prop} {f : ∀ a, p a → β} (H₁ H₂) :
+@[simp, grind =] theorem pmap_attachWith {xs : Vector α n} {p : {x // q x} → Prop} {f : ∀ a, p a → β} (H₁ H₂) :
     pmap f (xs.attachWith q H₁) H₂ =
       xs.pmap (P := fun a => ∃ h : q a, p ⟨a, h⟩)
         (fun a h => f ⟨a, h.1⟩ h.2) (fun a h => ⟨H₁ _ h, H₂ ⟨a, H₁ _ h⟩ (by simpa)⟩) := by
   ext <;> simp
 
+@[grind =]
 theorem foldl_pmap {xs : Vector α n} {P : α → Prop} {f : (a : α) → P a → β}
     (H : ∀ (a : α), a ∈ xs → P a) (g : γ → β → γ) (x : γ) :
     (xs.pmap f H).foldl g x = xs.attach.foldl (fun acc a => g acc (f a.1 (H _ a.2))) x := by
   rw [pmap_eq_map_attach, foldl_map]
 
+@[grind =]
 theorem foldr_pmap {xs : Vector α n} {P : α → Prop} {f : (a : α) → P a → β}
     (H : ∀ (a : α), a ∈ xs → P a) (g : β → γ → γ) (x : γ) :
     (xs.pmap f H).foldr g x = xs.attach.foldr (fun a acc => g (f a.1 (H _ a.2)) acc) x := by
@@ -303,18 +313,20 @@ theorem foldr_attach {xs : Vector α n} {f : α → β → β} {b : β} :
   rcases xs with ⟨xs, rfl⟩
   simp
 
+@[grind =]
 theorem attach_map {xs : Vector α n} {f : α → β} :
     (xs.map f).attach = xs.attach.map (fun ⟨x, h⟩ => ⟨f x, mem_map_of_mem h⟩) := by
   cases xs
   ext <;> simp
 
+@[grind =]
 theorem attachWith_map {xs : Vector α n} {f : α → β} {P : β → Prop} (H : ∀ (b : β), b ∈ xs.map f → P b) :
     (xs.map f).attachWith P H = (xs.attachWith (P ∘ f) (fun _ h => H _ (mem_map_of_mem h))).map
       fun ⟨x, h⟩ => ⟨f x, h⟩ := by
   rcases xs with ⟨xs, rfl⟩
   simp [Array.attachWith_map]
 
-@[simp] theorem map_attachWith {xs : Vector α n} {P : α → Prop} {H : ∀ (a : α), a ∈ xs → P a}
+@[simp, grind =] theorem map_attachWith {xs : Vector α n} {P : α → Prop} {H : ∀ (a : α), a ∈ xs → P a}
     {f : { x // P x } → β} :
     (xs.attachWith P H).map f = xs.attach.map fun ⟨x, h⟩ => f ⟨x, H _ h⟩ := by
   rcases xs with ⟨xs, rfl⟩
@@ -333,6 +345,10 @@ theorem map_attach_eq_pmap {xs : Vector α n} {f : { x // x ∈ xs } → β} :
   rcases xs with ⟨xs, rfl⟩
   ext <;> simp
 
+@[deprecated map_attach_eq_pmap (since := "2025-02-09")]
+abbrev map_attach := @map_attach_eq_pmap
+
+@[grind =]
 theorem pmap_pmap {p : α → Prop} {q : β → Prop} {g : ∀ a, p a → β} {f : ∀ b, q b → γ} {xs : Vector α n} (H₁ H₂) :
     pmap f (pmap g xs H₁) H₂ =
       pmap (α := { x // x ∈ xs }) (fun a h => f (g a h) (H₂ (g a h) (mem_pmap_of_mem a.2))) xs.attach
@@ -340,7 +356,7 @@ theorem pmap_pmap {p : α → Prop} {q : β → Prop} {g : ∀ a, p a → β} {f
   rcases xs with ⟨xs, rfl⟩
   ext <;> simp
 
-@[simp] theorem pmap_append {p : ι → Prop} {f : ∀ a : ι, p a → α} {xs : Vector ι n} {ys : Vector ι m}
+@[simp, grind =] theorem pmap_append {p : ι → Prop} {f : ∀ a : ι, p a → α} {xs : Vector ι n} {ys : Vector ι m}
     (h : ∀ a ∈ xs ++ ys, p a) :
     (xs ++ ys).pmap f h =
       (xs.pmap f fun a ha => h a (mem_append_left ys ha)) ++
@@ -355,66 +371,69 @@ theorem pmap_append' {p : α → Prop} {f : ∀ a : α, p a → β} {xs : Vector
       xs.pmap f h₁ ++ ys.pmap f h₂ :=
   pmap_append _
 
-@[simp] theorem attach_append {xs : Vector α n} {ys : Vector α m} :
+@[simp, grind =] theorem attach_append {xs : Vector α n} {ys : Vector α m} :
     (xs ++ ys).attach = xs.attach.map (fun ⟨x, h⟩ => (⟨x, mem_append_left ys h⟩ : { x // x ∈ xs ++ ys })) ++
       ys.attach.map (fun ⟨y, h⟩ => (⟨y, mem_append_right xs h⟩ : { y // y ∈ xs ++ ys })) := by
   rcases xs with ⟨xs, rfl⟩
   rcases ys with ⟨ys, rfl⟩
   simp [Array.map_attach_eq_pmap]
 
-@[simp] theorem attachWith_append {P : α → Prop} {xs : Vector α n} {ys : Vector α m}
+@[simp, grind =] theorem attachWith_append {P : α → Prop} {xs : Vector α n} {ys : Vector α m}
     {H : ∀ (a : α), a ∈ xs ++ ys → P a} :
     (xs ++ ys).attachWith P H = xs.attachWith P (fun a h => H a (mem_append_left ys h)) ++
       ys.attachWith P (fun a h => H a (mem_append_right xs h)) := by
   simp [attachWith]
 
-@[simp] theorem pmap_reverse {P : α → Prop} {f : (a : α) → P a → β} {xs : Vector α n}
+@[simp, grind =] theorem pmap_reverse {P : α → Prop} {f : (a : α) → P a → β} {xs : Vector α n}
     (H : ∀ (a : α), a ∈ xs.reverse → P a) :
     xs.reverse.pmap f H = (xs.pmap f (fun a h => H a (by simpa using h))).reverse := by
   induction xs <;> simp_all
 
+@[grind =]
 theorem reverse_pmap {P : α → Prop} {f : (a : α) → P a → β} {xs : Vector α n}
     (H : ∀ (a : α), a ∈ xs → P a) :
     (xs.pmap f H).reverse = xs.reverse.pmap f (fun a h => H a (by simpa using h)) := by
   rw [pmap_reverse]
 
-@[simp] theorem attachWith_reverse {P : α → Prop} {xs : Vector α n}
+@[simp, grind =] theorem attachWith_reverse {P : α → Prop} {xs : Vector α n}
     {H : ∀ (a : α), a ∈ xs.reverse → P a} :
     xs.reverse.attachWith P H =
       (xs.attachWith P (fun a h => H a (by simpa using h))).reverse := by
   cases xs
   simp
 
+@[grind =]
 theorem reverse_attachWith {P : α → Prop} {xs : Vector α n}
     {H : ∀ (a : α), a ∈ xs → P a} :
     (xs.attachWith P H).reverse = (xs.reverse.attachWith P (fun a h => H a (by simpa using h))) := by
   cases xs
   simp
 
-@[simp] theorem attach_reverse {xs : Vector α n} :
+@[simp, grind =] theorem attach_reverse {xs : Vector α n} :
     xs.reverse.attach = xs.attach.reverse.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
   cases xs
   rw [attach_congr (reverse_mk ..)]
   simp [Array.map_attachWith]
 
+@[grind =]
 theorem reverse_attach {xs : Vector α n} :
     xs.attach.reverse = xs.reverse.attach.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
   cases xs
   simp [Array.map_attach_eq_pmap]
 
-@[simp] theorem back?_pmap {P : α → Prop} {f : (a : α) → P a → β} {xs : Vector α n}
+@[simp, grind =] theorem back?_pmap {P : α → Prop} {f : (a : α) → P a → β} {xs : Vector α n}
     (H : ∀ (a : α), a ∈ xs → P a) :
     (xs.pmap f H).back? = xs.attach.back?.map fun ⟨a, m⟩ => f a (H a m) := by
   cases xs
   simp
 
-@[simp] theorem back?_attachWith {P : α → Prop} {xs : Vector α n}
+@[simp, grind =] theorem back?_attachWith {P : α → Prop} {xs : Vector α n}
     {H : ∀ (a : α), a ∈ xs → P a} :
     (xs.attachWith P H).back? = xs.back?.pbind (fun a h => some ⟨a, H _ (mem_of_back? h)⟩) := by
   cases xs
   simp
 
-@[simp]
+@[simp, grind =]
 theorem back?_attach {xs : Vector α n} :
     xs.attach.back? = xs.back?.pbind fun a h => some ⟨a, mem_of_back? h⟩ := by
   cases xs

src/Init/Data/Vector/Lemmas.lean

@@ -879,13 +879,11 @@ set_option linter.indexVariables false in
   rcases xs with ⟨xs, rfl⟩
   simp
 
-@[grind =]
 theorem getElem_push {xs : Vector α n} {x : α} {i : Nat} (h : i < n + 1) :
     (xs.push x)[i] = if h : i < n then xs[i] else x := by
   rcases xs with ⟨xs, rfl⟩
   simp [Array.getElem_push]
 
-@[grind =]
 theorem getElem?_push {xs : Vector α n} {x : α} {i : Nat} : (xs.push x)[i]? = if i = n then some x else xs[i]? := by
   simp [getElem?_def, getElem_push]
   (repeat' split) <;> first | rfl | omega
@@ -909,8 +907,6 @@ theorem getElem?_singleton {a : α} {i : Nat} : #v[a][i]? = if i = 0 then some a
 
 grind_pattern getElem_mem => xs[i] ∈ xs
 
-
-@[grind ←]
 theorem not_mem_empty (a : α) : ¬ a ∈ #v[] := nofun
 
 @[simp, grind =] theorem mem_push {xs : Vector α n} {x y : α} : x ∈ xs.push y ↔ x ∈ xs ∨ x = y := by

src/Init/GetElem.lean

@@ -250,6 +250,11 @@ theorem getElem_of_getElem? [GetElem? cont idx elem dom] [LawfulGetElem cont idx
     (c[i]? = some c[i]) ↔ True := by
   simp [h]
 
+@[deprecated getElem?_eq_none_iff (since := "2025-02-17")]
+abbrev getElem?_eq_none := @getElem?_eq_none_iff
+
+
+
 @[simp, grind =] theorem isSome_getElem? [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
     (c : cont) (i : idx) [Decidable (dom c i)] : c[i]?.isSome = dom c i := by
   simp only [getElem?_def]

src/Init/Grind/Attr.lean

@@ -135,7 +135,7 @@ Each time it encounters a subexpression which covers an argument which was not
 previously covered, it adds that subexpression as a pattern, until all arguments have been covered.
 If `grind!` is used, then only minimal indexable subexpressions are considered.
 -/
-syntax grindDef    := patternIgnore("." <|> "·") (grindGen)?
+syntax grindDef    := "." (grindGen)?
 /--
 The `usr` modifier indicates that this theorem was applied using a
 **user-defined instantiation pattern**. Such patterns are declared with
@@ -215,47 +215,9 @@ syntax grindMod :=
     <|> grindFwd <|> grindRL <|> grindLR <|> grindUsr <|> grindCasesEager
     <|> grindCases <|> grindIntro <|> grindExt <|> grindGen <|> grindSym <|> grindInj
     <|> grindDef
-
-/--
-Marks a theorem or definition for use by the `grind` tactic.
-
-An optional modifier (e.g. `=`, `→`, `←`, `cases`, `intro`, `ext`, `inj`, etc.)
-controls how `grind` uses the declaration:
-* whether it is applied forwards, backwards, or both,
-* whether equalities are used on the left, right, or both sides,
-* whether case-splits, constructors, extensionality, or injectivity are applied,
-* or whether custom instantiation patterns are used.
-
-See the individual modifier docstrings for details.
--/
 syntax (name := grind) "grind" (ppSpace grindMod)? : attr
-/--
-Like `@[grind]`, but enforces the **minimal indexable subexpression condition**:
-when several subterms cover the same free variables, `grind!` chooses the smallest one.
-
-This influences E-matching pattern selection.
-
-### Example
-```lean
-theorem fg_eq (h : x > 0) : f (g x) = x
-
-@[grind <-] theorem fg_eq (h : x > 0) : f (g x) = x
--- Pattern selected: `f (g x)`
-
--- With minimal subexpression:
-@[grind! <-] theorem fg_eq (h : x > 0) : f (g x) = x
--- Pattern selected: `g x`
--/
 syntax (name := grind!) "grind!" (ppSpace grindMod)? : attr
-/--
-Like `@[grind]`, but also prints the pattern(s) selected by `grind`
-as info messages. Useful for debugging annotations and modifiers.
--/
 syntax (name := grind?) "grind?" (ppSpace grindMod)? : attr
-/--
-Like `@[grind!]`, but also prints the pattern(s) selected by `grind`
-as info messages. Combines minimal subexpression selection with debugging output.
--/
 syntax (name := grind!?) "grind!?" (ppSpace grindMod)? : attr
 end Attr
 end Lean.Parser

src/Init/Grind/Injective.lean

@@ -7,7 +7,7 @@ module
 prelude
 public import Init.Data.Function
 public import Init.Classical
-public section
+
 namespace Lean.Grind
 open Function
 
@@ -31,11 +31,4 @@ noncomputable def leftInv {α : Sort u} {β : Sort v} (f : α → β) (hf : Inje
 theorem leftInv_eq {α : Sort u} {β : Sort v} (f : α → β) (hf : Injective f) [Nonempty α] (a : α) : leftInv f hf (f a) = a :=
   Classical.choose_spec (hf.leftInverse f) a
 
-@[app_unexpander leftInv]
-meta def leftInvUnexpander : PrettyPrinter.Unexpander := fun stx => do
-  match stx with
-  | `($_ $f:term $_) => `($f⁻¹)
-  | `($_ $f:term $_ $a:term) => `($f⁻¹ $a)
-  | _ => throw ()
-
 end Lean.Grind

src/Init/Grind/Ordered/Ring.lean

@@ -53,86 +53,6 @@ theorem ofNat_nonneg (x : Nat) : (OfNat.ofNat x : R) ≥ 0 := by
     have := Preorder.lt_of_lt_of_le this ih
     exact Preorder.le_of_lt this
 
-attribute [local instance] Semiring.natCast Ring.intCast
-
-theorem le_of_natCast_le_natCast (a b : Nat) : (a : R) ≤ (b : R) → a ≤ b := by
-  induction a generalizing b <;> cases b <;> simp
-  next n ih =>
-    simp [Semiring.natCast_succ, Semiring.natCast_zero]
-    intro h
-    have : (n:R) ≤ 0 := by
-      have := OrderedRing.zero_lt_one (R := R)
-      replace this := OrderedAdd.add_le_right (M := R) (n:R) (Std.le_of_lt this)
-      rw [Semiring.add_zero] at this
-      exact Std.IsPreorder.le_trans _ _ _ this h
-    replace ih := ih 0
-    simp [Semiring.natCast_zero] at ih
-    replace ih := ih this
-    subst n
-    clear this
-    have := OrderedRing.zero_lt_one (R := R)
-    rw [Semiring.natCast_zero, Semiring.add_comm, Semiring.add_zero] at h
-    replace this := Std.lt_of_lt_of_le this h
-    have := Preorder.lt_irrefl (0:R)
-    contradiction
-  next ih m =>
-    simp [Semiring.natCast_succ]
-    intro h
-    have := OrderedAdd.add_le_left_iff _ |>.mpr h
-    exact ih _ this
-
-theorem le_of_intCast_le_intCast (a b : Int) : (a : R) ≤ (b : R) → a ≤ b := by
-  intro h
-  replace h := OrderedAdd.sub_nonneg_iff.mpr h
-  rw [← Ring.intCast_sub] at h
-  suffices 0 ≤ b - a by omega
-  revert h
-  generalize b - a = x
-  cases x <;> simp [Ring.intCast_natCast, Int.negSucc_eq, Ring.intCast_neg, Ring.intCast_add]
-  intro h
-  replace h := OrderedAdd.neg_nonneg_iff.mp h
-  rw [Ring.intCast_one, ← Semiring.natCast_one, ← Semiring.natCast_add, ← Semiring.natCast_zero] at h
-  replace h := le_of_natCast_le_natCast _ _ h
-  omega
-
-theorem lt_of_natCast_lt_natCast (a b : Nat) : (a : R) < (b : R) → a < b := by
-  induction a generalizing b <;> cases b <;> simp
-  next =>
-    simp [Semiring.natCast_zero]
-    exact Preorder.lt_irrefl (0:R)
-  next n ih =>
-    simp [Semiring.natCast_succ, Semiring.natCast_zero]
-    intro h
-    have : (n:R) < 0 := by
-      have := OrderedRing.zero_lt_one (R := R)
-      replace this := OrderedAdd.add_le_right (M := R) (n:R) (Std.le_of_lt this)
-      rw [Semiring.add_zero] at this
-      exact Std.lt_of_le_of_lt this h
-    replace ih := ih 0
-    simp [Semiring.natCast_zero] at ih
-    exact ih this
-  next ih m =>
-    simp [Semiring.natCast_succ]
-    intro h
-    have := OrderedAdd.add_lt_left_iff _ |>.mpr h
-    exact ih _ this
-
-theorem lt_of_intCast_lt_intCast (a b : Int) : (a : R) < (b : R) → a < b := by
-  intro h
-  replace h := OrderedAdd.sub_pos_iff.mpr h
-  rw [← Ring.intCast_sub] at h
-  suffices 0 < b - a by omega
-  revert h
-  generalize b - a = x
-  cases x <;> simp [Ring.intCast_natCast, Int.negSucc_eq, Ring.intCast_neg, Ring.intCast_add]
-  next => intro h; rw [← Semiring.natCast_zero] at h; exact lt_of_natCast_lt_natCast _ _ h
-  next =>
-    intro h
-    replace h := OrderedAdd.neg_pos_iff.mp h
-    rw [Ring.intCast_one, ← Semiring.natCast_one, ← Semiring.natCast_add, ← Semiring.natCast_zero] at h
-    replace h := lt_of_natCast_lt_natCast _ _ h
-    omega
-
 instance [Ring R] [LE R] [LT R] [LawfulOrderLT R] [IsPreorder R] [OrderedRing R] :
     IsCharP R 0 := IsCharP.mk' _ _ <| by
   intro x

src/Init/Grind/Tactics.lean

@@ -4,9 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
+
 prelude
 public import Init.Grind.Attr
 public import Init.Core
+
 public section
 
 namespace Lean.Grind
@@ -96,16 +98,8 @@ structure Config where
   zeta := true
   /--
   When `true` (default: `true`), uses procedure for handling equalities over commutative rings.
-  This solver also support commutative semirings, fields, and normalizer non-commutative rings and
-  semirings.
   -/
   ring := true
-  /--
-  Maximum number of steps performed by the `ring` solver.
-  A step is counted whenever one polynomial is used to simplify another.
-  For example, given `x^2 + 1` and `x^2 * y^3 + x * y`, the first can be
-  used to simplify the second to `-1 * y^3 + x * y`.
-  -/
   ringSteps := 10000
   /--
   When `true` (default: `true`), uses procedure for handling linear arithmetic for `IntModule`, and
@@ -120,12 +114,6 @@ structure Config where
   When `true` (default: `true`), uses procedure for handling associative (and commutative) operators.
   -/
   ac := true
-  /--
-  Maximum number of steps performed by the `ac` solver.
-  A step is counted whenever one AC equation is used to simplify another.
-  For example, given `ma x z = w` and `max x (max y z) = x`, the first can be
-  used to simplify the second to `max w y = x`.
-  -/
   acSteps := 1000
   /--
   Maximum exponent eagerly evaluated while computing bounds for `ToInt` and
@@ -136,14 +124,6 @@ structure Config where
   When `true` (default: `true`), automatically creates an auxiliary theorem to store the proof.
   -/
   abstractProof := true
-  /--
-  When `true` (default: `true`), enables the procedure for handling injective functions.
-  In this mode, `grind` takes into account theorems such as:
-  ```
-  @[grind inj] theorem double_inj : Function.Injective double
-  ```
-  -/
-  inj := true
   deriving Inhabited, BEq
 
 /--

src/Init/Notation.lean

@@ -855,7 +855,7 @@ which would include `#guard_msgs` itself, and would cause duplicate and/or uncap
 The top-level command elaborator only runs the linters if `#guard_msgs` is not present.
 -/
 syntax (name := guardMsgsCmd)
-  (plainDocComment)? "#guard_msgs" (ppSpace guardMsgsSpec)? " in" ppLine command : command
+  (docComment)? "#guard_msgs" (ppSpace guardMsgsSpec)? " in" ppLine command : command
 
 /--
 Format and print the info trees for a given command.

src/Init/System/Promise.lean

@@ -71,6 +71,9 @@ def Promise.result! (promise : @& Promise α) : Task α :=
   let _ : Nonempty α := promise.h
   promise.result?.map (sync := true) Option.getOrBlock!
 
+@[inherit_doc Promise.result!, deprecated Promise.result! (since := "2025-02-05")]
+def Promise.result := @Promise.result!
+
 /--
 Like `Promise.result`, but resolves to `dflt` if the promise is dropped without ever being resolved.
 -/

src/Init/Tactics.lean

@@ -436,8 +436,8 @@ macro "rfl'" : tactic => `(tactic| set_option smartUnfolding false in with_unfol
 /--
 `ac_rfl` proves equalities up to application of an associative and commutative operator.
 ```
-instance : Std.Associative (α := Nat) (.+.) := ⟨Nat.add_assoc⟩
-instance : Std.Commutative (α := Nat) (.+.) := ⟨Nat.add_comm⟩
+instance : Associative (α := Nat) (.+.) := ⟨Nat.add_assoc⟩
+instance : Commutative (α := Nat) (.+.) := ⟨Nat.add_comm⟩
 
 example (a b c d : Nat) : a + b + c + d = d + (b + c) + a := by ac_rfl
 ```
@@ -1025,7 +1025,7 @@ The form
 ```
 fun_induction f
 ```
-(with no arguments to `f`) searches the goal for a unique eligible application of `f`, and uses
+(with no arguments to `f`) searches the goal for an unique eligible application of `f`, and uses
 these arguments. An application of `f` is eligible if it is saturated and the arguments that will
 become targets are free variables.
 
@@ -1058,7 +1058,7 @@ The form
 ```
 fun_cases f
 ```
-(with no arguments to `f`) searches the goal for a unique eligible application of `f`, and uses
+(with no arguments to `f`) searches the goal for an unique eligible application of `f`, and uses
 these arguments. An application of `f` is eligible if it is saturated and the arguments that will
 become targets are free variables.
 
@@ -1563,8 +1563,8 @@ syntax (name := normCastAddElim) "norm_cast_add_elim" ident : command
   list of hypotheses in the local context. In the latter case, a turnstile `⊢` or `|-`
   can also be used, to signify the target of the goal.
 ```
-instance : Std.Associative (α := Nat) (.+.) := ⟨Nat.add_assoc⟩
-instance : Std.Commutative (α := Nat) (.+.) := ⟨Nat.add_comm⟩
+instance : Associative (α := Nat) (.+.) := ⟨Nat.add_assoc⟩
+instance : Commutative (α := Nat) (.+.) := ⟨Nat.add_comm⟩
 
 example (a b c d : Nat) : a + b + c + d = d + (b + c) + a := by
  ac_nf

src/Lean/Compiler/LCNF/Main.lean

@@ -112,7 +112,7 @@ def run (declNames : Array Name) : CompilerM (Array IR.Decl) := withAtLeastMaxRe
   -- Check meta accesses now before optimizations may obscure references. This check should stay in
   -- `lean` if some compilation is moved out.
   for decl in decls do
-    checkMeta decl
+    checkMeta (isMeta (← getEnv) decl.name) decl
   let decls := markRecDecls decls
   let manager ← getPassManager
   let isCheckEnabled := compiler.check.get (← getOptions)

src/Lean/Compiler/LCNF/Passes.lean

@@ -85,9 +85,6 @@ def builtinPassManager : PassManager := {
     -/
     simp { etaPoly := true, inlinePartial := true, implementedBy := true } (occurrence := 1),
     eagerLambdaLifting,
-    -- Should be as early as possible but after `eagerLambdaLifting` to make sure instances are
-    -- checked without nested functions whose bodies specialization does not require access to.
-    checkTemplateVisibility,
     specialize,
     simp (occurrence := 2),
     cse (shouldElimFunDecls := false) (occurrence := 1),

src/Lean/Compiler/LCNF/Simp/ConstantFold.lean

@@ -101,32 +101,24 @@ instance : Literal Bool where
   getLit := getBoolLit
   mkLit := mkBoolLit
 
-private def getLitAux (fvarId : FVarId) (ofNat : Nat → α) (ofNatName : Name) : CompilerM (Option α) := do
+private partial def getLitAux [Inhabited α] (fvarId : FVarId) (ofNat : Nat → α) (ofNatName : Name) : CompilerM (Option α) := do
   let some (.const declName _ #[.fvar fvarId]) ← findLetValue? fvarId | return none
   unless declName == ofNatName do return none
   let some natLit ← getLit fvarId | return none
   return ofNat natLit
 
-def mkNatWrapperInstance (ofNat : Nat → α) (ofNatName : Name) (toNat : α → Nat) : Literal α where
+def mkNatWrapperInstance [Inhabited α] (ofNat : Nat → α) (ofNatName : Name) (toNat : α → Nat) : Literal α where
   getLit := (getLitAux · ofNat ofNatName)
   mkLit x := do
     let helperId ← mkAuxLit <| toNat x
     return .const ofNatName [] #[.fvar helperId]
 
+instance : Literal UInt8 := mkNatWrapperInstance UInt8.ofNat ``UInt8.ofNat UInt8.toNat
+instance : Literal UInt16 := mkNatWrapperInstance UInt16.ofNat ``UInt16.ofNat UInt16.toNat
+instance : Literal UInt32 := mkNatWrapperInstance UInt32.ofNat ``UInt32.ofNat UInt32.toNat
+instance : Literal UInt64 := mkNatWrapperInstance UInt64.ofNat ``UInt64.ofNat UInt64.toNat
 instance : Literal Char := mkNatWrapperInstance Char.ofNat ``Char.ofNat Char.toNat
 
-def mkUIntInstance (matchLit : LitValue → Option α) (litValueCtor : α → LitValue) : Literal α where
-  getLit fvarId := do
-    let some (.lit litVal) ← findLetValue? fvarId | return none
-    return matchLit litVal
-  mkLit x :=
-    return .lit <| litValueCtor x
-
-instance : Literal UInt8 := mkUIntInstance (fun | .uint8 x => some x | _ => none) .uint8
-instance : Literal UInt16 := mkUIntInstance (fun | .uint16 x => some x | _ => none) .uint16
-instance : Literal UInt32 := mkUIntInstance (fun | .uint32 x => some x | _ => none) .uint32
-instance : Literal UInt64 := mkUIntInstance (fun | .uint64 x => some x | _ => none) .uint64
-
 end Literals
 
 /--
@@ -394,7 +386,7 @@ def relationFolders : List (Name × Folder) := [
   (``UInt64.decLt, Folder.mkBinaryDecisionProcedure UInt64.decLt),
   (``UInt64.decLe, Folder.mkBinaryDecisionProcedure UInt64.decLe),
   (``Bool.decEq, Folder.mkBinaryDecisionProcedure Bool.decEq),
-  (``String.decEq, Folder.mkBinaryDecisionProcedure String.decEq)
+  (``Bool.decEq, Folder.mkBinaryDecisionProcedure String.decEq)
 ]
 
 def conversionFolders : List (Name × Folder) := [

src/Lean/Compiler/LCNF/Visibility.lean

@@ -57,21 +57,20 @@ partial def markDeclPublicRec (phase : Phase) (decl : Decl) : CompilerM Unit :=
             markDeclPublicRec phase refDecl
 
 /-- Checks whether references in the given declaration adhere to phase distinction. -/
-partial def checkMeta (origDecl : Decl) : CompilerM Unit := do
+partial def checkMeta (isMeta : Bool) (origDecl : Decl) : CompilerM Unit := do
   if !(← getEnv).header.isModule then
     return
-  let isMeta := isMeta (← getEnv) origDecl.name
   -- If the meta decl is public, we want to ensure it can only refer to public meta imports so that
   -- references to private imports cannot escape the current module. In particular, we check that
   -- decls with relevant global attrs are public (`Lean.ensureAttrDeclIsMeta`).
   let isPublic := !isPrivateName origDecl.name
-  go isMeta isPublic origDecl |>.run' {}
-where go (isMeta isPublic : Bool) (decl : Decl) : StateT NameSet CompilerM Unit := do
+  go isPublic origDecl |>.run' {}
+where go (isPublic : Bool) (decl : Decl) : StateT NameSet CompilerM Unit := do
   decl.value.forCodeM fun code =>
     for ref in collectUsedDecls code do
       if (← get).contains ref then
         continue
-      modify (·.insert ref)
+      modify (·.insert decl.name)
       if isMeta && isPublic then
         if let some modIdx := (← getEnv).getModuleIdxFor? ref then
           if (← getEnv).header.modules[modIdx]?.any (!·.isExported) then
@@ -86,7 +85,7 @@ where go (isMeta isPublic : Bool) (decl : Decl) : StateT NameSet CompilerM Unit
         -- *their* references in this case. We also need to do this for non-auxiliary defs in case a
         -- public meta def tries to use a private meta import via a local private meta def :/ .
         if let some refDecl ← getLocalDecl? ref then
-          go isMeta isPublic refDecl
+          go isPublic refDecl
 
 /--
 Checks meta availability just before `evalConst`. This is a "last line of defense" as accesses
@@ -105,48 +104,13 @@ where go (decl : Decl) : StateT NameSet (Except String) Unit :=
     for ref in collectUsedDecls code do
       if (← get).contains ref then
         continue
-      modify (·.insert ref)
+      modify (·.insert decl.name)
       if let some localDecl := baseExt.getState env |>.find? ref then
         go localDecl
       else
         if getIRPhases env ref == .runtime then
           throw s!"Cannot evaluate constant `{declName}` as it uses `{ref}` which is neither marked nor imported as `meta`"
 
-/--
-Checks that imports necessary for inlining/specialization are public as otherwise we may run into
-unknown declarations at the point of inlining/specializing. This is a limitation that we want to
-lift in the future by moving main compilation into a different process that can use a different
-import/incremental system.
--/
-partial def checkTemplateVisibility : Pass where
-  occurrence := 0
-  phase := .base
-  name := `checkTemplateVisibility
-  run decls := do
-    if (← getEnv).header.isModule then
-      for decl in decls do
-        -- A private template-like decl cannot directly be used by a different module. If it could be used
-        -- indirectly via a public template-like, we do a recursive check when checking the latter.
-        if !isPrivateName decl.name && (← decl.isTemplateLike) then
-          let isMeta := isMeta (← getEnv) decl.name
-          go isMeta decl decl |>.run' {}
-    return decls
-where go (isMeta : Bool) (origDecl decl : Decl) : StateT NameSet CompilerM Unit := do
-  decl.value.forCodeM fun code =>
-    for ref in collectUsedDecls code do
-      if (← get).contains ref then
-        continue
-      modify (·.insert decl.name)
-      if let some localDecl := baseExt.getState (← getEnv) |>.find? ref then
-        -- check transitively through local decls
-        if isPrivateName localDecl.name && (← localDecl.isTemplateLike) then
-          go isMeta origDecl localDecl
-      else if let some modIdx := (← getEnv).getModuleIdxFor? ref then
-        if (← getEnv).header.modules[modIdx]?.any (!·.isExported) then
-          throwError "Cannot compile inline/specializing declaration `{.ofConstName origDecl.name}` as \
-            it uses `{.ofConstName ref}` of module `{(← getEnv).header.moduleNames[modIdx]!}` \
-            which must be imported publicly. This limitation may be lifted in the future."
-
 def inferVisibility (phase : Phase) : Pass where
   occurrence := 0
   phase

src/Lean/Data/Array.lean

@@ -8,8 +8,8 @@ module
 prelude
 public import Init.Prelude
 import Init.Data.Stream
-public import Init.Data.Range.Polymorphic.Nat
-public import Init.Data.Range.Polymorphic.Iterators
+import Init.Data.Range.Polymorphic.Nat
+import Init.Data.Range.Polymorphic.Iterators
 
 namespace Array
 

src/Lean/Data/Lsp/Utf16.lean

@@ -94,10 +94,6 @@ def utf8PosToLspPos (text : FileMap) (pos : String.Pos) : Lsp.Position :=
 def utf8RangeToLspRange (text : FileMap) (range : String.Range) : Lsp.Range :=
   { start := text.utf8PosToLspPos range.start, «end» := text.utf8PosToLspPos range.stop }
 
-/-- Gets the LSP range of syntax `stx`. -/
-def lspRangeOfStx? (text : FileMap) (stx : Syntax) (canonicalOnly := false) : Option Lsp.Range :=
-  text.utf8RangeToLspRange <$> stx.getRange? canonicalOnly
-
 def lspRangeToUtf8Range (text : FileMap) (range : Lsp.Range) : String.Range :=
   { start := text.lspPosToUtf8Pos range.start, stop := text.lspPosToUtf8Pos range.end }
 

src/Lean/Data/NameMap.lean

@@ -8,3 +8,5 @@ module
 prelude
 public import Lean.Data.NameMap.Basic
 public import Lean.Data.NameMap.AdditionalOperations
+
+public section

src/Lean/DocString/Add.lean

@@ -14,7 +14,7 @@ import Lean.Elab.DocString
 import Lean.DocString.Extension
 import Lean.DocString.Links
 import Lean.Parser.Types
-public import Lean.DocString.Parser
+import Lean.DocString.Parser
 import Lean.ResolveName
 public import Lean.Elab.Term.TermElabM
 import Std.Data.HashMap
@@ -50,20 +50,23 @@ def validateDocComment
     else
       logError err
 
-open Lean.Parser Command in
-/--
-Parses a docstring as Verso, returning the syntax if successful.
 
-When not successful, parser errors are logged.
+open Lean.Doc in
+open Parser in
+/--
+Adds a Verso docstring to the specified declaration, which should already be present in the
+environment.
+
+`binders` should be the syntax of the parameters to the constant that is being documented, as a null
+node that contains a sequence of bracketed binders. It is used to allow interactive features such as
+document highlights and “find references” to work for documented parameters. If no parameter binders
+are available, pass `Syntax.missing` or an empty null node.
+
 -/
-def parseVersoDocString
-    [Monad m] [MonadFileMap m] [MonadError m] [MonadEnv m] [MonadOptions m] [MonadLog m]
-    [MonadResolveName m]
-    (docComment : TSyntax [``docComment, ``moduleDoc]) : m (Option Syntax) := do
-  if docComment.raw.getKind == ``docComment then
-    match docComment.raw[0] with
-    | docStx@(.node _ ``versoCommentBody _) => return docStx[1]?
-    | _ => pure ()
+def versoDocString
+    (declName : Name) (binders : Syntax) (docComment : TSyntax `Lean.Parser.Command.docComment) :
+    TermElabM (Array (Doc.Block ElabInline ElabBlock) × Array (Doc.Part ElabInline ElabBlock Empty)) := do
+
   let text ← getFileMap
   -- TODO fallback to string version without nice interactivity
   let some startPos := docComment.raw[1].getPos? (canonicalOnly := true)
@@ -90,7 +93,7 @@ def parseVersoDocString
   }
   let s := mkParserState text.source |>.setPos startPos
   -- TODO parse one block at a time for error recovery purposes
-  let s := Doc.Parser.document.run ictx pmctx (getTokenTable env) s
+  let s := (Doc.Parser.document).run ictx pmctx (getTokenTable env) s
 
   if !s.allErrors.isEmpty then
     for (pos, _, err) in s.allErrors do
@@ -100,42 +103,11 @@ def parseVersoDocString
         -- TODO end position
         data := err.toString
       }
-    return none
-  return some s.stxStack.back
-
-
-
-open Lean.Doc in
-open Lean.Parser.Command in
-/--
-Elaborates a Verso docstring for the specified declaration, which should already be present in the
-environment.
-
-`binders` should be the syntax of the parameters to the constant that is being documented, as a null
-node that contains a sequence of bracketed binders. It is used to allow interactive features such as
-document highlights and “find references” to work for documented parameters. If no parameter binders
-are available, pass `Syntax.missing` or an empty null node.
--/
-
-def versoDocString
-    (declName : Name) (binders : Syntax) (docComment : TSyntax ``docComment) :
-    TermElabM (Array (Doc.Block ElabInline ElabBlock) × Array (Doc.Part ElabInline ElabBlock Empty)) := do
-  if let some stx ← parseVersoDocString docComment then
-    Doc.elabBlocks (stx.getArgs.map (⟨·⟩)) |>.exec declName binders
-  else return (#[], #[])
-
-open Lean.Doc Parser in
-open Lean.Parser.Command in
-/--
-Parses and elaborates a Verso module docstring.
--/
-def versoModDocString
-    (range : DeclarationRange) (doc : TSyntax ``document) :
-    TermElabM VersoModuleDocs.Snippet := do
-  let level := getVersoModuleDocs (← getEnv) |>.terminalNesting |>.map (· + 1)
-  Doc.elabModSnippet range (doc.raw.getArgs.map (⟨·⟩)) (level.getD 0) |>.execForModule
-
-
+    return (#[], #[])
+  else
+    let stx := s.stxStack.back
+    let stx := stx.getArgs
+    Doc.elabBlocks (stx.map (⟨·⟩)) |>.exec declName binders
 
 open Lean.Doc in
 open Parser in
@@ -159,7 +131,7 @@ def versoDocStringFromString
   }
   let s := mkParserState docComment
   -- TODO parse one block at a time for error recovery purposes
-  let s := Doc.Parser.document.run ictx pmctx (getTokenTable env) s
+  let s := (Doc.Parser.document).run ictx pmctx (getTokenTable env) s
 
   if !s.allErrors.isEmpty then
     for (pos, _, err) in s.allErrors do
@@ -213,19 +185,6 @@ def addVersoDocStringCore [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] [MonadErr
   modifyEnv fun env =>
     versoDocStringExt.insert env declName docs
 
-/--
-Adds an elaborated Verso module docstring to the environment.
--/
-def addVersoModDocStringCore [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] [MonadError m]
-  (docs : VersoModuleDocs.Snippet) : m Unit := do
-  if (getMainModuleDoc (← getEnv)).isEmpty then
-    match addVersoModuleDocSnippet (← getEnv) docs with
-    | .error e => throwError "Error adding module docs: {indentD <| toMessageData e}"
-    | .ok env' => setEnv env'
-  else
-    throwError m!"Can't add Verso-format module docs because there is already Markdown-format content present."
-
-open Lean.Parser.Command in
 /--
 Adds a Verso docstring to the environment.
 
@@ -235,7 +194,7 @@ document highlights and “find references” to work for documented parameters.
 are available, pass `Syntax.missing` or an empty null node.
 -/
 def addVersoDocString
-    (declName : Name) (binders : Syntax) (docComment : TSyntax ``docComment) :
+    (declName : Name) (binders : Syntax) (docComment : TSyntax `Lean.Parser.Command.docComment) :
     TermElabM Unit := do
   unless (← getEnv).getModuleIdxFor? declName |>.isNone do
     throwError s!"invalid doc string, declaration '{declName}' is in an imported module"
@@ -319,20 +278,3 @@ def addDocString'
   match docString? with
   | some docString => addDocString declName binders docString
   | none => return ()
-
-
-open Lean.Parser.Command in
-open Lean.Doc.Parser in
-/--
-Adds a Verso docstring to the environment.
-
-`binders` should be the syntax of the parameters to the constant that is being documented, as a null
-node that contains a sequence of bracketed binders. It is used to allow interactive features such as
-document highlights and “find references” to work for documented parameters. If no parameter binders
-are available, pass `Syntax.missing` or an empty null node.
--/
-def addVersoModDocString
-    (range : DeclarationRange) (docComment : TSyntax ``document) :
-    TermElabM Unit := do
-  let snippet ← versoModDocString range docComment
-  addVersoModDocStringCore snippet

src/Lean/DocString/Extension.lean

@@ -12,7 +12,7 @@ public import Lean.DocString.Links
 public import Lean.MonadEnv
 public import Init.Data.String.Extra
 public import Lean.DocString.Types
-public import Lean.DocString.Markdown
+import Lean.DocString.Markdown
 
 public section
 
@@ -38,7 +38,7 @@ instance : Repr ElabInline where
       .group (.nestD ("{ name :=" ++ .line ++ repr v.name)) ++ .line ++
       .group (.nestD ("val :=" ++ .line ++ "Dynamic.mk " ++ repr v.val.typeName ++ " _ }"))
 
-instance : Doc.MarkdownInline ElabInline where
+private instance : Doc.MarkdownInline ElabInline where
   -- TODO extensibility
   toMarkdown go _i content := content.forM go
 
@@ -59,7 +59,7 @@ instance : Repr ElabBlock where
 
 
 -- TODO extensible toMarkdown
-instance : Doc.MarkdownBlock ElabInline ElabBlock where
+private instance : Doc.MarkdownBlock ElabInline ElabBlock where
   toMarkdown _goI goB _b content := content.forM goB
 
 structure VersoDocString where
@@ -214,211 +214,5 @@ def getModuleDoc? (env : Environment) (moduleName : Name) : Option (Array Module
 
 def getDocStringText [Monad m] [MonadError m] (stx : TSyntax `Lean.Parser.Command.docComment) : m String :=
   match stx.raw[1] with
-  | Syntax.atom _ val =>
-    return val.extract 0 (val.endPos - ⟨2⟩)
-  | Syntax.node _ `Lean.Parser.Command.versoCommentBody _ =>
-    match stx.raw[1][0] with
-    | Syntax.atom _ val =>
-      return val.extract 0 (val.endPos - ⟨2⟩)
-    | _ =>
-      throwErrorAt stx "unexpected doc string{indentD stx}"
-  | _ =>
-    throwErrorAt stx "unexpected doc string{indentD stx}"
-
-
-
-/--
-A snippet of a Verso module text.
-
-A snippet consists of text followed by subsections. Because the sequence of snippets that occur in a
-source file are conceptually a single document, they have a consistent header nesting structure.
-This means that initial textual content of a snippet is a continuation of the text at the end of the
-prior snippet.
-
-The actual hierarchical structure of the document is reconstructed from the sequence of snippets.
-
-The _terminal nesting_ of a sequence of snippets is 0 if there are no sections in the sequence.
-Otherwise, it is one greater than the nesting of the last snippet's last section. The module
-docstring elaborator maintains the invariant that each snippet's first section's level is at most
-the terminal nesting of the preceding snippets, and that the level of each section within a snippet
-is at most one greater than the preceding section's level.
--/
-structure VersoModuleDocs.Snippet where
-  /-- Text to be inserted after the prior snippet's ending text. -/
-  text : Array (Doc.Block ElabInline ElabBlock) := #[]
-  /--
-  A sequence of parts with their absolute document nesting levels and header positions.
-  None of these parts may contain sub-parts.
-  -/
-  sections : Array (Nat × DeclarationRange × Doc.Part ElabInline ElabBlock Empty) := #[]
-  /--
-  The location of the snippet in the source file.
-  -/
-  declarationRange : DeclarationRange
-deriving Inhabited, Repr
-
-namespace VersoModuleDocs.Snippet
-
-def canNestIn (level : Nat) (snippet : Snippet) : Bool :=
-  if let some s := snippet.sections[0]? then s.1 ≤ level + 1 else true
-
-def terminalNesting (snippet : Snippet) : Option Nat :=
-  if let some s := snippet.sections.back? then s.1
-  else none
-
-def addBlock (snippet : Snippet) (block : Doc.Block ElabInline ElabBlock) : Snippet :=
-  if h : snippet.sections.size = 0 then
-    { snippet with text := snippet.text.push block }
-  else
-    { snippet with
-      sections[snippet.sections.size - 1].2.2.content :=
-        snippet.sections[snippet.sections.size - 1].2.2.content.push block }
-
-def addPart (snippet : Snippet) (level : Nat) (range : DeclarationRange) (part : Doc.Part ElabInline ElabBlock Empty) : Snippet :=
-  { snippet with
-    sections := snippet.sections.push (level, range, part) }
-
-end VersoModuleDocs.Snippet
-
-open Lean Doc ToMarkdown MarkdownM in
-instance : ToMarkdown VersoModuleDocs.Snippet where
-  toMarkdown
-    | {text, sections, ..} => do
-      text.forM toMarkdown
-      endBlock
-      for (level, _, part) in sections do
-        push ("".pushn '#' (level + 1))
-        push " "
-        for i in part.title do toMarkdown i
-        endBlock
-        for b in part.content do toMarkdown b
-        endBlock
-
-structure VersoModuleDocs where
-  snippets : PersistentArray VersoModuleDocs.Snippet := {}
-  terminalNesting : Option Nat := snippets.findSomeRev? (·.terminalNesting)
-deriving Inhabited
-
-instance : Repr VersoModuleDocs where
-  reprPrec v _ :=
-    .group <| .nest 2 <|
-      "{ " ++
-      (.group <| .nest 2 <| "snippets := " ++ .line ++ repr v.snippets.toArray) ++ .line ++
-      (.group <| .nest 2 <| "snippets := " ++ .line ++ repr v.snippets.toArray) ++
-      " }"
-
-namespace VersoModuleDocs
-
-def isEmpty (docs : VersoModuleDocs) : Bool := docs.snippets.isEmpty
-
-def canAdd (docs : VersoModuleDocs) (snippet : Snippet) : Bool :=
-  if let some level := docs.terminalNesting then
-    snippet.canNestIn level
-  else true
-
-
-def add (docs : VersoModuleDocs) (snippet : Snippet) : Except String VersoModuleDocs := do
-  unless docs.canAdd snippet do
-    throw "Can't nest this snippet here"
-
-  return { docs with
-    snippets := docs.snippets.push snippet,
-    terminalNesting := snippet.terminalNesting
-  }
-
-def add! (docs : VersoModuleDocs) (snippet : Snippet) : VersoModuleDocs :=
-  let ok :=
-    if let some level := docs.terminalNesting then
-      snippet.canNestIn level
-    else true
-  if not ok then
-    panic! "Can't nest this snippet here"
-  else
-    { docs with
-      snippets := docs.snippets.push snippet,
-      terminalNesting := snippet.terminalNesting
-    }
-
-
-private structure DocFrame where
-  content : Array (Doc.Block ElabInline ElabBlock)
-  priorParts : Array (Doc.Part ElabInline ElabBlock Empty)
-  titleString : String
-  title : Array (Doc.Inline ElabInline)
-
-private structure DocContext where
-  content : Array (Doc.Block ElabInline ElabBlock)
-  priorParts : Array (Doc.Part ElabInline ElabBlock Empty)
-  context : Array DocFrame
-
-private def DocContext.level (ctx : DocContext) : Nat := ctx.context.size
-
-private def DocContext.close (ctx : DocContext) : Except String DocContext := do
-  if h : ctx.context.size = 0 then
-    throw "Can't close a section: none are open"
-  else
-    let last := ctx.context.back
-    pure {
-      content := last.content,
-      priorParts := last.priorParts.push {
-        title := last.title,
-        titleString := last.titleString,
-        metadata := none,
-        content := ctx.content,
-        subParts := ctx.priorParts,
-      },
-      context := ctx.context.pop
-    }
-
-private partial def DocContext.closeAll (ctx : DocContext) : Except String DocContext := do
-  if ctx.context.size = 0 then
-    return ctx
-  else
-    (← ctx.close).closeAll
-
-private partial def DocContext.addPart (ctx : DocContext) (partLevel : Nat) (part : Doc.Part ElabInline ElabBlock Empty) : Except String DocContext := do
-  if partLevel > ctx.level then throw s!"Invalid nesting: expected at most {ctx.level} but got {partLevel}"
-  else if partLevel = ctx.level then pure { ctx with priorParts := ctx.priorParts.push part }
-  else
-    let ctx ← ctx.close
-    ctx.addPart partLevel part
-
-private def DocContext.addBlocks (ctx : DocContext) (blocks : Array (Doc.Block ElabInline ElabBlock)) : Except String DocContext := do
-  if ctx.priorParts.isEmpty then pure { ctx with content := ctx.content ++ blocks }
-  else throw "Can't add content after sub-parts"
-
-private def DocContext.addSnippet (ctx : DocContext) (snippet : Snippet) : Except String DocContext := do
-  let mut ctx ← ctx.addBlocks snippet.text
-  for (l, _, p) in snippet.sections do
-    ctx ← ctx.addPart l p
-  return ctx
-
-def assemble (docs : VersoModuleDocs) : Except String VersoDocString := do
-  let mut ctx : DocContext := {content := #[], priorParts := #[], context := #[]}
-  for snippet in docs.snippets do
-    ctx ← ctx.addSnippet snippet
-  ctx ← ctx.closeAll
-  return { text := ctx.content, subsections := ctx.priorParts }
-
-end VersoModuleDocs
-
-private builtin_initialize versoModuleDocExt :
-    SimplePersistentEnvExtension VersoModuleDocs.Snippet VersoModuleDocs ← registerSimplePersistentEnvExtension {
-  addImportedFn := fun _ => {}
-  addEntryFn    := fun s e => s.add! e
-  exportEntriesFnEx? := some fun _ _ es level =>
-    if level < .server then
-      #[]
-    else
-      es.toArray
-}
-
-
-def getVersoModuleDocs (env : Environment) : VersoModuleDocs :=
-  versoModuleDocExt.getState env
-
-def addVersoModuleDocSnippet (env : Environment) (snippet : VersoModuleDocs.Snippet) : Except String Environment :=
-  let docs := getVersoModuleDocs env
-  if docs.canAdd snippet then
-    pure <| versoModuleDocExt.addEntry env snippet
-  else throw s!"Can't add - incorrect nesting {docs.terminalNesting.map (s!"(expected at most {·})") |>.getD ""})"
+  | Syntax.atom _ val => return val.extract 0 (val.endPos - ⟨2⟩)
+  | _                 => throwErrorAt stx "unexpected doc string{indentD stx.raw[1]}"

src/Lean/DocString/Formatter.lean

@@ -1,224 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: David Thrane Christiansen
--/
-
-module
-prelude
-public import Lean.PrettyPrinter.Formatter
-import Lean.DocString.Syntax
-
-
-namespace Lean.Doc.Parser
-
-open Lean.PrettyPrinter Formatter
-open Lean.Syntax.MonadTraverser
-
-open Lean.Doc.Syntax
-
-def atomString : Syntax → String
-  | .node _ _ #[x] => atomString x
-  | .atom _ x => x
-  | stx => s!"NON-ATOM {stx}"
-
-def pushAtomString : Formatter := do
-  push <| atomString (← getCur)
-  goLeft
-
-def pushAtomStrLit : Formatter := do
-  push <| (Syntax.decodeStrLit (atomString (← getCur))).getD ""
-  goLeft
-
-
-def identString : Syntax → String
-  | .node _ _ #[x] => identString x
-  | .ident _ _ x _ => toString x
-  | stx => s!"NON-IDENT {stx}"
-
-def pushIdent : Formatter := do
-  push <| identString (← getCur)
-  goLeft
-
-def rep (f : Formatter) : Formatter := concat do
-  let count := (← getCur).getArgs.size
-  visitArgs do count.forM fun _ _ => do f
-
-partial def versoSyntaxToString' (stx : Syntax) : ReaderT Nat (StateM String) Unit := do
-  if stx.getKind == nullKind then
-    stx.getArgs.forM versoSyntaxToString'
-  else
-    match stx with
-    | `(arg_val|$s:str) => out <| atomString s
-    | `(arg_val|$n:num) => out <| atomString n
-    | `(arg_val|$x:ident) => out <| identString x
-    | `(doc_arg|($x := $v)) | `(doc_arg|$x:ident := $v) =>
-      out "("
-      out <| identString x
-      out " := "
-      versoSyntaxToString' v
-      out ")"
-    | `(doc_arg|+%$tk$x:ident) | `(doc_arg|-%$tk$x:ident) =>
-      out <| atomString tk
-      out <| identString x
-    | `(doc_arg|$x:arg_val) => versoSyntaxToString' x
-    | `(inline|$s:str) => out s.getString
-    | `(inline|_[%$tk1 $inl* ]%$tk2) | `(inline|*[%$tk1 $inl* ]%$tk2) =>
-      out <| atomString tk1
-      inl.forM versoSyntaxToString'
-      out <| atomString tk2
-    | `(inline|link[%$tk1 $inl* ]%$tk2 $tgt) =>
-      out <| atomString tk1
-      inl.forM versoSyntaxToString'
-      out <| atomString tk2
-      versoSyntaxToString' tgt
-    | `(inline|image(%$tk1 $alt )%$tk2 $tgt) =>
-      out <| atomString tk1
-      out <| (Syntax.decodeStrLit (atomString alt)).getD ""
-      out <| atomString tk2
-      versoSyntaxToString' tgt
-    | `(inline|role{$name $args*}[$inls*]) =>
-      out "{"
-      out <| identString name
-      for arg in args do
-        out " "
-        versoSyntaxToString' arg
-      out "}["
-      inls.forM versoSyntaxToString'
-      out "]"
-    | `(inline|code(%$tk1$s)%$tk2) =>
-      out <| atomString tk1
-      out <| (Syntax.decodeStrLit (atomString s)).getD ""
-      out <| atomString tk2
-    | `(inline|footnote(%$tk1 $ref )%$tk2) =>
-      out <| atomString tk1
-      out <| (Syntax.decodeStrLit (atomString ref)).getD ""
-      out <| atomString tk2
-    | `(inline|line! $s) =>
-      out <| (Syntax.decodeStrLit (atomString s)).getD ""
-    | `(inline|\math%$tk1 code(%$tk2 $s )%$tk3)
-    | `(inline|\displaymath%$tk1 code(%$tk2 $s )%$tk3) =>
-      out <| atomString tk1
-      out <| atomString tk2
-      out <| (Syntax.decodeStrLit (atomString s)).getD ""
-      out <| atomString tk3
-    | `(link_target|[%$tk1 $ref ]%$tk2) =>
-      out <| atomString tk1
-      out <| (Syntax.decodeStrLit (atomString ref)).getD ""
-      out <| atomString tk2
-    | `(link_target|(%$tk1 $url )%$tk2) =>
-      out <| atomString tk1
-      out <| (Syntax.decodeStrLit (atomString url)).getD ""
-      out <| atomString tk2
-    | `(block|header($n){$inl*}) =>
-      out <| "#".pushn '#' n.getNat ++ " "
-      inl.forM versoSyntaxToString'
-      endBlock
-    | `(block|para[$inl*]) =>
-      startBlock
-      inl.forM versoSyntaxToString'
-      endBlock
-    | `(block|ul{$items*}) =>
-      startBlock
-      items.forM fun
-        | `(list_item|* $blks*) => do
-          out "* "
-          withReader (· + 2) (blks.forM versoSyntaxToString')
-          endBlock
-        | _ => pure ()
-      endBlock
-    | `(block|ol($n){$items*}) =>
-      startBlock
-      let mut n := n.getNat
-      for item in items do
-        match item with
-        | `(list_item|* $blks*) => do
-          out s!"{n}. "
-          withReader (· + 2) (blks.forM versoSyntaxToString')
-          endBlock
-          n := n + 1
-        | _ => pure ()
-      endBlock
-    | `(block| > $blks*) =>
-      startBlock
-      out "> "
-      withReader (· + 2) (blks.forM versoSyntaxToString')
-      endBlock
-    | `(block| ```%$tk1 $name $args* | $s ```%$tk2) =>
-      startBlock
-      out <| atomString tk1
-      out <| identString name
-      for arg in args do
-        out " "
-        versoSyntaxToString' arg
-      out "\n"
-      let i ← read
-      let s := Syntax.decodeStrLit (atomString s) |>.getD ""
-        |>.split (· == '\n')
-        |>.map ("".pushn ' ' i ++ · ) |> "\n".intercalate
-      out s
-      out <| "".pushn ' ' i
-      out <| atomString tk2
-      endBlock
-    | `(block| :::%$tk1 $name $args* {$blks*}%$tk2) =>
-      startBlock
-      out <| atomString tk1
-      out " "
-      out <| identString name
-      for arg in args do
-        out " "
-        versoSyntaxToString' arg
-      out "\n"
-      blks.forM versoSyntaxToString'
-      let i ← read
-      out <| "".pushn ' ' i
-      out <| atomString tk2
-      endBlock
-    | `(block|command{ $name $args* }) =>
-      startBlock
-      out <| "{"
-      out <| identString name
-      for arg in args do
-        out " "
-        versoSyntaxToString' arg
-      out "}"
-      endBlock
-
-    | other => out (toString other)
-where
-  out (s : String) : ReaderT Nat (StateM String) Unit := modify (· ++ s)
-  nl : ReaderT Nat (StateM String) Unit := read >>= fun n => modify (· ++ "\n".pushn ' ' n)
-  startBlock : ReaderT Nat (StateM String) Unit := do
-    let s ← get
-    if s.endsWith "\n" then
-      let i ← read
-      out ("".pushn ' ' i)
-  endBlock : ReaderT Nat (StateM String) Unit := do
-    let s ← get
-    if s.endsWith "\n\n" then return
-    else if s.endsWith "\n" then out "\n"
-    else out "\n\n"
-
-def formatMetadata : Formatter := do
-  visitArgs do
-    pushLine
-    visitAtom .anonymous
-    pushLine
-    metadataContents.formatter
-    pushLine
-    visitAtom .anonymous
-
-def versoSyntaxToString (stx : Syntax) : String :=
-  versoSyntaxToString' stx |>.run 0 |>.run "" |>.2
-
-public def document.formatter : Formatter := concat do
-  let stx ← getCur
-  let i := stx.getArgs.size
-  visitArgs do
-    for _ in [0:i] do
-      let blk ← getCur
-      if blk.getKind == ``Doc.Syntax.metadata_block then
-        formatMetadata
-      else
-        push (versoSyntaxToString blk)
-        goLeft

src/Lean/DocString/Markdown.lean

@@ -85,20 +85,11 @@ Generates Markdown, rendering the result from the final state, without producing
 public def MarkdownM.run' (act : MarkdownM Unit) (context : Context := {}) (state : State := {}) : String :=
   act.run context state |>.2
 
-/--
-Adds a string to the current Markdown output.
--/
-public def MarkdownM.push (txt : String) : MarkdownM Unit := modify (·.push txt)
+private def MarkdownM.push (txt : String) : MarkdownM Unit := modify (·.push txt)
 
-/--
-Terminates the current block.
--/
-public def MarkdownM.endBlock : MarkdownM Unit := modify (·.endBlock)
+private def MarkdownM.endBlock : MarkdownM Unit := modify (·.endBlock)
 
-/--
-Increases the indentation level by one.
--/
-public def MarkdownM.indent: MarkdownM α → MarkdownM α :=
+private def MarkdownM.indent: MarkdownM α → MarkdownM α :=
   withReader fun st => { st with linePrefix := st.linePrefix ++ "  " }
 
 /--
@@ -168,41 +159,6 @@ private def quoteCode (str : String) : String := Id.run do
   let str := if str.startsWith "`" || str.endsWith "`" then " " ++ str ++ " " else str
   backticks ++ str ++ backticks
 
-private partial def trimLeft (inline : Inline i) : (String × Inline i) := go [inline]
-where
-  go : List (Inline i) → String × Inline i
-    | [] => ("", .empty)
-    | .text s :: more =>
-      if s.all (·.isWhitespace) then
-        let (pre, post) := go more
-        (s ++ pre, post)
-      else
-        let s1 := s.takeWhile (·.isWhitespace)
-        let s2 := s.drop s1.length
-        (s1, .text s2 ++ .concat more.toArray)
-    | .concat xs :: more => go (xs.toList ++ more)
-    | here :: more => ("", here ++ .concat more.toArray)
-
-private partial def trimRight (inline : Inline i) : (Inline i × String) := go [inline]
-where
-  go : List (Inline i) → Inline i × String
-    | [] => (.empty, "")
-    | .text s :: more =>
-      if s.all (·.isWhitespace) then
-        let (pre, post) := go more
-        (pre, post ++ s)
-      else
-        let s1 := s.takeRightWhile (·.isWhitespace)
-        let s2 := s.dropRight s1.length
-        (.concat more.toArray.reverse ++ .text s2, s1)
-    | .concat xs :: more => go (xs.reverse.toList ++ more)
-    | here :: more => (.concat more.toArray.reverse ++ here, "")
-
-private def trim (inline : Inline i) : (String × Inline i × String) :=
-  let (pre, more) := trimLeft inline
-  let (mid, post) := trimRight more
-  (pre, mid, post)
-
 open MarkdownM in
 private partial def inlineMarkdown [MarkdownInline i] : Inline i → MarkdownM Unit
   | .text s =>
@@ -210,25 +166,19 @@ private partial def inlineMarkdown [MarkdownInline i] : Inline i → MarkdownM U
   | .linebreak s => do
     push <| s.replace "\n" ("\n" ++ (← read).linePrefix )
   | .emph xs => do
-    let (pre, mid, post) := trim (.concat xs)
-    push pre
     unless (← read).inEmph do
       push "*"
     withReader (fun ρ => { ρ with inEmph := true }) do
-      inlineMarkdown mid
+      for i in xs do inlineMarkdown i
     unless (← read).inEmph do
       push "*"
-    push post
   | .bold xs => do
-    let (pre, mid, post) := trim (.concat xs)
-    push pre
     unless (← read).inBold do
       push "**"
     withReader (fun ρ => { ρ with inEmph := true }) do
-      inlineMarkdown mid
+      for i in xs do inlineMarkdown i
     unless (← read).inBold do
       push "**"
-    push post
   | .concat xs =>
     for i in xs do inlineMarkdown i
   | .link content url => do

src/Lean/DocString/Parser.lean

@@ -7,8 +7,6 @@ module
 prelude
 public import Lean.Parser.Types
 public import Lean.DocString.Syntax
-import Lean.PrettyPrinter.Formatter
-import Lean.Parser.Term.Basic
 
 set_option linter.missingDocs true
 
@@ -233,16 +231,6 @@ public def fakeAtom (str : String) (info : SourceInfo := SourceInfo.none) : Pars
   let atom := .atom info str
   s.pushSyntax atom
 
-/--
-Construct a “fake” atom with the given string content, with zero-width source information at the
-current position.
-
-Normally, atoms are always substrings of the original input; however, Verso's concrete syntax is
-different enough from Lean's that this isn't always a good match.
--/
-private def fakeAtomHere (str : String) : ParserFn :=
-  withInfoSyntaxFn skip.fn (fun info => fakeAtom str (info := info))
-
 private def pushMissing : ParserFn := fun _c s =>
   s.pushSyntax .missing
 
@@ -598,7 +586,7 @@ A linebreak that isn't a block break (that is, there's non-space content on the
 def linebreak (ctxt : InlineCtxt) : ParserFn :=
   if ctxt.allowNewlines then
     nodeFn ``linebreak <|
-      andthenFn (fakeAtomHere "line!") <|
+      andthenFn (withInfoSyntaxFn skip.fn (fun info => fakeAtom "line!" info)) <|
         nodeFn strLitKind <|
         asStringFn (quoted := true) <|
           atomicFn (chFn '\n' >> lookaheadFn (manyFn (chFn ' ') >> notFollowedByFn (chFn '\n' <|> blockOpener) "newline"))
@@ -807,9 +795,6 @@ open Lean.Parser.Term in
 def metadataContents : Parser :=
   structInstFields (sepByIndent structInstField ", " (allowTrailingSep := true))
 
-def withPercents : ParserFn → ParserFn := fun p =>
-  adaptUncacheableContextFn (fun c => {c with tokens := c.tokens.insert "%%%" "%%%"}) p
-
 open Lean.Parser.Term in
 /--
 Parses a metadata block, which contains the contents of a Lean structure initialization but is
@@ -818,7 +803,8 @@ surrounded by `%%%` on each side.
 public def metadataBlock : ParserFn :=
   nodeFn ``metadata_block <|
     opener >>
-    withPercents metadataContents.fn >>
+    metadataContents.fn >>
+    takeWhileFn (·.isWhitespace) >>
     closer
 where
   opener := atomicFn (bolThen (eatSpaces >> strFn "%%%") "%%% (at line beginning)") >> eatSpaces >> ignoreFn (chFn '\n')
@@ -970,35 +956,35 @@ mutual
     nodeFn ``ul <|
       lookaheadUnorderedListIndicator ctxt fun type =>
         withCurrentColumn fun c =>
-          fakeAtomHere "ul{" >>
+          fakeAtom "ul{" >>
           many1Fn (listItem {ctxt with minIndent := c + 1 , inLists := ⟨c, .inr type⟩  :: ctxt.inLists}) >>
-          fakeAtomHere "}"
+          fakeAtom "}"
 
   /-- Parses an ordered list. -/
   public partial def orderedList (ctxt : BlockCtxt) : ParserFn :=
     nodeFn ``ol <|
-      fakeAtomHere "ol(" >>
+      fakeAtom "ol(" >>
       lookaheadOrderedListIndicator ctxt fun type _start => -- TODO? Validate list numbering?
         withCurrentColumn fun c =>
-          fakeAtomHere ")" >> fakeAtomHere "{" >>
+          fakeAtom ")" >> fakeAtom "{" >>
           many1Fn (listItem {ctxt with minIndent := c + 1 , inLists := ⟨c, .inl type⟩  :: ctxt.inLists}) >>
-          fakeAtomHere "}"
+          fakeAtom "}"
 
   /-- Parses a definition list. -/
   public partial def definitionList (ctxt : BlockCtxt) : ParserFn :=
     nodeFn ``dl <|
       atomicFn (onlyBlockOpeners >> takeWhileFn (· == ' ') >> ignoreFn (lookaheadFn (chFn ':' >> chFn ' ')) >> guardMinColumn ctxt.minIndent) >>
-      fakeAtomHere "dl{" >>
+      withInfoSyntaxFn skip.fn (fun info => fakeAtom "dl{" info) >>
       withCurrentColumn (fun c => many1Fn (descItem {ctxt with minIndent := c})) >>
-      fakeAtomHere "}"
+      withInfoSyntaxFn skip.fn (fun info => fakeAtom "}" info)
 
   /-- Parses a paragraph (that is, a sequence of otherwise-undecorated inlines). -/
   public partial def para (ctxt : BlockCtxt) : ParserFn :=
     nodeFn ``para <|
       atomicFn (takeWhileFn (· == ' ') >> notFollowedByFn blockOpener "block opener" >> guardMinColumn ctxt.minIndent) >>
-      fakeAtomHere "para{" >>
+      withInfoSyntaxFn skip.fn (fun info => fakeAtom "para{" (info := info)) >>
       textLine >>
-      fakeAtomHere "}"
+      withInfoSyntaxFn skip.fn (fun info => fakeAtom "}" (info := info))
 
   /-- Parses a header. -/
   public partial def header (ctxt : BlockCtxt) : ParserFn :=
@@ -1013,7 +999,7 @@ mutual
             fakeAtom ")") >>
       fakeAtom "{" >>
       textLine (allowNewlines := false) >>
-      fakeAtomHere "}"
+      fakeAtom "}"
 
   /--
   Parses a code block. The resulting string literal has already had the fences' leading indentation
@@ -1184,56 +1170,3 @@ mutual
   -/
   public partial def document (blockContext : BlockCtxt := {}) : ParserFn := ignoreFn (manyFn blankLine) >> blocks blockContext
 end
-
-section
-open Lean.PrettyPrinter
-
-/--
-Parses as `ifVerso` if the option `doc.verso` is `true`, or as `ifNotVerso` otherwise.
--/
-public def ifVersoFn (ifVerso ifNotVerso : ParserFn) : ParserFn := fun c s =>
-  if c.options.getBool `doc.verso then ifVerso c s
-  else ifNotVerso c s
-
-@[inherit_doc ifVersoFn]
-public def ifVerso (ifVerso ifNotVerso : Parser) : Parser where
-  fn :=
-    ifVersoFn ifVerso.fn ifNotVerso.fn
-
-/--
-Formatter for `ifVerso`—formats according to the underlying formatters.
--/
-@[combinator_formatter ifVerso, expose]
-public def ifVerso.formatter (f1 f2 : Formatter) : Formatter := f1 <|> f2
-
-/--
-Parenthesizer for `ifVerso`—parenthesizes according to the underlying parenthesizers.
--/
-@[combinator_parenthesizer ifVerso, expose]
-public def ifVerso.parenthesizer (p1 p2 : Parenthesizer) : Parenthesizer := p1 <|> p2
-
-/--
-Disables the option `doc.verso` while running a parser.
--/
-public def withoutVersoSyntax (p : Parser) : Parser where
-  fn :=
-    adaptUncacheableContextFn
-      (fun c => { c with options := c.options.setBool `doc.verso false })
-      p.fn
-  info := p.info
-
-/--
-Formatter for `withoutVersoSyntax`—formats according to the underlying formatter.
--/
-@[combinator_formatter withoutVersoSyntax, expose]
-public def withoutVersoSyntax.formatter (p : Formatter) : Formatter := p
-/--
-Parenthesizer for `withoutVersoSyntax`—parenthesizes according to the underlying parenthesizer.
--/
-@[combinator_parenthesizer withoutVersoSyntax, expose]
-public def withoutVersoSyntax.parenthesizer (p : Parenthesizer) : Parenthesizer := p
-
-end
-
-builtin_initialize
-  register_parser_alias withoutVersoSyntax

src/Lean/DocString/Syntax.lean

@@ -7,8 +7,14 @@ Author: David Thrane Christiansen
 module
 
 prelude
-public import Lean.Parser.Term.Basic
-meta import Lean.Parser.Term.Basic
+
+import Init.Prelude
+import Init.Notation
+public import Lean.Parser.Types
+import Lean.Syntax
+import Lean.Parser.Extra
+public import Lean.Parser.Term
+meta import Lean.Parser.Term
 
 
 /-!
@@ -57,28 +63,22 @@ scoped syntax (name:=arg_num) num : arg_val
 
 /-- Arguments -/
 declare_syntax_cat doc_arg
-/-- Anonymous positional argument -/
-@[builtin_doc]
+/-- Anonymous positional arguments -/
 scoped syntax (name:=anon) arg_val : doc_arg
-/-- Named argument -/
-@[builtin_doc]
+/-- Named arguments -/
 scoped syntax (name:=named) "(" ident " := " arg_val ")": doc_arg
-@[inherit_doc named, builtin_doc]
+/-- Named arguments, without parentheses. -/
 scoped syntax (name:=named_no_paren) ident " := " arg_val : doc_arg
-/-- Boolean flag, turned on -/
-@[builtin_doc]
+/-- Boolean flags, turned on -/
 scoped syntax (name:=flag_on) "+" ident : doc_arg
-/-- Boolean flag, turned off -/
-@[builtin_doc]
+/-- Boolean flags, turned off -/
 scoped syntax (name:=flag_off) "-" ident : doc_arg
 
 /-- Link targets, which may be URLs or named references -/
 declare_syntax_cat link_target
-/-- A URL target, written explicitly. Use square brackets for a named target. -/
-@[builtin_doc]
+/-- A reference to a URL -/
 scoped syntax (name:=url) "(" str ")" : link_target
-/-- A named reference to a URL defined elsewhere. Use parentheses to write the URL here. -/
-@[builtin_doc]
+/-- A named reference -/
 scoped syntax (name:=ref) "[" str "]" : link_target
 
 /--
@@ -91,87 +91,26 @@ This syntax uses the following conventions:
 -/
 declare_syntax_cat inline
 scoped syntax (name:=text) str : inline
-/--
-Emphasis, often rendered as italics.
-
-Emphasis may be nested by using longer sequences of `_` for the outer delimiters. For example:
-```
-Remember: __always butter the _rugbrød_ before adding toppings!__
-```
-Here, the outer `__` is used to emphasize the instructions, while the inner `_` indicates the use of
-a non-English word.
--/
-@[builtin_doc]
+/-- Emphasis (often rendered as italics) -/
 scoped syntax (name:=emph) "_[" inline* "]" : inline
-/--
-Bold emphasis.
-
-A single `*` suffices to make text bold. Using `_` for emphasis.
-
-Bold text may be nested by using longer sequences of `*` for the outer delimiters.
--/
-@[builtin_doc]
+/-- Bold emphasis   -/
 scoped syntax (name:=bold) "*[" inline* "]" : inline
-/--
-A link. The link's target may either be a concrete URL (written in parentheses) or a named URL
-(written in square brackets).
--/
-@[builtin_doc]
+/-- Link -/
 scoped syntax (name:=link) "link[" inline* "]" link_target : inline
-/--
-An image, with alternate text and a URL.
-
-The alternate text is a plain string, rather than Verso markup.
-
-The image URL may either be a concrete URL (written in parentheses) or a named URL (written in
-square brackets).
--/
-
-@[builtin_doc]
+/-- Image -/
 scoped syntax (name:=image) "image(" str ")" link_target : inline
-/--
-A footnote use site.
-
-Footnotes must be defined elsewhere using the `[^NAME]: TEXT` syntax.
--/
-@[builtin_doc]
+/-- A footnote use -/
 scoped syntax (name:=footnote) "footnote(" str ")" : inline
+/-- Line break -/
 scoped syntax (name:=linebreak) "line!" str : inline
-/--
-Literal code.
-
-Code may begin with any non-zero number of backticks. It must be terminated with the same number,
-and it may not contain a sequence of backticks that is at least as long as its starting or ending
-delimiters.
-
-If the first and last characters are space, and it contains at least one non-space character, then
-the resulting string has a single space stripped from each end. Thus, ``` `` `x `` ``` represents
-``"`x"``, not ``" `x "``.
--/
-@[builtin_doc]
+/-- Literal code. If the first and last characters are space, and it contains at least one non-space
+  character, then the resulting string has a single space stripped from each end.-/
 scoped syntax (name:=code) "code(" str ")" : inline
-/--
-A _role_: an extension to the Verso document language in an inline position.
-
-Text is given a role using the following syntax: `{NAME ARGS*}[CONTENT]`. The `NAME` is an
-identifier that determines which role is being used, akin to a function name. Each of the `ARGS` may
-have the following forms:
-* A value, which is a string literal, natural number, or identifier
-* A named argument, of the form `(NAME := VALUE)`
-* A flag, of the form `+NAME` or `-NAME`
-
-The `CONTENT` is a sequence of inline content. If there is only one piece of content and it has
-beginning and ending delimiters (e.g. code literals, links, or images, but not ordinary text), then
-the `[` and `]` may be omitted. In particular, `` {NAME ARGS*}`x` `` is equivalent to
-``{NAME ARGS*}[`x`]``.
--/
-@[builtin_doc]
+/-- A _role_: an extension to the Verso document language in an inline position -/
 scoped syntax (name:=role) "role{" ident doc_arg* "}" "[" inline* "]"  : inline
 /-- Inline mathematical notation (equivalent to LaTeX's `$` notation) -/
-@[builtin_doc]
 scoped syntax (name:=inline_math) "\\math" code : inline
 /-- Display-mode mathematical notation -/
-@[builtin_doc]
 scoped syntax (name:=display_math) "\\displaymath" code : inline
 
 /--
@@ -193,130 +132,40 @@ declare_syntax_cat block
 
 /-- Items from both ordered and unordered lists -/
 declare_syntax_cat list_item
-/-- A list item -/
-@[builtin_doc]
+/-- List item -/
 syntax (name:=li) "*" block* : list_item
 
 /-- A description of an item -/
 declare_syntax_cat desc_item
 /-- A description of an item -/
-@[builtin_doc]
 scoped syntax (name:=desc) ":" inline* "=>" block* : desc_item
 
-/-- Paragraph -/
-@[builtin_doc]
 scoped syntax (name:=para) "para[" inline+ "]" : block
 /-- Unordered List -/
-@[builtin_doc]
 scoped syntax (name:=ul) "ul{" list_item* "}" : block
-/-- Description list -/
-@[builtin_doc]
+/-- Definition list -/
 scoped syntax (name:=dl) "dl{" desc_item* "}" : block
 /-- Ordered list -/
-@[builtin_doc]
 scoped syntax (name:=ol) "ol(" num ")" "{" list_item* "}" : block
-/--
-A code block that contains literal code.
-
-Code blocks have the following syntax:
-````
-```(NAME ARGS*)?
-CONTENT
-```
-````
-
-`CONTENT` is a literal string. If the `CONTENT` contains a sequence of three or more backticks, then
-the opening and closing ` ``` ` (called _fences_) should have more backticks than the longest
-sequence in `CONTENT`. Additionally, the opening and closing fences should have the same number of
-backticks.
-
-If `NAME` and `ARGS` are not provided, then the code block represents literal text. If provided, the
-`NAME` is an identifier that selects an interpretation of the block. Unlike Markdown, this name is
-not necessarily the language in which the code is written, though many custom code blocks are, in
-practice, named after the language that they contain. `NAME` is more akin to a function name. Each
-of the `ARGS` may have the following forms:
-* A value, which is a string literal, natural number, or identifier
-* A named argument, of the form `(NAME := VALUE)`
-* A flag, of the form `+NAME` or `-NAME`
-
-The `CONTENT` is interpreted according to the indentation of the fences. If the fences are indented
-`n` spaces, then `n` spaces are removed from the start of each line of `CONTENT`.
--/
-@[builtin_doc]
+/-- Literal code -/
 scoped syntax (name:=codeblock) "```" (ident doc_arg*)? "|" str "```" : block
-/--
-A quotation, which contains a sequence of blocks that are at least as indented as the `>`.
--/
-@[builtin_doc]
+/-- Quotation -/
 scoped syntax (name:=blockquote) ">" block* : block
-/--
-A named URL that can be used in links and images.
--/
-@[builtin_doc]
+/-- A link reference definition -/
 scoped syntax (name:=link_ref)  "[" str "]:" str : block
-/--
-A footnote definition.
--/
-@[builtin_doc]
+/-- A footnote definition -/
 scoped syntax (name:=footnote_ref) "[^" str "]:" inline* : block
-/--
-A _directive_, which is an extension to the Verso language in block position.
-
-Directives have the following syntax:
-```
-:::NAME ARGS*
-CONTENT*
-:::
-```
-
-The `NAME` is an identifier that determines which directive is being used, akin to a function name.
-Each of the `ARGS` may have the following forms:
-* A value, which is a string literal, natural number, or identifier
-* A named argument, of the form `(NAME := VALUE)`
-* A flag, of the form `+NAME` or `-NAME`
-
-The `CONTENT` is a sequence of block content. Directives may be nested by using more colons in
-the outer directive. For example:
-```
-::::outer +flag (arg := 5)
-A paragraph.
-:::inner "label"
-* 1
-* 2
-:::
-::::
-```
-
--/
-@[builtin_doc]
+/-- Custom directive -/
 scoped syntax (name:=directive) ":::" rawIdent doc_arg* "{" block:max* "}" : block
-/--
-A header
-
-Headers must be correctly nested to form a tree structure. The first header in a document must
-start with `#`, and subsequent headers must have at most one more `#` than the preceding header.
--/
-@[builtin_doc]
+/-- A header -/
 scoped syntax (name:=header) "header(" num ")" "{" inline+ "}" : block
 
 open Lean.Parser Term in
-meta def metadataContents : Lean.Parser.Parser :=
+meta def metadataContents : Parser :=
   structInstFields (sepByIndent structInstField ", " (allowTrailingSep := true))
 
-/--
-Metadata for the preceding header.
--/
-@[builtin_doc]
+/-- Metadata for this section, defined by the current genre -/
 scoped syntax (name:=metadata_block) "%%%" metadataContents "%%%" : block
 
-/--
-A block-level command, which invokes an extension during documentation processing.
-
-The `NAME` is an identifier that determines which command is being used, akin to a function name.
-Each of the `ARGS` may have the following forms:
-* A value, which is a string literal, natural number, or identifier
-* A named argument, of the form `(NAME := VALUE)`
-* A flag, of the form `+NAME` or `-NAME`
--/
-@[builtin_doc]
+/-- A block-level command -/
 scoped syntax (name:=command) "command{" rawIdent doc_arg* "}" : block

src/Lean/Elab/BuiltinCommand.lean

@@ -23,20 +23,13 @@ public section
 namespace Lean.Elab.Command
 
 @[builtin_command_elab moduleDoc] def elabModuleDoc : CommandElab := fun stx => do
-  let some range ← Elab.getDeclarationRange? stx
-    | return  -- must be from partial syntax, ignore
-
   match stx[1] with
   | Syntax.atom _ val =>
-    if getVersoModuleDocs (← getEnv) |>.isEmpty then
-      let doc := val.extract 0 (val.endPos - ⟨2⟩)
-      modifyEnv fun env => addMainModuleDoc env ⟨doc, range⟩
-    else
-      throwError m!"Can't add Markdown-format module docs because there is already Verso-format content present."
-  | Syntax.node _ ``Lean.Parser.Command.versoCommentBody args =>
-    runTermElabM fun _ => do
-      addVersoModDocString range ⟨args.getD 0 .missing⟩
-  | _ => throwErrorAt stx "unexpected module doc string{indentD <| stx}"
+    let doc := val.extract 0 (val.endPos - ⟨2⟩)
+    let some range ← Elab.getDeclarationRange? stx
+      | return  -- must be from partial syntax, ignore
+    modifyEnv fun env => addMainModuleDoc env ⟨doc, range⟩
+  | _ => throwErrorAt stx "unexpected module doc string{indentD stx[1]}"
 
 private def addScope (isNewNamespace : Bool) (header : String) (newNamespace : Name)
     (isNoncomputable isPublic : Bool := false) (attrs : List (TSyntax ``Parser.Term.attrInstance) := []) :

src/Lean/Elab/DocString.lean

@@ -12,8 +12,6 @@ public import Lean.Elab.Term.TermElabM
 public import Lean.Elab.Command.Scope
 import Lean.DocString.Syntax
 import Lean.Meta.Hint
-import Lean.DocString.Markdown
-import Lean.BuiltinDocAttr
 
 set_option linter.missingDocs true
 
@@ -24,6 +22,7 @@ open Std
 open scoped Lean.Doc.Syntax
 
 
+
 public section
 
 private structure ElabLink where
@@ -113,6 +112,8 @@ deriving BEq, Repr
 
 /-- Context used as a reader in `DocM`. -/
 structure Context where
+  /-- The declaration for which documentation is being elaborated. -/
+  declName : Name
   /-- Whether suggestions should be provided interactively. -/
   suggestionMode : SuggestionMode
 
@@ -139,95 +140,32 @@ instance : MonadLift TermElabM DocM where
       act
     return v
 
-private structure ModuleDocstringState extends Lean.Doc.State where
-  scopedExts : Array (ScopedEnvExtension EnvExtensionEntry EnvExtensionEntry EnvExtensionState)
-
-
-private builtin_initialize modDocstringStateExt : EnvExtension (Option ModuleDocstringState) ←
-  registerEnvExtension (pure none)
-
-private def getModState
-    [Monad m] [MonadEnv m] [MonadLiftT IO m] [MonadLCtx m]
-    [MonadResolveName m] [MonadOptions m] : m ModuleDocstringState := do
-  if let some st := modDocstringStateExt.getState (← getEnv) then
-    return st
-  else
-    let lctx ← getLCtx
-    let openDecls ← getOpenDecls
-    let options ← getOptions
-    let scopes := [{header := "", isPublic := true}]
-    let st : ModuleDocstringState := { scopes, openDecls, lctx, options, scopedExts := #[] }
-    modifyEnv fun env =>
-      modDocstringStateExt.setState env st
-    return st
-
-private def setModState [Monad m] [MonadEnv m] (state : ModuleDocstringState) : m Unit := do
-  modifyEnv fun env =>
-    modDocstringStateExt.setState env state
-
-/--
-Runs a documentation elaborator in the module docstring context.
--/
-def DocM.execForModule (act : DocM α) (suggestionMode : SuggestionMode := .interactive) :
-    TermElabM α := withoutModifyingEnv do
-  let sc ← scopedEnvExtensionsRef.get
-  let st ← getModState
-  try
-    scopedEnvExtensionsRef.set st.scopedExts
-    let ((v, _), _) ←
-      act.run { suggestionMode } |>.run {} |>.run st.toState
-    pure v
-  finally
-    scopedEnvExtensionsRef.set sc
-
 open Lean.Parser.Term in
 /--
-Runs a documentation elaborator in a declaration's context, discarding changes made to the
-environment.
+Runs a documentation elaborator, discarding changes made to the environment.
 -/
 def DocM.exec (declName : Name) (binders : Syntax) (act : DocM α)
     (suggestionMode : SuggestionMode := .interactive) :
     TermElabM α := withoutModifyingEnv do
   let some ci := (← getEnv).constants.find? declName
     | throwError "Unknown constant {declName} when building docstring"
-  let st ← Term.saveState
-  Core.resetMessageLog -- We'll replay the messages after the elab loop
+  let (lctx, localInstances) ← buildContext ci.type binders
+  let sc ← scopedEnvExtensionsRef.get
   try
-    let (lctx, localInstances) ← buildContext ci.type binders
-    let sc ← scopedEnvExtensionsRef.get
-    try
-      let openDecls ← getOpenDecls
-      let options ← getOptions
-      let scopes := [{header := "", isPublic := true}]
-      let ((v, _), _) ← withTheReader Meta.Context (fun ρ => { ρ with localInstances }) <|
-        act.run { suggestionMode } |>.run {} |>.run { scopes, openDecls, lctx, options }
-      pure v
-    finally
-      scopedEnvExtensionsRef.set sc
+    let openDecls ← getOpenDecls
+    let options ← getOptions
+    let scopes := [{header := "", isPublic := true}]
+    let ((v, _), _) ← withTheReader Meta.Context (fun ρ => { ρ with localInstances }) <|
+      act.run { declName, suggestionMode } |>.run {} |>.run { scopes, openDecls, lctx, options }
+    pure v
   finally
-    let msgs ← Core.getMessageLog
-    st.restore
-    Core.setMessageLog ((← Core.getMessageLog) ++ msgs)
+    scopedEnvExtensionsRef.set sc
 where
   buildContext (type : Expr) (binders : Syntax) : TermElabM (LocalContext × LocalInstances) := do
-    -- Create a local context with all binders. The type will be updated as we introduce parameters.
+    -- Create a local context with all binders
     let mut type := type
-
-    -- We start with a local context that's reset to only include section variables
-    let mut localInstances ← Meta.getLocalInstances
-    let mut lctx ← getLCtx
-    let sectionFVars := (← read).sectionFVars.valuesArray.filterMap fun
-      | .fvar fv => some fv
-      | _ => none
-    repeat
-      if lctx.size = 0 then break
-      if let some decl := lctx.lastDecl then
-        if sectionFVars.any (· == decl.fvarId) then break
-        else
-          lctx := lctx.pop
-          localInstances := localInstances.filter (·.fvar != .fvar decl.fvarId)
-      else break
-
+    let mut localInstances := (← readThe Meta.Context).localInstances
+    let mut lctx := ← getLCtx
     let names ← binders.getArgs.flatMapM binderNames
     let mut i := 0
     let mut x := none
@@ -786,8 +724,6 @@ builtin_initialize registerBuiltinAttribute {
     let ret := .app (.const ``Inline [0]) (.const ``ElabInline [])
     let ((wrapper, _), _) ← genWrapper decl (some argTy) ret |>.run {} {} |>.run {} {}
     docRoleExt.add (roleName, wrapper)
-    if (← findInternalDocString? (← getEnv) decl).isSome then
-      addInheritedDocString wrapper decl
 }
 
 /--
@@ -813,12 +749,8 @@ builtin_initialize registerBuiltinAttribute {
         (mkApp3 (.const ``List.cons [0]) (.const ``SyntaxNodeKind []) (toExpr `inline) (.app (.const ``List.nil [0]) (.const ``SyntaxNodeKind [])))
     let ret := .app (.const ``Inline [0]) (.const ``ElabInline [])
     let ((wrapper, _), _) ← genWrapper decl (some argTy) ret |>.run {} {} |>.run {} {}
-    addDeclarationRangesFromSyntax wrapper stx
     declareBuiltin roleName <|
       mkApp3 (.const ``addBuiltinDocRole []) (toExpr roleName) (toExpr wrapper) (.const wrapper [])
-    if (← findInternalDocString? (← getEnv) decl).isSome then
-      addInheritedDocString wrapper decl
-    declareBuiltinDocStringAndRanges wrapper
 }
 
 builtin_initialize registerBuiltinAttribute {
@@ -834,8 +766,6 @@ builtin_initialize registerBuiltinAttribute {
     let ret := mkApp2 (.const ``Block [0, 0]) (.const ``ElabInline []) (.const ``ElabBlock [])
     let ((wrapper, _), _) ← genWrapper decl (some (.const ``StrLit [])) ret |>.run {} {} |>.run {} {}
     docCodeBlockExt.add (blockName, wrapper)
-    if (← findInternalDocString? (← getEnv) decl).isSome then
-      addInheritedDocString wrapper decl
 }
 
 /--
@@ -858,13 +788,9 @@ builtin_initialize registerBuiltinAttribute {
         pure decl
     let ret := mkApp2 (.const ``Block [0, 0]) (.const ``ElabInline []) (.const ``ElabBlock [])
     let ((wrapper, _), _) ← genWrapper decl (some (.const ``StrLit [])) ret |>.run {} {} |>.run {} {}
-    addDeclarationRangesFromSyntax wrapper stx
     declareBuiltin blockName <|
       mkApp3 (.const ``addBuiltinDocCodeBlock [])
         (toExpr blockName) (toExpr wrapper) (.const wrapper [])
-    if (← findInternalDocString? (← getEnv) decl).isSome then
-      addInheritedDocString wrapper decl
-    declareBuiltinDocStringAndRanges wrapper
 }
 
 /-- A suggestion about an applicable code block -/
@@ -946,9 +872,6 @@ builtin_initialize registerBuiltinAttribute {
     let ret := mkApp2 (.const ``Block [0, 0]) (.const ``ElabInline []) (.const ``ElabBlock [])
     let ((wrapper, _), _) ← genWrapper decl (some argTy) ret |>.run {} {} |>.run {} {}
     docDirectiveExt.add (directiveName, wrapper)
-    if (← findInternalDocString? (← getEnv) decl).isSome then
-      addInheritedDocString wrapper decl
-
 }
 
 /--
@@ -974,13 +897,9 @@ builtin_initialize registerBuiltinAttribute {
         (mkApp3 (.const ``List.cons [0]) (.const ``SyntaxNodeKind []) (toExpr `block) (.app (.const ``List.nil [0]) (.const ``SyntaxNodeKind [])))
     let ret := mkApp2 (.const ``Block [0, 0]) (.const ``ElabInline []) (.const ``ElabBlock [])
     let ((wrapper, _), _) ← genWrapper decl (some argTy) ret |>.run {} {} |>.run {} {}
-    addDeclarationRangesFromSyntax wrapper stx
     declareBuiltin directiveName <|
       mkApp3 (.const ``addBuiltinDocDirective [])
         (toExpr directiveName) (toExpr wrapper) (.const wrapper [])
-    if (← findInternalDocString? (← getEnv) decl).isSome then
-      addInheritedDocString wrapper decl
-    declareBuiltinDocStringAndRanges wrapper
 }
 
 builtin_initialize registerBuiltinAttribute {
@@ -997,8 +916,6 @@ builtin_initialize registerBuiltinAttribute {
     let ret := mkApp2 (.const ``Block [0, 0]) (.const ``ElabInline []) (.const ``ElabBlock [])
     let ((wrapper, _), _) ← genWrapper decl none ret |>.run {} {} |>.run {} {}
     docCommandExt.add (commandName, wrapper)
-    if (← findInternalDocString? (← getEnv) decl).isSome then
-      addInheritedDocString wrapper decl
 }
 
 /--
@@ -1022,13 +939,9 @@ builtin_initialize registerBuiltinAttribute {
 
     let ret := mkApp2 (.const ``Block [0, 0]) (.const ``ElabInline []) (.const ``ElabBlock [])
     let ((wrapper, _), _) ← genWrapper decl none ret |>.run {} {} |>.run {} {}
-    addDeclarationRangesFromSyntax wrapper stx
     declareBuiltin commandName <|
       mkApp3 (.const ``addBuiltinDocCommand [])
         (toExpr commandName) (toExpr wrapper) (.const wrapper [])
-    if (← findInternalDocString? (← getEnv) decl).isSome then
-      addInheritedDocString wrapper decl
-    declareBuiltinDocStringAndRanges wrapper
 }
 end
 
@@ -1046,88 +959,76 @@ private unsafe def codeBlockSuggestionsUnsafe : TermElabM (Array (StrLit → Doc
 @[implemented_by codeBlockSuggestionsUnsafe]
 private opaque codeBlockSuggestions : TermElabM (Array (StrLit → DocM (Array CodeBlockSuggestion)))
 
-private def builtinElabName (n : Name) : Option Name :=
-  if (`Lean.Doc).isPrefixOf n then some n
-  else if n matches (.str .anonymous _) then some <| `Lean.Doc ++ n
-  else none
-
-private unsafe def roleExpandersForUnsafe (roleName : Ident) :
-    TermElabM (Array (Name × (TSyntaxArray `inline → StateT (Array (TSyntax `doc_arg)) DocM (Inline ElabInline)))) := do
+private unsafe def roleExpandersForUnsafe (roleName : Ident) : TermElabM (Array (TSyntaxArray `inline → StateT (Array (TSyntax `doc_arg)) DocM (Inline ElabInline))) := do
   let x? ←
-    try some <$> realizeGlobalConstNoOverload roleName
+    try some <$> realizeGlobalConstNoOverloadWithInfo roleName
     catch | _ => pure none
   if let some x := x? then
     let names := (docRoleExt.getState (← getEnv)).get? x |>.getD #[]
     let builtins := (← builtinDocRoles.get).get? x |>.getD #[]
-    return (← names.mapM (fun x => do return (x, ← evalConst _ x))) ++ builtins
+    return (← names.mapM (evalConst _)) ++ builtins.map (·.2)
   else
     let x := roleName.getId
     let hasBuiltin :=
       (← builtinDocRoles.get).get? x <|> (← builtinDocRoles.get).get? (`Lean.Doc ++ x)
-    return hasBuiltin.toArray.flatten
+    return hasBuiltin.toArray.flatten.map (·.2)
 
 
 @[implemented_by roleExpandersForUnsafe]
 private opaque roleExpandersFor (roleName : Ident) :
-  TermElabM (Array (Name × (TSyntaxArray `inline → StateT (Array (TSyntax `doc_arg)) DocM (Inline ElabInline))))
+  TermElabM (Array (TSyntaxArray `inline → StateT (Array (TSyntax `doc_arg)) DocM (Inline ElabInline)))
 
-private unsafe def codeBlockExpandersForUnsafe (codeBlockName : Ident) :
-    TermElabM (Array (Name × (StrLit → StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock)))) := do
+private unsafe def codeBlockExpandersForUnsafe (codeBlockName : Ident) : TermElabM (Array (StrLit → StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock))) := do
   let x? ←
-    try some <$> realizeGlobalConstNoOverload codeBlockName
+    try some <$> realizeGlobalConstNoOverloadWithInfo codeBlockName
     catch | _ => pure none
   if let some x := x? then
     let names := (docCodeBlockExt.getState (← getEnv)).get? x |>.getD #[]
     let names' := (← builtinDocCodeBlocks.get).get? x |>.getD #[]
-    return (← names.mapM (fun x => do return (x, ← evalConst _ x))) ++ names'
+    return (← names.mapM (evalConst _)) ++ names'.map (·.2)
   else
     let x := codeBlockName.getId
     let hasBuiltin :=
       (← builtinDocCodeBlocks.get).get? x <|> (← builtinDocCodeBlocks.get).get? (`Lean.Doc ++ x)
-    return hasBuiltin.toArray.flatten
+    return hasBuiltin.toArray.flatten.map (·.2)
 
 
 @[implemented_by codeBlockExpandersForUnsafe]
-private opaque codeBlockExpandersFor (codeBlockName : Ident) :
-  TermElabM (Array (Name × (StrLit → StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock))))
+private opaque codeBlockExpandersFor (codeBlockName : Ident) : TermElabM (Array (StrLit → StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock)))
 
-private unsafe def directiveExpandersForUnsafe (directiveName : Ident) :
-    TermElabM (Array (Name × (TSyntaxArray `block → StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock)))) := do
+private unsafe def directiveExpandersForUnsafe (directiveName : Ident) : TermElabM (Array (TSyntaxArray `block → StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock))) := do
   let x? ←
-    try some <$> realizeGlobalConstNoOverload directiveName
+    try some <$> realizeGlobalConstNoOverloadWithInfo directiveName
     catch | _ => pure none
   if let some x := x? then
     let names := (docDirectiveExt.getState (← getEnv)).get? x |>.getD #[]
     let names' := (← builtinDocDirectives.get).get? x |>.getD #[]
-    return (← names.mapM (fun x => do return (x, ← evalConst _ x))) ++ names'
+    return (← names.mapM (evalConst _)) ++ names'.map (·.2)
   else
     let x := directiveName.getId
     let hasBuiltin :=
       (← builtinDocDirectives.get).get? x <|> (← builtinDocDirectives.get).get? (`Lean.Doc ++ x)
-    return hasBuiltin.toArray.flatten
+    return hasBuiltin.toArray.flatten.map (·.2)
 
 @[implemented_by directiveExpandersForUnsafe]
-private opaque directiveExpandersFor (directiveName : Ident) :
-  TermElabM (Array (Name × (TSyntaxArray `block → StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock))))
+private opaque directiveExpandersFor (directiveName : Ident) : TermElabM (Array (TSyntaxArray `block → StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock)))
 
-private unsafe def commandExpandersForUnsafe (commandName : Ident) :
-    TermElabM (Array (Name × StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock))) := do
+private unsafe def commandExpandersForUnsafe (commandName : Ident) : TermElabM (Array (StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock))) := do
   let x? ←
-    try some <$> realizeGlobalConstNoOverload commandName
+    try some <$> realizeGlobalConstNoOverloadWithInfo commandName
     catch | _ => pure none
   if let some x := x? then
     let names := (docCommandExt.getState (← getEnv)).get? x |>.getD #[]
     let names' := (← builtinDocCommands.get).get? x |>.getD #[]
-    return (← names.mapM (fun x => do return (x, ← evalConst _ x))) ++ names'
+    return (← names.mapM (evalConst _)) ++ names'.map (·.2)
   else
     let x := commandName.getId
     let hasBuiltin :=
       (← builtinDocCommands.get).get? x <|> (← builtinDocCommands.get).get? (`Lean.Doc ++ x)
-    return hasBuiltin.toArray.flatten
+    return hasBuiltin.toArray.flatten.map (·.2)
 
 @[implemented_by commandExpandersForUnsafe]
-private opaque commandExpandersFor (commandName : Ident) :
-  TermElabM (Array (Name × StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock)))
+private opaque commandExpandersFor (commandName : Ident) : TermElabM (Array (StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock)))
 
 
 private def mkArgVal (arg : TSyntax `arg_val) : DocM Term :=
@@ -1216,17 +1117,12 @@ private def mkSuggestion  (ref : Syntax) (hintTitle : MessageData) (newStrings :
       toMessageData <| Diff.linesToString <| d.filter (·.1 != Action.skip)
     pure m!"\n\nHint: {hintTitle}\n{indentD <| m!"\n".joinSep edits.toList}"
 
-def nameOrBuiltinName [Monad m] [MonadEnv m] (x : Name) : m Name := do
-  let env ← getEnv
-  if env.contains x then return x
-  else return `Lean.Doc ++ x
 
 /--
 Elaborates the syntax of an inline document element to an actual inline document element.
 -/
 public partial def elabInline (stx : TSyntax `inline) : DocM (Inline ElabInline) :=
-  withRef stx <|
-  withInfoContext (mkInfo := pure <| .ofDocInfo {elaborator := decl_name%, stx := stx}) do
+  withRef stx do
   match stx with
   | `(inline|$s:str) =>
     return .text s.getString
@@ -1258,15 +1154,14 @@ public partial def elabInline (stx : TSyntax `inline) : DocM (Inline ElabInline)
         unless suggestions.isEmpty do
           let text ← getFileMap
           let str := text.source.extract b e
-          let ss : Array (String × Option String × Option String) ←
-            suggestions.mapM fun {role, args, moreInfo} => do
-              pure {
-                fst :=
-                  "{" ++ (← suggestionName role).toString ++
-                  (args.map (" " ++ ·)).getD "" ++ "}" ++ str,
-                snd.fst := none
-                snd.snd := moreInfo.map withSpace
-              }
+          let ss : Array (String × Option String × Option String) ← suggestions.mapM fun {role, args, moreInfo} => do
+            pure {
+              fst :=
+                "{" ++ (← suggestionName role).toString ++
+                (args.map (" " ++ ·)).getD "" ++ "}" ++ str,
+              snd.fst := none
+              snd.snd := moreInfo.map withSpace
+            }
           let ss := ss.qsort (fun x y => x.1 < y.1)
           let hint ← mkSuggestion stx m!"Insert a role to document it:" ss
           logWarning m!"Code element could be more specific.{hint}"
@@ -1277,15 +1172,9 @@ public partial def elabInline (stx : TSyntax `inline) : DocM (Inline ElabInline)
     return .math .display s.getString
   | `(inline|role{$name $args*}[$inl*]) =>
     let expanders ← roleExpandersFor name
-    for (exName, ex) in expanders do
+    for ex in expanders do
       try
         let res ← ex inl args <&> (·.1)
-        pushInfoLeaf <| .ofDocElabInfo {
-          elaborator := exName,
-          stx := name,
-          name := exName,
-          kind := .role
-        }
         return res
       catch
         | e@(.internal id _) =>
@@ -1304,8 +1193,7 @@ where
 Elaborates the syntax of an block-level document element to an actual block-level document element.
 -/
 public partial def elabBlock (stx : TSyntax `block) : DocM (Block ElabInline ElabBlock) :=
-  withRef stx <|
-  withInfoContext (mkInfo := pure <| .ofDocInfo {elaborator := decl_name%, stx := stx}) do
+  withRef stx do
   match stx with
   | `(block|para[$inls*]) =>
     .para <$> inls.mapM elabInline
@@ -1343,15 +1231,9 @@ public partial def elabBlock (stx : TSyntax `block) : DocM (Block ElabInline Ela
     return .empty
   | `(block| ::: $name $args* { $content*}) =>
     let expanders ← directiveExpandersFor name
-    for (exName, ex) in expanders do
+    for ex in expanders do
       try
         let res ← ex content args <&> (·.1)
-        pushInfoLeaf <| .ofDocElabInfo {
-          elaborator := exName,
-          stx := name,
-          name := exName,
-          kind := .directive
-        }
         return res
       catch
         | e@(.internal id _) =>
@@ -1371,30 +1253,24 @@ public partial def elabBlock (stx : TSyntax `block) : DocM (Block ElabInline Ela
         unless suggestions.isEmpty do
           let text ← getFileMap
           let str := text.source.extract b e
-          let ss : Array (String × Option String × Option String) ←
-            suggestions.mapM fun {name, args, moreInfo} => do
-              pure {
-                fst :=
-                  str ++ (← suggestionName name).toString ++
-                  (args.map (" " ++ ·)).getD "",
-                snd.fst := moreInfo.map withSpace
-                snd.snd := none
-              }
+          let ss : Array (String × Option String × Option String) ← suggestions.mapM fun {name, args, moreInfo} => do
+            pure {
+              fst :=
+                str ++ (← suggestionName name).toString ++
+                (args.map (" " ++ ·)).getD "",
+              snd.fst := moreInfo.map withSpace
+              snd.snd := none
+            }
           let ss := ss.qsort (fun x y => x.1 < y.1)
           let hint ← mkSuggestion opener m!"Insert a specific kind of code block:" ss
           logWarning m!"Code block could be more specific.{hint}"
+
     return .code s.getString
   | `(block| ```$name $args* | $s ```) =>
     let expanders ← codeBlockExpandersFor name
-    for (exName, ex) in expanders do
+    for ex in expanders do
       try
         let res ← ex s args <&> (·.1)
-        pushInfoLeaf <| .ofDocElabInfo {
-          elaborator := exName,
-          stx := name,
-          name := exName,
-          kind := .codeBlock
-        }
         return res
       catch
         | e@(.internal id _) =>
@@ -1405,15 +1281,9 @@ public partial def elabBlock (stx : TSyntax `block) : DocM (Block ElabInline Ela
     throwErrorAt name "No code block expander for `{name}`"
   | `(block| command{$name $args*}) =>
     let expanders ← commandExpandersFor name
-    for (exName, ex) in expanders do
+    for ex in expanders do
       try
         let res ← ex args <&> (·.1)
-        pushInfoLeaf <| .ofDocElabInfo {
-          elaborator := exName,
-          stx := name,
-          name := exName,
-          kind := .command
-        }
         return res
       catch
         | e@(.internal id _) =>
@@ -1422,12 +1292,6 @@ public partial def elabBlock (stx : TSyntax `block) : DocM (Block ElabInline Ela
           else throw e
         | e => throw e
     throwErrorAt name "No document command elaborator for `{name}`"
-  | `(block|%%%$_*%%%) =>
-    let h ←
-      if stx.raw.getRange?.isSome then m!"Remove it".hint #[""] (ref? := stx)
-      else pure m!""
-    logError m!"Part metadata is not supported in docstrings.{h}"
-    return .empty
   | other => throwErrorAt other "Unsupported syntax: {other}"
 where
   withSpace (s : String) : String :=
@@ -1450,13 +1314,10 @@ private partial def elabBlocks' (level : Nat) :
         else if n = level then
           set xs
           let (content, subParts) ← elabBlocks' (level + 1)
-          let title ←
-            liftM <| withInfoContext (mkInfo := pure <| .ofDocInfo {elaborator := `no_elab, stx := x}) <|
-              name.mapM elabInline
-          let mdTitle := ToMarkdown.toMarkdown (Inline.concat title) |>.run'
+          let title ← liftM <| name.mapM elabInline
           sub := sub.push {
             title,
-            titleString := mdTitle
+            titleString := "" -- TODO get string from filemap?
             metadata := none
             content, subParts
           }
@@ -1470,120 +1331,83 @@ private partial def elabBlocks' (level : Nat) :
         catch
           | e =>
             logErrorAt e.getRef e.toMessageData
-    else
-      break
+    else break
   return (pre, sub)
 
-private def elabModSnippet'
-    (range : DeclarationRange) (level : Nat) (blocks : TSyntaxArray `block) :
-    DocM VersoModuleDocs.Snippet := do
-  let mut snippet : VersoModuleDocs.Snippet := {
-    declarationRange := range
-  }
-  let mut maxLevel := level
-  for b in blocks do
-    if let `(block|header($n){$name*}) := b then
-        let n := n.getNat
-        if n > maxLevel then
-          logErrorAt b m!"Incorrect header nesting: expected at most `{"#".pushn '#' maxLevel}` \
-            but got `{"#".pushn '#' n}`"
-        else
-          let title ←
-            liftM <| withInfoContext (mkInfo := pure <| .ofDocInfo {elaborator := `no_elab, stx := b}) <|
-              name.mapM elabInline
-          let some headerRange ← getDeclarationRange? b
-            | throwErrorAt b "Can't find header source position"
-          let mdTitle := ToMarkdown.toMarkdown (Inline.concat title) |>.run'
-          snippet := snippet.addPart n headerRange {
-            title,
-            titleString := mdTitle
-            metadata := none, content := #[], subParts := #[]
-          }
-      else
-        snippet := snippet.addBlock (← elabBlock b)
-  return snippet
-
-private partial def fixupInline (inl : Inline ElabInline) : DocM (Inline ElabInline) := do
-  match inl with
-  | .concat xs => .concat <$> xs.mapM fixupInline
-  | .emph xs => .emph <$> xs.mapM fixupInline
-  | .bold xs => .bold <$> xs.mapM fixupInline
-  | .link content url => (.link · url) <$> content.mapM fixupInline
-  | .footnote name content => .footnote name <$> content.mapM fixupInline
-  | .text s => pure (.text s)
-  | .image alt url => pure (.image alt url)
-  | .code s => pure (.code s)
-  | .math mode s => pure (.math mode s)
-  | .linebreak s => pure (.linebreak s)
-  | .other i@{ name, val } xs =>
-    match name with
-    | ``delayLink =>
-      let some {name} := val.get? ElabLink
-        | throwError "Wrong value for {name}: {val.typeName}"
-      let nameStr := name.getString
-      if let some r@{content := url, seen, .. } := (← getThe InternalState).urls[nameStr]? then
-        unless seen do modifyThe InternalState fun st => { st with urls := st.urls.insert nameStr { r with seen := true } }
-        return .link (← xs.mapM fixupInline) url
-      else
-        logErrorAt name "Reference not found"
-        return .concat (← xs.mapM fixupInline)
-    | ``delayImage =>
-      let some {alt, name} := val.get? ElabImage
-        | throwError "Wrong value for {name}: {val.typeName}"
-      let nameStr := name.getString
-      if let some r@{content := url, seen, ..} := (← getThe InternalState).urls[nameStr]? then
-        unless seen do modifyThe InternalState fun st => { st with urls := st.urls.insert nameStr { r with seen := true } }
-        return .image alt url
-      else
-        logErrorAt name "Reference not found"
-        return .empty
-    | ``delayFootnote =>
-      let some {name} := val.get? ElabFootnote
-        | throwError "Wrong value for {name}: {val.typeName}"
-      let nameStr := name.getString
-      if let some r@{content, seen, ..} := (← getThe InternalState).footnotes[nameStr]? then
-        unless seen do modifyThe InternalState fun st =>
-          { st with footnotes := st.footnotes.insert nameStr { r with seen := true } }
-        return .footnote nameStr #[← fixupInline content]
-      else
-        logErrorAt name "Footnote not found"
-        return .empty
-    | _ => .other i <$> xs.mapM fixupInline
-
-private partial def fixupBlock (block : Block ElabInline ElabBlock) : DocM (Block ElabInline ElabBlock) := do
-  match block with
-  | .para xs => .para <$> xs.mapM fixupInline
-  | .concat xs => .concat <$> xs.mapM fixupBlock
-  | .blockquote xs => .blockquote <$> xs.mapM fixupBlock
-  | .dl xs => .dl <$> xs.mapM fun { term, desc } => do
-    let term ← term.mapM fixupInline
-    let desc ← desc.mapM fixupBlock
-    pure { term, desc }
-  | .ul xs => .ul <$> xs.mapM fun ⟨bs⟩ => do return ⟨← bs.mapM fixupBlock⟩
-  | .ol n xs => .ol n <$> xs.mapM fun ⟨bs⟩ => do return ⟨← bs.mapM fixupBlock⟩
-  | .code s => pure (.code s)
-  | .other i xs => .other i <$> xs.mapM fixupBlock
-
-private partial def fixupPart (part : Part ElabInline ElabBlock Empty) : DocM (Part ElabInline ElabBlock Empty) := do
-  return { part with
-    title := ← part.title.mapM fixupInline
-    content := ← part.content.mapM fixupBlock,
-    subParts := ← part.subParts.mapM fixupPart
-  }
-
-
 private partial def fixupBlocks : (Array (Block ElabInline ElabBlock) × Array (Part ElabInline ElabBlock Empty)) → DocM (Array (Block ElabInline ElabBlock) × Array (Part ElabInline ElabBlock Empty))
   | (bs, ps) => do
-    let bs ← bs.mapM fixupBlock
-    let ps ← ps.mapM fixupPart
+    let bs ← bs.mapM fixB
+    let ps ← ps.mapM fixP
     return (bs, ps)
+where
+  fixI (inl : Inline ElabInline) : DocM (Inline ElabInline) := do
+    match inl with
+    | .concat xs => .concat <$> xs.mapM fixI
+    | .emph xs => .emph <$> xs.mapM fixI
+    | .bold xs => .bold <$> xs.mapM fixI
+    | .link content url => (.link · url) <$> content.mapM fixI
+    | .footnote name content => .footnote name <$> content.mapM fixI
+    | .text s => pure (.text s)
+    | .image alt url => pure (.image alt url)
+    | .code s => pure (.code s)
+    | .math mode s => pure (.math mode s)
+    | .linebreak s => pure (.linebreak s)
+    | .other i@{ name, val } xs =>
+      match name with
+      | ``delayLink =>
+        let some {name} := val.get? ElabLink
+          | throwError "Wrong value for {name}: {val.typeName}"
+        let nameStr := name.getString
+        if let some r@{content := url, seen, .. } := (← getThe InternalState).urls[nameStr]? then
+          unless seen do modifyThe InternalState fun st => { st with urls := st.urls.insert nameStr { r with seen := true } }
+          return .link (← xs.mapM fixI) url
+        else
+          logErrorAt name "Reference not found"
+          return .concat (← xs.mapM fixI)
+      | ``delayImage =>
+        let some {alt, name} := val.get? ElabImage
+          | throwError "Wrong value for {name}: {val.typeName}"
+        let nameStr := name.getString
+        if let some r@{content := url, seen, ..} := (← getThe InternalState).urls[nameStr]? then
+          unless seen do modifyThe InternalState fun st => { st with urls := st.urls.insert nameStr { r with seen := true } }
+          return .image alt url
+        else
+          logErrorAt name "Reference not found"
+          return .empty
+      | ``delayFootnote =>
+        let some {name} := val.get? ElabFootnote
+          | throwError "Wrong value for {name}: {val.typeName}"
+        let nameStr := name.getString
+        if let some r@{content, seen, ..} := (← getThe InternalState).footnotes[nameStr]? then
+          unless seen do modifyThe InternalState fun st =>
+            { st with footnotes := st.footnotes.insert nameStr { r with seen := true } }
+          return .footnote nameStr #[← fixI content]
+        else
+          logErrorAt name "Footnote not found"
+          return .empty
+      | _ => .other i <$> xs.mapM fixI
+
+  fixB (block : Block ElabInline ElabBlock) : DocM (Block ElabInline ElabBlock) := do
+    match block with
+    | .para xs => .para <$> xs.mapM fixI
+    | .concat xs => .concat <$> xs.mapM fixB
+    | .blockquote xs => .blockquote <$> xs.mapM fixB
+    | .dl xs => .dl <$> xs.mapM fun { term, desc } => do
+      let term ← term.mapM fixI
+      let desc ← desc.mapM fixB
+      pure { term, desc }
+    | .ul xs => .ul <$> xs.mapM fun ⟨bs⟩ => do return ⟨← bs.mapM fixB⟩
+    | .ol n xs => .ol n <$> xs.mapM fun ⟨bs⟩ => do return ⟨← bs.mapM fixB⟩
+    | .code s => pure (.code s)
+    | .other i xs => .other i <$> xs.mapM fixB
+
+  fixP (part : Part ElabInline ElabBlock Empty) : DocM (Part ElabInline ElabBlock Empty) := do
+    return { part with
+      title := ← part.title.mapM fixI
+      content := ← part.content.mapM fixB,
+      subParts := ← part.subParts.mapM fixP
+    }
 
-private partial def fixupSnippet (snippet : VersoModuleDocs.Snippet) : DocM VersoModuleDocs.Snippet := do
-  return {snippet with
-    text := ← snippet.text.mapM fixupBlock,
-    sections := ← snippet.sections.mapM fun (level, range, content) => do
-      return (level, range, ← fixupPart content)
-  }
 /--
 After fixing up the references, check to see which were not used and emit a suitable warning.
 -/
@@ -1595,19 +1419,10 @@ private def warnUnusedRefs : DocM Unit := do
     unless seen do
       logWarningAt location "Unused footnote"
 
-/-- Elaborates a sequence of blocks into a document. -/
+/-- Elaborates a sequence of blocks into a document -/
 public def elabBlocks (blocks : TSyntaxArray `block) :
     DocM (Array (Block ElabInline ElabBlock) × Array (Part ElabInline ElabBlock Empty)) := do
   let (v, _) ← elabBlocks' 0 |>.run blocks
   let res ← fixupBlocks v
   warnUnusedRefs
   return res
-
-/-- Elaborates a sequence of blocks into a module doc snippet. -/
-public def elabModSnippet
-    (range : DeclarationRange) (blocks : TSyntaxArray `block) (nestingLevel : Nat) :
-    DocM (VersoModuleDocs.Snippet) := do
-  let s ← elabModSnippet' range nestingLevel blocks
-  let s ← fixupSnippet s
-  warnUnusedRefs
-  return s

src/Lean/Elab/DocString/Builtin.lean

@@ -976,14 +976,8 @@ def suggestAttr (code : StrLit) : DocM (Array CodeSuggestion) := do
   catch
     | _ => pure ()
   try
-    let stx ← parseStrLit attrParser.fn code
-    if stx.getKind == ``Lean.Parser.Attr.simple then
-      let attrName := stx[0].getId.eraseMacroScopes
-      if isAttribute (← getEnv) attrName then
-        return #[.mk ``attr none none]
-      else return #[]
-    else
-      return #[.mk ``attr none none]
+    discard <| parseStrLit attrParser.fn code
+    return #[.mk ``attr none none]
   catch
     | _ => pure ()
   return #[]

src/Lean/Elab/DocString/Builtin/Parsing.lean

@@ -6,7 +6,7 @@ Author: David Thrane Christiansen
 module
 prelude
 import Lean.Elab.DocString
-public import Lean.Parser.Extension
+import Lean.Parser.Extension
 public import Lean.Parser.Types
 
 namespace Lean.Doc

src/Lean/Elab/InfoTree/Main.lean

@@ -221,12 +221,6 @@ def DelabTermInfo.format (ctx : ContextInfo) (info : DelabTermInfo) : IO Format
 def ChoiceInfo.format (ctx : ContextInfo) (info : ChoiceInfo) : Format :=
   f!"[Choice] @ {formatElabInfo ctx info.toElabInfo}"
 
-def DocInfo.format (ctx : ContextInfo) (info : DocInfo) : Format :=
-  f!"[Doc] {info.stx.getKind} @ {formatElabInfo ctx info.toElabInfo}"
-
-def DocElabInfo.format (ctx : ContextInfo) (info : DocElabInfo) : Format :=
-  f!"[DocElab] {info.name} ({repr info.kind}) @ {formatElabInfo ctx info.toElabInfo}"
-
 def Info.format (ctx : ContextInfo) : Info → IO Format
   | ofTacticInfo i         => i.format ctx
   | ofTermInfo i           => i.format ctx
@@ -243,8 +237,6 @@ def Info.format (ctx : ContextInfo) : Info → IO Format
   | ofFieldRedeclInfo i    => pure <| i.format ctx
   | ofDelabTermInfo i      => i.format ctx
   | ofChoiceInfo i         => pure <| i.format ctx
-  | ofDocInfo i            => pure <| i.format ctx
-  | ofDocElabInfo i        => pure <| i.format ctx
 
 def Info.toElabInfo? : Info → Option ElabInfo
   | ofTacticInfo i         => some i.toElabInfo
@@ -262,8 +254,6 @@ def Info.toElabInfo? : Info → Option ElabInfo
   | ofFieldRedeclInfo _    => none
   | ofDelabTermInfo i      => some i.toElabInfo
   | ofChoiceInfo i         => some i.toElabInfo
-  | ofDocInfo i            => some i.toElabInfo
-  | ofDocElabInfo i        => some i.toElabInfo
 
 /--
   Helper function for propagating the tactic metavariable context to its children nodes.

src/Lean/Elab/InfoTree/Types.lean

@@ -207,32 +207,6 @@ the language server provide interactivity even when all overloaded elaborators f
 -/
 structure ChoiceInfo extends ElabInfo where
 
-inductive DocElabKind where
-  | role | codeBlock | directive | command
-deriving Repr
-
-/--
-Indicates that an extensible document elaborator was used. This info is applied to the name on a
-role, directive, code block, or command, and is used to generate the hover.
-
-A `TermInfo` would not give the correct hover for a few reasons:
- 1. The name used to invoke a document extension is not necessarily the name of the elaborator that
-    was used, but the elaborator's docstring should be shown rather than that of the name as
-    written.
- 2. The underlying elaborator's Lean type is not an appropriate signature to show to users.
--/
-structure DocElabInfo extends ElabInfo where
-  name : Name
-  kind : DocElabKind
-
-/--
-Indicates that a piece of syntax was elaborated as documentation. This info is used for ordinary
-documentation constructs, such as paragraphs, list items, and links. It can be used to determine
-that a given piece of documentation syntax in fact has been elaborated.
--/
-structure DocInfo extends ElabInfo where
-
-
 /-- Header information for a node in `InfoTree`. -/
 inductive Info where
   | ofTacticInfo (i : TacticInfo)
@@ -250,8 +224,6 @@ inductive Info where
   | ofFieldRedeclInfo (i : FieldRedeclInfo)
   | ofDelabTermInfo (i : DelabTermInfo)
   | ofChoiceInfo (i : ChoiceInfo)
-  | ofDocInfo (i : DocInfo)
-  | ofDocElabInfo (i : DocElabInfo)
   deriving Inhabited
 
 /-- The InfoTree is a structure that is generated during elaboration and used

src/Lean/Elab/Tactic/BoolToPropSimps.lean

@@ -14,3 +14,8 @@ public section
 builtin_initialize bool_to_prop : Lean.Meta.SimpExtension ←
   Lean.Meta.registerSimpAttr `bool_to_prop
     "simp lemmas converting boolean expressions in terms of `decide` into propositional statements"
+
+@[deprecated bool_to_prop (since := "2025-02-10")]
+builtin_initialize boolToPropSimps : Lean.Meta.SimpExtension ←
+  Lean.Meta.registerSimpAttr `boolToPropSimps
+    "simp lemmas converting boolean expressions in terms of `decide` into propositional statements"

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

@@ -707,3 +707,8 @@ def evalOmega : Tactic
 builtin_initialize bitvec_to_nat : SimpExtension ←
   registerSimpAttr `bitvec_to_nat
     "simp lemmas converting `BitVec` goals to `Nat` goals"
+
+@[deprecated bitvec_to_nat (since := "2025-02-10")]
+builtin_initialize bvOmegaSimpExtension : SimpExtension ←
+  registerSimpAttr `bv_toNat
+    "simp lemmas converting `BitVec` goals to `Nat` goals, for the `bv_omega` preprocessor"

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

@@ -216,7 +216,7 @@ def analyzeAtom (e : Expr) : OmegaM (List Expr) := do
         | some _ =>
           let b_pos := mkApp4 (.const ``LT.lt [0]) (.const ``Nat []) (.const ``instLTNat [])
             (toExpr (0 : Nat)) b
-          let pow_pos := mkApp3 (.const ``Nat.pow_pos []) b exp (← mkDecideProof b_pos)
+          let pow_pos := mkApp3 (.const ``Nat.pos_pow_of_pos []) b exp (← mkDecideProof b_pos)
           let cast_pos := mkApp2 (.const ``Int.ofNat_pos_of_pos []) k' pow_pos
           pure [mkApp3 (.const ``Int.emod_nonneg []) x k
                   (mkApp3 (.const ``Int.ne_of_gt []) k (toExpr (0 : Int)) cast_pos),

src/Lean/Elab/Util.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Lean.Parser.Extension
+import Lean.Parser.Extension
 meta import Lean.Parser.Command
 public import Lean.KeyedDeclsAttribute
 public import Lean.Elab.Exception

src/Lean/Linter/MissingDocs.lean

@@ -126,10 +126,6 @@ def hasInheritDoc (attrs : Syntax) : Bool :=
     attr[1].isOfKind ``Parser.Attr.simple &&
     attr[1][0].getId.eraseMacroScopes == `inherit_doc
 
-def hasTacticAlt (attrs : Syntax) : Bool :=
-  attrs[0][1].getSepArgs.any fun attr =>
-    attr[1].isOfKind ``Parser.Attr.tactic_alt
-
 def declModifiersPubNoDoc (mods : Syntax) : CommandElabM Bool := do
   let isPublic := if (← getEnv).header.isModule && !(← getScope).isPublic then
     mods[2][0].getKind == ``Command.public else
@@ -205,7 +201,7 @@ def checkMixfix : SimpleHandler := fun stx => do
 
 @[builtin_missing_docs_handler «syntax»]
 def checkSyntax : SimpleHandler := fun stx => do
-  if stx[0].isNone && stx[2][0][0].getKind != ``«local» && !hasInheritDoc stx[1] && !hasTacticAlt stx[1] then
+  if stx[0].isNone && stx[2][0][0].getKind != ``«local» && !hasInheritDoc stx[1] then
     if stx[5].isNone then lint stx[3] "syntax"
     else lintNamed stx[5][0][3] "syntax"
 
@@ -221,13 +217,13 @@ def checkSyntaxCat : SimpleHandler := mkSimpleHandler "syntax category"
 
 @[builtin_missing_docs_handler «macro»]
 def checkMacro : SimpleHandler := fun stx => do
-  if stx[0].isNone && stx[2][0][0].getKind != ``«local» && !hasInheritDoc stx[1] && !hasTacticAlt stx[1] then
+  if stx[0].isNone && stx[2][0][0].getKind != ``«local» && !hasInheritDoc stx[1] then
     if stx[5].isNone then lint stx[3] "macro"
     else lintNamed stx[5][0][3] "macro"
 
 @[builtin_missing_docs_handler «elab»]
 def checkElab : SimpleHandler := fun stx => do
-  if stx[0].isNone && stx[2][0][0].getKind != ``«local» && !hasInheritDoc stx[1] && !hasTacticAlt stx[1] then
+  if stx[0].isNone && stx[2][0][0].getKind != ``«local» && !hasInheritDoc stx[1] then
     if stx[5].isNone then lint stx[3] "elab"
     else lintNamed stx[5][0][3] "elab"
 

src/Lean/Meta/Basic.lean

@@ -415,10 +415,6 @@ structure PostponedEntry where
 structure Diagnostics where
   /-- Number of times each declaration has been unfolded -/
   unfoldCounter : PHashMap Name Nat := {}
-  /--
-  Number of times each axiom was tried to be unfolded, which may point to an inaccessible def value.
-  -/
-  unfoldAxiomCounter : PHashMap Name Nat := {}
   /-- Number of times `f a =?= f b` heuristic has been used per function `f`. -/
   heuristicCounter : PHashMap Name Nat := {}
   /-- Number of times a TC instance is used. -/
@@ -674,30 +670,21 @@ def mkInfoCacheKey (expr : Expr) (nargs? : Option Nat) : MetaM InfoCacheKey :=
 
 /-- If diagnostics are enabled, record that `declName` has been unfolded. -/
 def recordUnfold (declName : Name) : MetaM Unit := do
-  modifyDiag fun { unfoldCounter, unfoldAxiomCounter, heuristicCounter, instanceCounter, synthPendingFailures } =>
+  modifyDiag fun { unfoldCounter, heuristicCounter, instanceCounter, synthPendingFailures } =>
     let newC := if let some c := unfoldCounter.find? declName then c + 1 else 1
-    { unfoldCounter := unfoldCounter.insert declName newC, unfoldAxiomCounter, heuristicCounter, instanceCounter, synthPendingFailures }
-
-def recordUnfoldAxiom (declName : Name) : MetaM Unit := do
-  modifyDiag fun { unfoldCounter, unfoldAxiomCounter, heuristicCounter, instanceCounter, synthPendingFailures } =>
-    let newC := if let some c := unfoldAxiomCounter.find? declName then c + 1 else 1
-    { unfoldCounter, unfoldAxiomCounter := unfoldAxiomCounter.insert declName newC, heuristicCounter, instanceCounter, synthPendingFailures }
-
-def resetUnfoldAxiom : MetaM Unit := do
-  modifyDiag fun { unfoldCounter, heuristicCounter, instanceCounter, synthPendingFailures, .. } =>
-    { unfoldCounter, unfoldAxiomCounter := {}, heuristicCounter, instanceCounter, synthPendingFailures }
+    { unfoldCounter := unfoldCounter.insert declName newC, heuristicCounter, instanceCounter, synthPendingFailures }
 
 /-- If diagnostics are enabled, record that heuristic for solving `f a =?= f b` has been used. -/
 def recordDefEqHeuristic (declName : Name) : MetaM Unit := do
-  modifyDiag fun { unfoldCounter, unfoldAxiomCounter, heuristicCounter, instanceCounter, synthPendingFailures } =>
+  modifyDiag fun { unfoldCounter, heuristicCounter, instanceCounter, synthPendingFailures } =>
     let newC := if let some c := heuristicCounter.find? declName then c + 1 else 1
-    { unfoldCounter, unfoldAxiomCounter, heuristicCounter := heuristicCounter.insert declName newC, instanceCounter, synthPendingFailures }
+    { unfoldCounter, heuristicCounter := heuristicCounter.insert declName newC, instanceCounter, synthPendingFailures }
 
 /-- If diagnostics are enabled, record that instance `declName` was used during TC resolution. -/
 def recordInstance (declName : Name) : MetaM Unit := do
-  modifyDiag fun { unfoldCounter, unfoldAxiomCounter, heuristicCounter, instanceCounter, synthPendingFailures } =>
+  modifyDiag fun { unfoldCounter, heuristicCounter, instanceCounter, synthPendingFailures } =>
     let newC := if let some c := instanceCounter.find? declName then c + 1 else 1
-    { unfoldCounter, unfoldAxiomCounter, heuristicCounter, instanceCounter := instanceCounter.insert declName newC, synthPendingFailures }
+    { unfoldCounter, heuristicCounter, instanceCounter := instanceCounter.insert declName newC, synthPendingFailures }
 
 /-- If diagnostics are enabled, record that synth pending failures. -/
 def recordSynthPendingFailure (type : Expr) : MetaM Unit := do
@@ -705,8 +692,8 @@ def recordSynthPendingFailure (type : Expr) : MetaM Unit := do
     unless (← get).diag.synthPendingFailures.contains type do
       -- We need to save the full context since type class resolution uses multiple metavar contexts and different local contexts
       let msg ← addMessageContextFull m!"{type}"
-      modifyDiag fun { unfoldCounter, unfoldAxiomCounter, heuristicCounter, instanceCounter, synthPendingFailures } =>
-        { unfoldCounter, unfoldAxiomCounter, heuristicCounter, instanceCounter, synthPendingFailures := synthPendingFailures.insert type msg }
+      modifyDiag fun { unfoldCounter, heuristicCounter, instanceCounter, synthPendingFailures } =>
+        { unfoldCounter, heuristicCounter, instanceCounter, synthPendingFailures := synthPendingFailures.insert type msg }
 
 def getLocalInstances : MetaM LocalInstances :=
   return (← read).localInstances

src/Lean/Meta/Check.lean

@@ -8,7 +8,6 @@ module
 prelude
 public import Lean.Meta.InferType
 public import Lean.Meta.Sorry
-import Lean.AddDecl
 
 public section
 
@@ -207,13 +206,13 @@ def mkHasTypeButIsExpectedMsg (givenType expectedType : Expr)
     (trailing? : Option MessageData := none) (trailingExprs : Array Expr := #[])
     : MetaM MessageData := do
   return MessageData.ofLazyM (es := #[givenType, expectedType] ++ trailingExprs) do
-    let mut msg ← (try
+    try
       let givenTypeType ← inferType givenType
       let expectedTypeType ← inferType expectedType
       if (← isDefEqGuarded givenTypeType expectedTypeType) then
         let (givenType, expectedType) ← addPPExplicitToExposeDiff givenType expectedType
         let trailing := trailing?.map (m!"\n" ++ ·) |>.getD .nil
-        pure m!"has type{indentExpr givenType}\n\
+        return m!"has type{indentExpr givenType}\n\
           but is expected to have type{indentExpr expectedType}{trailing}"
       else
         let (givenType, expectedType) ← addPPExplicitToExposeDiff givenType expectedType
@@ -221,25 +220,12 @@ def mkHasTypeButIsExpectedMsg (givenType expectedType : Expr)
         let trailing := match trailing? with
           | none => inlineExprTrailing expectedTypeType
           | some trailing => inlineExpr expectedTypeType ++ trailing
-        pure m!"has type{indentExpr givenType}\nof sort{inlineExpr givenTypeType}\
+        return m!"has type{indentExpr givenType}\nof sort{inlineExpr givenTypeType}\
           but is expected to have type{indentExpr expectedType}\nof sort{trailing}"
     catch _ =>
       let (givenType, expectedType) ← addPPExplicitToExposeDiff givenType expectedType
       let trailing := trailing?.map (m!"\n" ++ ·) |>.getD .nil
-      pure m!"has type{indentExpr givenType}\nbut is expected to have type{indentExpr expectedType}{trailing}")
-    let env ← getEnv
-    if env.header.isModule then
-      let origDiag := (← get).diag
-      let _ ← observing <| withOptions (diagnostics.set · true)  <| isDefEq givenType expectedType
-      let blocked := (← get).diag.unfoldAxiomCounter.toList.filterMap fun (n, count) => do
-        let count := count - origDiag.unfoldAxiomCounter.findD n 0
-        guard <| count > 0 && getOriginalConstKind? env n matches some .defn
-        return m!"{.ofConstName n} ↦ {count}"
-      if !blocked.isEmpty then
-        msg := msg ++ MessageData.note m!"The following definitions were not unfolded because \
-          their definition is not exposed:{indentD <| .joinSep blocked Format.line}"
-      modify ({ · with diag := origDiag })
-    return msg
+      return m!"has type{indentExpr givenType}\nbut is expected to have type{indentExpr expectedType}{trailing}"
 
 def throwAppTypeMismatch (f a : Expr) : MetaM α := do
   -- Clarify that `a` is "last" only if it may be confused with some preceding argument; otherwise,

src/Lean/Meta/GetUnfoldableConst.lean

@@ -58,7 +58,6 @@ def getUnfoldableConstNoEx? (constName : Name) : MetaM (Option ConstantInfo) :=
   match (← getEnv).find? constName with
   | some (info@(.thmInfo _))  => getTheoremInfo info
   | some (info@(.defnInfo _)) => if (← canUnfold info) then return info else return none
-  | some (.axiomInfo _)       => recordUnfoldAxiom constName; return none
   | _                         => return none
 
 end Meta

src/Lean/Meta/Tactic/Grind.lean

@@ -39,7 +39,6 @@ public import Lean.Meta.Tactic.Grind.SynthInstance
 public import Lean.Meta.Tactic.Grind.AC
 public import Lean.Meta.Tactic.Grind.VarRename
 public import Lean.Meta.Tactic.Grind.ProofUtil
-public import Lean.Meta.Tactic.Grind.PropagateInj
 
 public section
 
@@ -81,7 +80,7 @@ builtin_initialize registerTraceClass `grind.debug.final
 builtin_initialize registerTraceClass `grind.debug.forallPropagator
 builtin_initialize registerTraceClass `grind.debug.split
 builtin_initialize registerTraceClass `grind.debug.canon
-builtin_initialize registerTraceClass `grind.debug.theorem.activate
+builtin_initialize registerTraceClass `grind.debug.ematch.activate
 builtin_initialize registerTraceClass `grind.debug.ematch.pattern
 builtin_initialize registerTraceClass `grind.debug.beta
 builtin_initialize registerTraceClass `grind.debug.internalize

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

@@ -4,9 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
+
 prelude
 public import Lean.Meta.Tactic.Grind.ExprPtr
+
 public section
+
 namespace Lean.Meta.Grind
 
 private def hashChild (e : Expr) : UInt64 :=

src/Lean/Meta/Tactic/Grind/Arith/CommRing/DenoteExpr.lean

@@ -8,7 +8,7 @@ prelude
 public import Init.Grind.Ring.CommSemiringAdapter
 public import Lean.Meta.Tactic.Grind.Types
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadRing
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
 /-!

src/Lean/Meta/Tactic/Grind/Arith/CommRing/SemiringM.lean

@@ -12,7 +12,7 @@ public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadRing
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadSemiring
 import Init.Grind.Ring.CommSemiringAdapter
 import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
 

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/DvdCnstr.lean

@@ -6,8 +6,6 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
-import Init.Data.Int.OfNat
-import Init.Grind.Propagator
 import Lean.Meta.Tactic.Simp.Arith.Int
 import Lean.Meta.Tactic.Grind.Simp
 import Lean.Meta.Tactic.Grind.PropagatorAttr

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/LeCnstr.lean

@@ -6,7 +6,6 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
-import Init.Data.Int.OfNat
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
 import Lean.Meta.Tactic.Simp.Arith.Int
 import Lean.Meta.Tactic.Grind.PropagatorAttr

src/Lean/Meta/Tactic/Grind/Arith/Linear/DenoteExpr.lean

@@ -8,7 +8,7 @@ prelude
 public import Lean.Meta.Tactic.Grind.Types
 public import Lean.Meta.Tactic.Grind.Arith.Linear.LinearM
 import Lean.Meta.Tactic.Grind.Arith.Util
-public import Lean.Meta.Tactic.Grind.Arith.Linear.Util
+import Lean.Meta.Tactic.Grind.Arith.Linear.Util
 import Lean.Meta.Tactic.Grind.Simp
 import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
 import Lean.Meta.Tactic.Grind.Arith.Linear.Var

src/Lean/Meta/Tactic/Grind/Arith/Main.lean

@@ -6,7 +6,6 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Types
-import Init.Grind.Propagator
 import Lean.Meta.Tactic.Grind.PropagatorAttr
 import Lean.Meta.Tactic.Grind.Arith.Offset.Types
 import Lean.Meta.Tactic.Grind.Arith.Offset.Main

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

@@ -4,9 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
+
 prelude
 public import Lean.Meta.Tactic.Grind.Types
+
 public section
+
 namespace Lean.Meta.Grind
 
 /-- Returns all lambda expressions in the equivalence class with root `root`. -/

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

@@ -4,9 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
+
 prelude
 public import Lean.Meta.Tactic.Cases
+
 public section
+
 namespace Lean.Meta.Grind
 
 /-- Types that `grind` will case-split on. -/

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

@@ -7,7 +7,6 @@ module
 prelude
 public import Lean.Meta.Tactic.Util
 import Lean.Meta.Tactic.Grind.Types
-import Lean.Meta.Tactic.Grind.Util
 import Lean.Meta.Tactic.Cases
 import Lean.Meta.Match.MatcherApp
 import Lean.Meta.Tactic.Grind.MatchCond

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

@@ -4,18 +4,21 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
+
 prelude
+public import Init.Grind.Util
+public import Lean.Meta.LitValues
 public import Lean.Meta.Tactic.Grind.Types
-import Init.Grind.Util
-import Lean.Meta.LitValues
-import Lean.Meta.Tactic.Grind.Inv
-import Lean.Meta.Tactic.Grind.PP
-import Lean.Meta.Tactic.Grind.Ctor
-import Lean.Meta.Tactic.Grind.Util
-import Lean.Meta.Tactic.Grind.Beta
-import Lean.Meta.Tactic.Grind.Simp
-import Lean.Meta.Tactic.Grind.Internalize
+public import Lean.Meta.Tactic.Grind.Inv
+public import Lean.Meta.Tactic.Grind.PP
+public import Lean.Meta.Tactic.Grind.Ctor
+public import Lean.Meta.Tactic.Grind.Util
+public import Lean.Meta.Tactic.Grind.Beta
+public import Lean.Meta.Tactic.Grind.Internalize
+public import Lean.Meta.Tactic.Grind.Simp
+
 public section
+
 namespace Lean.Meta.Grind
 
 /--

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

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
+
 prelude
 public import Lean.Meta.Tactic.Grind.Types
 import Lean.Meta.Tactic.Grind.Simp

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

@@ -4,10 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
+
 prelude
+public import Init.Grind.Lemmas
 public import Lean.Meta.Tactic.Grind.Types
-import Init.Grind.Lemmas
+
 public section
+
 namespace Lean.Meta.Grind
 
 private def dummyEq : Expr := mkApp (mkConst ``Eq [1]) default

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

@@ -8,11 +8,9 @@ prelude
 public import Lean.Meta.Tactic.Grind.Types
 import Lean.Util.CollectLevelMVars
 import Lean.Meta.Tactic.Grind.Core
-import Lean.Meta.Tactic.Grind.Util
 import Lean.Meta.Tactic.Grind.MatchDiscrOnly
 import Lean.Meta.Tactic.Grind.ProveEq
 import Lean.Meta.Tactic.Grind.SynthInstance
-import Lean.Meta.Tactic.Grind.Simp
 public section
 namespace Lean.Meta.Grind
 namespace EMatch

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

@@ -5,16 +5,16 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
+public import Init.Grind.Util
+public import Init.Grind.Tactics
+public import Lean.HeadIndex
+public import Lean.Util.FoldConsts
+public import Lean.Util.CollectFVars
 public import Lean.Meta.Basic
+public import Lean.Meta.InferType
+public import Lean.Meta.Eqns
+public import Lean.Meta.Tactic.Grind.Util
 public import Lean.Meta.Tactic.Grind.Theorems
-import Init.Grind.Util
-import Init.Grind.Tactics
-import Lean.Util.FoldConsts
-import Lean.Util.CollectFVars
-import Lean.Meta.Basic
-import Lean.Meta.InferType
-import Lean.Meta.Eqns
-import Lean.Meta.Tactic.Grind.Util
 import Lean.Message
 import Lean.Meta.Tactic.FVarSubst
 import Lean.Meta.Match.Basic

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

@@ -4,12 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
+
 prelude
-public import Lean.Meta.Basic
-import Lean.Meta.AppBuilder
-import Lean.Meta.MatchUtil
-import Lean.Util.ForEachExpr
+public import Lean.Meta.AppBuilder
+public import Lean.Meta.MatchUtil
+public import Lean.Util.ForEachExpr
+
 public section
+
 namespace Lean.Meta.Grind
 /-! A basic "equality resolution" procedure. -/
 

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

@@ -4,9 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
+
 prelude
 public import Lean.Expr
+
 public section
+
 namespace Lean.Meta.Grind
 
 @[inline] def isSameExpr (a b : Expr) : Bool :=

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

@@ -4,10 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
+
 prelude
 public import Lean.Meta.Tactic.Grind.Types
-import Lean.Meta.Tactic.Grind.SynthInstance
+public import Lean.Meta.Tactic.Grind.SynthInstance
+
 public section
+
 namespace Lean.Meta.Grind
 /-! Extensionality theorems support. -/
 

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

@@ -4,9 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
+
 prelude
 public import Lean.Meta.Tactic.Ext
+
 public section
+
 namespace Lean.Meta.Grind
 /-! Grind extensionality attribute to mark which `[ext]` theorems should be used. -/
 

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

@@ -7,10 +7,8 @@ module
 prelude
 public import Lean.Meta.Tactic.Grind.Types
 public import Init.Grind.Propagator
-import Init.Simproc
 import Init.Grind.Lemmas
 import Init.Grind.Norm
-import Lean.Meta.Tactic.Grind.PropagatorAttr
 import Lean.Meta.Tactic.Grind.Propagate
 import Lean.Meta.Tactic.Grind.Internalize
 import Lean.Meta.Tactic.Grind.Simp
@@ -129,22 +127,23 @@ def propagateForallPropDown (e : Expr) : GoalM Unit := do
       let h := mkOfEqTrueCore e (← mkEqTrueProof e)
       let h' := mkApp h' h
       addNewRawFact h' e' (← getGeneration e) (.forallProp e)
-    if b.hasLooseBVars then
-      unless (← isProp a) do
-        /-
-        We used to waste a lot of time trying to process terms such as
-        ```
-        ∀ (h : i + 1 ≤ w), x.abs.getLsbD i = x.abs[i]
-        ```
-        as E-matching theorems. They are "dependent" implications, and should be handled
-        by `propagateForallPropUp`.
-        -/
-        addLocalEMatchTheorems e
     else
-      unless (← alreadyInternalized b) do return ()
-      if (← isEqFalse b <&&> isProp a) then
-      -- (a → b) = True → b = False → a = False
-      pushEqFalse a <| mkApp4 (mkConst ``Grind.eq_false_of_imp_eq_true) a b (← mkEqTrueProof e) (← mkEqFalseProof b)
+      if b.hasLooseBVars then
+        unless (← isProp a) do
+          /-
+          We used to waste a lot of time trying to process terms such as
+          ```
+          ∀ (h : i + 1 ≤ w), x.abs.getLsbD i = x.abs[i]
+          ```
+          as E-matching theorems. They are "dependent" implications, and should be handled
+          by `propagateForallPropUp`.
+          -/
+          addLocalEMatchTheorems e
+      else
+        unless (← alreadyInternalized b) do return ()
+        if (← isEqFalse b <&&> isProp a) then
+        -- (a → b) = True → b = False → a = False
+        pushEqFalse a <| mkApp4 (mkConst ``Grind.eq_false_of_imp_eq_true) a b (← mkEqTrueProof e) (← mkEqFalseProof b)
 
 builtin_grind_propagator propagateExistsDown ↓Exists := fun e => do
   if (← isEqFalse e) then

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

@@ -4,11 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
+
 prelude
-public import Lean.Meta.Basic
-import Lean.Meta.CtorRecognizer
-import Lean.Meta.Tactic.Util
-import Lean.Meta.Tactic.Clear
+public import Lean.Meta.CtorRecognizer
+public import Lean.Meta.Tactic.Util
+public import Lean.Meta.Tactic.Clear
 import Lean.Meta.AppBuilder
 
 public section

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

@@ -5,13 +5,11 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Lean.Meta.Tactic.Grind.EMatchTheorem
-import Lean.Meta.FunInfo
+public import Lean.Meta.Tactic.Grind.Theorems
 public section
 namespace Lean.Meta.Grind
 
 builtin_initialize registerTraceClass `grind.inj
-builtin_initialize registerTraceClass `grind.inj.assert
 builtin_initialize registerTraceClass `grind.debug.inj
 
 /-- A theorem marked with `@[grind inj]` -/
@@ -39,35 +37,16 @@ private builtin_initialize injectiveTheoremsExt : SimpleScopedEnvExtension Injec
       initial  := {}
     }
 
-private partial def getSymbols (proof : Expr) (hasUniverses : Bool) : MetaM (List HeadIndex) := do
+private def getSymbols (proof : Expr) : MetaM (List HeadIndex) := do
   let type ← inferType proof
-  forallTelescope type fun xs type => do
+  forallTelescope type fun _ type => do
     unless type.isAppOfArity ``Function.Injective 3 do
       throwError "invalid `[grind inj]` theorem, resulting type is not of the form `Function.Injective <fun>`{indentExpr type}"
-    if xs.isEmpty && hasUniverses then
-      throwError "invalid `[grind inj]` theorem, theorem has universe levels, but no hypotheses{indentExpr type}"
-    let f := type.appArg!.eta
-    let cs ← collectFnNames f
+    let f := type.appArg!
+    let cs : NameSet := f.foldConsts (init := {}) fun declName s => s.insert declName
     if cs.isEmpty then
-      throwError "invalid `[grind inj]` theorem, injective function must use at least one constant function symbol{indentExpr f}"
+      throwError "invalid `[grind inj]` theorem, injective function must use at least one constant symbol{indentExpr f}"
     return cs.toList.map (.const ·)
-where
-  collectFnNames (f : Expr) : MetaM NameSet := do
-    if let .const declName _ := f then
-      return { declName }
-    else
-      Prod.snd <$> (go f |>.run {})
-
-  go (e : Expr) : StateRefT NameSet MetaM Unit := do
-    if e.isApp then e.withApp fun f args => do
-      if let .const declName _ := f then
-        modify (·.insert declName)
-      let kinds ← NormalizePattern.getPatternArgKinds f args.size
-      for h : i in *...args.size do
-        let arg  := args[i]
-        let kind := kinds[i]?.getD .relevant
-        if kind matches .relevant | .typeFormer then
-          go arg
 
 private def symbolsToNames (s : List HeadIndex) : List Name :=
   s.map fun
@@ -75,9 +54,8 @@ private def symbolsToNames (s : List HeadIndex) : List Name :=
     | _ => Name.anonymous
 
 def mkInjectiveTheorem (declName : Name) : MetaM InjectiveTheorem := do
-  let info ← getConstInfo declName
   let proof ← getProofForDecl declName
-  let symbols ← getSymbols proof !info.levelParams.isEmpty
+  let symbols ← getSymbols proof
   trace[grind.inj] "{declName}: {symbolsToNames symbols}"
   return {
     levelParams := #[]

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

@@ -5,10 +5,9 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Lean.Meta.Tactic.Grind.Types
-import Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
-import Init.Grind.Util
-import Init.Grind.Lemmas
+public import Init.Grind.Util
+public import Init.Grind.Lemmas
+public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
 import Lean.Meta.LitValues
 import Lean.Meta.Match.MatcherInfo
 import Lean.Meta.Match.MatchEqsExt
@@ -19,7 +18,6 @@ import Lean.Meta.Tactic.Grind.Beta
 import Lean.Meta.Tactic.Grind.MatchCond
 import Lean.Meta.Tactic.Grind.Simp
 import Lean.Meta.Tactic.Grind.MarkNestedSubsingletons
-import Lean.Meta.Tactic.Grind.PropagateInj
 public section
 namespace Lean.Meta.Grind
 
@@ -237,65 +235,22 @@ private def addMatchEqns (f : Expr) (generation : Nat) : GoalM Unit := do
     -- We disable pattern normalization to prevent the `match`-expression to be reduced.
     activateTheorem (← mkEMatchEqTheorem eqn (normalizePattern := false)) generation
 
-@[specialize]
-private def activateTheoremsCore [TheoremLike α] (declName : Name)
-    (getThms : GoalM (Theorems α))
-    (setThms : Theorems α → GoalM Unit)
-    (reinsertThm : α → GoalM Unit)
-    (activateThm : α → GoalM Unit) : GoalM Unit := do
-  if let some (thms, s) := (← getThms).retrieve? declName then
-    setThms s
+private def activateTheoremPatterns (fName : Name) (generation : Nat) : GoalM Unit := do
+  if let some (thms, thmMap) := (← get).ematch.thmMap.retrieve? fName then
+    modify fun s => { s with ematch.thmMap := thmMap }
     for thm in thms do
-      let origin := TheoremLike.getOrigin thm
-      trace_goal[grind.debug.theorem.activate] "`{declName}` => `{origin.key}`"
-      unless s.isErased origin do
-        let appMap  := (← get).appMap
-        let symbols := TheoremLike.getSymbols thm
-        let symbols := symbols.filter fun sym => !appMap.contains sym
-        let thm     := TheoremLike.setSymbols thm symbols
+      trace_goal[grind.debug.ematch.activate] "`{fName}` => `{thm.origin.key}`"
+      unless (← get).ematch.thmMap.isErased thm.origin do
+        let appMap := (← get).appMap
+        let symbols := thm.symbols.filter fun sym => !appMap.contains sym
+        let thm := { thm with symbols }
         match symbols with
         | [] =>
-          trace_goal[grind.debug.theorem.activate] "`{origin.key}`"
-          activateThm thm
+          trace_goal[grind.debug.ematch.activate] "`{thm.origin.key}`"
+          activateTheorem thm generation
         | _ =>
-          trace_goal[grind.debug.theorem.activate] "reinsert `{origin.key}`"
-          reinsertThm thm
-
-private def activateTheoremPatterns (fName : Name) (generation : Nat) : GoalM Unit := do
-  activateTheoremsCore fName (return (← get).ematch.thmMap)
-    (fun thmMap => modify fun s => { s with ematch.thmMap := thmMap })
-    (fun thm => modify fun s => { s with ematch.thmMap := s.ematch.thmMap.insert thm })
-    (fun thm => activateTheorem thm generation)
-
-private def mkEMatchTheoremWithKind'? (origin : Origin) (levelParams : Array Name) (proof : Expr) (kind : EMatchTheoremKind)
-    (symPrios : SymbolPriorities) : MetaM (Option EMatchTheorem) := do
-  try
-    mkEMatchTheoremWithKind? origin levelParams proof kind symPrios (minIndexable := true)
-  catch _ =>
-    return none
-
-private def activateInjectiveTheorem (injThm : InjectiveTheorem) (generation : Nat) : GoalM Unit := do
-  let type ← inferType injThm.proof
-  if type.isForall then
-    let symPrios ← getSymbolPriorities
-    let thm? ← mkEMatchTheoremWithKind'? injThm.origin injThm.levelParams injThm.proof .fwd symPrios
-      <||>
-      mkEMatchTheoremWithKind'? injThm.origin injThm.levelParams injThm.proof (.default false) symPrios
-    let some thm := thm? | reportIssue! "failed to assert injectivity theorem `{injThm.origin.pp}`"
-    activateTheorem thm generation
-  else
-    addNewRawFact injThm.proof type generation (.inj injThm.origin)
-
-private def activateInjectiveTheorems (declName : Name) (generation : Nat) : GoalM Unit := do
-  if (← getConfig).inj then
-    activateTheoremsCore declName (return (← get).inj.thms)
-      (fun thms => modify fun s => { s with inj.thms := thms })
-      (fun thm => modify fun s => { s with inj.thms := s.inj.thms.insert thm })
-      (fun thm => activateInjectiveTheorem thm generation)
-
-private def activateTheorems (declName : Name) (generation : Nat) : GoalM Unit := do
-  activateTheoremPatterns declName generation
-  activateInjectiveTheorems declName generation
+          trace_goal[grind.debug.ematch.activate] "reinsert `{thm.origin.key}`"
+          modify fun s => { s with ematch.thmMap := s.ematch.thmMap.insert thm }
 
 /--
 If type of `a` is a structure and is tagged with `[grind ext]` attribute,
@@ -456,7 +411,7 @@ where
       mkENode e generation
     | .const declName _ =>
       mkENode e generation
-      activateTheorems declName generation
+      activateTheoremPatterns declName generation
     | .mvar .. =>
       if (← reportMVarInternalization) then
         reportIssue! "unexpected metavariable during internalization{indentExpr e}\n`grind` is not supposed to be used in goals containing metavariables."
@@ -499,7 +454,7 @@ where
           registerParent e c
         else
           if let .const fName _ := f then
-            activateTheorems fName generation
+            activateTheoremPatterns fName generation
           else
             internalizeImpl f generation e
           registerParent e f
@@ -511,6 +466,5 @@ where
         Solvers.internalize e parent?
         propagateUp e
         propagateBetaForNewApp e
-        mkInjEq e
 
 end Lean.Meta.Grind

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

@@ -11,7 +11,6 @@ public import Lean.Meta.Tactic.Grind.SearchM
 import Lean.Meta.Tactic.Assert
 import Lean.Meta.Tactic.Apply
 import Lean.Meta.Tactic.Grind.Simp
-import Lean.Meta.Tactic.Grind.Util
 import Lean.Meta.Tactic.Grind.Cases
 import Lean.Meta.Tactic.Grind.CasesMatch
 import Lean.Meta.Tactic.Grind.Injection

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

@@ -6,10 +6,8 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Types
-import Init.Grind.Util
 import Lean.Meta.Tactic.Grind.Proof
 import Lean.Meta.Tactic.Grind.MatchCond
-import Lean.Meta.Tactic.Grind.Util
 namespace Lean.Meta.Grind
 /-!
 Debugging support code for checking basic invariants.

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

@@ -4,20 +4,23 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
+
 prelude
 public import Lean.Meta.Tactic.Grind.Types
-import Lean.Meta.Tactic.Grind.Util
-import Lean.Meta.Tactic.Grind.SynthInstance
+public import Lean.Meta.Tactic.Grind.SynthInstance
+
 public section
-namespace Lean.Meta.Grind
+
 /-!
 Support for type class `LawfulEqCmp`.
 -/
 /-
-**Note**: we will have similar support for `Associative` and `Commutative`. In the future, we should have
+Note: we will have similar support for `Associative` and `Commutative`. In the future, we should have
 a mechanism for letting users to install their own handlers.
 -/
 
+namespace Lean.Meta.Grind
+
 /--
 If `op` implements `LawfulEqCmp`, then returns the proof term for
 `∀ a b, op a b = .eq → a = b`

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

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Types
-import Lean.Meta.Tactic.Grind.Canon
+public import Lean.Meta.Tactic.Grind.Canon
 import Lean.Meta.Tactic.Grind.CastLike
 public section
 namespace Lean.Meta.Grind

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

@@ -8,10 +8,8 @@ prelude
 public import Lean.Meta.Tactic.Util
 public import Lean.Meta.Tactic.Grind.Types
 import Init.Grind.Lemmas
-import Lean.PrettyPrinter
 import Lean.Meta.Tactic.ExposeNames
 import Lean.Meta.Tactic.Simp.Diagnostics
-import Lean.Meta.Tactic.Simp.Rewrite
 import Lean.Meta.Tactic.Grind.Split
 import Lean.Meta.Tactic.Grind.RevertAll
 import Lean.Meta.Tactic.Grind.PropagatorAttr
@@ -22,7 +20,6 @@ import Lean.Meta.Tactic.Grind.Inv
 import Lean.Meta.Tactic.Grind.Intro
 import Lean.Meta.Tactic.Grind.EMatch
 import Lean.Meta.Tactic.Grind.Solve
-import Lean.Meta.Tactic.Grind.Internalize
 import Lean.Meta.Tactic.Grind.SimpUtil
 import Lean.Meta.Tactic.Grind.Cases
 import Lean.Meta.Tactic.Grind.LawfulEqCmp

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

@@ -4,16 +4,19 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
+
 prelude
+public import Init.Grind.Util
+public import Lean.Util.PtrSet
+public import Lean.Meta.Transform
+public import Lean.Meta.Basic
+public import Lean.Meta.InferType
+public import Lean.Meta.Tactic.Grind.ExprPtr
+public import Lean.Meta.Tactic.Grind.Util
 public import Lean.Meta.Tactic.Grind.Types
-import Init.Grind.Util
-import Lean.Util.PtrSet
-import Lean.Meta.Transform
-import Lean.Meta.Basic
-import Lean.Meta.InferType
-import Lean.Meta.Tactic.Grind.ExprPtr
-import Lean.Meta.Tactic.Grind.Util
+
 public section
+
 namespace Lean.Meta.Grind
 
 private abbrev M := StateRefT (Std.HashMap ExprPtr Expr) GrindM

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

@@ -4,14 +4,16 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
+
 prelude
-public import Lean.Meta.Tactic.Grind.Types
-import Init.Grind
-import Init.Simproc
-import Lean.Meta.Tactic.Contradiction
-import Lean.Meta.Tactic.Grind.ProveEq
-import Lean.Meta.Tactic.Grind.PropagatorAttr
+public import Init.Grind
+public import Init.Simproc
+public import Lean.Meta.Tactic.Contradiction
+public import Lean.Meta.Tactic.Grind.ProveEq
+public import Lean.Meta.Tactic.Grind.PropagatorAttr
+
 public section
+
 namespace Lean.Meta.Grind
 /-
 Remark: the `simp` module has some support for `MatchCond`, but it is