feat: normalization for IntModule

This PR adds helper theorems for normalizing input atoms and support
for disequality in the new linear arithmetic procedure in `grind`

.github/workflows/build-template.yml

@@ -105,11 +105,11 @@ jobs:
           path: |
             .ccache
             ${{ matrix.name == 'Linux Lake' && 'build/stage1/**/*.trace
-            build/stage1/**/*.olean
+            build/stage1/**/*.olean*
             build/stage1/**/*.ilean
             build/stage1/**/*.c
             build/stage1/**/*.c.o*' || '' }}
-          key: ${{ matrix.name }}-build-v3-${{ github.event.pull_request.head.sha }}
+          key: ${{ matrix.name }}-build-v3-${{ github.sha }}
           # fall back to (latest) previous cache
           restore-keys: |
             ${{ matrix.name }}-build-v3
@@ -243,7 +243,7 @@ jobs:
           path: |
             .ccache
             ${{ matrix.name == 'Linux Lake' && 'build/stage1/**/*.trace
-            build/stage1/**/*.olean
+            build/stage1/**/*.olean*
             build/stage1/**/*.ilean
             build/stage1/**/*.c
             build/stage1/**/*.c.o*' || '' }}

.github/workflows/pr-release.yml

@@ -34,7 +34,7 @@ jobs:
       - name: Download artifact from the previous workflow.
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         id: download-artifact
-        uses: dawidd6/action-download-artifact@v9 # https://github.com/marketplace/actions/download-workflow-artifact
+        uses: dawidd6/action-download-artifact@v10 # https://github.com/marketplace/actions/download-workflow-artifact
         with:
           run_id: ${{ github.event.workflow_run.id }}
           path: artifacts

src/Init/Core.lean

@@ -95,7 +95,8 @@ structure Thunk (α : Type u) : Type u where
   -/
   mk ::
   /-- Extract the getter function out of a thunk. Use `Thunk.get` instead. -/
-  private fn : Unit → α
+  -- The field is public so as to allow computation through it.
+  fn : Unit → α
 
 attribute [extern "lean_mk_thunk"] Thunk.mk
 
@@ -117,6 +118,10 @@ Computed values are cached, so the value is not recomputed.
 @[extern "lean_thunk_get_own"] protected def Thunk.get (x : @& Thunk α) : α :=
   x.fn ()
 
+-- Ensure `Thunk.fn` is still computable even if it shouldn't be accessed directly.
+@[inline] private def Thunk.fnImpl (x : Thunk α) : Unit → α := fun _ => x.get
+@[csimp] private theorem Thunk.fn_eq_fnImpl : @Thunk.fn = @Thunk.fnImpl := rfl
+
 /--
 Constructs a new thunk that forces `x` and then applies `x` to the result. Upon forcing, the result
 of `f` is cached and the reference to the thunk `x` is dropped.

src/Init/Data/Array/Lemmas.lean

@@ -133,7 +133,6 @@ grind_pattern Array.getElem?_eq_none => xs.size ≤ i, xs[i]?
 theorem getElem?_eq_some_iff {xs : Array α} : xs[i]? = some b ↔ ∃ h : i < xs.size, xs[i] = b :=
   _root_.getElem?_eq_some_iff
 
-@[grind →]
 theorem getElem_of_getElem? {xs : Array α} : xs[i]? = some a → ∃ h : i < xs.size, xs[i] = a :=
   getElem?_eq_some_iff.mp
 
@@ -176,7 +175,7 @@ theorem getElem_push_lt {xs : Array α} {x : α} {i : Nat} (h : i < xs.size) :
   simp only [push, ← getElem_toList, List.concat_eq_append]
   rw [List.getElem_append_right] <;> simp [← getElem_toList, Nat.zero_lt_one]
 
-theorem getElem_push {xs : Array α} {x : α} {i : Nat} (h : i < (xs.push x).size) :
+@[grind =] theorem getElem_push {xs : Array α} {x : α} {i : Nat} (h : i < (xs.push x).size) :
     (xs.push x)[i] = if h : i < xs.size then xs[i] else x := by
   by_cases h' : i < xs.size
   · simp [getElem_push_lt, h']
@@ -763,6 +762,7 @@ theorem all_eq_false' {p : α → Bool} {as : Array α} :
   rw [Bool.eq_false_iff, Ne, all_eq_true']
   simp
 
+@[grind =]
 theorem any_eq {xs : Array α} {p : α → Bool} : xs.any p = decide (∃ i : Nat, ∃ h, p (xs[i]'h)) := by
   by_cases h : xs.any p
   · simp_all [any_eq_true]
@@ -777,6 +777,7 @@ theorem any_eq' {xs : Array α} {p : α → Bool} : xs.any p = decide (∃ x, x
     simp only [any_eq_false'] at h
     simpa using h
 
+@[grind =]
 theorem all_eq {xs : Array α} {p : α → Bool} : xs.all p = decide (∀ i, (_ : i < xs.size) → p xs[i]) := by
   by_cases h : xs.all p
   · simp_all [all_eq_true]
@@ -952,6 +953,13 @@ theorem set_push {xs : Array α} {x y : α} {h} :
         · simp at h
           omega
 
+@[grind _=_]
+theorem set_pop {xs : Array α} {x : α} {i : Nat} (h : i < xs.pop.size) :
+    xs.pop.set i x h = (xs.set i x (by simp at h; omega)).pop := by
+  ext i h₁ h₂
+  · simp
+  · simp [getElem_set]
+
 @[simp] theorem set_eq_empty_iff {xs : Array α} {i : Nat} {a : α} {h : i < xs.size} :
     xs.set i a = #[] ↔ xs = #[] := by
   cases xs <;> cases i <;> simp [set]
@@ -984,7 +992,11 @@ theorem mem_or_eq_of_mem_set
 @[simp, grind] theorem setIfInBounds_empty {i : Nat} {a : α} :
     #[].setIfInBounds i a = #[] := rfl
 
-@[simp] theorem set!_eq_setIfInBounds : @set! = @setIfInBounds := rfl
+@[simp, grind =] theorem set!_eq_setIfInBounds : set! xs i v = setIfInBounds xs i v := rfl
+
+@[grind]
+theorem setIfInBounds_def (xs : Array α) (i : Nat) (a : α) :
+    xs.setIfInBounds i a = if h : i < xs.size then xs.set i a else xs := rfl
 
 @[deprecated set!_eq_setIfInBounds (since := "2024-12-12")]
 abbrev set!_is_setIfInBounds := @set!_eq_setIfInBounds
@@ -1076,7 +1088,7 @@ theorem mem_or_eq_of_mem_setIfInBounds
   by_cases h : i < xs.size <;>
     simp [setIfInBounds, Nat.not_lt_of_le, h,  getD_getElem?]
 
-@[simp] theorem toList_setIfInBounds {xs : Array α} {i : Nat} {x : α} :
+@[simp, grind =] theorem toList_setIfInBounds {xs : Array α} {i : Nat} {x : α} :
     (xs.setIfInBounds i x).toList = xs.toList.set i x := by
   simp only [setIfInBounds]
   split <;> rename_i h
@@ -1258,7 +1270,8 @@ theorem map_singleton {f : α → β} {a : α} : map f #[a] = #[f a] := by simp
 
 -- We use a lower priority here as there are more specific lemmas in downstream libraries
 -- which should be able to fire first.
-@[simp 500] theorem mem_map {f : α → β} {xs : Array α} : b ∈ xs.map f ↔ ∃ a, a ∈ xs ∧ f a = b := by
+@[simp 500, grind =] theorem mem_map {f : α → β} {xs : Array α} :
+    b ∈ xs.map f ↔ ∃ a, a ∈ xs ∧ f a = b := by
   simp only [mem_def, toList_map, List.mem_map]
 
 theorem exists_of_mem_map (h : b ∈ map f l) : ∃ a, a ∈ l ∧ f a = b := mem_map.1 h
@@ -2994,6 +3007,10 @@ theorem extract_empty_of_size_le_start {xs : Array α} {start stop : Nat} (h : x
   apply ext'
   simp
 
+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
@@ -3731,7 +3748,7 @@ theorem back?_replicate {a : α} {n : Nat} :
 @[deprecated back?_replicate (since := "2025-03-18")]
 abbrev back?_mkArray := @back?_replicate
 
-@[simp] theorem back_replicate (w : 0 < n) : (replicate n a).back (by simpa using w) = a := by
+@[simp] theorem back_replicate {xs : Array α} (w : 0 < n) : (replicate n xs).back (by simpa using w) = xs := by
   simp [back_eq_getElem]
 
 @[deprecated back_replicate (since := "2025-03-18")]
@@ -4074,11 +4091,11 @@ abbrev all_mkArray := @all_replicate
 
 /-! ### modify -/
 
-@[simp] theorem size_modify {xs : Array α} {i : Nat} {f : α → α} : (xs.modify i f).size = xs.size := by
+@[simp, grind =] theorem size_modify {xs : Array α} {i : Nat} {f : α → α} : (xs.modify i f).size = xs.size := by
   unfold modify modifyM
   split <;> simp
 
-theorem getElem_modify {xs : Array α} {j i} (h : i < (xs.modify j f).size) :
+@[grind =] theorem getElem_modify {xs : Array α} {j i} (h : i < (xs.modify j f).size) :
     (xs.modify j f)[i] = if j = i then f (xs[i]'(by simpa using h)) else xs[i]'(by simpa using h) := by
   simp only [modify, modifyM]
   split
@@ -4086,7 +4103,7 @@ theorem getElem_modify {xs : Array α} {j i} (h : i < (xs.modify j f).size) :
   · simp only [Id.run_pure]
     rw [if_neg (mt (by rintro rfl; exact h) (by simp_all))]
 
-@[simp] theorem toList_modify {xs : Array α} {f : α → α} {i : Nat} :
+@[simp, grind =] theorem toList_modify {xs : Array α} {f : α → α} {i : Nat} :
     (xs.modify i f).toList = xs.toList.modify i f := by
   apply List.ext_getElem
   · simp
@@ -4101,7 +4118,7 @@ theorem getElem_modify_of_ne {xs : Array α} {i : Nat} (h : i ≠ j)
     (xs.modify i f)[j] = xs[j]'(by simpa using hj) := by
   simp [getElem_modify hj, h]
 
-theorem getElem?_modify {xs : Array α} {i : Nat} {f : α → α} {j : Nat} :
+@[grind =] theorem getElem?_modify {xs : Array α} {i : Nat} {f : α → α} {j : Nat} :
     (xs.modify i f)[j]? = if i = j then xs[j]?.map f else xs[j]? := by
   simp only [getElem?_def, size_modify, getElem_modify, Option.map_dif]
   split <;> split <;> rfl
@@ -4150,18 +4167,18 @@ theorem swap_comm {xs : Array α} {i j : Nat} (hi hj) : xs.swap i j hi hj = xs.s
     · split <;> simp_all
     · split <;> simp_all
 
-@[simp] theorem size_swapIfInBounds {xs : Array α} {i j : Nat} :
+@[simp, grind =] theorem size_swapIfInBounds {xs : Array α} {i j : Nat} :
     (xs.swapIfInBounds i j).size = xs.size := by unfold swapIfInBounds; split <;> (try split) <;> simp [size_swap]
 
 /-! ### swapAt -/
 
-@[simp] theorem swapAt_def {xs : Array α} {i : Nat} {v : α} (hi) :
+@[simp, grind =] theorem swapAt_def {xs : Array α} {i : Nat} {v : α} (hi) :
     xs.swapAt i v hi = (xs[i], xs.set i v) := rfl
 
 theorem size_swapAt {xs : Array α} {i : Nat} {v : α} (hi) :
     (xs.swapAt i v hi).2.size = xs.size := by simp
 
-@[simp]
+@[simp, grind =]
 theorem swapAt!_def {xs : Array α} {i : Nat} {v : α} (h : i < xs.size) :
     xs.swapAt! i v = (xs[i], xs.set i v) := by simp [swapAt!, h]
 
@@ -4329,42 +4346,44 @@ theorem getElem?_ofFn {f : Fin n → α} {i : Nat} :
 
 /-! ### Preliminaries about `range` and `range'` -/
 
-@[simp] theorem size_range' {start size step} : (range' start size step).size = size := by
+@[simp, grind =] theorem size_range' {start size step} : (range' start size step).size = size := by
   simp [range']
 
-@[simp] theorem toList_range' {start size step} :
+@[simp, grind =] theorem toList_range' {start size step} :
      (range' start size step).toList = List.range' start size step := by
   apply List.ext_getElem <;> simp [range']
 
-@[simp]
+@[simp, grind =]
 theorem getElem_range' {start size step : Nat} {i : Nat}
     (h : i < (Array.range' start size step).size) :
     (Array.range' start size step)[i] = start + step * i := by
   simp [← getElem_toList]
 
+@[grind =]
 theorem getElem?_range' {start size step : Nat} {i : Nat} :
     (Array.range' start size step)[i]? = if i < size then some (start + step * i) else none := by
   simp [getElem?_def, getElem_range']
 
-@[simp] theorem _root_.List.toArray_range' {start size step : Nat} :
+@[simp, grind =] theorem _root_.List.toArray_range' {start size step : Nat} :
     (List.range' start size step).toArray = Array.range' start size step := by
   apply ext'
   simp
 
-@[simp] theorem size_range {n : Nat} : (range n).size = n := by
+@[simp, grind =] theorem size_range {n : Nat} : (range n).size = n := by
   simp [range]
 
-@[simp] theorem toList_range {n : Nat} : (range n).toList = List.range n := by
+@[simp, grind =] theorem toList_range {n : Nat} : (range n).toList = List.range n := by
   apply List.ext_getElem <;> simp [range]
 
-@[simp]
+@[simp, grind =]
 theorem getElem_range {n : Nat} {i : Nat} (h : i < (Array.range n).size) : (Array.range n)[i] = i := by
   simp [← getElem_toList]
 
+@[grind =]
 theorem getElem?_range {n : Nat} {i : Nat} : (Array.range n)[i]? = if i < n then some i else none := by
   simp [getElem?_def, getElem_range]
 
-@[simp] theorem _root_.List.toArray_range {n : Nat} : (List.range n).toArray = Array.range n := by
+@[simp, grind =] theorem _root_.List.toArray_range {n : Nat} : (List.range n).toArray = Array.range n := by
   apply ext'
   simp
 

src/Init/Data/Array/MapIdx.lean

@@ -414,7 +414,7 @@ theorem mapIdx_eq_mapIdx_iff {xs : Array α} :
   rcases xs with ⟨xs⟩
   simp [List.mapIdx_eq_mapIdx_iff]
 
-@[simp] theorem mapIdx_set {xs : Array α} {i : Nat} {h : i < xs.size} {a : α} :
+@[simp] theorem mapIdx_set {f : Nat → α → β} {xs : Array α} {i : Nat} {h : i < xs.size} {a : α} :
     (xs.set i a).mapIdx f = (xs.mapIdx f).set i (f i a) (by simpa) := by
   rcases xs with ⟨xs⟩
   simp [List.mapIdx_set]

src/Init/Data/Array/Range.lean

@@ -29,6 +29,7 @@ open Nat
 
 /-! ### range' -/
 
+@[grind _=_]
 theorem range'_succ {s n step} : range' s (n + 1) step = #[s] ++ range' (s + step) n step := by
   rw [← toList_inj]
   simp [List.range'_succ]
@@ -39,16 +40,17 @@ theorem range'_succ {s n step} : range' s (n + 1) step = #[s] ++ range' (s + ste
 theorem range'_ne_empty_iff : range' s n step ≠ #[] ↔ n ≠ 0 := by
   cases n <;> simp
 
-@[simp] theorem range'_zero : range' s 0 step = #[] := by
+@[simp, grind =] theorem range'_zero : range' s 0 step = #[] := by
   simp
 
-@[simp] theorem range'_one {s step : Nat} : range' s 1 step = #[s] := by
+@[simp, grind =] theorem range'_one {s step : Nat} : range' s 1 step = #[s] := by
   simp [range', ofFn, ofFn.go]
 
 @[simp] theorem range'_inj : range' s n = range' s' n' ↔ n = n' ∧ (n = 0 ∨ s = s') := by
   rw [← toList_inj]
   simp [List.range'_inj]
 
+@[grind =]
 theorem mem_range' {n} : m ∈ range' s n step ↔ ∃ i < n, m = s + step * i := by
   simp [range']
   constructor
@@ -57,6 +59,7 @@ theorem mem_range' {n} : m ∈ range' s n step ↔ ∃ i < n, m = s + step * i :
   · rintro ⟨i, w, h'⟩
     exact ⟨⟨i, w⟩, by simp_all⟩
 
+@[simp, grind =]
 theorem pop_range' : (range' s n step).pop = range' s (n - 1) step := by
   ext <;> simp
 
@@ -66,6 +69,7 @@ theorem map_add_range' {a} (s n step) : map (a + ·) (range' s n step) = range'
 theorem range'_succ_left : range' (s + 1) n step = (range' s n step).map (· + 1) := by
   ext <;> simp <;> omega
 
+@[grind _=_]
 theorem range'_append {s m n step : Nat} :
     range' s m step ++ range' (s + step * m) n step = range' s (m + n) step := by
   ext i h₁ h₂
@@ -77,7 +81,8 @@ theorem range'_append {s m n step : Nat} :
     have : step * m ≤ step * i := by exact mul_le_mul_left step h
     omega
 
-@[simp] theorem range'_append_1 {s m n : Nat} :
+@[simp, grind _=_]
+theorem range'_append_1 {s m n : Nat} :
     range' s m ++ range' (s + m) n = range' s (m + n) := by simpa using range'_append (step := 1)
 
 theorem range'_concat {s n : Nat} : range' s (n + 1) step = range' s n step ++ #[s + step * n] := by
@@ -86,7 +91,7 @@ theorem range'_concat {s n : Nat} : range' s (n + 1) step = range' s n step ++ #
 theorem range'_1_concat {s n : Nat} : range' s (n + 1) = range' s n ++ #[s + n] := by
   simp [range'_concat]
 
-@[simp] theorem mem_range'_1 : m ∈ range' s n ↔ s ≤ m ∧ m < s + n := by
+@[simp, grind =] theorem mem_range'_1 : m ∈ range' s n ↔ s ≤ m ∧ m < s + n := by
   simp [mem_range']; exact ⟨
     fun ⟨i, h, e⟩ => e ▸ ⟨Nat.le_add_right .., Nat.add_lt_add_left h _⟩,
     fun ⟨h₁, h₂⟩ => ⟨m - s, Nat.sub_lt_left_of_lt_add h₁ h₂, (Nat.add_sub_cancel' h₁).symm⟩⟩
@@ -116,6 +121,7 @@ theorem range'_eq_append_iff : range' s n = xs ++ ys ↔ ∃ k, k ≤ n ∧ xs =
   simp only [List.find?_toArray]
   simp
 
+@[grind =]
 theorem erase_range' :
     (range' s n).erase i =
       range' s (min n (i - s)) ++ range' (max s (i + 1)) (min s (i + 1) + n - (i + 1)) := by
@@ -124,6 +130,7 @@ theorem erase_range' :
 
 /-! ### range -/
 
+@[grind _=_]
 theorem range_eq_range' {n : Nat} : range n = range' 0 n := by
   simp [range, range']
 
@@ -145,6 +152,7 @@ theorem range'_eq_map_range {s n : Nat} : range' s n = map (s + ·) (range n) :=
 theorem range_ne_empty_iff {n : Nat} : range n ≠ #[] ↔ n ≠ 0 := by
   cases n <;> simp
 
+@[grind _=_]
 theorem range_succ {n : Nat} : range (succ n) = range n ++ #[n] := by
   ext i h₁ h₂
   · simp
@@ -160,7 +168,7 @@ theorem range_add {n m : Nat} : range (n + m) = range n ++ (range m).map (n + ·
 theorem reverse_range' {s n : Nat} : reverse (range' s n) = map (s + n - 1 - ·) (range n) := by
   simp [← toList_inj, List.reverse_range']
 
-@[simp]
+@[simp, grind =]
 theorem mem_range {m n : Nat} : m ∈ range n ↔ m < n := by
   simp only [range_eq_range', mem_range'_1, Nat.zero_le, true_and, Nat.zero_add]
 
@@ -168,7 +176,7 @@ theorem not_mem_range_self {n : Nat} : n ∉ range n := by simp
 
 theorem self_mem_range_succ {n : Nat} : n ∈ range (n + 1) := by simp
 
-@[simp] theorem take_range {i n : Nat} : take (range n) i = range (min i n) := by
+@[simp, grind =] theorem take_range {i n : Nat} : take (range n) i = range (min i n) := by
   ext <;> simp
 
 @[simp] theorem find?_range_eq_some {n : Nat} {i : Nat} {p : Nat → Bool} :
@@ -179,6 +187,7 @@ theorem self_mem_range_succ {n : Nat} : n ∈ range (n + 1) := by simp
     (range n).find? p = none ↔ ∀ i, i < n → !p i := by
   simp only [← List.toArray_range, List.find?_toArray, List.find?_range_eq_none]
 
+@[grind =]
 theorem erase_range : (range n).erase i = range (min n i) ++ range' (i + 1) (n - (i + 1)) := by
   simp [range_eq_range', erase_range']
 

src/Init/Data/BitVec/Bitblast.lean

@@ -1752,6 +1752,116 @@ theorem toInt_srem (x y : BitVec w) : (x.srem y).toInt = x.toInt.tmod y.toInt :=
         ((not_congr neg_eq_zero_iff).mpr hyz)]
       exact neg_le_intMin_of_msb_eq_true h'
 
+@[simp]
+theorem msb_intMin_umod_neg_of_msb_true {y : BitVec w} (hy : y.msb = true) :
+    (intMin w % -y).msb = false := by
+  by_cases hyintmin : y = intMin w
+  · simp [hyintmin]
+  · rw [msb_umod_of_msb_false_of_ne_zero (by simp [hyintmin, hy])]
+    simp [hy]
+
+@[simp]
+theorem msb_neg_umod_neg_of_msb_true_of_msb_true {x y : BitVec w} (hx : x.msb = true) (hy : y.msb = true) :
+      (-x % -y).msb = false := by
+  by_cases hx' : x = intMin w
+  · simp only [hx', neg_intMin, msb_intMin_umod_neg_of_msb_true hy]
+  · simp [show (-x).msb = false by simp [hx, hx']]
+
+theorem toInt_dvd_toInt_iff {x y : BitVec w} :
+    y.toInt ∣ x.toInt ↔ (if x.msb then -x else x) % (if y.msb then -y else y) = 0#w := by
+  constructor
+  <;> by_cases hxmsb : x.msb <;> by_cases hymsb: y.msb
+  <;> intros h
+  <;> simp only [hxmsb, hymsb, reduceIte, false_eq_true, toNat_eq, toNat_umod, toNat_ofNat,
+        zero_mod, toInt_eq_neg_toNat_neg_of_msb_true, Int.dvd_neg, Int.neg_dvd,
+        toInt_eq_toNat_of_msb] at h
+  <;> simp only [hxmsb, hymsb, toInt_eq_neg_toNat_neg_of_msb_true, toInt_eq_toNat_of_msb,
+        Int.dvd_neg, Int.neg_dvd, toNat_eq, toNat_umod, reduceIte, toNat_ofNat, zero_mod]
+  <;> norm_cast
+  <;> norm_cast at h
+  <;> simp only [dvd_of_mod_eq_zero, h, dvd_iff_mod_eq_zero.mp, reduceIte]
+
+theorem toInt_dvd_toInt_iff_of_msb_true_msb_false {x y : BitVec w} (hx : x.msb = true) (hy : y.msb = false) :
+    y.toInt ∣ x.toInt ↔ (-x) % y = 0#w := by
+  simpa [hx, hy] using toInt_dvd_toInt_iff (x := x) (y := y)
+
+theorem toInt_dvd_toInt_iff_of_msb_false_msb_true {x y : BitVec w} (hx : x.msb = false) (hy : y.msb = true) :
+    y.toInt ∣ x.toInt ↔ x % (-y) = 0#w := by
+  simpa [hx, hy] using toInt_dvd_toInt_iff (x := x) (y := y)
+
+@[simp]
+theorem neg_toInt_neg_umod_eq_of_msb_true_msb_true {x y : BitVec w} (hx : x.msb = true) (hy : y.msb = true) :
+    -(-(-x % -y)).toInt = (-x % -y).toNat := by
+  rw [neg_toInt_neg]
+  by_cases h : -x % -y = 0#w
+  · simp [h]
+  · rw [msb_neg_umod_neg_of_msb_true_of_msb_true hx hy]
+
+@[simp]
+theorem toInt_umod_neg_add {x y : BitVec w} (hymsb : y.msb = true) (hxmsb : x.msb = false) (hdvd : ¬y.toInt ∣ x.toInt) :
+    (x % -y + y).toInt = x.toInt % y.toInt + y.toInt := by
+  rcases w with _|w ; simp [of_length_zero]
+  have hypos : 0 < y.toNat := toNat_pos_of_ne_zero (by simp [hymsb])
+  have hxnonneg := toInt_nonneg_of_msb_false hxmsb
+  have hynonpos := toInt_neg_of_msb_true hymsb
+  have hylt : (-y).toNat ≤ 2 ^ (w) := toNat_neg_lt_of_msb y hymsb
+  have hmodlt := Nat.mod_lt x.toNat (y := (-y).toNat)
+      (by rw [toNat_neg, Nat.mod_eq_of_lt (by omega)]; omega)
+  simp only [hdvd, reduceIte, toInt_add, hxnonneg, show ¬0 ≤ y.toInt by omega]
+  rw [toInt_umod, toInt_eq_neg_toNat_neg_of_msb_true hymsb, Int.bmod_add_bmod,
+    Int.bmod_eq_of_le (by omega) (by omega),
+    toInt_eq_toNat_of_msb hxmsb, Int.emod_neg]
+
+@[simp]
+theorem toInt_sub_neg_umod {x y : BitVec w} (hxmsb : x.msb = true) (hymsb : y.msb = false) (hdvd : ¬y.toInt ∣ x.toInt) :
+    (y - -x % y).toInt = x.toInt % y.toInt := by
+  rcases w with _|w
+  · simp [of_length_zero]
+  · have : y.toNat < 2 ^ w := toNat_lt_of_msb_false hymsb
+    by_cases hyzero : y = 0#(w+1)
+    · subst hyzero; simp
+    · simp only [toNat_eq, toNat_ofNat, zero_mod] at hyzero
+      have hypos : 0 < y.toNat := by omega
+      simp only [reduceIte, toInt_sub, toInt_eq_toNat_of_msb hymsb, toInt_umod,
+        Int.sub_bmod_bmod, toInt_eq_neg_toNat_neg_of_msb_true hxmsb, Int.neg_emod]
+      have hmodlt := Nat.mod_lt (x := (-x).toNat) (y := y.toNat) hypos
+      rw [Int.bmod_eq_of_le (by omega) (by omega)]
+      simp only [toInt_eq_toNat_of_msb hymsb, BitVec.toInt_eq_neg_toNat_neg_of_msb_true hxmsb,
+        Int.dvd_neg] at hdvd
+      simp only [hdvd, ↓reduceIte, Int.natAbs_cast]
+
+theorem toInt_smod {x y : BitVec w} :
+    (x.smod y).toInt = x.toInt.fmod y.toInt := by
+  rcases w with _|w
+  · decide +revert
+  · by_cases hyzero : y = 0#(w + 1)
+    · simp [hyzero]
+    · rw [smod_eq]
+      cases hxmsb : x.msb <;> cases hymsb : y.msb
+      <;> simp only [umod_eq]
+      · have : 0 < y.toNat := by simp [toNat_eq] at hyzero; omega
+        have : y.toNat < 2 ^ w := toNat_lt_of_msb_false hymsb
+        have : x.toNat % y.toNat < y.toNat := Nat.mod_lt x.toNat (by omega)
+        rw [toInt_umod, Int.fmod_eq_emod_of_nonneg x.toInt (toInt_nonneg_of_msb_false hymsb),
+          toInt_eq_toNat_of_msb hxmsb, toInt_eq_toNat_of_msb hymsb,
+          Int.bmod_eq_of_le_mul_two (by omega) (by omega)]
+      · have := toInt_dvd_toInt_iff_of_msb_false_msb_true hxmsb hymsb
+        by_cases hx_dvd_y : y.toInt ∣ x.toInt
+        · simp [show x % -y = 0#(w + 1) by simp_all, hx_dvd_y, Int.fmod_eq_zero_of_dvd]
+        · have hynonpos := toInt_neg_of_msb_true hymsb
+          simp only [show ¬x % -y = 0#(w + 1) by simp_all, ↓reduceIte,
+            toInt_umod_neg_add hymsb hxmsb hx_dvd_y, Int.fmod_eq_emod, show ¬0 ≤ y.toInt by omega,
+            hx_dvd_y, _root_.or_self]
+      · have hynonneg := toInt_nonneg_of_msb_false hymsb
+        rw [Int.fmod_eq_emod_of_nonneg x.toInt (b := y.toInt) (by omega)]
+        have hdvd := toInt_dvd_toInt_iff_of_msb_true_msb_false hxmsb hymsb
+        by_cases hx_dvd_y : y.toInt ∣ x.toInt
+        · simp [show -x % y = 0#(w + 1) by simp_all, hx_dvd_y, Int.emod_eq_zero_of_dvd]
+        · simp [show ¬-x % y = 0#(w + 1) by simp_all, toInt_sub_neg_umod hxmsb hymsb hx_dvd_y]
+      · rw [←Int.neg_inj, neg_toInt_neg_umod_eq_of_msb_true_msb_true hxmsb hymsb]
+        simp [BitVec.toInt_eq_neg_toNat_neg_of_msb_true, hxmsb, hymsb,
+          Int.fmod_eq_emod_of_nonneg _, show 0 ≤ (-y).toNat by omega]
+
 /-! ### Lemmas that use bit blasting circuits -/
 
 theorem add_sub_comm {x y : BitVec w} : x + y - z = x - z + y := by

src/Init/Data/BitVec/Lemmas.lean

@@ -319,6 +319,7 @@ theorem ofFin_ofNat (n : Nat) :
 @[simp] theorem ofFin_neg {x : Fin (2 ^ w)} : ofFin (-x) = -(ofFin x) := by
   rfl
 
+open Fin.NatCast in
 @[simp, norm_cast] theorem ofFin_natCast (n : Nat) : ofFin (n : Fin (2^w)) = (n : BitVec w) := by
   rfl
 
@@ -337,6 +338,7 @@ theorem toFin_zero : toFin (0 : BitVec w) = 0 := rfl
 theorem toFin_one  : toFin (1 : BitVec w) = 1 := by
   rw [toFin_inj]; simp only [ofNat_eq_ofNat, ofFin_ofNat]
 
+open Fin.NatCast in
 @[simp, norm_cast] theorem toFin_natCast (n : Nat) : toFin (n : BitVec w) = (n : Fin (2^w)) := by
   rfl
 
@@ -880,6 +882,19 @@ theorem slt_eq_sle_and_ne {x y : BitVec w} : x.slt y = (x.sle y && x != y) := by
   apply Bool.eq_iff_iff.2
   simp [BitVec.slt, BitVec.sle, Int.lt_iff_le_and_ne, BitVec.toInt_inj]
 
+/-- For all bitvectors `x, y`, either `x` is signed less than `y`,
+or is equal to `y`, or is signed greater than `y`. -/
+theorem slt_trichotomy (x y : BitVec w) : x.slt y ∨ x = y ∨ y.slt x := by
+  simpa [slt_iff_toInt_lt, ← toInt_inj]
+    using Int.lt_trichotomy x.toInt y.toInt
+
+/-- For all bitvectors `x, y`, either `x` is unsigned less than `y`,
+or is equal to `y`, or is unsigned greater than `y`. -/
+theorem lt_trichotomy (x y : BitVec w) :
+    x < y ∨ x = y ∨ y < x := by
+  simpa [← ult_iff_lt, ult_eq_decide, decide_eq_true_eq, ← toNat_inj]
+    using Nat.lt_trichotomy x.toNat y.toNat
+
 /-! ### setWidth, zeroExtend and truncate -/
 
 @[simp]
@@ -2974,7 +2989,7 @@ theorem extractLsb'_append_eq_ite {v w} {xhi : BitVec v} {xlo : BitVec w} {start
     extractLsb' start len (xhi ++ xlo) =
     if hstart : start < w
     then
-      if hlen : start + len < w
+      if hlen : start + len ≤ w
       then extractLsb' start len xlo
       else
         (((extractLsb' (start - w) (len - (w - start)) xhi) ++
@@ -2983,7 +2998,7 @@ theorem extractLsb'_append_eq_ite {v w} {xhi : BitVec v} {xlo : BitVec w} {start
       extractLsb' (start - w) len xhi := by
   by_cases hstart : start < w
   · simp only [hstart, ↓reduceDIte]
-    by_cases hlen : start + len < w
+    by_cases hlen : start + len ≤ w
     · simp only [hlen, ↓reduceDIte]
       ext i hi
       simp only [getElem_extractLsb', getLsbD_append, ite_eq_left_iff, Nat.not_lt]
@@ -3006,11 +3021,14 @@ theorem extractLsb'_append_eq_ite {v w} {xhi : BitVec v} {xlo : BitVec w} {start
 /-- Extracting bits `[start..start+len)` from `(xhi ++ xlo)` equals extracting
 the bits from `xlo` when `start + len` is within `xlo`.
 -/
-theorem extractLsb'_append_eq_of_lt {v w} {xhi : BitVec v} {xlo : BitVec w}
-    {start len : Nat} (h : start + len < w) :
+theorem extractLsb'_append_eq_of_add_le {v w} {xhi : BitVec v} {xlo : BitVec w}
+    {start len : Nat} (h : start + len ≤ w) :
     extractLsb' start len (xhi ++ xlo) = extractLsb' start len xlo := by
-  simp [extractLsb'_append_eq_ite, h]
-  omega
+  simp only [extractLsb'_append_eq_ite, h, ↓reduceDIte, dite_eq_ite, ite_eq_left_iff, Nat.not_lt]
+  intro h'
+  have : len = 0 := by omega
+  subst this
+  simp
 
 /-- Extracting bits `[start..start+len)` from `(xhi ++ xlo)` equals extracting
 the bits from `xhi` when `start` is outside `xlo`.
@@ -3179,7 +3197,7 @@ theorem getElem_concat (x : BitVec w) (b : Bool) (i : Nat) (h : i < w + 1) :
   · simp [Nat.mod_eq_of_lt b.toNat_lt]
   · simp [Nat.div_eq_of_lt b.toNat_lt, Nat.testBit_add_one]
 
-@[simp] theorem getElem_concat_zero : (concat x b)[0] = b := by
+@[simp] theorem getElem_concat_zero {x : BitVec w} : (concat x b)[0] = b := by
   simp [getElem_concat]
 
 theorem getLsbD_concat_zero : (concat x b).getLsbD 0 = b := by
@@ -3995,6 +4013,15 @@ theorem pos_of_msb {x : BitVec w} (hx : x.msb = true) : 0#w < x := by
   rw [BitVec.not_lt, le_zero_iff] at h
   simp [h] at hx
 
+@[simp]
+theorem lt_of_msb_false_of_msb_true {x y : BitVec w} (hx : x.msb = false) (hy : y.msb = true) :
+    x < y := by
+  simp only [LT.lt]
+  have := toNat_ge_of_msb_true hy
+  have := toNat_lt_of_msb_false hx
+  simp
+  omega
+
 /-! ### udiv -/
 
 theorem udiv_def {x y : BitVec n} : x / y = BitVec.ofNat n (x.toNat / y.toNat) := by
@@ -4176,6 +4203,14 @@ theorem toInt_umod_of_msb {x y : BitVec w} (h : x.msb = false) :
     (x % y).toInt = x.toInt % y.toNat := by
   simp [toInt_eq_msb_cond, h]
 
+@[simp]
+theorem msb_umod_of_msb_false_of_ne_zero {x y : BitVec w} (hmsb : y.msb = false) (h_ne_zero : y ≠ 0#w) :
+    (x % y).msb = false := by
+  simp only [msb_umod, Bool.and_eq_false_imp, Bool.or_eq_false_iff, beq_eq_false_iff_ne,
+    ne_eq, h_ne_zero]
+  intro h
+  simp [BitVec.le_of_lt, lt_of_msb_false_of_msb_true hmsb h]
+
 /-! ### smtUDiv -/
 
 theorem smtUDiv_eq (x y : BitVec w) : smtUDiv x y = if y = 0#w then allOnes w else x / y := by
@@ -5410,6 +5445,27 @@ theorem neg_ofNat_eq_ofInt_neg {w : Nat} {x : Nat} :
   apply BitVec.eq_of_toInt_eq
   simp [BitVec.toInt_neg, BitVec.toInt_ofNat]
 
+@[simp]
+theorem neg_toInt_neg {x : BitVec w} (h : x.msb = false) :
+    -(-x).toInt = x.toNat := by
+  simp [toInt_neg_eq_of_msb h, toInt_eq_toNat_of_msb, h]
+
+theorem toNat_pos_of_ne_zero {x : BitVec w} (hx : x ≠ 0#w) :
+    0 < x.toNat := by
+  simp [toNat_eq] at hx; omega
+
+theorem toNat_neg_lt_of_msb (x : BitVec w) (hmsb : x.msb = true) :
+    (-x).toNat ≤ 2^(w-1) := by
+  rcases w with _|w
+  · simp [BitVec.eq_nil x]
+  · by_cases hx : x = 0#(w + 1)
+    · simp [hx]
+    · have := BitVec.le_toNat_of_msb_true hmsb
+      have := toNat_pos_of_ne_zero hx
+      rw [toNat_neg, Nat.mod_eq_of_lt (by omega), ← Nat.two_pow_pred_add_two_pow_pred (by omega),
+        ← Nat.two_mul]
+      omega
+
 /-! ### abs -/
 
 theorem abs_eq (x : BitVec w) : x.abs = if x.msb then -x else x := rfl

src/Init/Data/Fin/Basic.lean

@@ -81,7 +81,7 @@ Examples:
  * `(2 : Fin 3) + (2 : Fin 3) = (1 : Fin 3)`
 -/
 protected def add : Fin n → Fin n → Fin n
-  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(a + b) % n, mlt h⟩
+  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(a + b) % n, by exact mlt h⟩
 
 /--
 Multiplication modulo `n`, usually invoked via the `*` operator.
@@ -92,7 +92,7 @@ Examples:
  * `(3 : Fin 10) * (7 : Fin 10) = (1 : Fin 10)`
 -/
 protected def mul : Fin n → Fin n → Fin n
-  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(a * b) % n, mlt h⟩
+  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(a * b) % n, by exact mlt h⟩
 
 /--
 Subtraction modulo `n`, usually invoked via the `-` operator.
@@ -119,7 +119,7 @@ protected def sub : Fin n → Fin n → Fin n
   using recursion on the second argument.
   See issue #4413.
   -/
-  | ⟨a, h⟩, ⟨b, _⟩ => ⟨((n - b) + a) % n, mlt h⟩
+  | ⟨a, h⟩, ⟨b, _⟩ => ⟨((n - b) + a) % n, by exact mlt h⟩
 
 /-!
 Remark: land/lor can be defined without using (% n), but
@@ -161,19 +161,19 @@ def modn : Fin n → Nat → Fin n
 Bitwise and.
 -/
 def land : Fin n → Fin n → Fin n
-  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(Nat.land a b) % n, mlt h⟩
+  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(Nat.land a b) % n, by exact mlt h⟩
 
 /--
 Bitwise or.
 -/
 def lor : Fin n → Fin n → Fin n
-  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(Nat.lor a b) % n, mlt h⟩
+  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(Nat.lor a b) % n, by exact mlt h⟩
 
 /--
 Bitwise xor (“exclusive or”).
 -/
 def xor : Fin n → Fin n → Fin n
-  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(Nat.xor a b) % n, mlt h⟩
+  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(Nat.xor a b) % n, by exact mlt h⟩
 
 /--
 Bitwise left shift of bounded numbers, with wraparound on overflow.
@@ -184,7 +184,7 @@ Examples:
  * `(1 : Fin 10) <<< (4 : Fin 10) = (6 : Fin 10)`
 -/
 def shiftLeft : Fin n → Fin n → Fin n
-  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(a <<< b) % n, mlt h⟩
+  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(a <<< b) % n, by exact mlt h⟩
 
 /--
 Bitwise right shift of bounded numbers.
@@ -198,7 +198,7 @@ Examples:
  * `(15 : Fin 17) >>> (2 : Fin 17) = (3 : Fin 17)`
 -/
 def shiftRight : Fin n → Fin n → Fin n
-  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(a >>> b) % n, mlt h⟩
+  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(a >>> b) % n, by exact mlt h⟩
 
 instance : Add (Fin n) where
   add := Fin.add

src/Init/Data/Fin/Fold.lean

@@ -184,8 +184,9 @@ theorem foldrM_loop [Monad m] [LawfulMonad m] (f : Fin (n+1) → α → m α) (x
     rw [foldrM_loop_zero, foldrM_loop_succ, pure_bind]
     conv => rhs; rw [←bind_pure (f 0 x)]
     congr
-    funext
-    simp [foldrM_loop_zero]
+    try  -- TODO: block can be deleted after bootstrapping
+      funext
+      simp [foldrM_loop_zero]
   | succ i ih =>
     rw [foldrM_loop_succ, foldrM_loop_succ, bind_assoc]
     congr; funext; exact ih ..

src/Init/Data/Fin/Lemmas.lean

@@ -102,9 +102,30 @@ theorem dite_val {n : Nat} {c : Prop} [Decidable c] {x y : Fin n} :
     (if c then x else y).val = if c then x.val else y.val := by
   by_cases c <;> simp [*]
 
-instance (n : Nat) [NeZero n] : NatCast (Fin n) where
+namespace NatCast
+
+/--
+This is not a global instance, but may be activated locally via `open Fin.NatCast in ...`.
+
+This is not an instance because the `binop%` elaborator assumes that
+there are no non-trivial coercion loops,
+but this introduces a coercion from `Nat` to `Fin n` and back.
+
+Non-trivial loops lead to undesirable and counterintuitive elaboration behavior.
+For example, for `x : Fin k` and `n : Nat`,
+it causes `x < n` to be elaborated as `x < ↑n` rather than `↑x < n`,
+silently introducing wraparound arithmetic.
+
+Note: as of 2025-06-03, Mathlib has such a coercion for `Fin n` anyway!
+-/
+@[expose]
+def instNatCast (n : Nat) [NeZero n] : NatCast (Fin n) where
   natCast a := Fin.ofNat n a
 
+attribute [scoped instance] instNatCast
+
+end NatCast
+
 @[expose]
 def intCast [NeZero n] (a : Int) : Fin n :=
   if 0 ≤ a then
@@ -112,9 +133,22 @@ def intCast [NeZero n] (a : Int) : Fin n :=
   else
     - Fin.ofNat n a.natAbs
 
-instance (n : Nat) [NeZero n] : IntCast (Fin n) where
+namespace IntCast
+
+/--
+This is not a global instance, but may be activated locally via `open Fin.IntCast in ...`.
+
+See the doc-string for `Fin.NatCast.instNatCast` for more details.
+-/
+@[expose]
+def instIntCast (n : Nat) [NeZero n] : IntCast (Fin n) where
   intCast := Fin.intCast
 
+attribute [scoped instance] instIntCast
+
+end IntCast
+
+open IntCast in
 theorem intCast_def {n : Nat} [NeZero n] (x : Int) :
     (x : Fin n) = if 0 ≤ x then Fin.ofNat n x.natAbs else -Fin.ofNat n x.natAbs := rfl
 
@@ -1045,6 +1079,17 @@ theorem val_neg {n : Nat} [NeZero n] (x : Fin n) :
     have := Fin.val_ne_zero_iff.mpr h
     omega
 
+protected theorem sub_eq_add_neg {n : Nat} (x y : Fin n) : x - y = x + -y := by
+  by_cases h : n = 0
+  · subst h
+    apply elim0 x
+  · replace h : NeZero n := ⟨h⟩
+    ext
+    rw [Fin.coe_sub, Fin.val_add, val_neg]
+    split
+    · simp_all
+    · simp [Nat.add_comm]
+
 /-! ### mul -/
 
 theorem ofNat_mul [NeZero n] (x : Nat) (y : Fin n) :

src/Init/Data/Format/Basic.lean

@@ -317,7 +317,7 @@ private structure State where
   out    : String := ""
   column : Nat    := 0
 
-instance : MonadPrettyFormat (StateM State) where
+private instance : MonadPrettyFormat (StateM State) where
   -- We avoid a structure instance update, and write these functions using pattern matching because of issue #316
   pushOutput s       := modify fun ⟨out, col⟩ => ⟨out ++ s, col + s.length⟩
   pushNewline indent := modify fun ⟨out, _⟩ => ⟨out ++ "\n".pushn ' ' indent, indent⟩

src/Init/Data/Int/Basic.lean

@@ -269,7 +269,7 @@ set_option bootstrap.genMatcherCode false in
 
   Implemented by efficient native code. -/
 @[extern "lean_int_dec_nonneg"]
-private def decNonneg (m : @& Int) : Decidable (NonNeg m) :=
+def decNonneg (m : @& Int) : Decidable (NonNeg m) :=
   match m with
   | ofNat m => isTrue <| NonNeg.mk m
   | -[_ +1] => isFalse <| fun h => nomatch h

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

@@ -203,6 +203,9 @@ theorem tdiv_eq_ediv_of_nonneg : ∀ {a b : Int}, 0 ≤ a → a.tdiv b = a / b
   | succ _, succ _, _ => rfl
   | succ _, -[_+1], _ => rfl
 
+@[simp] theorem natCast_tdiv_eq_ediv {a : Nat} {b : Int} : (a : Int).tdiv b = a / b :=
+    tdiv_eq_ediv_of_nonneg (by simp)
+
 theorem tdiv_eq_ediv {a b : Int} :
     a.tdiv b = a / b + if 0 ≤ a ∨ b ∣ a then 0 else sign b := by
   simp only [dvd_iff_emod_eq_zero]

src/Init/Data/List/Erase.lean

@@ -126,9 +126,10 @@ theorem le_length_eraseP {l : List α} : l.length - 1 ≤ (l.eraseP p).length :=
   rw [length_eraseP]
   split <;> simp
 
+@[grind →]
 theorem mem_of_mem_eraseP {l : List α} : a ∈ l.eraseP p → a ∈ l := (eraseP_subset ·)
 
-@[simp] theorem mem_eraseP_of_neg {l : List α} (pa : ¬p a) : a ∈ l.eraseP p ↔ a ∈ l := by
+@[simp, grind] theorem mem_eraseP_of_neg {l : List α} (pa : ¬p a) : a ∈ l.eraseP p ↔ a ∈ l := by
   refine ⟨mem_of_mem_eraseP, fun al => ?_⟩
   match exists_or_eq_self_of_eraseP p l with
   | .inl h => rw [h]; assumption
@@ -260,6 +261,7 @@ theorem eraseP_eq_iff {p} {l : List α} :
 theorem Pairwise.eraseP (q) : Pairwise p l → Pairwise p (l.eraseP q) :=
   Pairwise.sublist <| eraseP_sublist
 
+@[grind]
 theorem Nodup.eraseP (p) : Nodup l → Nodup (l.eraseP p) :=
   Pairwise.eraseP p
 
@@ -378,9 +380,10 @@ theorem le_length_erase [LawfulBEq α] {a : α} {l : List α} : l.length - 1 ≤
   rw [length_erase]
   split <;> simp
 
+@[grind →]
 theorem mem_of_mem_erase {a b : α} {l : List α} (h : a ∈ l.erase b) : a ∈ l := erase_subset h
 
-@[simp] theorem mem_erase_of_ne [LawfulBEq α] {a b : α} {l : List α} (ab : a ≠ b) :
+@[simp, grind] theorem mem_erase_of_ne [LawfulBEq α] {a b : α} {l : List α} (ab : a ≠ b) :
     a ∈ l.erase b ↔ a ∈ l :=
   erase_eq_eraseP b l ▸ mem_eraseP_of_neg (mt eq_of_beq ab.symm)
 
@@ -487,6 +490,10 @@ theorem Nodup.mem_erase_iff [LawfulBEq α] {a : α} (d : Nodup l) : a ∈ l.eras
 theorem Nodup.not_mem_erase [LawfulBEq α] {a : α} (h : Nodup l) : a ∉ l.erase a := fun H => by
   simpa using ((Nodup.mem_erase_iff h).mp H).left
 
+-- Only activate `not_mem_erase` when `l.Nodup` is already available.
+grind_pattern List.Nodup.not_mem_erase => a ∈ l.erase a, l.Nodup
+
+@[grind]
 theorem Nodup.erase [LawfulBEq α] (a : α) : Nodup l → Nodup (l.erase a) :=
   Pairwise.erase a
 

src/Init/Data/List/Lemmas.lean

@@ -575,9 +575,9 @@ theorem isEmpty_iff_length_eq_zero {l : List α} : l.isEmpty ↔ l.length = 0 :=
 
 /-! ### any / all -/
 
-theorem any_eq {l : List α} : l.any p = decide (∃ x, x ∈ l ∧ p x) := by induction l <;> simp [*]
+@[grind =] theorem any_eq {l : List α} : l.any p = decide (∃ x, x ∈ l ∧ p x) := by induction l <;> simp [*]
 
-theorem all_eq {l : List α} : l.all p = decide (∀ x, x ∈ l → p x) := by induction l <;> simp [*]
+@[grind =] theorem all_eq {l : List α} : l.all p = decide (∀ x, x ∈ l → p x) := by induction l <;> simp [*]
 
 theorem decide_exists_mem {l : List α} {p : α → Prop} [DecidablePred p] :
     decide (∃ x, x ∈ l ∧ p x) = l.any p := by
@@ -1128,7 +1128,8 @@ theorem map_singleton {f : α → β} {a : α} : map f [a] = [f a] := rfl
 
 -- We use a lower priority here as there are more specific lemmas in downstream libraries
 -- which should be able to fire first.
-@[simp 500] theorem mem_map {f : α → β} : ∀ {l : List α}, b ∈ l.map f ↔ ∃ a, a ∈ l ∧ f a = b
+@[simp 500, grind =] theorem mem_map {f : α → β} :
+    ∀ {l : List α}, b ∈ l.map f ↔ ∃ a, a ∈ l ∧ f a = b
   | [] => by simp
   | _ :: l => by simp [mem_map (l := l), eq_comm (a := b)]
 

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

@@ -156,7 +156,7 @@ theorem modifyHead_eq_modify_zero (f : α → α) (l : List α) :
 @[simp] theorem modify_eq_nil_iff {f : α → α} {i} {l : List α} :
     l.modify i f = [] ↔ l = [] := by cases l <;> cases i <;> simp
 
-theorem getElem?_modify (f : α → α) :
+@[grind =] theorem getElem?_modify (f : α → α) :
     ∀ i (l : List α) j, (l.modify i f)[j]? = (fun a => if i = j then f a else a) <$> l[j]?
   | n, l, 0 => by cases l <;> cases n <;> simp
   | n, [], _+1 => by cases n <;> rfl
@@ -167,7 +167,7 @@ theorem getElem?_modify (f : α → α) :
     cases h' : l[j]? <;> by_cases h : i = j <;>
       simp [h, if_pos, if_neg, Option.map, mt Nat.succ.inj, not_false_iff, h']
 
-@[simp] theorem length_modify (f : α → α) : ∀ (l : List α) i, (l.modify i f).length = l.length :=
+@[simp, grind =] theorem length_modify (f : α → α) : ∀ (l : List α) i, (l.modify i f).length = l.length :=
   length_modifyTailIdx _ fun l => by cases l <;> rfl
 
 @[simp] theorem getElem?_modify_eq (f : α → α) (i) (l : List α) :
@@ -178,7 +178,7 @@ theorem getElem?_modify (f : α → α) :
     (l.modify i f)[j]? = l[j]? := by
   simp only [getElem?_modify, if_neg h, id_map']
 
-theorem getElem_modify (f : α → α) (i) (l : List α) (j) (h : j < (l.modify i f).length) :
+@[grind =] theorem getElem_modify (f : α → α) (i) (l : List α) (j) (h : j < (l.modify i f).length) :
     (l.modify i f)[j] =
       if i = j then f (l[j]'(by simp at h; omega)) else l[j]'(by simp at h; omega) := by
   rw [getElem_eq_iff, getElem?_modify]
@@ -245,6 +245,7 @@ theorem exists_of_modify (f : α → α) {i} {l : List α} (h : i < l.length) :
 @[simp] theorem modify_id (i) (l : List α) : l.modify i id = l := by
   simp [modify]
 
+@[grind =]
 theorem take_modify (f : α → α) (i j) (l : List α) :
     (l.modify i f).take j = (l.take j).modify i f := by
   induction j generalizing l i with
@@ -257,6 +258,7 @@ theorem take_modify (f : α → α) (i j) (l : List α) :
       | zero => simp
       | succ i => simp [ih]
 
+@[grind =]
 theorem drop_modify_of_lt (f : α → α) (i j) (l : List α) (h : i < j) :
     (l.modify i f).drop j = l.drop j := by
   apply ext_getElem
@@ -266,6 +268,7 @@ theorem drop_modify_of_lt (f : α → α) (i j) (l : List α) (h : i < j) :
     intro h'
     omega
 
+@[grind =]
 theorem drop_modify_of_ge (f : α → α) (i j) (l : List α) (h : i ≥ j) :
     (l.modify i f).drop j = (l.drop j).modify (i - j) f  := by
   apply ext_getElem

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

@@ -55,7 +55,7 @@ theorem sublist_eq_map_getElem {l l' : List α} (h : l' <+ l) : ∃ is : List (F
     simp [Function.comp_def, pairwise_map, IH, ← get_eq_getElem, get_cons_zero, get_cons_succ']
 
 set_option linter.listVariables false in
-theorem pairwise_iff_getElem : Pairwise R l ↔
+theorem pairwise_iff_getElem {l : List α} : Pairwise R l ↔
     ∀ (i j : Nat) (_hi : i < l.length) (_hj : j < l.length) (_hij : i < j), R l[i] l[j] := by
   rw [pairwise_iff_forall_sublist]
   constructor <;> intro h

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

@@ -30,7 +30,7 @@ theorem IsSuffix.getElem {xs ys : List α} (h : xs <:+ ys) {i} (hn : i < xs.leng
   have := h.length_le
   omega
 
-theorem suffix_iff_getElem? : l₁ <:+ l₂ ↔
+theorem suffix_iff_getElem? {l₁ l₂ : List α} : l₁ <:+ l₂ ↔
     l₁.length ≤ l₂.length ∧ ∀ i (h : i < l₁.length), l₂[i + l₂.length - l₁.length]? = some l₁[i] := by
   suffices l₁.length ≤ l₂.length ∧ l₁ <:+ l₂ ↔
       l₁.length ≤ l₂.length ∧ ∀ i (h : i < l₁.length), l₂[i + l₂.length - l₁.length]? = some l₁[i] by
@@ -78,7 +78,7 @@ theorem suffix_iff_getElem {l₁ l₂ : List α} :
     rw [getElem?_eq_getElem]
     simpa using w
 
-theorem infix_iff_getElem? : l₁ <:+: l₂ ↔
+theorem infix_iff_getElem? {l₁ l₂ : List α} : l₁ <:+: l₂ ↔
     ∃ k, l₁.length + k ≤ l₂.length ∧ ∀ i (h : i < l₁.length), l₂[i + k]? = some l₁[i] := by
   constructor
   · intro h

src/Init/Data/List/Pairwise.lean

@@ -211,6 +211,7 @@ theorem pairwise_append_comm {R : α → α → Prop} (s : ∀ {x y}, R x y →
 @[grind] theorem Pairwise.take {l : List α} {i : Nat} (h : List.Pairwise R l) : List.Pairwise R (l.take i) :=
   h.sublist (take_sublist _ _)
 
+@[grind =]
 theorem pairwise_iff_forall_sublist : l.Pairwise R ↔ (∀ {a b}, [a,b] <+ l → R a b) := by
   induction l with
   | nil => simp
@@ -268,6 +269,8 @@ theorem pairwise_of_forall_mem_list {l : List α} {r : α → α → Prop} (h :
 
 /-! ### Nodup -/
 
+@[grind =] theorem nodup_iff_pairwise_ne : List.Nodup l ↔ List.Pairwise (· ≠ ·) l := Iff.rfl
+
 @[simp, grind]
 theorem nodup_nil : @Nodup α [] :=
   Pairwise.nil
@@ -276,7 +279,7 @@ theorem nodup_nil : @Nodup α [] :=
 theorem nodup_cons {a : α} {l : List α} : Nodup (a :: l) ↔ a ∉ l ∧ Nodup l := by
   simp only [Nodup, pairwise_cons, forall_mem_ne]
 
-theorem Nodup.sublist : l₁ <+ l₂ → Nodup l₂ → Nodup l₁ :=
+@[grind →] theorem Nodup.sublist : l₁ <+ l₂ → Nodup l₂ → Nodup l₁ :=
   Pairwise.sublist
 
 grind_pattern Nodup.sublist => l₁ <+ l₂, Nodup l₁

src/Init/Data/List/Sort/Impl.lean

@@ -153,12 +153,12 @@ where
     mergeTR (run' r) (run l) le
 
 theorem splitRevInTwo'_fst (l : { l : List α // l.length = n }) :
-    (splitRevInTwo' l).1 = ⟨(splitInTwo ⟨l.1.reverse, by simpa using l.2⟩).2.1, by simp; omega⟩ := by
+    (splitRevInTwo' l).1 = ⟨(splitInTwo (n := n) ⟨l.1.reverse, by simpa using l.2⟩).2.1, by simp; omega⟩ := by
   simp only [splitRevInTwo', splitRevAt_eq, reverse_take, splitInTwo_snd]
   congr
   omega
 theorem splitRevInTwo'_snd (l : { l : List α // l.length = n }) :
-    (splitRevInTwo' l).2 = ⟨(splitInTwo ⟨l.1.reverse, by simpa using l.2⟩).1.1.reverse, by simp; omega⟩ := by
+    (splitRevInTwo' l).2 = ⟨(splitInTwo (n := n) ⟨l.1.reverse, by simpa using l.2⟩).1.1.reverse, by simp; omega⟩ := by
   simp only [splitRevInTwo', splitRevAt_eq, reverse_take, splitInTwo_fst, reverse_reverse]
   congr 2
   simp

src/Init/Data/List/Sublist.lean

@@ -932,7 +932,8 @@ theorem infix_concat_iff {l₁ l₂ : List α} {a : α} :
   rw [← reverse_infix, reverse_concat, infix_cons_iff, reverse_infix,
     ← reverse_prefix, reverse_concat]
 
-theorem prefix_iff_getElem? : l₁ <+: l₂ ↔ ∀ i (h : i < l₁.length), l₂[i]? = some l₁[i] := by
+theorem prefix_iff_getElem? {l₁ l₂ : List α} :
+    l₁ <+: l₂ ↔ ∀ i (h : i < l₁.length), l₂[i]? = some l₁[i] := by
   induction l₁ generalizing l₂ with
   | nil => simp
   | cons a l₁ ih =>

src/Init/Data/List/TakeDrop.lean

@@ -257,6 +257,17 @@ theorem dropLast_eq_take {l : List α} : l.dropLast = l.take (l.length - 1) := b
     dsimp
     rw [map_drop]
 
+theorem drop_eq_extract {l : List α} {k : Nat} :
+    l.drop k = l.extract k := by
+  induction l generalizing k
+  case nil => simp
+  case cons _ _ ih =>
+    match k with
+    | 0 => simp
+    | _ + 1 =>
+      simp only [List.drop_succ_cons, List.length_cons, ih]
+      simp only [List.extract_eq_drop_take, List.drop_succ_cons, Nat.succ_sub_succ]
+
 /-! ### takeWhile and dropWhile -/
 
 theorem takeWhile_cons {p : α → Bool} {a : α} {l : List α} :

src/Init/Data/Nat/Lemmas.lean

@@ -1767,8 +1767,10 @@ instance decidableExistsLT' {p : (m : Nat) → m < k → Prop} [I : ∀ m h, Dec
 /-- Dependent version of `decidableExistsLE`. -/
 instance decidableExistsLE' {p : (m : Nat) → m ≤ k → Prop} [I : ∀ m h, Decidable (p m h)] :
     Decidable (∃ m : Nat, ∃ h : m ≤ k, p m h) :=
-  decidable_of_iff (∃ m, ∃ h : m < k + 1, p m (by omega)) (exists_congr fun _ =>
-    ⟨fun ⟨h, w⟩ => ⟨le_of_lt_succ h, w⟩, fun ⟨h, w⟩ => ⟨lt_add_one_of_le h, w⟩⟩)
+  decidable_of_iff (∃ m, ∃ h : m < k + 1, p m (by omega)) <| by
+    apply exists_congr
+    intro
+    exact ⟨fun ⟨h, w⟩ => ⟨le_of_lt_succ h, w⟩, fun ⟨h, w⟩ => ⟨lt_add_one_of_le h, w⟩⟩
 
 /-! ### Results about `List.sum` specialized to `Nat` -/
 

src/Init/Data/Option/Basic.lean

@@ -435,7 +435,7 @@ This is the monadic analogue of `Option.getD`.
 @[simp, grind] theorem getDM_some [Pure m] (a : α) (y : m α) : (some a).getDM y = pure a := rfl
 
 instance (α) [BEq α] [ReflBEq α] : ReflBEq (Option α) where
-  rfl {x} :=
+  rfl {x} := private
     match x with
     | some _ => BEq.rfl (α := α)
     | none => rfl

src/Init/Data/Option/Lemmas.lean

@@ -1163,8 +1163,11 @@ end ite
 
 /-! ### pbind -/
 
-@[simp, grind] theorem pbind_none : pbind none f = none := rfl
-@[simp, grind] theorem pbind_some : pbind (some a) f = f a rfl := rfl
+@[simp] theorem pbind_none : pbind none f = none := rfl
+@[simp] theorem pbind_some : pbind (some a) f = f a rfl := rfl
+
+@[grind = gen] theorem pbind_none' (h : x = none) : pbind x f = none := by subst h; rfl
+@[grind = gen] theorem pbind_some' (h : x = some a) : pbind x f = f a h := by subst h; rfl
 
 @[simp, grind] theorem map_pbind {o : Option α} {f : (a : α) → o = some a → Option β}
     {g : β → γ} : (o.pbind f).map g = o.pbind (fun a h => (f a h).map g) := by
@@ -1227,12 +1230,18 @@ theorem get_pbind {o : Option α} {f : (a : α) → o = some a → Option β} {h
 
 /-! ### pmap -/
 
-@[simp, grind] theorem pmap_none {p : α → Prop} {f : ∀ (a : α), p a → β} {h} :
+@[simp] theorem pmap_none {p : α → Prop} {f : ∀ (a : α), p a → β} {h} :
     pmap f none h = none := rfl
 
-@[simp, grind] theorem pmap_some {p : α → Prop} {f : ∀ (a : α), p a → β} {h} :
+@[simp] theorem pmap_some {p : α → Prop} {f : ∀ (a : α), p a → β} {h} :
     pmap f (some a) h = some (f a (h a rfl)) := rfl
 
+@[grind = gen] theorem pmap_none' {p : α → Prop} {f : ∀ (a : α), p a → β} (he : x = none) {h} :
+    pmap f x h = none := by subst he; rfl
+
+@[grind = gen] theorem pmap_some' {p : α → Prop} {f : ∀ (a : α), p a → β} (he : x = some a) {h} :
+    pmap f x h = some (f a (h a he)) := by subst he; rfl
+
 @[simp] theorem pmap_eq_none_iff {p : α → Prop} {f : ∀ (a : α), p a → β} {h} :
     pmap f o h = none ↔ o = none := by
   cases o <;> simp
@@ -1315,8 +1324,11 @@ theorem get_pmap {p : α → Bool} {f : (x : α) → p x → β} {o : Option α}
 
 /-! ### pelim -/
 
-@[simp, grind] theorem pelim_none : pelim none b f = b := rfl
-@[simp, grind] theorem pelim_some : pelim (some a) b f = f a rfl := rfl
+@[simp] theorem pelim_none : pelim none b f = b := rfl
+@[simp] theorem pelim_some : pelim (some a) b f = f a rfl := rfl
+
+@[grind = gen] theorem pelim_none' (h : x = none) : pelim x b f = b := by subst h; rfl
+@[grind = gen] theorem pelim_some' (h : x = some a) : pelim x b f = f a h := by subst h; rfl
 
 @[simp] theorem pelim_eq_elim : pelim o b (fun a _ => f a) = o.elim b f := by
   cases o <;> simp

src/Init/Data/Repr.lean

@@ -210,7 +210,7 @@ protected def _root_.USize.repr (n : @& USize) : String :=
 private def reprArray : Array String := Id.run do
   List.range 128 |>.map (·.toUSize.repr) |> Array.mk
 
-private def reprFast (n : Nat) : String :=
+def reprFast (n : Nat) : String :=
   if h : n < Nat.reprArray.size then Nat.reprArray.getInternal n h else
   if h : n < USize.size then (USize.ofNatLT n h).repr
   else (toDigits 10 n).asString

src/Init/Data/Vector/Lemmas.lean

@@ -1138,6 +1138,7 @@ theorem all_eq_false' {p : α → Bool} {xs : Vector α n} :
   simp only [all_mk, Array.all_eq_false']
   simp
 
+@[grind =]
 theorem any_eq {xs : Vector α n} {p : α → Bool} : xs.any p = decide (∃ i : Nat, ∃ h, p (xs[i]'h)) := by
   by_cases h : xs.any p
   · simp_all [any_eq_true]
@@ -1152,6 +1153,7 @@ theorem any_eq' {xs : Vector α n} {p : α → Bool} : xs.any p = decide (∃ x,
     simp only [any_eq_false'] at h
     simpa using h
 
+@[grind =]
 theorem all_eq {xs : Vector α n} {p : α → Bool} : xs.all p = decide (∀ i, (_ : i < n) → p xs[i]) := by
   by_cases h : xs.all p
   · simp_all [all_eq_true]
@@ -1473,7 +1475,8 @@ theorem map_singleton {f : α → β} {a : α} : map f #v[a] = #v[f a] := by sim
 
 -- We use a lower priority here as there are more specific lemmas in downstream libraries
 -- which should be able to fire first.
-@[simp 500] theorem mem_map {f : α → β} {xs : Vector α n} : b ∈ xs.map f ↔ ∃ a, a ∈ xs ∧ f a = b := by
+@[simp 500, grind =] theorem mem_map {f : α → β} {xs : Vector α n} :
+    b ∈ xs.map f ↔ ∃ a, a ∈ xs ∧ f a = b := by
   cases xs
   simp
 
@@ -2965,7 +2968,7 @@ abbrev all_mkVector := @all_replicate
 section replace
 variable [BEq α]
 
-@[simp] theorem replace_cast {xs : Vector α n} {a b : α} :
+@[simp] theorem replace_cast {h : n = m} {xs : Vector α n} {a b : α} :
     (xs.cast h).replace a b = (xs.replace a b).cast (by simp [h]) := by
   rcases xs with ⟨xs, rfl⟩
   simp

src/Init/Data/Vector/Range.lean

@@ -29,7 +29,7 @@ open Nat
 
 /-! ### range' -/
 
-@[simp] theorem toArray_range' {start size step} :
+@[simp, grind =] theorem toArray_range' {start size step} :
     (range' start size step).toArray = Array.range' start size step := by
   rfl
 
@@ -37,11 +37,11 @@ theorem range'_eq_mk_range' {start size step} :
     range' start size step = Vector.mk (Array.range' start size step) (by simp) := by
   rfl
 
-@[simp] theorem getElem_range' {start size step i} (h : i < size) :
+@[simp, grind =] theorem getElem_range' {start size step i} (h : i < size) :
    (range' start size step)[i] = start + step * i := by
   simp [range', h]
 
-@[simp] theorem getElem?_range' {start size step i} :
+@[simp, grind =] theorem getElem?_range' {start size step i} :
    (range' start size step)[i]? = if i < size then some (start + step * i) else none := by
   simp [getElem?_def, range']
 
@@ -50,18 +50,21 @@ theorem range'_succ {s n step} :
   rw [← toArray_inj]
   simp [Array.range'_succ]
 
+@[grind =]
 theorem range'_zero : range' s 0 step = #v[] := by
   simp
 
-@[simp] theorem range'_one {s step : Nat} : range' s 1 step = #v[s] := by simp
+@[simp, grind =] theorem range'_one {s step : Nat} : range' s 1 step = #v[s] := by simp
 
 @[simp] theorem range'_inj : range' s n = range' s' n ↔ (n = 0 ∨ s = s') := by
   rw [← toArray_inj]
   simp [List.range'_inj]
 
+@[grind =]
 theorem mem_range' {n} : m ∈ range' s n step ↔ ∃ i < n, m = s + step * i := by
   simp [range', Array.mem_range']
 
+@[simp, grind =]
 theorem pop_range' : (range' s n step).pop = range' s (n - 1) step := by
   ext <;> simp
 
@@ -71,6 +74,7 @@ theorem map_add_range' {a} (s n step) : map (a + ·) (range' s n step) = range'
 theorem range'_succ_left : range' (s + 1) n step = (range' s n step).map (· + 1) := by
   ext <;> simp <;> omega
 
+@[grind _=_]
 theorem range'_append {s m n step : Nat} :
     range' s m step ++ range' (s + step * m) n step = range' s (m + n) step := by
   rw [← toArray_inj]
@@ -85,7 +89,7 @@ theorem range'_concat {s n : Nat} : range' s (n + 1) step = range' s n step ++ #
 theorem range'_1_concat {s n : Nat} : range' s (n + 1) = range' s n ++ #v[s + n] := by
   simp [range'_concat]
 
-@[simp] theorem mem_range'_1 : m ∈ range' s n ↔ s ≤ m ∧ m < s + n := by
+@[simp, grind =] theorem mem_range'_1 : m ∈ range' s n ↔ s ≤ m ∧ m < s + n := by
   simp [mem_range']; exact ⟨
     fun ⟨i, h, e⟩ => e ▸ ⟨Nat.le_add_right .., Nat.add_lt_add_left h _⟩,
     fun ⟨h₁, h₂⟩ => ⟨m - s, Nat.sub_lt_left_of_lt_add h₁ h₂, (Nat.add_sub_cancel' h₁).symm⟩⟩
@@ -118,9 +122,10 @@ theorem range'_eq_append_iff : range' s (n + m) = xs ++ ys ↔ xs = range' s n
 
 /-! ### range -/
 
-@[simp] theorem getElem_range {i : Nat} (hi : i < n) : (Vector.range n)[i] = i := by
+@[simp, grind =] theorem getElem_range {i : Nat} (hi : i < n) : (Vector.range n)[i] = i := by
   simp [Vector.range]
 
+@[grind _=_]
 theorem range_eq_range' {n : Nat} : range n = range' 0 n := by
   simp [range, range', Array.range_eq_range']
 
@@ -133,6 +138,7 @@ theorem range_succ_eq_map {n : Nat} :
 theorem range'_eq_map_range {s n : Nat} : range' s n = map (s + ·) (range n) := by
   rw [range_eq_range', map_add_range']; rfl
 
+@[grind _=_]
 theorem range_succ {n : Nat} : range (succ n) = range n ++ #v[n] := by
   rw [← toArray_inj]
   simp [Array.range_succ]
@@ -144,7 +150,7 @@ theorem range_add {n m : Nat} : range (n + m) = range n ++ (range m).map (n + ·
 theorem reverse_range' {s n : Nat} : reverse (range' s n) = map (s + n - 1 - ·) (range n) := by
   simp [← toArray_inj, Array.reverse_range']
 
-@[simp]
+@[simp, grind =]
 theorem mem_range {m n : Nat} : m ∈ range n ↔ m < n := by
   simp only [range_eq_range', mem_range'_1, Nat.zero_le, true_and, Nat.zero_add]
 

src/Init/GetElem.lean

@@ -164,25 +164,25 @@ export LawfulGetElem (getElem?_def getElem!_def)
 instance (priority := low) [GetElem coll idx elem valid] [∀ xs i, Decidable (valid xs i)] :
     LawfulGetElem coll idx elem valid where
 
-@[simp] theorem getElem?_pos [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
+@[simp, grind] theorem getElem?_pos [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
     (c : cont) (i : idx) (h : dom c i) : c[i]? = some (c[i]'h) := by
   have : Decidable (dom c i) := .isTrue h
   rw [getElem?_def]
   exact dif_pos h
 
-@[simp] theorem getElem?_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
+@[simp, grind] theorem getElem?_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
     (c : cont) (i : idx) (h : ¬dom c i) : c[i]? = none := by
   have : Decidable (dom c i) := .isFalse h
   rw [getElem?_def]
   exact dif_neg h
 
-@[simp] theorem getElem!_pos [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
+@[simp, grind] theorem getElem!_pos [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
     [Inhabited elem] (c : cont) (i : idx) (h : dom c i) :
     c[i]! = c[i]'h := by
   have : Decidable (dom c i) := .isTrue h
   simp [getElem!_def, getElem?_def, h]
 
-@[simp] theorem getElem!_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
+@[simp, grind] theorem getElem!_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
     [Inhabited elem] (c : cont) (i : idx) (h : ¬dom c i) : c[i]! = default := by
   have : Decidable (dom c i) := .isFalse h
   simp [getElem!_def, getElem?_def, h]
@@ -193,7 +193,7 @@ instance (priority := low) [GetElem coll idx elem valid] [∀ xs i, Decidable (v
   simp only [getElem?_def] at h ⊢
   split <;> simp_all
 
-@[simp, grind =] theorem getElem?_eq_none_iff [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
+@[simp] theorem getElem?_eq_none_iff [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
     (c : cont) (i : idx) [Decidable (dom c i)] : c[i]? = none ↔ ¬dom c i := by
   simp only [getElem?_def]
   split <;> simp_all
@@ -238,8 +238,6 @@ theorem getElem_of_getElem? [GetElem? cont idx elem dom] [LawfulGetElem cont idx
     {c : cont} {i : idx} [Decidable (dom c i)] (h : c[i]? = some e) : Exists fun h : dom c i => c[i] = e :=
   getElem?_eq_some_iff.mp h
 
-grind_pattern getElem_of_getElem? => c[i]?, some e
-
 @[simp] theorem some_getElem_eq_getElem?_iff [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
     {c : cont} {i : idx} [Decidable (dom c i)] (h : dom c i):
     (some c[i] = c[i]?) ↔ True := by
@@ -275,12 +273,12 @@ instance [GetElem? cont Nat elem dom] [h : LawfulGetElem cont Nat elem dom] :
   getElem?_def _c _i _d := h.getElem?_def ..
   getElem!_def _c _i := h.getElem!_def ..
 
-@[simp] theorem getElem_fin [GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n) (h : Dom a i) :
+@[simp, grind =] theorem getElem_fin [GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n) (h : Dom a i) :
     a[i] = a[i.1] := rfl
 
-@[simp] theorem getElem?_fin [h : GetElem? Cont Nat Elem Dom] (a : Cont) (i : Fin n) : a[i]? = a[i.1]? := rfl
+@[simp, grind =] theorem getElem?_fin [h : GetElem? Cont Nat Elem Dom] (a : Cont) (i : Fin n) : a[i]? = a[i.1]? := rfl
 
-@[simp] theorem getElem!_fin [GetElem? Cont Nat Elem Dom] (a : Cont) (i : Fin n) [Inhabited Elem] : a[i]! = a[i.1]! := rfl
+@[simp, grind =] theorem getElem!_fin [GetElem? Cont Nat Elem Dom] (a : Cont) (i : Fin n) [Inhabited Elem] : a[i]! = a[i.1]! := rfl
 
 macro_rules
   | `(tactic| get_elem_tactic_trivial) => `(tactic| (with_reducible apply Fin.val_lt_of_le); get_elem_tactic_trivial; done)
@@ -313,13 +311,15 @@ theorem getElem_cons_drop_succ_eq_drop {as : List α} {i : Nat} (h : i < as.leng
 /-! ### getElem? -/
 
 /-- Internal implementation of `as[i]?`. Do not use directly. -/
-private def get?Internal : (as : List α) → (i : Nat) → Option α
+-- We still keep it public for reduction purposes
+def get?Internal : (as : List α) → (i : Nat) → Option α
   | a::_,  0   => some a
   | _::as, n+1 => get?Internal as n
   | _,     _   => none
 
 /-- Internal implementation of `as[i]!`. Do not use directly. -/
-private def get!Internal [Inhabited α] : (as : List α) → (i : Nat) → α
+-- We still keep it public for reduction purposes
+def get!Internal [Inhabited α] : (as : List α) → (i : Nat) → α
   | a::_,  0   => a
   | _::as, n+1 => get!Internal as n
   | _,     _   => panic! "invalid index"

src/Init/Grind.lean

@@ -18,3 +18,5 @@ import Init.Grind.CommRing
 import Init.Grind.Module
 import Init.Grind.Ordered
 import Init.Grind.Ext
+import Init.Grind.ToInt
+import Init.Data.Int.OfNat -- This may not have otherwise been imported, breaking `grind` proofs.

src/Init/Grind/CommRing/Basic.lean

@@ -71,7 +71,9 @@ class CommRing (α : Type u) extends Ring α, CommSemiring α
 attribute [instance 100] Semiring.toAdd Semiring.toMul Semiring.toHPow Ring.toNeg Ring.toSub
 
 -- This is a low-priority instance, to avoid conflicts with existing `OfNat`, `NatCast`, and `IntCast` instances.
-attribute [instance 100] Semiring.ofNat Semiring.natCast Ring.intCast
+attribute [instance 100] Semiring.ofNat
+
+attribute [local instance] Semiring.natCast Ring.intCast
 
 namespace Semiring
 
@@ -118,7 +120,6 @@ theorem pow_add (a : α) (k₁ k₂ : Nat) : a ^ (k₁ + k₂) = a^k₁ * a^k₂
 instance : NatModule α where
   hMul a x := a * x
   add_zero := by simp [add_zero]
-  zero_add := by simp [zero_add]
   add_assoc := by simp [add_assoc]
   add_comm := by simp [add_comm]
   zero_hmul := by simp [natCast_zero, zero_mul]
@@ -271,7 +272,6 @@ theorem intCast_pow (x : Int) (k : Nat) : ((x ^ k : Int) : α) = (x : α) ^ k :=
 instance : IntModule α where
   hMul a x := a * x
   add_zero := by simp [add_zero]
-  zero_add := by simp [zero_add]
   add_assoc := by simp [add_assoc]
   add_comm := by simp [add_comm]
   zero_hmul := by simp [intCast_zero, zero_mul]

src/Init/Grind/CommRing/BitVec.lean

@@ -34,4 +34,9 @@ instance : CommRing (BitVec w) where
 instance : IsCharP (BitVec w) (2 ^ w) where
   ofNat_eq_zero_iff {x} := by simp [BitVec.ofInt, BitVec.toNat_eq]
 
+-- Verify we can derive the instances showing how `toInt` interacts with operations:
+example : ToInt.Add (BitVec w) (some 0) (some (2^w)) := inferInstance
+example : ToInt.Neg (BitVec w) (some 0) (some (2^w)) := inferInstance
+example : ToInt.Sub (BitVec w) (some 0) (some (2^w)) := inferInstance
+
 end Lean.Grind

src/Init/Grind/CommRing/Fin.lean

@@ -14,22 +14,6 @@ namespace Lean.Grind
 
 namespace Fin
 
-instance (n : Nat) [NeZero n] : NatCast (Fin n) where
-  natCast a := Fin.ofNat n a
-
-@[expose]
-def intCast [NeZero n] (a : Int) : Fin n :=
-  if 0 ≤ a then
-    Fin.ofNat n a.natAbs
-  else
-    - Fin.ofNat n a.natAbs
-
-instance (n : Nat) [NeZero n] : IntCast (Fin n) where
-  intCast := Fin.intCast
-
-theorem intCast_def {n : Nat} [NeZero n] (x : Int) :
-    (x : Fin n) = if 0 ≤ x then Fin.ofNat n x.natAbs else -Fin.ofNat n x.natAbs := rfl
-
 -- TODO: we should replace this at runtime with either repeated squaring,
 -- or a GMP accelerated function.
 @[expose]
@@ -78,18 +62,22 @@ theorem sub_eq_add_neg [NeZero n] (a b : Fin n) : a - b = a + -b := by
   cases a; cases b; simp [Fin.neg_def, Fin.sub_def, Fin.add_def, Nat.add_comm]
 
 private theorem neg_neg [NeZero n] (a : Fin n) : - - a = a := by
-  cases a; simp [Fin.neg_def, Fin.sub_def];
+  cases a; simp [Fin.neg_def, Fin.sub_def]
   next a h => cases a; simp; next a =>
    rw [Nat.self_sub_mod n (a+1)]
    have : NeZero (n - (a + 1)) := ⟨by omega⟩
    rw [Nat.self_sub_mod, Nat.sub_sub_eq_min, Nat.min_eq_right (Nat.le_of_lt h)]
 
+open Fin.NatCast Fin.IntCast in
 theorem intCast_neg [NeZero n] (i : Int) : Int.cast (R := Fin n) (-i) = - Int.cast (R := Fin n) i := by
-  simp [Int.cast, IntCast.intCast, Fin.intCast]; split <;> split <;> try omega
+  simp [Int.cast, IntCast.intCast, Fin.intCast]
+  split <;> split <;> try omega
   next h₁ h₂ => simp [Int.le_antisymm h₁ h₂, Fin.neg_def]
   next => simp [Fin.neg_neg]
 
 instance (n : Nat) [NeZero n] : CommRing (Fin n) where
+  natCast := Fin.NatCast.instNatCast n
+  intCast := Fin.IntCast.instIntCast n
   add_assoc := Fin.add_assoc
   add_comm := Fin.add_comm
   add_zero := Fin.add_zero
@@ -112,6 +100,9 @@ instance (n : Nat) [NeZero n] : IsCharP (Fin n) n where
     simp only [Nat.zero_mod]
     simp only [Fin.mk.injEq]
 
+example [NeZero n] : ToInt.Neg (Fin n) (some 0) (some n) := inferInstance
+example [NeZero n] : ToInt.Sub (Fin n) (some 0) (some n) := inferInstance
+
 end Fin
 
 end Lean.Grind

src/Init/Grind/CommRing/Poly.lean

@@ -15,6 +15,9 @@ import Init.Grind.CommRing.Basic
 namespace Lean.Grind
 namespace CommRing
 
+-- These are no longer global instances, so we need to turn them on here.
+attribute [local instance] Semiring.natCast Ring.intCast
+
 abbrev Var := Nat
 
 inductive Expr where

src/Init/Grind/CommRing/SInt.lean

@@ -45,6 +45,11 @@ instance : IsCharP Int8 (2 ^ 8) where
     simp [Int8.ofInt_eq_iff_bmod_eq_toInt,
       ← Int.dvd_iff_bmod_eq_zero, ← Nat.dvd_iff_mod_eq_zero, Int.ofNat_dvd_right]
 
+-- Verify we can derive the instances showing how `toInt` interacts with operations:
+example : ToInt.Add Int8 (some (-(2^7))) (some (2^7)) := inferInstance
+example : ToInt.Neg Int8 (some (-(2^7))) (some (2^7)) := inferInstance
+example : ToInt.Sub Int8 (some (-(2^7))) (some (2^7)) := inferInstance
+
 instance : NatCast Int16 where
   natCast x := Int16.ofNat x
 
@@ -76,6 +81,11 @@ instance : IsCharP Int16 (2 ^ 16) where
     simp [Int16.ofInt_eq_iff_bmod_eq_toInt,
       ← Int.dvd_iff_bmod_eq_zero, ← Nat.dvd_iff_mod_eq_zero, Int.ofNat_dvd_right]
 
+-- Verify we can derive the instances showing how `toInt` interacts with operations:
+example : ToInt.Add Int16 (some (-(2^15))) (some (2^15)) := inferInstance
+example : ToInt.Neg Int16 (some (-(2^15))) (some (2^15)) := inferInstance
+example : ToInt.Sub Int16 (some (-(2^15))) (some (2^15)) := inferInstance
+
 instance : NatCast Int32 where
   natCast x := Int32.ofNat x
 
@@ -107,6 +117,11 @@ instance : IsCharP Int32 (2 ^ 32) where
     simp [Int32.ofInt_eq_iff_bmod_eq_toInt,
       ← Int.dvd_iff_bmod_eq_zero, ← Nat.dvd_iff_mod_eq_zero, Int.ofNat_dvd_right]
 
+-- Verify we can derive the instances showing how `toInt` interacts with operations:
+example : ToInt.Add Int32 (some (-(2^31))) (some (2^31)) := inferInstance
+example : ToInt.Neg Int32 (some (-(2^31))) (some (2^31)) := inferInstance
+example : ToInt.Sub Int32 (some (-(2^31))) (some (2^31)) := inferInstance
+
 instance : NatCast Int64 where
   natCast x := Int64.ofNat x
 
@@ -138,6 +153,11 @@ instance : IsCharP Int64 (2 ^ 64) where
     simp [Int64.ofInt_eq_iff_bmod_eq_toInt,
       ← Int.dvd_iff_bmod_eq_zero, ← Nat.dvd_iff_mod_eq_zero, Int.ofNat_dvd_right]
 
+-- Verify we can derive the instances showing how `toInt` interacts with operations:
+example : ToInt.Add Int64 (some (-(2^63))) (some (2^63)) := inferInstance
+example : ToInt.Neg Int64 (some (-(2^63))) (some (2^63)) := inferInstance
+example : ToInt.Sub Int64 (some (-(2^63))) (some (2^63)) := inferInstance
+
 instance : NatCast ISize where
   natCast x := ISize.ofNat x
 
@@ -171,4 +191,9 @@ instance : IsCharP ISize (2 ^ numBits) where
     simp [ISize.ofInt_eq_iff_bmod_eq_toInt,
       ← Int.dvd_iff_bmod_eq_zero, ← Nat.dvd_iff_mod_eq_zero, Int.ofNat_dvd_right]
 
+-- Verify we can derive the instances showing how `toInt` interacts with operations:
+example : ToInt.Add ISize (some (-(2^(numBits-1)))) (some (2^(numBits-1))) := inferInstance
+example : ToInt.Neg ISize (some (-(2^(numBits-1)))) (some (2^(numBits-1))) := inferInstance
+example : ToInt.Sub ISize (some (-(2^(numBits-1)))) (some (2^(numBits-1))) := inferInstance
+
 end Lean.Grind

src/Init/Grind/CommRing/UInt.lean

@@ -149,6 +149,11 @@ instance : IsCharP UInt8 256 where
     have : OfNat.ofNat x = UInt8.ofNat x := rfl
     simp [this, UInt8.ofNat_eq_iff_mod_eq_toNat]
 
+-- Verify we can derive the instances showing how `toInt` interacts with operations:
+example : ToInt.Add UInt8 (some 0) (some (2^8)) := inferInstance
+example : ToInt.Neg UInt8 (some 0) (some (2^8)) := inferInstance
+example : ToInt.Sub UInt8 (some 0) (some (2^8)) := inferInstance
+
 instance : CommRing UInt16 where
   add_assoc := UInt16.add_assoc
   add_comm := UInt16.add_comm
@@ -174,6 +179,11 @@ instance : IsCharP UInt16 65536 where
     have : OfNat.ofNat x = UInt16.ofNat x := rfl
     simp [this, UInt16.ofNat_eq_iff_mod_eq_toNat]
 
+-- Verify we can derive the instances showing how `toInt` interacts with operations:
+example : ToInt.Add UInt16 (some 0) (some (2^16)) := inferInstance
+example : ToInt.Neg UInt16 (some 0) (some (2^16)) := inferInstance
+example : ToInt.Sub UInt16 (some 0) (some (2^16)) := inferInstance
+
 instance : CommRing UInt32 where
   add_assoc := UInt32.add_assoc
   add_comm := UInt32.add_comm
@@ -199,6 +209,11 @@ instance : IsCharP UInt32 4294967296 where
     have : OfNat.ofNat x = UInt32.ofNat x := rfl
     simp [this, UInt32.ofNat_eq_iff_mod_eq_toNat]
 
+-- Verify we can derive the instances showing how `toInt` interacts with operations:
+example : ToInt.Add UInt32 (some 0) (some (2^32)) := inferInstance
+example : ToInt.Neg UInt32 (some 0) (some (2^32)) := inferInstance
+example : ToInt.Sub UInt32 (some 0) (some (2^32)) := inferInstance
+
 instance : CommRing UInt64 where
   add_assoc := UInt64.add_assoc
   add_comm := UInt64.add_comm
@@ -224,6 +239,11 @@ instance : IsCharP UInt64 18446744073709551616 where
     have : OfNat.ofNat x = UInt64.ofNat x := rfl
     simp [this, UInt64.ofNat_eq_iff_mod_eq_toNat]
 
+-- Verify we can derive the instances showing how `toInt` interacts with operations:
+example : ToInt.Add UInt64 (some 0) (some (2^64)) := inferInstance
+example : ToInt.Neg UInt64 (some 0) (some (2^64)) := inferInstance
+example : ToInt.Sub UInt64 (some 0) (some (2^64)) := inferInstance
+
 instance : CommRing USize where
   add_assoc := USize.add_assoc
   add_comm := USize.add_comm
@@ -251,4 +271,9 @@ instance : IsCharP USize (2 ^ numBits) where
     have : OfNat.ofNat x = USize.ofNat x := rfl
     simp [this, USize.ofNat_eq_iff_mod_eq_toNat]
 
+-- Verify we can derive the instances showing how `toInt` interacts with operations:
+example : ToInt.Add USize (some 0) (some (2^numBits)) := inferInstance
+example : ToInt.Neg USize (some 0) (some (2^numBits)) := inferInstance
+example : ToInt.Sub USize (some 0) (some (2^numBits)) := inferInstance
+
 end Lean.Grind

src/Init/Grind/Module/Basic.lean

@@ -7,12 +7,12 @@ module
 
 prelude
 import Init.Data.Int.Order
+import Init.Grind.ToInt
 
 namespace Lean.Grind
 
 class NatModule (M : Type u) extends Zero M, Add M, HMul Nat M M where
   add_zero : ∀ a : M, a + 0 = a
-  zero_add : ∀ a : M, 0 + a = a
   add_comm : ∀ a b : M, a + b = b + a
   add_assoc : ∀ a b c : M, a + b + c = a + (b + c)
   zero_hmul : ∀ a : M, 0 * a = 0
@@ -26,7 +26,6 @@ attribute [instance 100] NatModule.toZero NatModule.toAdd NatModule.toHMul
 
 class IntModule (M : Type u) extends Zero M, Add M, Neg M, Sub M, HMul Int M M where
   add_zero : ∀ a : M, a + 0 = a
-  zero_add : ∀ a : M, 0 + a = a
   add_comm : ∀ a b : M, a + b = b + a
   add_assoc : ∀ a b c : M, a + b + c = a + (b + c)
   zero_hmul : ∀ a : M, (0 : Int) * a = 0
@@ -52,9 +51,15 @@ instance toNatModule (M : Type u) [i : IntModule M] : NatModule M :=
 
 variable {M : Type u} [IntModule M]
 
+theorem zero_add (a : M) : 0 + a = a := by
+  rw [add_comm, add_zero]
+
 theorem add_neg_cancel (a : M) : a + -a = 0 := by
   rw [add_comm, neg_add_cancel]
 
+theorem add_left_comm (a b c : M) : a + (b + c) = b + (a + c) := by
+  rw [← add_assoc, ← add_assoc, add_comm a]
+
 theorem add_left_inj {a b : M} (c : M) : a + c = b + c ↔ a = b :=
   ⟨fun h => by simpa [add_assoc, add_neg_cancel, add_zero] using (congrArg (· + -c) h),
    fun g => congrArg (· + c) g⟩
@@ -111,4 +116,17 @@ class NoNatZeroDivisors (α : Type u) [Zero α] [HMul Nat α α] where
 
 export NoNatZeroDivisors (no_nat_zero_divisors)
 
+instance [ToInt α (some lo) (some hi)] [IntModule α] [ToInt.Zero α (some lo) (some hi)] [ToInt.Add α (some lo) (some hi)] : ToInt.Neg α (some lo) (some hi) where
+  toInt_neg x := by
+    have := (ToInt.Add.toInt_add (-x) x).symm
+    rw [IntModule.neg_add_cancel, ToInt.Zero.toInt_zero] at this
+    rw [ToInt.wrap_eq_wrap_iff] at this
+    simp at this
+    rw [← ToInt.wrap_toInt]
+    rw [ToInt.wrap_eq_wrap_iff]
+    simpa
+
+instance [ToInt α (some lo) (some hi)] [IntModule α] [ToInt.Add α (some lo) (some hi)] [ToInt.Neg α (some lo) (some hi)] : ToInt.Sub α (some lo) (some hi) :=
+  ToInt.Sub.of_sub_eq_add_neg IntModule.sub_eq_add_neg
+
 end Lean.Grind

src/Init/Grind/Ordered.lean

@@ -11,3 +11,4 @@ import Init.Grind.Ordered.Module
 import Init.Grind.Ordered.Ring
 import Init.Grind.Ordered.Field
 import Init.Grind.Ordered.Int
+import Init.Grind.Ordered.Linarith

src/Init/Grind/Ordered/Linarith.lean

@@ -0,0 +1,432 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+import Init.Grind.Ordered.Module
+import all Init.Data.Ord
+import all Init.Data.AC
+import Init.Data.RArray
+
+/-!
+Support for the linear arithmetic module for `IntModule` in `grind`
+-/
+
+namespace Lean.Grind.Linarith
+abbrev Var := Nat
+open IntModule
+
+attribute [local simp] add_zero zero_add zero_hmul hmul_zero one_hmul
+
+inductive Expr where
+  | zero
+  | var  (i : Var)
+  | add  (a b : Expr)
+  | sub  (a b : Expr)
+  | neg  (a : Expr)
+  | mul  (k : Int) (a : Expr)
+  deriving Inhabited, BEq
+
+abbrev Context (α : Type u) := RArray α
+
+def Var.denote {α} (ctx : Context α) (v : Var) : α :=
+  ctx.get v
+
+def Expr.denote {α} [IntModule α] (ctx : Context α) : Expr → α
+  | zero      => 0
+  | .var v    => v.denote ctx
+  | .add a b  => denote ctx a + denote ctx b
+  | .sub a b  => denote ctx a - denote ctx b
+  | .mul k a  => k * denote ctx a
+  | .neg a    => -denote ctx a
+
+inductive Poly where
+  | nil
+  | add (k : Int) (v : Var) (p : Poly)
+  deriving BEq
+
+def Poly.denote {α} [IntModule α] (ctx : Context α) (p : Poly) : α :=
+  match p with
+  | .nil => 0
+  | .add k v p => k * v.denote ctx + denote ctx p
+
+/--
+Similar to `Poly.denote`, but produces a denotation better for normalization.
+-/
+def Poly.denote' {α} [IntModule α] (ctx : Context α) (p : Poly) : α :=
+  match p with
+  | .nil => 0
+  | .add 1 v p => go (v.denote ctx) p
+  | .add k v p => go (k * v.denote ctx) p
+where
+  go (r : α)  (p : Poly) : α :=
+    match p with
+    | .nil => r
+    | .add 1 v p => go (r + v.denote ctx) p
+    | .add k v p => go (r + k * v.denote ctx) p
+
+-- Helper instance for `ac_rfl`
+local instance {α} [IntModule α] : Std.Associative (· + · : α → α → α) where
+  assoc := IntModule.add_assoc
+-- Helper instance for `ac_rfl`
+local instance {α} [IntModule α] : Std.Commutative (· + · : α → α → α) where
+  comm := IntModule.add_comm
+
+theorem Poly.denote'_go_eq_denote {α} [IntModule α] (ctx : Context α) (p : Poly) (r : α) : denote'.go ctx r p = p.denote ctx + r := by
+  induction r, p using denote'.go.induct ctx <;> simp [denote'.go, denote]
+  next ih => rw [ih]; ac_rfl
+  next ih => rw [ih]; ac_rfl
+
+theorem Poly.denote'_eq_denote {α} [IntModule α] (ctx : Context α) (p : Poly) : p.denote' ctx = p.denote ctx := by
+  unfold denote' <;> split <;> simp [denote, denote'_go_eq_denote] <;> ac_rfl
+
+def Poly.insert (k : Int) (v : Var) (p : Poly) : Poly :=
+  match p with
+  | .nil => .add k v .nil
+  | .add k' v' p =>
+    bif Nat.blt v' v then
+      .add k v <| .add k' v' p
+    else bif Nat.beq v v' then
+      if Int.add k k' == 0 then
+        p
+      else
+        .add (Int.add k k') v' p
+    else
+      .add k' v' (insert k v p)
+
+/-- Normalizes the given polynomial by fusing monomial and constants. -/
+def Poly.norm (p : Poly) : Poly :=
+  match p with
+  | .nil => .nil
+  | .add k v p => (norm p).insert k v
+
+def Poly.append (p₁ p₂ : Poly) : Poly :=
+  match p₁ with
+  | .nil => p₂
+  | .add k x p₁ => .add k x (append p₁ p₂)
+
+def Poly.combine' (fuel : Nat) (p₁ p₂ : Poly) : Poly :=
+  match fuel with
+  | 0 => p₁.append p₂
+  | fuel + 1 => match p₁, p₂ with
+    | .nil, p₂ => p₂
+    | p₁, .nil => p₁
+    | .add a₁ x₁ p₁, .add a₂ x₂ p₂ =>
+      bif Nat.beq x₁ x₂ then
+        let a := a₁ + a₂
+        bif a == 0 then
+          combine' fuel p₁ p₂
+        else
+          .add a x₁ (combine' fuel p₁ p₂)
+      else bif Nat.blt x₂ x₁ then
+        .add a₁ x₁ (combine' fuel p₁ (.add a₂ x₂ p₂))
+      else
+        .add a₂ x₂ (combine' fuel (.add a₁ x₁ p₁) p₂)
+
+def Poly.combine (p₁ p₂ : Poly) : Poly :=
+  combine' 100000000 p₁ p₂
+
+/-- Converts the given expression into a polynomial. -/
+def Expr.toPoly' (e : Expr) : Poly :=
+  go 1 e .nil
+where
+  go (coeff : Int) : Expr → (Poly → Poly)
+    | .zero     => id
+    | .var v    => (.add coeff v ·)
+    | .add a b  => go coeff a ∘ go coeff b
+    | .sub a b  => go coeff a ∘ go (-coeff) b
+    | .mul k a  => bif k == 0 then id else go (Int.mul coeff k) a
+    | .neg a    => go (-coeff) a
+
+/-- Converts the given expression into a polynomial, and then normalizes it. -/
+def Expr.norm (e : Expr) : Poly :=
+  e.toPoly'.norm
+
+/--
+`p.mul k` multiplies all coefficients and constant of the polynomial `p` by `k`.
+-/
+def Poly.mul' (p : Poly) (k : Int) : Poly :=
+  match p with
+  | .nil => .nil
+  | .add k' v p => .add (k*k') v (mul' p k)
+
+def Poly.mul (p : Poly) (k : Int) : Poly :=
+  if k == 0 then
+    .nil
+  else
+    p.mul' k
+
+@[simp] theorem Poly.denote_mul {α} [IntModule α] (ctx : Context α) (p : Poly) (k : Int) : (p.mul k).denote ctx = k * p.denote ctx := by
+  simp [mul]
+  split
+  next => simp [*, denote]
+  next =>
+    induction p <;> simp [mul', denote, *]
+    rw [mul_hmul, hmul_add]
+
+theorem Poly.denote_insert {α} [IntModule α] (ctx : Context α) (k : Int) (v : Var) (p : Poly) :
+    (p.insert k v).denote ctx = p.denote ctx + k * v.denote ctx := by
+  fun_induction p.insert k v <;> simp [denote]
+  next => ac_rfl
+  next h₁ h₂ h₃ =>
+    simp at h₃; simp at h₂; subst h₂
+    rw [add_comm, ← add_assoc, ← add_hmul, h₃, zero_hmul, zero_add]
+  next h _ => simp at h; subst h; rw [add_hmul]; ac_rfl
+  next ih => rw [ih]; ac_rfl
+
+attribute [local simp] Poly.denote_insert
+
+theorem Poly.denote_norm {α} [IntModule α] (ctx : Context α) (p : Poly) : p.norm.denote ctx = p.denote ctx := by
+  induction p <;> simp [denote, norm, add_comm, *]
+
+attribute [local simp] Poly.denote_norm
+
+theorem Poly.denote_append {α} [IntModule α] (ctx : Context α) (p₁ p₂ : Poly) : (p₁.append p₂).denote ctx = p₁.denote ctx + p₂.denote ctx := by
+  induction p₁ <;> simp [append, denote, *]; ac_rfl
+
+attribute [local simp] Poly.denote_append
+
+theorem Poly.denote_combine' {α} [IntModule α] (ctx : Context α) (fuel : Nat) (p₁ p₂ : Poly) : (p₁.combine' fuel p₂).denote ctx = p₁.denote ctx + p₂.denote ctx := by
+  fun_induction p₁.combine' fuel p₂ <;>
+    simp_all +zetaDelta [denote, ← Int.add_mul]
+  next h _ =>
+    rw [Int.add_comm] at h
+    rw [add_left_comm, add_assoc, ← add_assoc, ← add_hmul, h, zero_hmul, zero_add]
+  next => rw [add_hmul]; ac_rfl
+  all_goals ac_rfl
+
+theorem Poly.denote_combine {α} [IntModule α] (ctx : Context α) (p₁ p₂ : Poly) : (p₁.combine p₂).denote ctx = p₁.denote ctx + p₂.denote ctx := by
+  simp [combine, denote_combine']
+
+attribute [local simp] Poly.denote_combine
+
+theorem Expr.denote_toPoly'_go {α} [IntModule α] {k p} (ctx : Context α) (e : Expr)
+    : (toPoly'.go k e p).denote ctx = k * e.denote ctx + p.denote ctx := by
+  induction k, e using Expr.toPoly'.go.induct generalizing p <;> simp [toPoly'.go, denote, Poly.denote, *, hmul_add]
+  next => ac_rfl
+  next => rw [sub_eq_add_neg, neg_hmul, hmul_add, hmul_neg]; ac_rfl
+  next h => simp at h; subst h; simp
+  next ih => simp at ih; rw [ih, mul_hmul]
+  next => rw [hmul_neg, neg_hmul]
+
+theorem Expr.denote_norm {α} [IntModule α] (ctx : Context α) (e : Expr) : e.norm.denote ctx = e.denote ctx := by
+  simp [norm, toPoly', Expr.denote_toPoly'_go, Poly.denote]
+
+attribute [local simp] Expr.denote_norm
+
+instance : LawfulBEq Poly where
+  eq_of_beq {a} := by
+    induction a <;> intro b <;> cases b <;> simp_all! [BEq.beq]
+    next ih =>
+      intro _ _ h
+      exact ih h
+  rfl := by
+    intro a
+    induction a <;> simp! [BEq.beq]
+    assumption
+
+attribute [local simp] Poly.denote'_eq_denote
+
+def Poly.leadCoeff (p : Poly) : Int :=
+  match p with
+  | .add a _ _ => a
+  | _ => 1
+
+open IntModule.IsOrdered
+
+/-!
+Helper theorems for conflict resolution during model construction.
+-/
+
+private theorem le_add_le {α} [IntModule α] [Preorder α] [IntModule.IsOrdered α] {a b : α}
+    (h₁ : a ≤ 0) (h₂ : b ≤ 0) : a + b ≤ 0 := by
+  replace h₁ := add_le_left h₁ b; simp at h₁
+  exact Preorder.le_trans h₁ h₂
+
+private theorem le_add_lt {α} [IntModule α] [Preorder α] [IntModule.IsOrdered α] {a b : α}
+    (h₁ : a ≤ 0) (h₂ : b < 0) : a + b < 0 := by
+  replace h₁ := add_le_left h₁ b; simp at h₁
+  exact Preorder.lt_of_le_of_lt h₁ h₂
+
+private theorem lt_add_lt {α} [IntModule α] [Preorder α] [IntModule.IsOrdered α] {a b : α}
+    (h₁ : a < 0) (h₂ : b < 0) : a + b < 0 := by
+  replace h₁ := add_lt_left h₁ b; simp at h₁
+  exact Preorder.lt_trans h₁ h₂
+
+private theorem coe_natAbs_nonneg (a : Int) : (a.natAbs : Int) ≥ 0 := by
+  exact Int.natCast_nonneg a.natAbs
+
+def le_le_combine_cert (p₁ p₂ p₃ : Poly) : Bool :=
+  let a₁ := p₁.leadCoeff.natAbs
+  let a₂ := p₂.leadCoeff.natAbs
+  p₃ == (p₁.mul a₂ |>.combine (p₂.mul a₁))
+
+theorem le_le_combine {α} [IntModule α] [Preorder α] [IntModule.IsOrdered α] (ctx : Context α) (p₁ p₂ p₃ : Poly)
+    : le_le_combine_cert p₁ p₂ p₃ → p₁.denote' ctx ≤ 0 → p₂.denote' ctx ≤ 0 → p₃.denote' ctx ≤ 0 := by
+  simp [le_le_combine_cert]; intro _ h₁ h₂; subst p₃; simp
+  replace h₁ := hmul_nonpos (coe_natAbs_nonneg p₂.leadCoeff) h₁
+  replace h₂ := hmul_nonpos (coe_natAbs_nonneg p₁.leadCoeff) h₂
+  exact le_add_le h₁ h₂
+
+def le_lt_combine_cert (p₁ p₂ p₃ : Poly) : Bool :=
+  let a₁ := p₁.leadCoeff.natAbs
+  let a₂ := p₂.leadCoeff.natAbs
+  a₁ > (0 : Int) && p₃ == (p₁.mul a₂ |>.combine (p₂.mul a₁))
+
+theorem le_lt_combine {α} [IntModule α] [Preorder α] [IntModule.IsOrdered α] (ctx : Context α) (p₁ p₂ p₃ : Poly)
+    : le_lt_combine_cert p₁ p₂ p₃ → p₁.denote' ctx ≤ 0 → p₂.denote' ctx < 0 → p₃.denote' ctx < 0 := by
+  simp [-Int.natAbs_pos, -Int.ofNat_pos, le_lt_combine_cert]; intro hp _ h₁ h₂; subst p₃; simp
+  replace h₁ := hmul_nonpos (coe_natAbs_nonneg p₂.leadCoeff) h₁
+  replace h₂ := hmul_neg (↑p₁.leadCoeff.natAbs) h₂ |>.mp hp
+  exact le_add_lt h₁ h₂
+
+theorem le_eq_combine {α} [IntModule α] [Preorder α] [IntModule.IsOrdered α] (ctx : Context α) (p₁ p₂ p₃ : Poly)
+    : le_le_combine_cert p₁ p₂ p₃ → p₁.denote' ctx ≤ 0 → p₂.denote' ctx = 0 → p₃.denote' ctx ≤ 0 := by
+  simp [le_le_combine_cert]; intro _ h₁ h₂; subst p₃; simp [h₂]
+  replace h₁ := hmul_nonpos (coe_natAbs_nonneg p₂.leadCoeff) h₁
+  assumption
+
+def lt_lt_combine_cert (p₁ p₂ p₃ : Poly) : Bool :=
+  let a₁ := p₁.leadCoeff.natAbs
+  let a₂ := p₂.leadCoeff.natAbs
+  a₂ > (0 : Int) && a₁ > (0 : Int) && p₃ == (p₁.mul a₂ |>.combine (p₂.mul a₁))
+
+theorem lt_lt_combine {α} [IntModule α] [Preorder α] [IntModule.IsOrdered α] (ctx : Context α) (p₁ p₂ p₃ : Poly)
+    : lt_lt_combine_cert p₁ p₂ p₃ → p₁.denote' ctx < 0 → p₂.denote' ctx < 0 → p₃.denote' ctx < 0 := by
+  simp [-Int.natAbs_pos, -Int.ofNat_pos, lt_lt_combine_cert]; intro hp₁ hp₂ _ h₁ h₂; subst p₃; simp
+  replace h₁ := hmul_neg (↑p₂.leadCoeff.natAbs) h₁ |>.mp hp₁
+  replace h₂ := hmul_neg (↑p₁.leadCoeff.natAbs) h₂ |>.mp hp₂
+  exact lt_add_lt h₁ h₂
+
+def lt_eq_combine_cert (p₁ p₂ p₃ : Poly) : Bool :=
+  let a₁ := p₁.leadCoeff.natAbs
+  let a₂ := p₂.leadCoeff.natAbs
+  a₂ > (0 : Int) && p₃ == (p₁.mul a₂ |>.combine (p₂.mul a₁))
+
+theorem lt_eq_combine {α} [IntModule α] [Preorder α] [IntModule.IsOrdered α] (ctx : Context α) (p₁ p₂ p₃ : Poly)
+    : lt_eq_combine_cert p₁ p₂ p₃ → p₁.denote' ctx < 0 → p₂.denote' ctx = 0 → p₃.denote' ctx < 0 := by
+  simp [-Int.natAbs_pos, -Int.ofNat_pos, lt_eq_combine_cert]; intro hp₁ _ h₁ h₂; subst p₃; simp [h₂]
+  replace h₁ := hmul_neg (↑p₂.leadCoeff.natAbs) h₁ |>.mp hp₁
+  assumption
+
+theorem eq_eq_combine {α} [IntModule α] [Preorder α] [IntModule.IsOrdered α] (ctx : Context α) (p₁ p₂ p₃ : Poly)
+    : le_le_combine_cert p₁ p₂ p₃ → p₁.denote' ctx = 0 → p₂.denote' ctx = 0 → p₃.denote' ctx = 0 := by
+  simp [le_le_combine_cert]; intro _ h₁ h₂; subst p₃; simp [h₁, h₂]
+
+def diseq_split_cert (p₁ p₂ : Poly) : Bool :=
+  p₂ == p₁.mul (-1)
+
+-- We need `LinearOrder` to use `trichotomy`
+theorem diseq_split {α} [IntModule α] [LinearOrder α] [IntModule.IsOrdered α] (ctx : Context α) (p₁ p₂ : Poly)
+    : diseq_split_cert p₁ p₂ → p₁.denote' ctx ≠ 0 → p₁.denote' ctx < 0 ∨ p₂.denote' ctx < 0 := by
+  simp [diseq_split_cert]; intro _ h₁; subst p₂; simp
+  cases LinearOrder.trichotomy (p₁.denote ctx) 0
+  next h => exact Or.inl h
+  next h =>
+    apply Or.inr
+    simp [h₁] at h
+    rw [← neg_pos_iff, neg_hmul, neg_neg, one_hmul]; assumption
+
+def eq_diseq_combine_cert (p₁ p₂ p₃ : Poly) : Bool :=
+  let a₁ := p₁.leadCoeff.natAbs
+  let a₂ := p₂.leadCoeff.natAbs
+  a₁ ≠ 0 && p₃ == (p₁.mul a₂ |>.combine (p₂.mul a₁))
+
+theorem eq_diseq_combine {α} [IntModule α] [NoNatZeroDivisors α] (ctx : Context α) (p₁ p₂ p₃ : Poly)
+    : eq_diseq_combine_cert p₁ p₂ p₃ → p₁.denote' ctx = 0 → p₂.denote' ctx ≠ 0 → p₃.denote' ctx ≠ 0 := by
+  simp [- Int.natAbs_eq_zero, -Int.natCast_eq_zero, eq_diseq_combine_cert]; intro hne _ h₁ h₂; subst p₃
+  simp [h₁, h₂]; intro h
+  have := no_nat_zero_divisors (p₁.leadCoeff.natAbs) (p₂.denote ctx) hne h
+  contradiction
+
+def eq_diseq_combine_cert' (p₁ p₂ p₃ : Poly) (k : Int) : Bool :=
+  p₃ == (p₁.mul k |>.combine p₂)
+
+/-
+Special case of `eq_diseq_combine` where leading coefficient `c₁` of `p₁` is `-k*c₂`, where
+`c₂` is the leading coefficient of `p₂`.
+-/
+theorem eq_diseq_combine' {α} [IntModule α] (ctx : Context α) (p₁ p₂ p₃ : Poly) (k : Int)
+    : eq_diseq_combine_cert' p₁ p₂ p₃ k → p₁.denote' ctx = 0 → p₂.denote' ctx ≠ 0 → p₃.denote' ctx ≠ 0 := by
+  simp [eq_diseq_combine_cert']; intro _ h₁ h₂; subst p₃
+  simp [h₁, h₂]
+
+/-!
+Helper theorems for internalizing facts into the linear arithmetic procedure
+-/
+
+def norm_cert (lhs rhs : Expr) (p : Poly) :=
+  p == (lhs.sub rhs).norm
+
+theorem eq_norm {α} [IntModule α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
+    : norm_cert lhs rhs p → lhs.denote ctx = rhs.denote ctx → p.denote ctx = 0 := by
+  simp [norm_cert]; intro _ h₁; subst p; simp [Expr.denote, h₁, sub_self]
+
+theorem diseq_norm {α} [IntModule α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
+    : norm_cert lhs rhs p → lhs.denote ctx ≠ rhs.denote ctx → p.denote ctx ≠ 0 := by
+  simp [norm_cert]; intro _ h₁; subst p; simp [Expr.denote, h₁, sub_self]
+  intro h
+  replace h := congrArg (rhs.denote ctx + ·) h; simp [sub_eq_add_neg] at h
+  rw [add_left_comm, ← sub_eq_add_neg, sub_self, add_zero] at h
+  contradiction
+
+theorem le_norm {α} [IntModule α] [Preorder α] [IntModule.IsOrdered α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
+    : norm_cert lhs rhs p → lhs.denote ctx ≤ rhs.denote ctx → p.denote ctx ≤ 0 := by
+  simp [norm_cert]; intro _ h₁; subst p; simp [Expr.denote, h₁, sub_self]
+  replace h₁ := add_le_left h₁ (-rhs.denote ctx)
+  simp [← sub_eq_add_neg, sub_self] at h₁
+  assumption
+
+theorem lt_norm {α} [IntModule α] [Preorder α] [IntModule.IsOrdered α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
+    : norm_cert lhs rhs p → lhs.denote ctx < rhs.denote ctx → p.denote ctx < 0 := by
+  simp [norm_cert]; intro _ h₁; subst p; simp [Expr.denote, h₁, sub_self]
+  replace h₁ := add_lt_left h₁ (-rhs.denote ctx)
+  simp [← sub_eq_add_neg, sub_self] at h₁
+  assumption
+
+private theorem le_of_not_lt {α} [LinearOrder α] {a b : α} (h : ¬ a < b) : b ≤ a := by
+  cases LinearOrder.trichotomy a b
+  next => contradiction
+  next h => apply PartialOrder.le_iff_lt_or_eq.mpr; cases h <;> simp [*]
+
+private theorem lt_of_not_le {α} [LinearOrder α] {a b : α} (h : ¬ a ≤ b) : b < a := by
+  cases LinearOrder.trichotomy a b
+  next h₁ h₂ => have := Preorder.lt_iff_le_not_le.mp h₂; simp [h] at this
+  next h =>
+    cases h
+    next h => subst a; exact False.elim <| h (Preorder.le_refl b)
+    next => assumption
+
+theorem not_le_norm {α} [IntModule α] [LinearOrder α] [IntModule.IsOrdered α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
+    : norm_cert rhs lhs p → ¬ lhs.denote ctx ≤ rhs.denote ctx → p.denote ctx < 0 := by
+  simp [norm_cert]; intro _ h₁; subst p; simp [Expr.denote, h₁, sub_self]
+  replace h₁ := lt_of_not_le h₁
+  replace h₁ := add_lt_left h₁ (-lhs.denote ctx)
+  simp [← sub_eq_add_neg, sub_self] at h₁
+  assumption
+
+theorem not_lt_norm {α} [IntModule α] [LinearOrder α] [IntModule.IsOrdered α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
+    : norm_cert rhs lhs p → ¬ lhs.denote ctx < rhs.denote ctx → p.denote ctx ≤ 0 := by
+  simp [norm_cert]; intro _ h₁; subst p; simp [Expr.denote, h₁, sub_self]
+  replace h₁ := le_of_not_lt h₁
+  replace h₁ := add_le_left h₁ (-lhs.denote ctx)
+  simp [← sub_eq_add_neg, sub_self] at h₁
+  assumption
+
+/-!
+Helper theorems for closing the goal
+-/
+
+theorem diseq_unsat {α} [IntModule α] (ctx : Context α) : (Poly.nil).denote ctx ≠ 0 → False := by
+  simp [Poly.denote]
+
+theorem lt_unsat {α} [IntModule α] [Preorder α] (ctx : Context α) : (Poly.nil).denote ctx < 0 → False := by
+  simp [Poly.denote]; intro h
+  have := Preorder.lt_iff_le_not_le.mp h
+  simp at this
+
+-- TODO: support for the special variable representing (1 : α). Example: `3 * (1 : α) ≤ 0`
+
+end Lean.Grind.Linarith

src/Init/Grind/Tactics.lean

@@ -8,6 +8,57 @@ module
 prelude
 import Init.Tactics
 
+namespace Lean.Grind
+/--
+Gadget for representing generalization steps `h : x = val` in patterns
+This gadget is used to represent patterns in theorems that have been generalized to reduce the
+number of casts introduced during E-matching based instantiation.
+
+For example, consider the theorem
+```
+Option.pbind_some {α1 : Type u_1} {a : α1} {α2 : Type u_2}
+    {f : (a_1 : α1) → some a = some a_1 → Option α2}
+    : (some a).pbind f = f a rfl
+```
+Now, suppose we have a goal containing the term `c.pbind g` and the equivalence class
+`{c, some b}`. The E-matching module generates the instance
+```
+(some b).pbind (cast ⋯ g)
+```
+The `cast` is necessary because `g`'s type contains `c` instead of `some b.
+This `cast` problematic because we don't have a systematic way of pushing casts over functions
+to its arguments. Moreover, heterogeneous equality is not effective because the following theorem
+is not provable in DTT:
+```
+theorem hcongr (h₁ : f ≍ g) (h₂ : a ≍ b)  : f a ≍ g b := ...
+```
+The standard solution is to generalize the theorem above and write it as
+```
+theorem Option.pbind_some'
+        {α1 : Type u_1} {a : α1} {α2 : Type u_2}
+        {x : Option α1}
+        {f : (a_1 : α1) → x = some a_1 → Option α2}
+        (h : x = some a)
+        : x.pbind f = f a h := by
+  subst h
+  apply Option.pbind_some
+```
+Internally, we use this gadget to mark the E-matching pattern as
+```
+(genPattern h x (some a)).pbind f
+```
+This pattern is matched in the same way we match `(some a).pbind f`, but it saves the proof
+for the actual term to the `some`-application in `f`, and the actual term in `x`.
+
+In the example above, `c.pbind g` also matches the pattern `(genPattern h x (some a)).pbind f`,
+and stores `c` in `x`, `b` in `a`, and the proof that `c = some b` in `h`.
+-/
+def genPattern {α : Sort u} (_h : Prop) (x : α) (_val : α) : α := x
+
+/-- Similar to `genPattern` but for the heterogenous case -/
+def genHEqPattern {α β : Sort u} (_h : Prop) (x : α) (_val : β) : α := x
+end Lean.Grind
+
 namespace Lean.Parser
 /--
 Reset all `grind` attributes. This command is intended for testing purposes only and should not be used in applications.
@@ -15,12 +66,13 @@ Reset all `grind` attributes. This command is intended for testing purposes only
 syntax (name := resetGrindAttrs) "reset_grind_attrs%" : command
 
 namespace Attr
-syntax grindEq     := "= "
-syntax grindEqBoth := atomic("_" "=" "_ ")
-syntax grindEqRhs  := atomic("=" "_ ")
+syntax grindGen    := &"gen "
+syntax grindEq     := "= " (grindGen)?
+syntax grindEqBoth := atomic("_" "=" "_ ") (grindGen)?
+syntax grindEqRhs  := atomic("=" "_ ") (grindGen)?
 syntax grindEqBwd  := atomic("←" "= ") <|> atomic("<-" "= ")
-syntax grindBwd    := "← " <|> "-> "
-syntax grindFwd    := "→ " <|> "<- "
+syntax grindBwd    := ("← " <|> "<- ") (grindGen)?
+syntax grindFwd    := "→ " <|> "-> "
 syntax grindRL     := "⇐ " <|> "<= "
 syntax grindLR     := "⇒ " <|> "=> "
 syntax grindUsr    := &"usr "
@@ -28,7 +80,10 @@ syntax grindCases  := &"cases "
 syntax grindCasesEager := atomic(&"cases" &"eager ")
 syntax grindIntro  := &"intro "
 syntax grindExt    := &"ext "
-syntax grindMod := grindEqBoth <|> grindEqRhs <|> grindEq <|> grindEqBwd <|> grindBwd <|> grindFwd <|> grindRL <|> grindLR <|> grindUsr <|> grindCasesEager <|> grindCases <|> grindIntro <|> grindExt
+syntax grindMod :=
+    grindEqBoth <|> grindEqRhs <|> grindEq <|> grindEqBwd <|> grindBwd
+    <|> grindFwd <|> grindRL <|> grindLR <|> grindUsr <|> grindCasesEager
+    <|> grindCases <|> grindIntro <|> grindExt <|> grindGen
 syntax (name := grind) "grind" (grindMod)? : attr
 syntax (name := grind?) "grind?" (grindMod)? : attr
 end Attr
@@ -122,7 +177,7 @@ structure Config where
   /--
   When `true` (default: `false`), uses procedure for handling equalities over commutative rings.
   -/
-  ring := false
+  ring := true
   ringSteps := 10000
   /--
   When `true` (default: `false`), the commutative ring procedure in `grind` constructs stepwise

src/Init/Grind/ToInt.lean

@@ -0,0 +1,513 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+module
+
+prelude
+
+import Init.Data.Int.DivMod.Basic
+import Init.Data.Int.Lemmas
+import Init.Data.Int.Order
+import Init.Data.Fin.Lemmas
+import Init.Data.UInt.Lemmas
+import Init.Data.SInt.Lemmas
+
+/-!
+# Typeclasses for types that can be embedded into an interval of `Int`.
+
+The typeclass `ToInt α lo? hi?` carries the data of a function `ToInt.toInt : α → Int`
+which is injective, lands between the (optional) lower and upper bounds `lo?` and `hi?`.
+
+The function `ToInt.wrap` is the identity if either bound is `none`,
+and otherwise wraps the integers into the interval `[lo, hi)`.
+
+The typeclass `ToInt.Add α lo? hi?` then asserts that `toInt (x + y) = wrap lo? hi? (toInt x + toInt y)`.
+There are many variants for other operations.
+
+These typeclasses are used solely in the `grind` tactic to lift linear inequalities into `Int`.
+-/
+
+namespace Lean.Grind
+
+class ToInt (α : Type u) (lo? hi? : outParam (Option Int)) where
+  toInt : α → Int
+  toInt_inj : ∀ x y, toInt x = toInt y → x = y
+  le_toInt : lo? = some lo → lo ≤ toInt x
+  toInt_lt : hi? = some hi → toInt x < hi
+
+@[simp]
+def ToInt.wrap (lo? hi? : Option Int) (x : Int) : Int :=
+  match lo?, hi? with
+  | some lo, some hi => (x - lo) % (hi - lo) + lo
+  | _, _ => x
+
+class ToInt.Zero (α : Type u) [Zero α] (lo? hi? : outParam (Option Int)) [ToInt α lo? hi?] where
+  toInt_zero : toInt (0 : α) = wrap lo? hi? 0
+
+class ToInt.Add (α : Type u) [Add α] (lo? hi? : outParam (Option Int)) [ToInt α lo? hi?] where
+  toInt_add : ∀ x y : α, toInt (x + y) = wrap lo? hi? (toInt x + toInt y)
+
+class ToInt.Neg (α : Type u) [Neg α] (lo? hi? : outParam (Option Int)) [ToInt α lo? hi?] where
+  toInt_neg : ∀ x : α, toInt (-x) = wrap lo? hi? (-toInt x)
+
+class ToInt.Sub (α : Type u) [Sub α] (lo? hi? : outParam (Option Int)) [ToInt α lo? hi?] where
+  toInt_sub : ∀ x y : α, toInt (x - y) = wrap lo? hi? (toInt x - toInt y)
+
+class ToInt.Mod (α : Type u) [Mod α] (lo? hi? : outParam (Option Int)) [ToInt α lo? hi?] where
+  /-- One might expect a `wrap` on the right hand side,
+  but in practice this stronger statement is usually true. -/
+  toInt_mod : ∀ x y : α, toInt (x % y) = toInt x % toInt y
+
+class ToInt.LE (α : Type u) [LE α] (lo? hi? : outParam (Option Int)) [ToInt α lo? hi?] where
+  le_iff : ∀ x y : α, x ≤ y ↔ toInt x ≤ toInt y
+
+class ToInt.LT (α : Type u) [LT α] (lo? hi? : outParam (Option Int)) [ToInt α lo? hi?] where
+  lt_iff : ∀ x y : α, x < y ↔ toInt x < toInt y
+
+/-! ## Helper theorems -/
+
+theorem ToInt.wrap_add (lo? hi? : Option Int) (x y : Int) :
+    ToInt.wrap lo? hi? (x + y) = ToInt.wrap lo? hi? (ToInt.wrap lo? hi? x + ToInt.wrap lo? hi? y) := by
+  simp only [wrap]
+  split <;> rename_i lo hi
+  · dsimp
+    rw [Int.add_left_inj, Int.emod_eq_emod_iff_emod_sub_eq_zero, Int.emod_def (x - lo), Int.emod_def (y - lo)]
+    have : (x + y - lo -
+        (x - lo - (hi - lo) * ((x - lo) / (hi - lo)) + lo +
+          (y - lo - (hi - lo) * ((y - lo) / (hi - lo)) + lo) - lo)) =
+        (hi - lo) * ((x - lo) / (hi - lo) + (y - lo) / (hi - lo)) := by
+      simp only [Int.mul_add]
+      omega
+    rw [this]
+    exact Int.mul_emod_right ..
+  · simp
+
+@[simp]
+theorem ToInt.wrap_toInt (lo? hi? : Option Int) [ToInt α lo? hi?] (x : α) :
+    ToInt.wrap lo? hi? (ToInt.toInt x) = ToInt.toInt x := by
+  simp only [wrap]
+  split
+  · have := ToInt.le_toInt (x := x) rfl
+    have := ToInt.toInt_lt (x := x) rfl
+    rw [Int.emod_eq_of_lt (by omega) (by omega)]
+    omega
+  · rfl
+
+theorem ToInt.wrap_eq_bmod {i : Int} (h : 0 ≤ i) :
+    ToInt.wrap (some (-i)) (some i) x = x.bmod ((2 * i).toNat) := by
+  match i, h with
+  | (i : Nat), _ =>
+    have : (2 * (i : Int)).toNat = 2 * i := by omega
+    rw [this]
+    simp [Int.bmod_eq_emod, ← Int.two_mul]
+    have : (2 * (i : Int) + 1) / 2 = i := by omega
+    rw [this]
+    by_cases h : i = 0
+    · simp [h]
+    split
+    · rw [← Int.sub_eq_add_neg, Int.sub_eq_iff_eq_add, Nat.two_mul, Int.natCast_add,
+        ← Int.sub_sub, Int.sub_add_cancel]
+      rw [Int.emod_eq_iff (by omega)]
+      refine ⟨?_, ?_, ?_⟩
+      · omega
+      · have := Int.emod_lt x (b := 2 * (i : Int)) (by omega)
+        omega
+      · rw [Int.emod_def]
+        have : x - 2 * ↑i * (x / (2 * ↑i)) - ↑i - (x + ↑i) = (2 * (i : Int)) * (- (x / (2 * i)) - 1) := by
+          simp only [Int.mul_sub, Int.mul_neg]
+          omega
+        rw [this]
+        exact Int.dvd_mul_right ..
+    · rw [← Int.sub_eq_add_neg, Int.sub_eq_iff_eq_add, Int.natCast_zero, Int.sub_zero]
+      rw [Int.emod_eq_iff (by omega)]
+      refine ⟨?_, ?_, ?_⟩
+      · have := Int.emod_nonneg x (b := 2 * (i : Int)) (by omega)
+        omega
+      · omega
+      · rw [Int.emod_def]
+        have : x - 2 * ↑i * (x / (2 * ↑i)) + ↑i - (x + ↑i) = (2 * (i : Int)) * (- (x / (2 * i))) := by
+          simp only [Int.mul_neg]
+          omega
+        rw [this]
+        exact Int.dvd_mul_right ..
+
+theorem ToInt.wrap_eq_wrap_iff :
+    ToInt.wrap (some lo) (some hi) x = ToInt.wrap (some lo) (some hi) y ↔ (x - y) % (hi - lo) = 0 := by
+  simp only [wrap]
+  rw [Int.add_left_inj]
+  rw [Int.emod_eq_emod_iff_emod_sub_eq_zero]
+  have : x - lo - (y - lo)  = x - y := by omega
+  rw [this]
+
+/-- Construct a `ToInt.Sub` instance from a `ToInt.Add` and `ToInt.Neg` instance and
+a `sub_eq_add_neg` assumption. -/
+def ToInt.Sub.of_sub_eq_add_neg {α : Type u} [_root_.Add α] [_root_.Neg α] [_root_.Sub α]
+    (sub_eq_add_neg : ∀ x y : α, x - y = x + -y)
+    {lo? hi? : Option Int} [ToInt α lo? hi?] [Add α lo? hi?] [Neg α lo? hi?] : ToInt.Sub α lo? hi? where
+  toInt_sub x y := by
+    rw [sub_eq_add_neg, ToInt.Add.toInt_add, ToInt.Neg.toInt_neg, Int.sub_eq_add_neg]
+    conv => rhs; rw [ToInt.wrap_add, ToInt.wrap_toInt]
+
+/-! ## Instances for concrete types-/
+
+instance : ToInt Int none none where
+  toInt := id
+  toInt_inj := by simp
+  le_toInt := by simp
+  toInt_lt := by simp
+
+@[simp] theorem toInt_int (x : Int) : ToInt.toInt x = x := rfl
+
+instance : ToInt.Add Int none none where
+  toInt_add := by simp
+
+instance : ToInt.Neg Int none none where
+  toInt_neg x := by simp
+
+instance : ToInt.Sub Int none none where
+  toInt_sub x y := by simp
+
+instance : ToInt.Mod Int none none where
+  toInt_mod x y := by simp
+
+instance : ToInt.LE Int none none where
+  le_iff x y := by simp
+
+instance : ToInt.LT Int none none where
+  lt_iff x y := by simp
+
+instance : ToInt Nat (some 0) none where
+  toInt := Nat.cast
+  toInt_inj x y := Int.ofNat_inj.mp
+  le_toInt {lo x} w := by simp at w; subst w; exact Int.natCast_nonneg x
+  toInt_lt := by simp
+
+@[simp] theorem toInt_nat (x : Nat) : ToInt.toInt x = (x : Int) := rfl
+
+instance : ToInt.Add Nat (some 0) none where
+  toInt_add := by simp
+
+instance : ToInt.Mod Nat (some 0) none where
+  toInt_mod x y := by simp
+
+instance : ToInt.LE Nat (some 0) none where
+  le_iff x y := by simp
+
+instance : ToInt.LT Nat (some 0) none where
+  lt_iff x y := by simp
+
+-- Mathlib will add a `ToInt ℕ+ (some 1) none` instance.
+
+instance : ToInt (Fin n) (some 0) (some n) where
+  toInt x := x.val
+  toInt_inj x y w := Fin.eq_of_val_eq (Int.ofNat_inj.mp w)
+  le_toInt {lo x} w := by simp only [Option.some.injEq] at w; subst w; exact Int.natCast_nonneg x
+  toInt_lt {hi x} w := by simp only [Option.some.injEq] at w; subst w; exact Int.ofNat_lt.mpr x.isLt
+
+@[simp] theorem toInt_fin (x : Fin n) : ToInt.toInt x = (x.val : Int) := rfl
+
+instance : ToInt.Add (Fin n) (some 0) (some n) where
+  toInt_add x y := by rfl
+
+instance [NeZero n] : ToInt.Zero (Fin n) (some 0) (some n) where
+  toInt_zero := by rfl
+
+-- The `ToInt.Neg` and `ToInt.Sub` instances are generated automatically from the `IntModule (Fin n)` instance.
+
+instance : ToInt.Mod (Fin n) (some 0) (some n) where
+  toInt_mod x y := by
+    simp only [toInt_fin, Fin.mod_val, Int.natCast_emod]
+
+instance : ToInt.LE (Fin n) (some 0) (some n) where
+  le_iff x y := by simpa using Fin.le_def
+
+instance : ToInt.LT (Fin n) (some 0) (some n) where
+  lt_iff x y := by simpa using Fin.lt_def
+
+instance : ToInt UInt8 (some 0) (some (2^8)) where
+  toInt x := (x.toNat : Int)
+  toInt_inj x y w := UInt8.toNat_inj.mp (Int.ofNat_inj.mp w)
+  le_toInt {lo x} w := by simp at w; subst w; exact Int.natCast_nonneg x.toNat
+  toInt_lt {hi x} w := by simp at w; subst w; exact Int.lt_toNat.mp (UInt8.toNat_lt x)
+
+@[simp] theorem toInt_uint8 (x : UInt8) : ToInt.toInt x = (x.toNat : Int) := rfl
+
+instance : ToInt.Add UInt8 (some 0) (some (2^8)) where
+  toInt_add x y := by simp
+
+instance : ToInt.Zero UInt8 (some 0) (some (2^8)) where
+  toInt_zero := by simp
+
+instance : ToInt.Mod UInt8 (some 0) (some (2^8)) where
+  toInt_mod x y := by simp
+
+instance : ToInt.LE UInt8 (some 0) (some (2^8)) where
+  le_iff x y := by simpa using UInt8.le_iff_toBitVec_le
+
+instance : ToInt.LT UInt8 (some 0) (some (2^8)) where
+  lt_iff x y := by simpa using UInt8.lt_iff_toBitVec_lt
+
+instance : ToInt UInt16 (some 0) (some (2^16)) where
+  toInt x := (x.toNat : Int)
+  toInt_inj x y w := UInt16.toNat_inj.mp (Int.ofNat_inj.mp w)
+  le_toInt {lo x} w := by simp at w; subst w; exact Int.natCast_nonneg x.toNat
+  toInt_lt {hi x} w := by simp at w; subst w; exact Int.lt_toNat.mp (UInt16.toNat_lt x)
+
+@[simp] theorem toInt_uint16 (x : UInt16) : ToInt.toInt x = (x.toNat : Int) := rfl
+
+instance : ToInt.Add UInt16 (some 0) (some (2^16)) where
+  toInt_add x y := by simp
+
+instance : ToInt.Zero UInt16 (some 0) (some (2^16)) where
+  toInt_zero := by simp
+
+instance : ToInt.Mod UInt16 (some 0) (some (2^16)) where
+  toInt_mod x y := by simp
+
+instance : ToInt.LE UInt16 (some 0) (some (2^16)) where
+  le_iff x y := by simpa using UInt16.le_iff_toBitVec_le
+
+instance : ToInt.LT UInt16 (some 0) (some (2^16)) where
+  lt_iff x y := by simpa using UInt16.lt_iff_toBitVec_lt
+
+instance : ToInt UInt32 (some 0) (some (2^32)) where
+  toInt x := (x.toNat : Int)
+  toInt_inj x y w := UInt32.toNat_inj.mp (Int.ofNat_inj.mp w)
+  le_toInt {lo x} w := by simp at w; subst w; exact Int.natCast_nonneg x.toNat
+  toInt_lt {hi x} w := by simp at w; subst w; exact Int.lt_toNat.mp (UInt32.toNat_lt x)
+
+@[simp] theorem toInt_uint32 (x : UInt32) : ToInt.toInt x = (x.toNat : Int) := rfl
+
+instance : ToInt.Add UInt32 (some 0) (some (2^32)) where
+  toInt_add x y := by simp
+
+instance : ToInt.Zero UInt32 (some 0) (some (2^32)) where
+  toInt_zero := by simp
+
+instance : ToInt.Mod UInt32 (some 0) (some (2^32)) where
+  toInt_mod x y := by simp
+
+instance : ToInt.LE UInt32 (some 0) (some (2^32)) where
+  le_iff x y := by simpa using UInt32.le_iff_toBitVec_le
+
+instance : ToInt.LT UInt32 (some 0) (some (2^32)) where
+  lt_iff x y := by simpa using UInt32.lt_iff_toBitVec_lt
+
+instance : ToInt UInt64 (some 0) (some (2^64)) where
+  toInt x := (x.toNat : Int)
+  toInt_inj x y w := UInt64.toNat_inj.mp (Int.ofNat_inj.mp w)
+  le_toInt {lo x} w := by simp at w; subst w; exact Int.natCast_nonneg x.toNat
+  toInt_lt {hi x} w := by simp at w; subst w; exact Int.lt_toNat.mp (UInt64.toNat_lt x)
+
+@[simp] theorem toInt_uint64 (x : UInt64) : ToInt.toInt x = (x.toNat : Int) := rfl
+
+instance : ToInt.Add UInt64 (some 0) (some (2^64)) where
+  toInt_add x y := by simp
+
+instance : ToInt.Zero UInt64 (some 0) (some (2^64)) where
+  toInt_zero := by simp
+
+instance : ToInt.Mod UInt64 (some 0) (some (2^64)) where
+  toInt_mod x y := by simp
+
+instance : ToInt.LE UInt64 (some 0) (some (2^64)) where
+  le_iff x y := by simpa using UInt64.le_iff_toBitVec_le
+
+instance : ToInt.LT UInt64 (some 0) (some (2^64)) where
+  lt_iff x y := by simpa using UInt64.lt_iff_toBitVec_lt
+
+instance : ToInt USize (some 0) (some (2^System.Platform.numBits)) where
+  toInt x := (x.toNat : Int)
+  toInt_inj x y w := USize.toNat_inj.mp (Int.ofNat_inj.mp w)
+  le_toInt {lo x} w := by simp at w; subst w; exact Int.natCast_nonneg x.toNat
+  toInt_lt {hi x} w := by
+    simp at w; subst w
+    rw [show (2 : Int) ^ System.Platform.numBits = (2 ^ System.Platform.numBits : Nat) by simp,
+      Int.ofNat_lt]
+    exact USize.toNat_lt_two_pow_numBits x
+
+@[simp] theorem toInt_usize (x : USize) : ToInt.toInt x = (x.toNat : Int) := rfl
+
+instance : ToInt.Add USize (some 0) (some (2^System.Platform.numBits)) where
+  toInt_add x y := by simp
+
+instance : ToInt.Zero USize (some 0) (some (2^System.Platform.numBits)) where
+  toInt_zero := by simp
+
+instance : ToInt.Mod USize (some 0) (some (2^System.Platform.numBits)) where
+  toInt_mod x y := by simp
+
+instance : ToInt.LE USize (some 0) (some (2^System.Platform.numBits)) where
+  le_iff x y := by simpa using USize.le_iff_toBitVec_le
+
+instance : ToInt.LT USize (some 0) (some (2^System.Platform.numBits)) where
+  lt_iff x y := by simpa using USize.lt_iff_toBitVec_lt
+
+instance : ToInt Int8 (some (-2^7)) (some (2^7)) where
+  toInt x := x.toInt
+  toInt_inj x y w := Int8.toInt_inj.mp w
+  le_toInt {lo x} w := by simp at w; subst w; exact Int8.le_toInt x
+  toInt_lt {hi x} w := by simp at w; subst w; exact Int8.toInt_lt x
+
+@[simp] theorem toInt_int8 (x : Int8) : ToInt.toInt x = (x.toInt : Int) := rfl
+
+instance : ToInt.Add Int8 (some (-2^7)) (some (2^7)) where
+  toInt_add x y := by
+    simp [Int.bmod_eq_emod]
+    split <;> · simp; omega
+
+instance : ToInt.Zero Int8 (some (-2^7)) (some (2^7)) where
+  toInt_zero := by
+    --  simp -- FIXME: succeeds, but generates a `(kernel) application type mismatch` error!
+    change (0 : Int8).toInt = _
+    rw [Int8.toInt_zero]
+    decide
+
+-- Note that we can not define `ToInt.Mod` instances for `Int8`,
+-- because the condition does not hold unless `0 ≤ x.toInt ∨ y.toInt ∣ x.toInt ∨ y = 0`.
+
+instance : ToInt.LE Int8 (some (-2^7)) (some (2^7)) where
+  le_iff x y := by simpa using Int8.le_iff_toInt_le
+
+instance : ToInt.LT Int8 (some (-2^7)) (some (2^7)) where
+  lt_iff x y := by simpa using Int8.lt_iff_toInt_lt
+
+instance : ToInt Int16 (some (-2^15)) (some (2^15)) where
+  toInt x := x.toInt
+  toInt_inj x y w := Int16.toInt_inj.mp w
+  le_toInt {lo x} w := by simp at w; subst w; exact Int16.le_toInt x
+  toInt_lt {hi x} w := by simp at w; subst w; exact Int16.toInt_lt x
+
+@[simp] theorem toInt_int16 (x : Int16) : ToInt.toInt x = (x.toInt : Int) := rfl
+
+instance : ToInt.Add Int16 (some (-2^15)) (some (2^15)) where
+  toInt_add x y := by
+    simp [Int.bmod_eq_emod]
+    split <;> · simp; omega
+
+instance : ToInt.Zero Int16 (some (-2^15)) (some (2^15)) where
+  toInt_zero := by
+    -- simp -- FIXME: succeeds, but generates a `(kernel) application type mismatch` error!
+    change (0 : Int16).toInt = _
+    rw [Int16.toInt_zero]
+    decide
+
+instance : ToInt.LE Int16 (some (-2^15)) (some (2^15)) where
+  le_iff x y := by simpa using Int16.le_iff_toInt_le
+
+instance : ToInt.LT Int16 (some (-2^15)) (some (2^15)) where
+  lt_iff x y := by simpa using Int16.lt_iff_toInt_lt
+
+instance : ToInt Int32 (some (-2^31)) (some (2^31)) where
+  toInt x := x.toInt
+  toInt_inj x y w := Int32.toInt_inj.mp w
+  le_toInt {lo x} w := by simp at w; subst w; exact Int32.le_toInt x
+  toInt_lt {hi x} w := by simp at w; subst w; exact Int32.toInt_lt x
+
+@[simp] theorem toInt_int32 (x : Int32) : ToInt.toInt x = (x.toInt : Int) := rfl
+
+instance : ToInt.Add Int32 (some (-2^31)) (some (2^31)) where
+  toInt_add x y := by
+    simp [Int.bmod_eq_emod]
+    split <;> · simp; omega
+
+instance : ToInt.Zero Int32 (some (-2^31)) (some (2^31)) where
+  toInt_zero := by
+    -- simp -- FIXME: succeeds, but generates a `(kernel) application type mismatch` error!
+    change (0 : Int32).toInt = _
+    rw [Int32.toInt_zero]
+    decide
+
+instance : ToInt.LE Int32 (some (-2^31)) (some (2^31)) where
+  le_iff x y := by simpa using Int32.le_iff_toInt_le
+
+instance : ToInt.LT Int32 (some (-2^31)) (some (2^31)) where
+  lt_iff x y := by simpa using Int32.lt_iff_toInt_lt
+
+instance : ToInt Int64 (some (-2^63)) (some (2^63)) where
+  toInt x := x.toInt
+  toInt_inj x y w := Int64.toInt_inj.mp w
+  le_toInt {lo x} w := by simp at w; subst w; exact Int64.le_toInt x
+  toInt_lt {hi x} w := by simp at w; subst w; exact Int64.toInt_lt x
+
+@[simp] theorem toInt_int64 (x : Int64) : ToInt.toInt x = (x.toInt : Int) := rfl
+
+instance : ToInt.Add Int64 (some (-2^63)) (some (2^63)) where
+  toInt_add x y := by
+    simp [Int.bmod_eq_emod]
+    split <;> · simp; omega
+
+instance : ToInt.Zero Int64 (some (-2^63)) (some (2^63)) where
+  toInt_zero := by
+    -- simp -- FIXME: succeeds, but generates a `(kernel) application type mismatch` error!
+    change (0 : Int64).toInt = _
+    rw [Int64.toInt_zero]
+    decide
+
+instance : ToInt.LE Int64 (some (-2^63)) (some (2^63)) where
+  le_iff x y := by simpa using Int64.le_iff_toInt_le
+
+instance : ToInt.LT Int64 (some (-2^63)) (some (2^63)) where
+  lt_iff x y := by simpa using Int64.lt_iff_toInt_lt
+
+instance : ToInt (BitVec v) (some 0) (some (2^v)) where
+  toInt x := (x.toNat : Int)
+  toInt_inj x y w :=
+    BitVec.eq_of_toNat_eq (Int.ofNat_inj.mp w)
+  le_toInt {lo x} w := by simp at w; subst w; exact Int.natCast_nonneg x.toNat
+  toInt_lt {hi x} w := by
+    simp at w; subst w;
+    simpa using Int.ofNat_lt.mpr (BitVec.isLt x)
+
+@[simp] theorem toInt_bitVec (x : BitVec v) : ToInt.toInt x = (x.toNat : Int) := rfl
+
+instance : ToInt.Add (BitVec v) (some 0) (some (2^v)) where
+  toInt_add x y := by simp
+
+instance : ToInt.Zero (BitVec v) (some 0) (some (2^v)) where
+  toInt_zero := by simp
+
+instance : ToInt.Mod (BitVec v) (some 0) (some (2^v)) where
+  toInt_mod x y := by simp
+
+instance : ToInt.LE (BitVec v) (some 0) (some (2^v)) where
+  le_iff x y := by simpa using BitVec.le_def
+
+instance : ToInt.LT (BitVec v) (some 0) (some (2^v)) where
+  lt_iff x y := by simpa using BitVec.lt_def
+
+instance : ToInt ISize (some (-2^(System.Platform.numBits-1))) (some (2^(System.Platform.numBits-1))) where
+  toInt x := x.toInt
+  toInt_inj x y w := ISize.toInt_inj.mp w
+  le_toInt {lo x} w := by simp at w; subst w; exact ISize.two_pow_numBits_le_toInt x
+  toInt_lt {hi x} w := by simp at w; subst w; exact ISize.toInt_lt_two_pow_numBits x
+
+@[simp] theorem toInt_isize (x : ISize) : ToInt.toInt x = x.toInt := rfl
+
+instance : ToInt.Add ISize (some (-2^(System.Platform.numBits-1))) (some (2^(System.Platform.numBits-1))) where
+  toInt_add x y := by
+    rw [toInt_isize, ISize.toInt_add, ToInt.wrap_eq_bmod (Int.pow_nonneg (by decide))]
+    have p₁ : (2 : Int) * 2 ^ (System.Platform.numBits - 1) = 2 ^ System.Platform.numBits := by
+      have := System.Platform.numBits_pos
+      have : System.Platform.numBits - 1 + 1 = System.Platform.numBits := by omega
+      simp [← Int.pow_succ', this]
+    have p₂ : ((2 : Int) ^ System.Platform.numBits).toNat = 2 ^ System.Platform.numBits := by
+      rw [Int.toNat_pow_of_nonneg (by decide)]
+      simp
+    simp [p₁, p₂]
+
+instance : ToInt.Zero ISize (some (-2^(System.Platform.numBits-1))) (some (2^(System.Platform.numBits-1))) where
+  toInt_zero := by
+    rw [toInt_isize]
+    rw [ISize.toInt_zero, ToInt.wrap_eq_bmod (Int.pow_nonneg (by decide))]
+    simp
+
+instance instToIntLEISize : ToInt.LE ISize (some (-2^(System.Platform.numBits-1))) (some (2^(System.Platform.numBits-1))) where
+  le_iff x y := by simpa using ISize.le_iff_toInt_le
+
+instance instToIntLTISize : ToInt.LT ISize (some (-2^(System.Platform.numBits-1))) (some (2^(System.Platform.numBits-1))) where
+  lt_iff x y := by simpa using ISize.lt_iff_toInt_lt
+
+end Lean.Grind

src/Init/Grind/Util.lean

@@ -32,55 +32,6 @@ def offset (a b : Nat) : Nat := a + b
 /-- Gadget for representing `a = b` in patterns for backward propagation. -/
 def eqBwdPattern (a b : α) : Prop := a = b
 
-/--
-Gadget for representing generalization steps `h : x = val` in patterns
-This gadget is used to represent patterns in theorems that have been generalized to reduce the
-number of casts introduced during E-matching based instantiation.
-
-For example, consider the theorem
-```
-Option.pbind_some {α1 : Type u_1} {a : α1} {α2 : Type u_2}
-    {f : (a_1 : α1) → some a = some a_1 → Option α2}
-    : (some a).pbind f = f a rfl
-```
-Now, suppose we have a goal containing the term `c.pbind g` and the equivalence class
-`{c, some b}`. The E-matching module generates the instance
-```
-(some b).pbind (cast ⋯ g)
-```
-The `cast` is necessary because `g`'s type contains `c` instead of `some b.
-This `cast` problematic because we don't have a systematic way of pushing casts over functions
-to its arguments. Moreover, heterogeneous equality is not effective because the following theorem
-is not provable in DTT:
-```
-theorem hcongr (h₁ : f ≍ g) (h₂ : a ≍ b)  : f a ≍ g b := ...
-```
-The standard solution is to generalize the theorem above and write it as
-```
-theorem Option.pbind_some'
-        {α1 : Type u_1} {a : α1} {α2 : Type u_2}
-        {x : Option α1}
-        {f : (a_1 : α1) → x = some a_1 → Option α2}
-        (h : x = some a)
-        : x.pbind f = f a h := by
-  subst h
-  apply Option.pbind_some
-```
-Internally, we use this gadget to mark the E-matching pattern as
-```
-(genPattern h x (some a)).pbind f
-```
-This pattern is matched in the same way we match `(some a).pbind f`, but it saves the proof
-for the actual term to the `some`-application in `f`, and the actual term in `x`.
-
-In the example above, `c.pbind g` also matches the pattern `(genPattern h x (some a)).pbind f`,
-and stores `c` in `x`, `b` in `a`, and the proof that `c = some b` in `h`.
--/
-def genPattern {α : Sort u} (_h : Prop) (x : α) (_val : α) : α := x
-
-/-- Similar to `genPattern` but for the heterogenous case -/
-def genHEqPattern {α β : Sort u} (_h : Prop) (x : α) (_val : β) : α := x
-
 /--
 Gadget for annotating the equalities in `match`-equations conclusions.
 `_origin` is the term used to instantiate the `match`-equation using E-matching.

src/Init/Meta.lean

@@ -8,6 +8,7 @@ Additional goodies for writing macros
 module
 
 prelude
+import all Init.Prelude  -- for unfolding `Name.beq`
 import Init.MetaTypes
 import Init.Syntax
 import Init.Data.Array.GetLit
@@ -1203,7 +1204,8 @@ def quoteNameMk : Name → Term
   | .num n i => Syntax.mkCApp ``Name.mkNum #[quoteNameMk n, quote i]
 
 instance : Quote Name `term where
-  quote n := match getEscapedNameParts? [] n with
+  quote n := private
+    match getEscapedNameParts? [] n with
     | some ss => ⟨mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit ("`" ++ ".".intercalate ss)]⟩
     | none    => ⟨quoteNameMk n⟩
 
@@ -1216,7 +1218,7 @@ private def quoteList [Quote α `term] : List α → Term
   | (x::xs) => Syntax.mkCApp ``List.cons #[quote x, quoteList xs]
 
 instance [Quote α `term] : Quote (List α) `term where
-  quote := quoteList
+  quote := private quoteList
 
 private def quoteArray [Quote α `term] (xs : Array α) : Term :=
   if xs.size <= 8 then
@@ -1233,7 +1235,7 @@ where
   decreasing_by decreasing_trivial_pre_omega
 
 instance [Quote α `term] : Quote (Array α) `term where
-  quote := quoteArray
+  quote := private quoteArray
 
 instance Option.hasQuote {α : Type} [Quote α `term] : Quote (Option α) `term where
   quote

src/Init/Notation.lean

@@ -432,7 +432,7 @@ recommended_spelling "not" for "!" in [not, «term!_»]
 notation:50 a:50 " ∉ " b:50 => ¬ (a ∈ b)
 
 recommended_spelling "mem" for "∈" in [Membership.mem, «term_∈_»]
-recommended_spelling "not_mem" for "∉" in [«term_∉_»]
+recommended_spelling "notMem" for "∉" in [«term_∉_»]
 
 @[inherit_doc] infixr:67 " :: " => List.cons
 @[inherit_doc] infixr:100 " <$> " => Functor.map
@@ -531,8 +531,21 @@ is interpreted as `f (g x)` rather than `(f g) x`.
 syntax:min term " <| " term:min : term
 
 macro_rules
-  | `($f $args* <| $a) => `($f $args* $a)
-  | `($f <| $a) => `($f $a)
+  | `($f $args* <| $a) =>
+    if a.raw.isMissing then
+      -- Ensures that `$f $args* <|` is elaborated as `$f $args*`, not `$f $args* sorry`.
+      -- For the latter, the elaborator produces `TermInfo` where the missing argument has already
+      -- been applied as `sorry`, which inhibits some language server functionality that relies
+      -- on this `TermInfo` (e.g. signature help).
+      -- The parser will still produce an error for `$f $args* <|` in this case.
+      `($f $args*)
+    else
+      `($f $args* $a)
+  | `($f <| $a) =>
+    if a.raw.isMissing then
+      `($f)
+    else
+      `($f $a)
 
 /--
 Haskell-like pipe operator `|>`. `x |> f` means the same as the same as `f x`,
@@ -553,8 +566,21 @@ is interpreted as `f (g x)` rather than `(f g) x`.
 syntax:min term atomic(" $" ws) term:min : term
 
 macro_rules
-  | `($f $args* $ $a) => `($f $args* $a)
-  | `($f $ $a) => `($f $a)
+  | `($f $args* $ $a) =>
+    if a.raw.isMissing then
+      -- Ensures that `$f $args* $` is elaborated as `$f $args*`, not `$f $args* sorry`.
+      -- For the latter, the elaborator produces `TermInfo` where the missing argument has already
+      -- been applied as `sorry`, which inhibits some language server functionality that relies
+      -- on this `TermInfo` (e.g. signature help).
+      -- The parser will still produce an error for `$f $args* <|` in this case.
+      `($f $args*)
+    else
+      `($f $args* $a)
+  | `($f $ $a) =>
+    if a.raw.isMissing then
+      `($f)
+    else
+      `($f $a)
 
 @[inherit_doc Subtype] syntax "{ " withoutPosition(ident (" : " term)? " // " term) " }" : term
 

src/Init/Prelude.lean

@@ -861,7 +861,7 @@ instance : Inhabited NonemptyType.{u} where
 Lifts a type to a higher universe level.
 
 `ULift α` wraps a value of type `α`. Instead of occupying the same universe as `α`, which would be
-the minimal level, it takes a further level parameter and occupies their minimum. The resulting type
+the minimal level, it takes a further level parameter and occupies their maximum. The resulting type
 may occupy any universe that's at least as large as that of `α`.
 
 The resulting universe of the lifting operator is the first parameter, and may be written explicitly
@@ -2500,8 +2500,12 @@ Pack a `Nat` encoding a valid codepoint into a `Char`.
 This function is overridden with a native implementation.
 -/
 @[extern "lean_uint32_of_nat"]
-def Char.ofNatAux (n : @& Nat) (h : n.isValidChar) : Char :=
-  { val := ⟨BitVec.ofNatLT n (isValidChar_UInt32 h)⟩, valid := h }
+def Char.ofNatAux (n : @& Nat) (h : n.isValidChar) : Char where
+  val := ⟨BitVec.ofNatLT n
+    -- We would conventionally use `by exact` here to enter a private context, but `exact` does not
+    -- exist here yet.
+    (private_decl% isValidChar_UInt32 h)⟩
+  valid := h
 
 /--
 Converts a `Nat` into a `Char`. If the `Nat` does not encode a valid Unicode scalar value, `'\0'` is
@@ -4092,8 +4096,13 @@ protected opaque String.hash (s : @& String) : UInt64
 instance : Hashable String where
   hash := String.hash
 
+end  -- don't expose `Lean` defs
+
 namespace Lean
 
+open BEq (beq)
+open HAdd (hAdd)
+
 /--
 Hierarchical names consist of a sequence of components, each of
 which is either a string or numeric, that are written separated by dots (`.`).
@@ -4178,35 +4187,35 @@ abbrev mkSimple (s : String) : Name :=
   .str .anonymous s
 
 /-- Make name `s₁` -/
-@[reducible] def mkStr1 (s₁ : String) : Name :=
+@[expose, reducible] def mkStr1 (s₁ : String) : Name :=
   .str .anonymous s₁
 
 /-- Make name `s₁.s₂` -/
-@[reducible] def mkStr2 (s₁ s₂ : String) : Name :=
+@[expose, reducible] def mkStr2 (s₁ s₂ : String) : Name :=
   .str (.str .anonymous s₁) s₂
 
 /-- Make name `s₁.s₂.s₃` -/
-@[reducible] def mkStr3 (s₁ s₂ s₃ : String) : Name :=
+@[expose, reducible] def mkStr3 (s₁ s₂ s₃ : String) : Name :=
   .str (.str (.str .anonymous s₁) s₂) s₃
 
 /-- Make name `s₁.s₂.s₃.s₄` -/
-@[reducible] def mkStr4 (s₁ s₂ s₃ s₄ : String) : Name :=
+@[expose, reducible] def mkStr4 (s₁ s₂ s₃ s₄ : String) : Name :=
   .str (.str (.str (.str .anonymous s₁) s₂) s₃) s₄
 
 /-- Make name `s₁.s₂.s₃.s₄.s₅` -/
-@[reducible] def mkStr5 (s₁ s₂ s₃ s₄ s₅ : String) : Name :=
+@[expose, reducible] def mkStr5 (s₁ s₂ s₃ s₄ s₅ : String) : Name :=
   .str (.str (.str (.str (.str .anonymous s₁) s₂) s₃) s₄) s₅
 
 /-- Make name `s₁.s₂.s₃.s₄.s₅.s₆` -/
-@[reducible] def mkStr6 (s₁ s₂ s₃ s₄ s₅ s₆ : String) : Name :=
+@[expose, reducible] def mkStr6 (s₁ s₂ s₃ s₄ s₅ s₆ : String) : Name :=
   .str (.str (.str (.str (.str (.str .anonymous s₁) s₂) s₃) s₄) s₅) s₆
 
 /-- Make name `s₁.s₂.s₃.s₄.s₅.s₆.s₇` -/
-@[reducible] def mkStr7 (s₁ s₂ s₃ s₄ s₅ s₆ s₇ : String) : Name :=
+@[expose, reducible] def mkStr7 (s₁ s₂ s₃ s₄ s₅ s₆ s₇ : String) : Name :=
   .str (.str (.str (.str (.str (.str (.str .anonymous s₁) s₂) s₃) s₄) s₅) s₆) s₇
 
 /-- Make name `s₁.s₂.s₃.s₄.s₅.s₆.s₇.s₈` -/
-@[reducible] def mkStr8 (s₁ s₂ s₃ s₄ s₅ s₆ s₇ s₈ : String) : Name :=
+@[expose, reducible] def mkStr8 (s₁ s₂ s₃ s₄ s₅ s₆ s₇ s₈ : String) : Name :=
   .str (.str (.str (.str (.str (.str (.str (.str .anonymous s₁) s₂) s₃) s₄) s₅) s₆) s₇) s₈
 
 /-- (Boolean) equality comparator for names. -/
@@ -4455,7 +4464,7 @@ def Syntax.node8 (info : SourceInfo) (kind : SyntaxNodeKind) (a₁ a₂ a₃ a
 Singleton `SyntaxNodeKinds` are extremely common. They are written as name literals, rather than as
 lists; list syntax is required only for empty or non-singleton sets of kinds.
 -/
-def SyntaxNodeKinds := List SyntaxNodeKind
+@[expose] def SyntaxNodeKinds := List SyntaxNodeKind
 
 /--
 Typed syntax, which tracks the potential kinds of the `Syntax` it contains.
@@ -5140,11 +5149,13 @@ end Syntax
 namespace Macro
 
 /-- References -/
-private opaque MethodsRefPointed : NonemptyType.{0}
+-- TODO: make private again and make Nonempty instance no_expose instead after bootstrapping
+opaque MethodsRefPointed : NonemptyType.{0}
 
-private def MethodsRef : Type := MethodsRefPointed.type
+set_option linter.missingDocs false in
+@[expose] def MethodsRef : Type := MethodsRefPointed.type
 
-private instance : Nonempty MethodsRef := MethodsRefPointed.property
+instance : Nonempty MethodsRef := MethodsRefPointed.property
 
 /-- The read-only context for the `MacroM` monad. -/
 structure Context where

src/Init/System/IO.lean

@@ -1014,7 +1014,10 @@ inductive FileType where
   | dir
   /-- Ordinary files that have contents and are not directories. -/
   | file
-  /-- Symbolic links that are pointers to other named files. -/
+  /--
+  Symbolic links that are pointers to other named files. Note that `System.FilePath.metadata` never
+  indicates this type as it follows symlinks; use `System.FilePath.symlinkMetadata` instead.
+  -/
   | symlink
   /-- Files that are neither ordinary files, directories, or symbolic links. -/
   | other
@@ -1036,7 +1039,8 @@ instance : LE SystemTime := leOfOrd
 /--
 File metadata.
 
-The metadata for a file can be accessed with `System.FilePath.metadata`.
+The metadata for a file can be accessed with `System.FilePath.metadata`/
+`System.FilePath.symlinkMetadata`.
 -/
 structure Metadata where
   --permissions : ...
@@ -1066,14 +1070,22 @@ is not a directory.
 opaque readDir : @& FilePath → IO (Array IO.FS.DirEntry)
 
 /--
-Returns metadata for the indicated file. Throws an exception if the file does not exist or the
-metadata cannot be accessed.
+Returns metadata for the indicated file, following symlinks. Throws an exception if the file does
+not exist or the metadata cannot be accessed.
 -/
 @[extern "lean_io_metadata"]
 opaque metadata : @& FilePath → IO IO.FS.Metadata
 
 /--
-Checks whether the indicated path can be read and is a directory.
+Returns metadata for the indicated file without following symlinks. Throws an exception if the file
+does not exist or the metadata cannot be accessed.
+-/
+@[extern "lean_io_symlink_metadata"]
+opaque symlinkMetadata : @& FilePath → IO IO.FS.Metadata
+
+/--
+Checks whether the indicated path can be read and is a directory. This function will traverse
+symlinks.
 -/
 def isDir (p : FilePath) : BaseIO Bool := do
   match (← p.metadata.toBaseIO) with
@@ -1081,7 +1093,8 @@ def isDir (p : FilePath) : BaseIO Bool := do
   | Except.error _ => return false
 
 /--
-Checks whether the indicated path points to a file that exists.
+Checks whether the indicated path points to a file that exists. This function will traverse
+symlinks.
 -/
 def pathExists (p : FilePath) : BaseIO Bool :=
   return (← p.metadata.toBaseIO).toBool
@@ -1243,11 +1256,14 @@ partial def createDirAll (p : FilePath) : IO Unit := do
         throw e
 
 /--
-  Fully remove given directory by deleting all contained files and directories in an unspecified order.
-  Fails if any contained entry cannot be deleted or was newly created during execution. -/
+Fully remove given directory by deleting all contained files and directories in an unspecified order.
+Symlinks are deleted but not followed. Fails if any contained entry cannot be deleted or was newly
+created during execution.
+-/
 partial def removeDirAll (p : FilePath) : IO Unit := do
   for ent in (← p.readDir) do
-    if (← ent.path.isDir : Bool) then
+    -- Do not follow symlinks
+    if (← ent.path.symlinkMetadata).type == .dir then
       removeDirAll ent.path
     else
       removeFile ent.path
@@ -1468,7 +1484,9 @@ terminates with any other exit code.
 def run (args : SpawnArgs) : IO String := do
   let out ← output args
   if out.exitCode != 0 then
-    throw <| IO.userError <| "process '" ++ args.cmd ++ "' exited with code " ++ toString out.exitCode
+    throw <| IO.userError s!"process '{args.cmd}' exited with code {out.exitCode}\
+      \nstderr:\
+      \n{out.stderr}"
   pure out.stdout
 
 /--

src/Init/Util.lean

@@ -32,13 +32,13 @@ def dbgStackTrace {α : Type u} (f : Unit → α) : α := f ()
 @[extern "lean_dbg_sleep"]
 def dbgSleep {α : Type u} (ms : UInt32) (f : Unit → α) : α := f ()
 
-@[noinline] private def mkPanicMessage (modName : String) (line col : Nat) (msg : String) : String :=
+@[noinline] def mkPanicMessage (modName : String) (line col : Nat) (msg : String) : String :=
   "PANIC at " ++ modName ++ ":" ++ toString line ++ ":" ++ toString col ++ ": " ++ msg
 
 @[never_extract, inline, expose] def panicWithPos {α : Sort u} [Inhabited α] (modName : String) (line col : Nat) (msg : String) : α :=
   panic (mkPanicMessage modName line col msg)
 
-@[noinline, expose] private def mkPanicMessageWithDecl (modName : String) (declName : String) (line col : Nat) (msg : String) : String :=
+@[noinline, expose] def mkPanicMessageWithDecl (modName : String) (declName : String) (line col : Nat) (msg : String) : String :=
   "PANIC at " ++ declName ++ " " ++ modName ++ ":" ++ toString line ++ ":" ++ toString col ++ ": " ++ msg
 
 @[never_extract, inline, expose] def panicWithPosWithDecl {α : Sort u} [Inhabited α] (modName : String) (declName : String) (line col : Nat) (msg : String) : α :=

src/Init/WF.lean

@@ -157,14 +157,8 @@ end Subrelation
 namespace InvImage
 variable {α : Sort u} {β : Sort v} {r : β → β → Prop}
 
-private def accAux (f : α → β) {b : β} (ac : Acc r b) : (x : α) → f x = b → Acc (InvImage r f) x := by
-  induction ac with
-  | intro x acx ih =>
-    intro z e
-    apply Acc.intro
-    intro y lt
-    subst x
-    apply ih (f y) lt y rfl
+def accAux (f : α → β) {b : β} (ac : Acc r b) : (x : α) → f x = b → Acc (InvImage r f) x :=
+  Acc.recOn ac fun _ _ ih => fun _ e => Acc.intro _ (fun y lt => ih (f y) (e ▸ lt) y rfl)
 
 -- `def` for `WellFounded.fix`
 def accessible {a : α} (f : α → β) (ac : Acc r (f a)) : Acc (InvImage r f) a :=

src/Lean/AddDecl.lean

@@ -84,9 +84,6 @@ def addDecl (decl : Declaration) : CoreM Unit := do
   -- namespaces
   modifyEnv (decl.getNames.foldl registerNamePrefixes)
 
-  if !Elab.async.get (← getOptions) then
-    return (← addSynchronously)
-
   -- convert `Declaration` to `ConstantInfo` to use as a preliminary value in the environment until
   -- kernel checking has finished; not all cases are supported yet
   let mut exportedInfo? := none
@@ -106,44 +103,45 @@ def addDecl (decl : Declaration) : CoreM Unit := do
         exportedInfo? := some <| .axiomInfo { defn with isUnsafe := defn.safety == .unsafe }
       pure (defn.name, .defnInfo defn, .defn)
     | .axiomDecl ax => pure (ax.name, .axiomInfo ax, .axiom)
-    | _ => return (← addSynchronously)
+    | _ => return (← doAdd)
 
-  -- preserve original constant kind in extension if different from exported one
-  if exportedInfo?.isSome then
-    modifyEnv (privateConstKindsExt.insert · name kind)
+  if decl.getTopLevelNames.all isPrivateName then
+    exportedInfo? := none
+  else
+    -- preserve original constant kind in extension if different from exported one
+    if exportedInfo?.isSome then
+      modifyEnv (privateConstKindsExt.insert · name kind)
+    else
+      exportedInfo? := some info
 
   -- no environment extension changes to report after kernel checking; ensures we do not
   -- accidentally wait for this snapshot when querying extension states
   let env ← getEnv
   let async ← env.addConstAsync (reportExts := false) name kind
-    (exportedKind := exportedInfo?.map (.ofConstantInfo) |>.getD kind)
+    (exportedKind? := exportedInfo?.map (.ofConstantInfo))
   -- report preliminary constant info immediately
   async.commitConst async.asyncEnv (some info) (exportedInfo? <|> info)
   setEnv async.mainEnv
-  let cancelTk ← IO.CancelToken.new
-  let checkAct ← Core.wrapAsyncAsSnapshot (cancelTk? := cancelTk) fun _ => do
+
+  let doAddAndCommit := do
     setEnv async.asyncEnv
     try
       doAdd
     finally
       async.commitCheckEnv (← getEnv)
-  let t ← BaseIO.mapTask checkAct env.checked
-  let endRange? := (← getRef).getTailPos?.map fun pos => ⟨pos, pos⟩
-  Core.logSnapshotTask { stx? := none, reportingRange? := endRange?, task := t, cancelTk? := cancelTk }
+
+  if Elab.async.get (← getOptions) then
+    let cancelTk ← IO.CancelToken.new
+    let checkAct ← Core.wrapAsyncAsSnapshot (cancelTk? := cancelTk) fun _ => doAddAndCommit
+    let t ← BaseIO.mapTask checkAct env.checked
+    let endRange? := (← getRef).getTailPos?.map fun pos => ⟨pos, pos⟩
+    Core.logSnapshotTask { stx? := none, reportingRange? := endRange?, task := t, cancelTk? := cancelTk }
+  else
+    try
+      doAddAndCommit
+    finally
+      setEnv async.mainEnv
 where
-  addSynchronously := do
-    doAdd
-    -- make constants known to the elaborator; in the synchronous case, we can simply read them from
-    -- the kernel env
-    for n in decl.getNames do
-      let env ← getEnv
-      let some info := env.checked.get.find? n | unreachable!
-      -- do *not* report extensions in synchronous case at this point as they are usually set only
-      -- after adding the constant itself
-      let res ← env.addConstAsync (reportExts := false) n (.ofConstantInfo info)
-      res.commitConst env (info? := info)
-      res.commitCheckEnv res.asyncEnv
-      setEnv res.mainEnv
   doAdd := do
     profileitM Exception "type checking" (← getOptions) do
       withTraceNode `Kernel (fun _ => return m!"typechecking declarations {decl.getTopLevelNames}") do

src/Lean/Compiler/ConstFolding.lean

@@ -150,36 +150,8 @@ def natFoldFns : List (Name × BinFoldFn) :=
    (``Nat.ble,   foldNatBle)
 ]
 
-def getBoolLit : Expr → Option Bool
-  | Expr.const ``Bool.true _  => some true
-  | Expr.const ``Bool.false _ => some false
-  | _                         => none
-
-def foldStrictAnd (_ : Bool) (a₁ a₂ : Expr) : Option Expr :=
-  let v₁ := getBoolLit a₁
-  let v₂ := getBoolLit a₂
-  match v₁, v₂ with
-  | some true,  _ => a₂
-  | some false, _ => a₁
-  | _, some true  => a₁
-  | _, some false => a₂
-  | _, _          => none
-
-def foldStrictOr (_ : Bool) (a₁ a₂ : Expr) : Option Expr :=
-  let v₁ := getBoolLit a₁
-  let v₂ := getBoolLit a₂
-  match v₁, v₂ with
-  | some true,  _ => a₁
-  | some false, _ => a₂
-  | _, some true  => a₂
-  | _, some false => a₁
-  | _, _          => none
-
-def boolFoldFns : List (Name × BinFoldFn) :=
-  [(``strictOr, foldStrictOr), (``strictAnd, foldStrictAnd)]
-
 def binFoldFns : List (Name × BinFoldFn) :=
-  boolFoldFns ++ uintBinFoldFns ++ natFoldFns
+  uintBinFoldFns ++ natFoldFns
 
 def foldNatSucc (_ : Bool) (a : Expr) : Option Expr := do
   let n ← getNumLit a

src/Lean/Compiler/ImplementedByAttr.lean

@@ -17,17 +17,19 @@ builtin_initialize implementedByAttr : ParametricAttribute Name ← registerPara
   getParam := fun declName stx => do
     let decl ← getConstInfo declName
     let fnNameStx ← Attribute.Builtin.getIdent stx
-    let fnName ← Elab.realizeGlobalConstNoOverloadWithInfo fnNameStx
-    let fnDecl ← getConstVal fnName
-    unless decl.levelParams.length == fnDecl.levelParams.length do
-      throwError "invalid 'implemented_by' argument '{fnName}', '{fnName}' has {fnDecl.levelParams.length} universe level parameter(s), but '{declName}' has {decl.levelParams.length}"
-    let declType := decl.type
-    let fnType ← Core.instantiateTypeLevelParams fnDecl (decl.levelParams.map mkLevelParam)
-    unless declType == fnType do
-      throwError "invalid 'implemented_by' argument '{fnName}', '{fnName}' has type{indentExpr fnType}\nbut '{declName}' has type{indentExpr declType}"
-    if decl.name == fnDecl.name then
-      throwError "invalid 'implemented_by' argument '{fnName}', function cannot be implemented by itself"
-    return fnName
+    -- IR is (currently) exported always, so access to private decls is fine here.
+    withoutExporting do
+      let fnName ← Elab.realizeGlobalConstNoOverloadWithInfo fnNameStx
+      let fnDecl ← getConstVal fnName
+      unless decl.levelParams.length == fnDecl.levelParams.length do
+        throwError "invalid 'implemented_by' argument '{fnName}', '{fnName}' has {fnDecl.levelParams.length} universe level parameter(s), but '{declName}' has {decl.levelParams.length}"
+      let declType := decl.type
+      let fnType ← Core.instantiateTypeLevelParams fnDecl (decl.levelParams.map mkLevelParam)
+      unless declType == fnType do
+        throwError "invalid 'implemented_by' argument '{fnName}', '{fnName}' has type{indentExpr fnType}\nbut '{declName}' has type{indentExpr declType}"
+      if decl.name == fnDecl.name then
+        throwError "invalid 'implemented_by' argument '{fnName}', function cannot be implemented by itself"
+      return fnName
 }
 
 @[export lean_get_implemented_by]

src/Lean/Compiler/LCNF/ExtractClosed.lean

@@ -148,8 +148,13 @@ partial def Decl.extractClosed (decl : Decl) (sccDecls : Array Decl) : CompilerM
 def extractClosed : Pass where
   phase := .mono
   name := `extractClosed
-  run := fun decls =>
-    decls.foldlM (init := #[]) fun newDecls decl => return newDecls ++ (← decl.extractClosed decls)
+  run := fun decls => do
+    -- Reuse the option from the old compiler for now.
+    if (← getOptions).getBool `compiler.extract_closed true then
+      decls.foldlM (init := #[]) fun newDecls decl =>
+        return newDecls ++ (← decl.extractClosed decls)
+    else
+      return decls
 
 builtin_initialize registerTraceClass `Compiler.extractClosed (inherited := true)
 

src/Lean/Compiler/LCNF/MonoTypes.lean

@@ -46,6 +46,8 @@ def hasTrivialStructure? (declName : Name) : CoreM (Option TrivialStructureInfo)
   let .inductInfo info ← getConstInfo declName | return none
   if info.isUnsafe || info.isRec then return none
   let [ctorName] := info.ctors | return none
+  let ctorType ← getOtherDeclBaseType ctorName []
+  if ctorType.isErased then return none
   let mask ← getRelevantCtorFields ctorName
   let mut result := none
   for h : i in [:mask.size] do

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

@@ -308,14 +308,33 @@ def higherOrderLiteralFolders : List (Name × Folder) := [
 def Folder.mulShift [Literal α] [BEq α] (shiftLeft : Name) (pow2 : α → α) (log2 : α → α) : Folder :=
   Folder.first #[Folder.mulLhsShift shiftLeft pow2 log2, Folder.mulRhsShift shiftLeft pow2 log2]
 
+-- TODO: add option for controlling the limit
+def natPowThreshold := 256
+
+def foldNatPow (args : Array Arg) : FolderM (Option LetValue) := do
+  let #[.fvar fvarId₁, .fvar fvarId₂] := args | return none
+  let some value₁ ← getNatLit fvarId₁ | return none
+  let some value₂ ← getNatLit fvarId₂ | return none
+  if value₂ < natPowThreshold then
+    return .some (.lit (.nat (value₁ ^ value₂)))
+  else
+    return none
+
 /--
 Folder for ofNat operations on fixed-sized integer types.
 -/
-def Folder.ofNat (f : Nat → LitValue) (args : Array Arg): FolderM (Option LetValue) := do
+def Folder.ofNat (f : Nat → LitValue) (args : Array Arg) : FolderM (Option LetValue) := do
   let #[.fvar fvarId] := args | return none
   let some value ← getNatLit fvarId | return none
   return some (.lit (f value))
 
+def Folder.toNat (args : Array Arg) : FolderM (Option LetValue) := do
+  let #[.fvar fvarId] := args | return none
+  let some (.lit lit) ← findLetValue? fvarId | return none
+  match lit with
+  | .uint8 v | .uint16 v | .uint32 v | .uint64 v | .usize v => return some (.lit (.nat v.toNat))
+  | .nat _ | .str _ => return none
+
 /--
 All arithmetic folders.
 -/
@@ -331,7 +350,8 @@ def arithmeticFolders : List (Name × Folder) := [
   (``UInt16.sub,  Folder.first #[Folder.mkBinary UInt16.sub, Folder.leftRightNeutral (0 : UInt16)]),
   (``UInt32.sub,  Folder.first #[Folder.mkBinary UInt32.sub, Folder.leftRightNeutral (0 : UInt32)]),
   (``UInt64.sub,  Folder.first #[Folder.mkBinary UInt64.sub, Folder.leftRightNeutral (0 : UInt64)]),
-  (``Nat.mul,    Folder.first #[Folder.mkBinary Nat.mul, Folder.leftRightNeutral 1, Folder.leftRightAnnihilator 0 0, Folder.mulShift ``Nat.shiftLeft (Nat.pow 2) Nat.log2]),
+  -- We don't convert Nat multiplication by a power of 2 into a left shift, because the fast path
+  -- for multiplication isn't any slower than a fast path for left shift that checks for overflow.
   (``UInt8.mul,  Folder.first #[Folder.mkBinary UInt8.mul, Folder.leftRightNeutral (1 : UInt8), Folder.leftRightAnnihilator (0 : UInt8) 0, Folder.mulShift ``UInt8.shiftLeft (UInt8.shiftLeft 1 ·) UInt8.log2]),
   (``UInt16.mul,  Folder.first #[Folder.mkBinary UInt16.mul, Folder.leftRightNeutral (1 : UInt16), Folder.leftRightAnnihilator (0 : UInt16) 0, Folder.mulShift ``UInt16.shiftLeft (UInt16.shiftLeft 1 ·) UInt16.log2]),
   (``UInt32.mul,  Folder.first #[Folder.mkBinary UInt32.mul, Folder.leftRightNeutral (1 : UInt32), Folder.leftRightAnnihilator (0 : UInt32) 0, Folder.mulShift ``UInt32.shiftLeft (UInt32.shiftLeft 1 ·) UInt32.log2]),
@@ -340,7 +360,9 @@ def arithmeticFolders : List (Name × Folder) := [
   (``UInt8.div,  Folder.first #[Folder.mkBinary UInt8.div, Folder.rightNeutral (1 : UInt8), Folder.divShift ``UInt8.shiftRight (UInt8.shiftLeft 1 ·) UInt8.log2]),
   (``UInt16.div,  Folder.first #[Folder.mkBinary UInt16.div, Folder.rightNeutral (1 : UInt16), Folder.divShift ``UInt16.shiftRight (UInt16.shiftLeft 1 ·) UInt16.log2]),
   (``UInt32.div,  Folder.first #[Folder.mkBinary UInt32.div, Folder.rightNeutral (1 : UInt32), Folder.divShift ``UInt32.shiftRight (UInt32.shiftLeft 1 ·) UInt32.log2]),
-  (``UInt64.div,  Folder.first #[Folder.mkBinary UInt64.div, Folder.rightNeutral (1 : UInt64), Folder.divShift ``UInt64.shiftRight (UInt64.shiftLeft 1 ·) UInt64.log2])
+  (``UInt64.div,  Folder.first #[Folder.mkBinary UInt64.div, Folder.rightNeutral (1 : UInt64), Folder.divShift ``UInt64.shiftRight (UInt64.shiftLeft 1 ·) UInt64.log2]),
+  (``Nat.pow, foldNatPow),
+  (``Nat.nextPowerOfTwo, Folder.mkUnary Nat.nextPowerOfTwo),
 ]
 
 def relationFolders : List (Name × Folder) := [
@@ -369,6 +391,11 @@ def conversionFolders : List (Name × Folder) := [
   (``UInt32.ofNat, Folder.ofNat (fun v => .uint32 (UInt32.ofNat v))),
   (``UInt64.ofNat, Folder.ofNat (fun v => .uint64 (UInt64.ofNat v))),
   (``USize.ofNat, Folder.ofNat (fun v => .usize (UInt64.ofNat v))),
+  (``UInt8.toNat, Folder.toNat),
+  (``UInt16.toNat, Folder.toNat),
+  (``UInt32.toNat, Folder.toNat),
+  (``UInt64.toNat, Folder.toNat),
+  (``USize.toNat, Folder.toNat),
 ]
 
 /--

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

@@ -32,10 +32,13 @@ def simpAppApp? (e : LetValue) : OptionT SimpM LetValue := do
   let some decl ← findLetDecl? g | failure
   match decl.value with
   | .fvar f args' =>
-    /- If `args'` is empty then `g` is an alias that is going to be eliminated by `elimVar?` -/
-    guard (!args'.isEmpty)
+    /- If `args` is empty then `g` is an alias that is going to be eliminated by `elimVar?` -/
+    guard (!args.isEmpty)
     return .fvar f (args' ++ args)
-  | .const declName us args' => return .const declName us (args' ++ args)
+  | .const declName us args' =>
+    /- If `args` is empty then `g` is an alias that is going to be eliminated by `elimVar?` -/
+    guard (!args.isEmpty)
+    return .const declName us (args' ++ args)
   | .erased => return .erased
   | .proj .. | .lit .. => failure
 

src/Lean/Compiler/LCNF/Specialize.lean

@@ -268,8 +268,12 @@ def getRemainingArgs (paramsInfo : Array SpecParamInfo) (args : Array Arg) : Arr
       result := result.push arg
   return result ++ args[paramsInfo.size:]
 
-def paramsToVarSet (params : Array Param) : FVarIdSet :=
-  params.foldl (fun r p => r.insert p.fvarId) {}
+def paramsToGroundVars (params : Array Param) : CompilerM FVarIdSet :=
+  params.foldlM (init := {}) fun r p => do
+    if isTypeFormerType p.type || (← isArrowClass? p.type).isSome then
+      return r.insert p.fvarId
+    else
+      return r
 
 mutual
   /--
@@ -305,7 +309,7 @@ mutual
       specDecl.saveBase
       let specDecl ← specDecl.simp {}
       let specDecl ← specDecl.simp { etaPoly := true, inlinePartial := true, implementedBy := true }
-      let ground := paramsToVarSet specDecl.params
+      let ground ← paramsToGroundVars specDecl.params
       let value ← withReader (fun _ => { declName := specDecl.name, ground }) do
          withParams specDecl.params <| specDecl.value.mapCodeM visitCode
       let specDecl := { specDecl with value }
@@ -352,7 +356,7 @@ def main (decl : Decl) : SpecializeM Decl := do
 end Specialize
 
 partial def Decl.specialize (decl : Decl) : CompilerM (Array Decl) := do
-  let ground := Specialize.paramsToVarSet decl.params
+  let ground ← Specialize.paramsToGroundVars decl.params
   let (decl, s) ← Specialize.main decl |>.run { declName := decl.name, ground } |>.run {}
   return s.decls.push decl
 

src/Lean/Compiler/LCNF/ToLCNF.lean

@@ -704,7 +704,7 @@ where
         visitQuotLift e
       else if declName == ``Quot.mk then
         visitCtor 3 e
-      else if declName == ``Eq.casesOn || declName == ``Eq.rec || declName == ``Eq.ndrec then
+      else if declName == ``Eq.casesOn || declName == ``Eq.rec || declName == ``Eq.recOn || declName == ``Eq.ndrec then
         visitEqRec e
       else if declName == ``HEq.casesOn || declName == ``HEq.rec || declName == ``HEq.ndrec then
         visitHEqRec e

src/Lean/Compiler/LCNF/ToMono.lean

@@ -12,14 +12,14 @@ import Lean.Compiler.NoncomputableAttr
 namespace Lean.Compiler.LCNF
 
 structure ToMonoM.State where
-  typeParams : FVarIdSet := {}
-  noncomputableVars : FVarIdMap Name := {}
+  typeParams : FVarIdHashSet := {}
+  noncomputableVars : Std.HashMap FVarId Name := {}
 
 abbrev ToMonoM := StateRefT ToMonoM.State CompilerM
 
 def Param.toMono (param : Param) : ToMonoM Param := do
   if isTypeFormerType param.type then
-    modify fun { typeParams, .. } => { typeParams := typeParams.insert param.fvarId }
+    modify fun s => { s with typeParams := s.typeParams.insert param.fvarId }
   param.update (← toMonoType param.type)
 
 def isTrivialConstructorApp? (declName : Name) (args : Array Arg) : ToMonoM (Option LetValue) := do
@@ -28,8 +28,7 @@ def isTrivialConstructorApp? (declName : Name) (args : Array Arg) : ToMonoM (Opt
   return args[ctorInfo.numParams + info.fieldIdx]!.toLetValue
 
 def checkFVarUse (fvarId : FVarId) : ToMonoM Unit := do
-  if (← get).noncomputableVars.contains fvarId then
-    let declName := (← get).noncomputableVars.find! fvarId
+  if let some declName := (← get).noncomputableVars.get? fvarId then
     throwError f!"failed to compile definition, consider marking it as 'noncomputable' because it depends on '{declName}', which is 'noncomputable'"
 
 def argToMono (arg : Arg) : ToMonoM Arg := do
@@ -78,14 +77,15 @@ partial def LetValue.toMono (e : LetValue) (fvarId : FVarId) : ToMonoM LetValue
     else
       checkFVarUse fvarId
       return .fvar fvarId (← args.mapM argToMono)
-  | .proj structName fieldIdx fvarId =>
-    if (← get).typeParams.contains fvarId then
+  | .proj structName fieldIdx baseFVar =>
+    if (← get).typeParams.contains baseFVar then
       return .erased
     else
-      checkFVarUse fvarId
+      if let some declName := (← get).noncomputableVars.get? baseFVar then
+        modify fun s => { s with noncomputableVars := s.noncomputableVars.insert fvarId declName }
       if let some info ← hasTrivialStructure? structName then
         if info.fieldIdx == fieldIdx then
-          return .fvar fvarId #[]
+          return .fvar baseFVar #[]
         else
           return .erased
       else

src/Lean/CoreM.lean

@@ -102,14 +102,23 @@ partial def mkUniqueName (env : Environment) (g : DeclNameGenerator) («infix»
   let «infix» := if g.namePrefix.hasMacroScopes && infix.hasMacroScopes then infix.eraseMacroScopes else «infix»
   let base := g.namePrefix ++ «infix»
   let mut g := g
+  while isConflict (curr g base) do
+    g := g.next
+  return (curr g base, g)
+where
+  -- Check whether the name conflicts with an existing one. Conflicts ignore privacy.
   -- NOTE: We only check the current branch and rely on the documented invariant instead because we
   -- do not want to block here and because it would not solve the issue for completely separated
   -- threads of elaboration such as in Aesop's backtracking search.
-  while env.containsOnBranch (curr g base) do
-    g := g.next
-  return (curr g base, g)
-where curr (g : DeclNameGenerator) (base : Name) : Name :=
-  g.idxs.foldr (fun i n => n.appendIndexAfter i) base
+  isConflict (n : Name) : Bool :=
+    (env.setExporting false).containsOnBranch n ||
+    isPrivateName n && (env.setExporting false).containsOnBranch (privateToUserName n) ||
+    !isPrivateName n && (env.setExporting false).containsOnBranch (mkPrivateName env n)
+  curr (g : DeclNameGenerator) (base : Name) : Name := Id.run do
+    let mut n := g.idxs.foldr (fun i n => n.appendIndexAfter i) base
+    if env.header.isModule && !env.isExporting && !isPrivateName n then
+      n := mkPrivateName env n
+    return n
 
 def mkChild (g : DeclNameGenerator) : DeclNameGenerator × DeclNameGenerator :=
   ({ g with parentIdxs := g.idx :: g.parentIdxs, idx := 1 },
@@ -709,8 +718,9 @@ where doCompile := do
     return
   let opts ← getOptions
   if compiler.enableNew.get opts then
-    try compileDeclsNew decls catch e =>
-      if logErrors then throw e else return ()
+    withoutExporting
+      try compileDeclsNew decls catch e =>
+        if logErrors then throw e else return ()
   else
     let res ← withTraceNode `compiler (fun _ => return m!"compiling old: {decls}") do
       return compileDeclsOld (← getEnv) opts decls

src/Lean/Data/Lsp/Capabilities.lean

@@ -100,6 +100,7 @@ structure ServerCapabilities where
   semanticTokensProvider?   : Option SemanticTokensOptions   := none
   codeActionProvider?       : Option CodeActionOptions       := none
   inlayHintProvider?        : Option InlayHintOptions        := none
+  signatureHelpProvider?    : Option SignatureHelpOptions    := none
   deriving ToJson, FromJson
 
 end Lsp

src/Lean/Data/Lsp/LanguageFeatures.lean

@@ -521,5 +521,73 @@ structure InlayHintOptions extends WorkDoneProgressOptions where
   resolveProvider? : Option Bool := none
   deriving FromJson, ToJson
 
+inductive ParameterInformationLabel
+  | name (name : String)
+  | range (startUtf16Offset endUtf16Offset : Nat)
+
+instance : FromJson ParameterInformationLabel where
+  fromJson?
+    | .str name => .ok <| .name name
+    | .arr #[startUtf16OffsetJson, endUtf16OffsetJson] => do
+      return .range (← fromJson? startUtf16OffsetJson) (← fromJson? endUtf16OffsetJson)
+    | _ => .error "unexpected JSON for `ParameterInformationLabel`"
+
+instance : ToJson ParameterInformationLabel where
+  toJson
+    | .name name => .str name
+    | .range startUtf16Offset endUtf16Offset => .arr #[startUtf16Offset, endUtf16Offset]
+
+structure ParameterInformation where
+  label : ParameterInformationLabel
+  documentation? : Option MarkupContent := none
+  deriving FromJson, ToJson
+
+structure SignatureInformation where
+  label : String
+  documentation? : Option MarkupContent := none
+  parameters? : Option (Array ParameterInformation) := none
+  activeParameter? : Option Nat := none
+  deriving FromJson, ToJson
+
+structure SignatureHelp where
+  signatures : Array SignatureInformation
+  activeSignature? : Option Nat := none
+  activeParameter? : Option Nat := none
+  deriving FromJson, ToJson
+
+inductive SignatureHelpTriggerKind where
+  | invoked
+  | triggerCharacter
+  | contentChange
+
+instance : FromJson SignatureHelpTriggerKind where
+  fromJson?
+    | (1 : Nat) => .ok .invoked
+    | (2 : Nat) => .ok .triggerCharacter
+    | (3 : Nat) => .ok .contentChange
+    | _ => .error "Unexpected JSON in `SignatureHelpTriggerKind`"
+
+instance : ToJson SignatureHelpTriggerKind where
+  toJson
+    | .invoked => 1
+    | .triggerCharacter => 2
+    | .contentChange => 3
+
+structure SignatureHelpContext where
+  triggerKind : SignatureHelpTriggerKind
+  triggerCharacter? : Option String := none
+  isRetrigger : Bool
+  activeSignatureHelp? : Option SignatureHelp := none
+  deriving FromJson, ToJson
+
+structure SignatureHelpParams extends TextDocumentPositionParams, WorkDoneProgressParams where
+  context? : Option SignatureHelpContext := none
+  deriving FromJson, ToJson
+
+structure SignatureHelpOptions extends WorkDoneProgressOptions where
+  triggerCharacters? : Option (Array String) := none
+  retriggerCharacters? : Option (Array String) := none
+  deriving FromJson, ToJson
+
 end Lsp
 end Lean

src/Lean/Elab/App.lean

@@ -1191,6 +1191,12 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
       if (← getEnv).contains fullName then
         return LValResolution.const `Function `Function fullName
     | _ => pure ()
+  else if eType.getAppFn.isMVar then
+    let field :=
+      match lval with
+      |  .fieldName _ fieldName _ _ => toString fieldName
+      | .fieldIdx _ i => toString i
+    throwError "Invalid field notation: type of{indentExpr e}\nis not known; cannot resolve field '{field}'"
   match eType.getAppFn.constName?, lval with
   | some structName, LVal.fieldIdx _ idx =>
     if idx == 0 then
@@ -1506,15 +1512,19 @@ where
     let resultTypeFn := resultType.cleanupAnnotations.getAppFn
     try
       tryPostponeIfMVar resultTypeFn
-      let .const declName .. := resultTypeFn.cleanupAnnotations
-        | throwError "invalid dotted identifier notation, expected type is not of the form (... → C ...) where C is a constant{indentExpr expectedType}"
-      let idNew := declName ++ id.getId.eraseMacroScopes
-      if (← getEnv).contains idNew then
-        mkConst idNew
-      else if let some (fvar, []) ← resolveLocalName idNew then
-        return fvar
-      else
-        throwUnknownIdentifierAt id m!"invalid dotted identifier notation, unknown identifier `{idNew}` from expected type{indentExpr expectedType}"
+      match resultTypeFn.cleanupAnnotations with
+      | .const declName .. =>
+        let idNew := declName ++ id.getId.eraseMacroScopes
+        if (← getEnv).contains idNew then
+          mkConst idNew
+        else if let some (fvar, []) ← resolveLocalName idNew then
+          return fvar
+        else
+          throwUnknownIdentifierAt id m!"invalid dotted identifier notation, unknown identifier `{idNew}` from expected type{indentExpr expectedType}"
+      | .sort .. =>
+        throwError "Invalid dotted identifier notation: not supported on type{indentExpr resultTypeFn}"
+      | _ =>
+        throwError "invalid dotted identifier notation, expected type is not of the form (... → C ...) where C is a constant{indentExpr expectedType}"
     catch
       | ex@(.error ..) =>
         match (← unfoldDefinition? resultType) with

src/Lean/Elab/AuxDef.lean

@@ -27,7 +27,8 @@ def elabAuxDef : CommandElab
     -- We use a new generator here because we want more control over the name; the default would
     -- create a private name that then breaks the macro below. We assume that `aux_def` is not used
     -- with the same arguments in parallel contexts.
-    let (id, _) := { namePrefix := ns : DeclNameGenerator }.mkUniqueName (← getEnv) («infix» := Name.mkSimple id)
+    let env := (← getEnv).setExporting true
+    let (id, _) := { namePrefix := ns : DeclNameGenerator }.mkUniqueName env («infix» := Name.mkSimple id)
     let id := id.replacePrefix ns Name.anonymous -- TODO: replace with def _root_.id
     elabCommand <|
       ← `($[$doc?:docComment]? $[$attrs?:attributes]?

src/Lean/Elab/BuiltinCommand.lean

@@ -546,4 +546,9 @@ where
       elabCommand cmd
   | _ => throwUnsupportedSyntax
 
+@[builtin_command_elab Parser.Command.dumpAsyncEnvState] def elabDumpAsyncEnvState : CommandElab :=
+  fun _ => do
+    let env ← getEnv
+    IO.eprintln (← env.dbgFormatAsyncState)
+
 end Lean.Elab.Command

src/Lean/Elab/BuiltinEvalCommand.lean

@@ -208,7 +208,7 @@ unsafe def elabEvalCoreUnsafe (bang : Bool) (tk term : Syntax) (expectedType? :
       -- `evalConst` may emit IO, but this is collected by `withIsolatedStreams` below.
       let r ← toMessageData <$> evalConst t declName
       return { eval := pure r, printVal := some (← inferType e) }
-  let (output, exOrRes) ← IO.FS.withIsolatedStreams do
+  let (output, exOrRes) ← IO.FS.withIsolatedStreams (isolateStderr := Core.stderrAsMessages.get (← getOptions)) do
     try
       -- Generate an action without executing it. We use `withoutModifyingEnv` to ensure
       -- we don't pollute the environment with auxiliary declarations.

src/Lean/Elab/BuiltinTerm.lean

@@ -155,7 +155,10 @@ private def getMVarFromUserName (ident : Syntax) : MetaM Expr := do
 @[builtin_term_elab byTactic] def elabByTactic : TermElab := fun stx expectedType? => do
   match expectedType? with
   | some expectedType =>
-    mkTacticMVar expectedType stx .term
+    -- `by` switches from an exported to a private context, so we must disallow unassigned
+    -- metavariables in the goal in this case as they could otherwise leak private data back into
+    -- the exported context.
+    mkTacticMVar expectedType stx .term (delayOnMVars := (← getEnv).isExporting)
   | none =>
     tryPostpone
     throwError ("invalid 'by' tactic, expected type has not been provided")
@@ -372,7 +375,10 @@ private opaque evalFilePath (stx : Syntax) : TermElabM System.FilePath
       let name ← mkAuxDeclName `_private
       withoutExporting do
         let e ← elabTerm e expectedType?
-        mkAuxDefinitionFor name e
+        -- Inline as changing visibility should not affect run time.
+        -- Eventually we would like to be more conscious about inlining of instance fields,
+        -- irrespective of `private` use.
+        mkAuxDefinitionFor name e <* setInlineAttribute name
     else
       elabTerm e expectedType?
   | _ => throwUnsupportedSyntax

src/Lean/Elab/DeclModifiers.lean

@@ -28,7 +28,7 @@ def checkNotAlreadyDeclared {m} [Monad m] [MonadEnv m] [MonadError m] [MonadInfo
     match privateToUserName? declName with
     | none          => throwError "'{.ofConstName declName true}' has already been declared"
     | some declName => throwError "private declaration '{.ofConstName declName true}' has already been declared"
-  if isReservedName env declName then
+  if isReservedName env (privateToUserName declName) || isReservedName env (mkPrivateName (← getEnv) declName) then
     throwError "'{declName}' is a reserved name"
   if env.contains (mkPrivateName env declName) then
     addInfo (mkPrivateName env declName)

src/Lean/Elab/Deriving/DecEq.lean

@@ -97,7 +97,7 @@ def mkAuxFunction (ctx : Context) (auxFunName : Name) (indVal : InductiveVal): T
     then `(Parser.Termination.suffix|termination_by structural $target₁)
     else `(Parser.Termination.suffix|)
   let type    ← `(Decidable ($target₁ = $target₂))
-  `(private def $(mkIdent auxFunName):ident $binders:bracketedBinder* : $type:term := $body:term
+  `(def $(mkIdent auxFunName):ident $binders:bracketedBinder* : $type:term := $body:term
     $termSuffix:suffix)
 
 def mkAuxFunctions (ctx : Context) : TermElabM (TSyntax `command) := do

src/Lean/Elab/Deriving/Hashable.lean

@@ -66,9 +66,9 @@ def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Command := do
   let binders    := header.binders
   if ctx.usePartial then
     -- TODO(Dany): Get rid of this code branch altogether once we have well-founded recursion
-    `(private partial def $(mkIdent auxFunName):ident $binders:bracketedBinder* : UInt64 := $body:term)
+    `(partial def $(mkIdent auxFunName):ident $binders:bracketedBinder* : UInt64 := $body:term)
   else
-    `(private def $(mkIdent auxFunName):ident $binders:bracketedBinder* : UInt64 := $body:term)
+    `(def $(mkIdent auxFunName):ident $binders:bracketedBinder* : UInt64 := $body:term)
 
 def mkHashFuncs (ctx : Context) : TermElabM Syntax := do
   let mut auxDefs := #[]

src/Lean/Elab/Deriving/Ord.lean

@@ -72,9 +72,9 @@ def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Command := do
     body ← mkLet letDecls body
   let binders    := header.binders
   if ctx.usePartial || indVal.isRec then
-    `(private partial def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Ordering := $body:term)
+    `(partial def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Ordering := $body:term)
   else
-    `(private def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Ordering := $body:term)
+    `(def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Ordering := $body:term)
 
 def mkMutualBlock (ctx : Context) : TermElabM Syntax := do
   let mut auxDefs := #[]

src/Lean/Elab/Deriving/Repr.lean

@@ -97,9 +97,9 @@ def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Command := do
     body ← mkLet letDecls body
   let binders    := header.binders
   if ctx.usePartial then
-    `(private partial def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Format := $body:term)
+    `(partial def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Format := $body:term)
   else
-    `(private def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Format := $body:term)
+    `(def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Format := $body:term)
 
 def mkMutualBlock (ctx : Context) : TermElabM Syntax := do
   let mut auxDefs := #[]

src/Lean/Elab/Do.lean

@@ -221,7 +221,7 @@ inductive Code where
   /-- Recall that an if-then-else may declare a variable using `optIdent` for the branches `thenBranch` and `elseBranch`. We store the variable name at `var?`. -/
   | ite          (ref : Syntax) (h? : Option Var) (optIdent : Syntax) (cond : Syntax) (thenBranch : Code) (elseBranch : Code)
   | match        (ref : Syntax) (gen : Syntax) (discrs : Syntax) (optMotive : Syntax) (alts : Array (Alt Code))
-  | matchExpr    (ref : Syntax) (meta : Bool) (discr : Syntax) (alts : Array (AltExpr Code)) (elseBranch : Code)
+  | matchExpr    (ref : Syntax) («meta» : Bool) (discr : Syntax) (alts : Array (AltExpr Code)) (elseBranch : Code)
   | jmp          (ref : Syntax) (jpName : Name) (args : Array Syntax)
   deriving Inhabited
 
@@ -268,8 +268,8 @@ partial def CodeBlocl.toMessageData (codeBlock : CodeBlock) : MessageData :=
     | .match _ _ ds _ alts   =>
       m!"match {ds} with"
       ++ alts.foldl (init := m!"") fun acc alt => acc ++ m!"\n| {alt.patterns} => {loop alt.rhs}"
-    | .matchExpr _ meta d alts elseCode =>
-      let r := m!"match_expr {if meta then "" else "(meta := false)"} {d} with"
+    | .matchExpr _ «meta» d alts elseCode =>
+      let r := m!"match_expr {if «meta» then "" else "(meta := false)"} {d} with"
       let r := r ++ alts.foldl (init := m!"") fun acc alt =>
             let acc := acc ++ m!"\n| {if let some var := alt.var? then m!"{var}@" else ""}"
             let acc := acc ++ m!"{alt.funName}"
@@ -341,10 +341,10 @@ partial def convertTerminalActionIntoJmp (code : Code) (jp : Name) (xs : Array V
       return Code.jmp ref jp jmpArgs
     | .match ref g ds t alts =>
       return .match ref g ds t (← alts.mapM fun alt => do pure { alt with rhs := (← loop alt.rhs) })
-    | .matchExpr ref meta d alts e => do
+    | .matchExpr ref «meta» d alts e => do
       let alts ← alts.mapM fun alt => do pure { alt with rhs := (← loop alt.rhs) }
       let e ← loop e
-      return .matchExpr ref meta d alts e
+      return .matchExpr ref «meta» d alts e
     | c => return c
   loop code
 
@@ -430,10 +430,10 @@ partial def pullExitPointsAux (rs : VarSet) (c : Code) : StateRefT (Array JPDecl
   | .match ref g ds t alts =>
     let alts ← alts.mapM fun alt => do pure { alt with rhs := (← pullExitPointsAux (eraseVars rs alt.vars) alt.rhs) }
     return .match ref g ds t alts
-  | .matchExpr ref meta d alts e =>
+  | .matchExpr ref «meta» d alts e =>
     let alts ← alts.mapM fun alt => do pure { alt with rhs := (← pullExitPointsAux (eraseVars rs alt.vars) alt.rhs) }
     let e ← pullExitPointsAux rs e
-    return .matchExpr ref meta d alts e
+    return .matchExpr ref «meta» d alts e
 
 /--
 Auxiliary operation for adding new variables to the collection of updated variables in a CodeBlock.
@@ -502,14 +502,14 @@ partial def extendUpdatedVarsAux (c : Code) (ws : VarSet) : TermElabM Code :=
         pullExitPoints c
       else
         return .match ref g ds t (← alts.mapM fun alt => do pure { alt with rhs := (← update alt.rhs) })
-    | .matchExpr ref meta d alts e =>
+    | .matchExpr ref «meta» d alts e =>
       if alts.any fun alt => alt.vars.any fun x => ws.contains x.getId then
         -- If a pattern variable is shadowing a variable in ws, we `pullExitPoints`
         pullExitPoints c
       else
         let alts ← alts.mapM fun alt => do pure { alt with rhs := (← update alt.rhs) }
         let e ← update e
-        return .matchExpr ref meta d alts e
+        return .matchExpr ref «meta» d alts e
     | .ite ref none o c t e => return .ite ref none o c (← update t) (← update e)
     | .ite ref (some h) o cond t e =>
       if ws.contains h.getId then
@@ -623,7 +623,7 @@ def mkMatch (ref : Syntax) (genParam : Syntax) (discrs : Syntax) (optMotive : Sy
     return { ref := alt.ref, vars := alt.vars, patterns := alt.patterns, rhs := rhs.code : Alt Code }
   return { code := .match ref genParam discrs optMotive alts, uvars := ws }
 
-def mkMatchExpr (ref : Syntax) (meta : Bool) (discr : Syntax) (alts : Array (AltExpr CodeBlock)) (elseBranch : CodeBlock) : TermElabM CodeBlock := do
+def mkMatchExpr (ref : Syntax) («meta» : Bool) (discr : Syntax) (alts : Array (AltExpr CodeBlock)) (elseBranch : CodeBlock) : TermElabM CodeBlock := do
   -- nary version of homogenize
   let ws := alts.foldl (union · ·.rhs.uvars) {}
   let ws := union ws elseBranch.uvars
@@ -631,7 +631,7 @@ def mkMatchExpr (ref : Syntax) (meta : Bool) (discr : Syntax) (alts : Array (Alt
     let rhs ← extendUpdatedVars alt.rhs ws
     return { alt with rhs := rhs.code : AltExpr Code }
   let elseBranch ← extendUpdatedVars elseBranch ws
-  return { code := .matchExpr ref meta discr alts elseBranch.code, uvars := ws }
+  return { code := .matchExpr ref «meta» discr alts elseBranch.code, uvars := ws }
 
 /-- Return a code block that executes `terminal` and then `k` with the value produced by `terminal`.
    This method assumes `terminal` is a terminal -/
@@ -1148,7 +1148,7 @@ where
         termAlts := termAlts.push termAlt
       let termMatchAlts := mkNode ``Parser.Term.matchAlts #[mkNullNode termAlts]
       return mkNode ``Parser.Term.«match» #[mkAtomFrom ref "match", genParam, optMotive, discrs, mkAtomFrom ref "with", termMatchAlts]
-    | .matchExpr ref meta d alts elseBranch => withFreshMacroScope do
+    | .matchExpr ref «meta» d alts elseBranch => withFreshMacroScope do
       let d' ← `(discr)
       let mut termAlts := #[]
       for alt in alts do
@@ -1160,7 +1160,7 @@ where
       let elseBranch := mkNode ``Parser.Term.matchExprElseAlt #[mkAtomFrom ref "|", mkHole ref, mkAtomFrom ref "=>", (← toTerm elseBranch)]
       let termMatchExprAlts := mkNode ``Parser.Term.matchExprAlts #[mkNullNode termAlts, elseBranch]
       let body := mkNode ``Parser.Term.matchExpr #[mkAtomFrom ref "match_expr", d', mkAtomFrom ref "with", termMatchExprAlts]
-      if meta then
+      if «meta» then
         `(Bind.bind (instantiateMVarsIfMVarApp $d) fun discr => $body)
       else
         `(let discr := $d; $body)
@@ -1625,7 +1625,7 @@ mutual
   /-- Generate `CodeBlock` for `doMatchExpr; doElems` -/
   partial def doMatchExprToCode (doMatchExpr : Syntax) (doElems: List Syntax) : M CodeBlock := do
     let ref       := doMatchExpr
-    let meta      := doMatchExpr[1].isNone
+    let «meta»    := doMatchExpr[1].isNone
     let discr     := doMatchExpr[2]
     let alts      := doMatchExpr[4][0].getArgs -- Array of `doMatchExprAlt`
     let alts ← alts.mapM fun alt => do
@@ -1637,7 +1637,7 @@ mutual
       let rhs ← doSeqToCode (getDoSeqElems rhs)
       pure { ref, var?, funName, pvars, rhs }
     let elseBranch ← doSeqToCode (getDoSeqElems doMatchExpr[4][1][3])
-    let matchCode ← mkMatchExpr ref meta discr alts elseBranch
+    let matchCode ← mkMatchExpr ref «meta» discr alts elseBranch
     concatWith matchCode doElems
 
   /--

src/Lean/Elab/GuardMsgs.lean

@@ -17,7 +17,7 @@ See the docstring on the `#guard_msgs` command.
 open Lean Parser.Tactic Elab Command
 
 register_builtin_option guard_msgs.diff : Bool := {
-  defValue := false
+  defValue := true
   descr := "When true, show a diff between expected and actual messages if they don't match. "
 }
 

src/Lean/Elab/Import.lean

@@ -22,8 +22,9 @@ def HeaderSyntax.imports : HeaderSyntax → Array Import
   | `(Parser.Module.header| $[module%$moduleTk]? $[prelude%$preludeTk]? $importsStx*) =>
     let imports := if preludeTk.isNone then #[{ module := `Init : Import }] else #[]
     imports ++ importsStx.map fun
-      | `(Parser.Module.import| $[private%$privateTk]? import $[all%$allTk]? $n) =>
-        { module := n.getId, importAll := allTk.isSome, isExported := privateTk.isNone }
+      | `(Parser.Module.import| $[private%$privateTk]? $[meta%$metaTk]? import $[all%$allTk]? $n) =>
+        { module := n.getId, importAll := allTk.isSome, isExported := privateTk.isNone
+          isMeta := metaTk.isSome }
       | _ => unreachable!
   | _ => unreachable!
 

src/Lean/Elab/InfoTree/Main.lean

@@ -72,7 +72,7 @@ def CompletionInfo.lctx : CompletionInfo → LocalContext
   | _                   => .empty
 
 def CustomInfo.format : CustomInfo → Format
-  | i => f!"CustomInfo({i.value.typeName})"
+  | i => f!"[CustomInfo({i.value.typeName})]"
 
 instance : ToFormat CustomInfo := ⟨CustomInfo.format⟩
 
@@ -105,6 +105,9 @@ def InfoState.substituteLazy (s : InfoState) : Task InfoState :=
 
 /-- Embeds a `CoreM` action in `IO` by supplying the information stored in `info`. -/
 def ContextInfo.runCoreM (info : ContextInfo) (x : CoreM α) : IO α := do
+  -- We assume that this function is used only outside elaboration, mostly in the language server,
+  -- and so we can and should provide access to information regardless whether it is exported.
+  let env := info.env.setExporting false
   /-
     We must execute `x` using the `ngen` stored in `info`. Otherwise, we may create `MVarId`s and `FVarId`s that
     have been used in `lctx` and `info.mctx`.
@@ -113,7 +116,7 @@ def ContextInfo.runCoreM (info : ContextInfo) (x : CoreM α) : IO α := do
     (withOptions (fun _ => info.options) x).toIO
       { currNamespace := info.currNamespace, openDecls := info.openDecls
         fileName := "<InfoTree>", fileMap := default }
-      { env := info.env, ngen := info.ngen }
+      { env, ngen := info.ngen }
 
 def ContextInfo.runMetaM (info : ContextInfo) (lctx : LocalContext) (x : MetaM α) : IO α := do
   (·.1) <$> info.runCoreM (x.run { lctx := lctx } { mctx := info.mctx })
@@ -152,26 +155,26 @@ def TermInfo.format (ctx : ContextInfo) (info : TermInfo) : IO Format := do
         Meta.ppExpr (← Meta.inferType info.expr)
       catch _ =>
         pure "<failed-to-infer-type>"
-    return f!"{← Meta.ppExpr info.expr} {if info.isBinder then "(isBinder := true) " else ""}: {ty} @ {formatElabInfo ctx info.toElabInfo}"
+    return f!"[Term] {← Meta.ppExpr info.expr} {if info.isBinder then "(isBinder := true) " else ""}: {ty} @ {formatElabInfo ctx info.toElabInfo}"
 
 def PartialTermInfo.format (ctx : ContextInfo) (info : PartialTermInfo) : Format :=
-  f!"Partial term @ {formatElabInfo ctx info.toElabInfo}"
+  f!"[PartialTerm] @ {formatElabInfo ctx info.toElabInfo}"
 
 def CompletionInfo.format (ctx : ContextInfo) (info : CompletionInfo) : IO Format :=
   match info with
-  | .dot i (expectedType? := expectedType?) .. => return f!"[.] {← i.format ctx} : {expectedType?}"
-  | .id stx _ _ lctx expectedType? => ctx.runMetaM lctx do return f!"[.] {← ctx.ppSyntax lctx stx} : {expectedType?} @ {formatStxRange ctx info.stx}"
-  | _ => return f!"[.] {info.stx} @ {formatStxRange ctx info.stx}"
+  | .dot i (expectedType? := expectedType?) .. => return f!"[Completion-Dot] {← i.format ctx} : {expectedType?}"
+  | .id stx _ _ lctx expectedType? => ctx.runMetaM lctx do return f!"[Completion-Id] {← ctx.ppSyntax lctx stx} : {expectedType?} @ {formatStxRange ctx info.stx}"
+  | _ => return f!"[Completion] {info.stx} @ {formatStxRange ctx info.stx}"
 
 def CommandInfo.format (ctx : ContextInfo) (info : CommandInfo) : IO Format := do
-  return f!"command @ {formatElabInfo ctx info.toElabInfo}"
+  return f!"[Command] @ {formatElabInfo ctx info.toElabInfo}"
 
 def OptionInfo.format (ctx : ContextInfo) (info : OptionInfo) : IO Format := do
-  return f!"option {info.optionName} @ {formatStxRange ctx info.stx}"
+  return f!"[Option] {info.optionName} @ {formatStxRange ctx info.stx}"
 
 def FieldInfo.format (ctx : ContextInfo) (info : FieldInfo) : IO Format := do
   ctx.runMetaM info.lctx do
-    return f!"{info.fieldName} : {← Meta.ppExpr (← Meta.inferType info.val)} := {← Meta.ppExpr info.val} @ {formatStxRange ctx info.stx}"
+    return f!"[Field] {info.fieldName} : {← Meta.ppExpr (← Meta.inferType info.val)} := {← Meta.ppExpr info.val} @ {formatStxRange ctx info.stx}"
 
 def ContextInfo.ppGoals (ctx : ContextInfo) (goals : List MVarId) : IO Format :=
   if goals.isEmpty then
@@ -184,31 +187,31 @@ def TacticInfo.format (ctx : ContextInfo) (info : TacticInfo) : IO Format := do
   let ctxA := { ctx with mctx := info.mctxAfter }
   let goalsBefore ← ctxB.ppGoals info.goalsBefore
   let goalsAfter  ← ctxA.ppGoals info.goalsAfter
-  return f!"Tactic @ {formatElabInfo ctx info.toElabInfo}\n{info.stx}\nbefore {goalsBefore}\nafter {goalsAfter}"
+  return f!"[Tactic] @ {formatElabInfo ctx info.toElabInfo}\n{info.stx}\nbefore {goalsBefore}\nafter {goalsAfter}"
 
 def MacroExpansionInfo.format (ctx : ContextInfo) (info : MacroExpansionInfo) : IO Format := do
   let stx    ← ctx.ppSyntax info.lctx info.stx
   let output ← ctx.ppSyntax info.lctx info.output
-  return f!"Macro expansion\n{stx}\n===>\n{output}"
+  return f!"[MacroExpansion]\n{stx}\n===>\n{output}"
 
 def UserWidgetInfo.format (info : UserWidgetInfo) : Format :=
-  f!"UserWidget {info.id}\n{Std.ToFormat.format <| info.props.run' {}}"
+  f!"[UserWidget] {info.id}\n{Std.ToFormat.format <| info.props.run' {}}"
 
 def FVarAliasInfo.format (info : FVarAliasInfo) : Format :=
-  f!"FVarAlias {info.userName.eraseMacroScopes}: {info.id.name} -> {info.baseId.name}"
+  f!"[FVarAlias] {info.userName.eraseMacroScopes}: {info.id.name} -> {info.baseId.name}"
 
 def FieldRedeclInfo.format (ctx : ContextInfo) (info : FieldRedeclInfo) : Format :=
-  f!"FieldRedecl @ {formatStxRange ctx info.stx}"
+  f!"[FieldRedecl] @ {formatStxRange ctx info.stx}"
 
 def DelabTermInfo.format (ctx : ContextInfo) (info : DelabTermInfo) : IO Format := do
   let loc := if let some loc := info.location? then f!"{loc.module} {loc.range.pos}-{loc.range.endPos}" else "none"
-  return f!"DelabTermInfo @ {← TermInfo.format ctx info.toTermInfo}\n\
+  return f!"[DelabTerm] @ {← TermInfo.format ctx info.toTermInfo}\n\
     Location: {loc}\n\
     Docstring: {repr info.docString?}\n\
     Explicit: {info.explicit}"
 
 def ChoiceInfo.format (ctx : ContextInfo) (info : ChoiceInfo) : Format :=
-  f!"Choice @ {formatElabInfo ctx info.toElabInfo}"
+  f!"[Choice] @ {formatElabInfo ctx info.toElabInfo}"
 
 def Info.format (ctx : ContextInfo) : Info → IO Format
   | ofTacticInfo i         => i.format ctx

src/Lean/Elab/InfoTree/Types.lean

@@ -96,7 +96,6 @@ inductive CompletionInfo where
   | option (stx : Syntax)
   | endSection (stx : Syntax) (scopeNames : List String)
   | tactic (stx : Syntax)
-  -- TODO `import`
 
 /-- Info for an option reference (e.g. in `set_option`). -/
 structure OptionInfo where

src/Lean/Elab/MutualDef.lean

@@ -1069,6 +1069,7 @@ where
     let tacPromises ← views.mapM fun _ => IO.Promise.new
     let expandedDeclIds ← views.mapM fun view => withRef view.headerRef do
       Term.expandDeclId (← getCurrNamespace) (← getLevelNames) view.declId view.modifiers
+    withExporting (isExporting := !expandedDeclIds.all (isPrivateName ·.declName)) do
     let headers ← elabHeaders views expandedDeclIds bodyPromises tacPromises
     let headers ← levelMVarToParamHeaders views headers
     -- If the decl looks like a `rfl` theorem, we elaborate is synchronously as we need to wait for
@@ -1102,7 +1103,8 @@ where
     processDeriving headers
   elabAsync header view declId := do
     let env ← getEnv
-    let async ← env.addConstAsync declId.declName .thm (exportedKind := .axiom)
+    let async ← env.addConstAsync declId.declName .thm
+      (exportedKind? := guard (!isPrivateName declId.declName) *> some .axiom)
     setEnv async.mainEnv
 
     -- TODO: parallelize header elaboration as well? Would have to refactor auto implicits catch,
@@ -1163,14 +1165,16 @@ where
     Core.logSnapshotTask { stx? := none, task := (← BaseIO.asTask (act ())), cancelTk? := cancelTk }
     applyAttributesAt declId.declName view.modifiers.attrs .afterTypeChecking
     applyAttributesAt declId.declName view.modifiers.attrs .afterCompilation
-  finishElab headers (isExporting := false) := withFunLocalDecls headers fun funFVars => withExporting
-    (isExporting := isExporting ||
-      (headers.all (·.kind == .def) && sc.attrs.any (· matches `(attrInstance| expose))) ||
-      headers.all fun header =>
-        !header.modifiers.isPrivate &&
-        (header.kind matches .abbrev | .instance || header.modifiers.attrs.any (·.name == `expose))) do
+  finishElab headers (isExporting := false) := withFunLocalDecls headers fun funFVars =>
+    withExporting (isExporting :=
+      !headers.all (fun header =>
+        header.modifiers.isPrivate || header.modifiers.attrs.any (·.name == `no_expose)) &&
+      (isExporting ||
+       headers.all (fun header => (header.kind matches .abbrev | .instance)) ||
+       (headers.all (·.kind == .def) && sc.attrs.any (· matches `(attrInstance| expose))) ||
+       headers.any (·.modifiers.attrs.any (·.name == `expose)))) do
     let headers := headers.map fun header =>
-      { header with modifiers.attrs := header.modifiers.attrs.filter (·.name != `expose) }
+      { header with modifiers.attrs := header.modifiers.attrs.filter (!·.name ∈ [`expose, `no_expose]) }
     for view in views, funFVar in funFVars do
       addLocalVarInfo view.declId funFVar
     let values ← try

src/Lean/Elab/MutualInductive.lean

@@ -952,6 +952,7 @@ private def elabInductiveViews (vars : Array Expr) (elabs : Array InductiveElabS
   let view0 := elabs[0]!.view
   let ref := view0.ref
   Term.withDeclName view0.declName do withRef ref do
+  withExporting (isExporting := !isPrivateName view0.declName) do
     let res ← mkInductiveDecl vars elabs
     mkAuxConstructions (elabs.map (·.view.declName))
     unless view0.isClass do

src/Lean/Elab/PreDefinition/EqUnfold.lean

@@ -23,8 +23,9 @@ This is not extensible, and always builds on the unfold theorem (`f.eq_def`).
 -/
 def getConstUnfoldEqnFor? (declName : Name) : MetaM (Option Name) := do
   if (← getUnfoldEqnFor? (nonRec := true) declName).isNone then
+    trace[ReservedNameAction] "getConstUnfoldEqnFor? {declName} failed, no unfold theorem available"
     return none
-  let name := .str declName eqUnfoldThmSuffix
+  let name := mkEqLikeNameFor (← getEnv) declName eqUnfoldThmSuffix
   realizeConst declName name do
     -- we have to call `getUnfoldEqnFor?` again to make `unfoldEqnName` available in this context
     let some unfoldEqnName ← getUnfoldEqnFor? (nonRec := true) declName | unreachable!
@@ -58,9 +59,11 @@ def getConstUnfoldEqnFor? (declName : Name) : MetaM (Option Name) := do
 builtin_initialize
   registerReservedNameAction fun name => do
     let .str p s := name | return false
-    unless (← getEnv).isSafeDefinition p do return false
     if s == eqUnfoldThmSuffix then
-      return (← MetaM.run' <| getConstUnfoldEqnFor? p).isSome
+      let env := (← getEnv).setExporting false
+      for p in [p, privateToUserName p] do
+        if env.isSafeDefinition p then
+          return (← MetaM.run' <| getConstUnfoldEqnFor? p).isSome
     return false
 
 end Lean.Meta

src/Lean/Elab/PreDefinition/Eqns.lean

@@ -401,6 +401,7 @@ This is currently used for non-recursive functions, well-founded recursion and p
 but not for structural recursion.
 -/
 def mkEqns (declName : Name) (declNames : Array Name) (tryRefl := true): MetaM (Array Name) := do
+  trace[Elab.definition.eqns] "mkEqns: {declName}"
   let info ← getConstInfoDefn declName
   let us := info.levelParams.map mkLevelParam
   withOptions (tactic.hygienic.set · false) do
@@ -414,7 +415,7 @@ def mkEqns (declName : Name) (declNames : Array Name) (tryRefl := true): MetaM (
   for h : i in [: eqnTypes.size] do
     let type := eqnTypes[i]
     trace[Elab.definition.eqns] "eqnType[{i}]: {eqnTypes[i]}"
-    let name := (Name.str declName eqnThmSuffixBase).appendIndexAfter (i+1)
+    let name := mkEqLikeNameFor (← getEnv) declName s!"{eqnThmSuffixBasePrefix}{i+1}"
     thmNames := thmNames.push name
     -- determinism: `type` should be independent of the environment changes since `baseName` was
     -- added

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

@@ -18,11 +18,10 @@ open Eqns
 /--
 Simple, coarse-grained equation theorem for nonrecursive definitions.
 -/
-private def mkSimpleEqThm (declName : Name) (suffix := Name.mkSimple unfoldThmSuffix) : MetaM (Option Name) := do
+private def mkSimpleEqThm (declName : Name) : MetaM (Option Name) := do
   if let some (.defnInfo info) := (← getEnv).find? declName then
-    let name := declName ++ suffix
-    -- determinism: `name` and `info` are dependent only on `declName`, not any later env
-    -- modifications
+    let name := mkEqLikeNameFor (← getEnv) declName eqn1ThmSuffix
+    trace[Elab.definition.eqns] "mkSimpleEqnThm: {name}"
     realizeConst declName name (doRealize name info)
     return some name
   else

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

@@ -72,7 +72,7 @@ private def rwFixEq (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
 
 /-- Generate the "unfold" lemma for `declName`. -/
 def mkUnfoldEq (declName : Name) (info : EqnInfo) : MetaM Name := do
-  let name := Name.str declName unfoldThmSuffix
+  let name := mkEqLikeNameFor (← getEnv) declName unfoldThmSuffix
   realizeConst declName name (doRealize name)
   return name
 where
@@ -104,7 +104,7 @@ where
       }
 
 def getUnfoldFor? (declName : Name) : MetaM (Option Name) := do
-  let name := Name.str declName unfoldThmSuffix
+  let name := mkEqLikeNameFor (← getEnv) declName unfoldThmSuffix
   let env ← getEnv
   if env.contains name then return name
   let some info := eqnInfoExt.find? env declName | return none

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

@@ -68,12 +68,11 @@ def mkEqns (info : EqnInfo) : MetaM (Array Name) :=
     let target ← mkEq (mkAppN (Lean.mkConst info.declName us) xs) body
     let goal ← mkFreshExprSyntheticOpaqueMVar target
     mkEqnTypes info.declNames goal.mvarId!
-  let baseName := info.declName
   let mut thmNames := #[]
   for h : i in [: eqnTypes.size] do
     let type := eqnTypes[i]
     trace[Elab.definition.structural.eqns] "eqnType {i}: {type}"
-    let name := (Name.str baseName eqnThmSuffixBase).appendIndexAfter (i+1)
+    let name := mkEqLikeNameFor (← getEnv) info.declName s!"{eqnThmSuffixBasePrefix}{i+1}"
     thmNames := thmNames.push name
     -- determinism: `type` should be independent of the environment changes since `baseName` was
     -- added
@@ -104,7 +103,7 @@ def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
 
 /-- Generate the "unfold" lemma for `declName`. -/
 def mkUnfoldEq (declName : Name) (info : EqnInfo) : MetaM Name := do
-  let name := Name.str declName unfoldThmSuffix
+  let name := mkEqLikeNameFor (← getEnv) info.declName unfoldThmSuffix
   realizeConst info.declNames[0]! name (doRealize name)
   return name
 where

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

@@ -51,4 +51,32 @@ def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
 builtin_initialize
   registerGetEqnsFn getEqnsFor?
 
+
+/--
+This is a hack to fix fallout from #8519, where a non-exposed wfrec definition `foo`
+in a module would cause `foo.eq_def` to be defined eagerly and privately,
+but it should still be visible from non-mudule files.
+
+So we create a unfold equation generator that aliases an existing private `eq_def` to
+wherever the current module expects it.
+-/
+def copyPrivateUnfoldTheorem : GetUnfoldEqnFn := fun declName => do
+  withTraceNode `ReservedNameAction (pure m!"{exceptOptionEmoji ·} copyPrivateUnfoldTheorem running for {declName}") do
+  let name := mkEqLikeNameFor (← getEnv) declName unfoldThmSuffix
+  if let some mod ← findModuleOf? declName then
+    let unfoldName' := mkPrivateNameCore mod (.str declName unfoldThmSuffix)
+    if let some (.thmInfo info) := (← getEnv).find? unfoldName' then
+      realizeConst declName name do
+        addDecl <| Declaration.thmDecl {
+          name,
+          type := info.type,
+          value := .const unfoldName' (info.levelParams.map mkLevelParam),
+          levelParams := info.levelParams
+        }
+      return name
+  return none
+
+builtin_initialize
+  registerGetUnfoldEqnFn copyPrivateUnfoldTheorem
+
 end Lean.Elab.WF

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

@@ -74,6 +74,7 @@ def wfRecursion (preDefs : Array PreDefinition) (termMeasure?s : Array (Option T
   let unaryPreDef ← Mutual.cleanPreDef (cacheProofs := false) unaryPreDef
   let preDefs ← preDefs.mapM (Mutual.cleanPreDef (cacheProofs := false) ·)
   registerEqnsInfo preDefs preDefNonRec.declName fixedParamPerms argsPacker
+  markAsRecursive unaryPreDef.declName
   unless (← isProp unaryPreDef.type) do
     WF.mkUnfoldEq unaryPreDef preDefNonRec.declName wfPreprocessProof
   for preDef in preDefs do

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

@@ -73,8 +73,7 @@ private partial def mkUnfoldProof (declName : Name) (mvarId : MVarId) : MetaM Un
         throwError "failed to generate equational theorem for '{declName}'\n{MessageData.ofGoal mvarId}"
 
 def mkUnfoldEq (preDef : PreDefinition) (unaryPreDefName : Name) (wfPreprocessProof : Simp.Result) : MetaM Unit := do
-  let baseName := preDef.declName
-  let name := Name.str baseName unfoldThmSuffix
+  let name := mkEqLikeNameFor (← getEnv) preDef.declName unfoldThmSuffix
   prependError m!"Cannot derive {name}" do
   withOptions (tactic.hygienic.set · false) do
     lambdaTelescope preDef.value fun xs body => do
@@ -106,9 +105,8 @@ theorem of `foo._unary` or `foo._binary`.
 It should just be a specialization of that one, due to defeq.
 -/
 def mkBinaryUnfoldEq (preDef : PreDefinition) (unaryPreDefName : Name) : MetaM Unit := do
-  let baseName := preDef.declName
-  let name := Name.str baseName unfoldThmSuffix
-  let unaryEqName := Name.str unaryPreDefName unfoldThmSuffix
+  let name := mkEqLikeNameFor (← getEnv) preDef.declName unfoldThmSuffix
+  let unaryEqName:= mkEqLikeNameFor (← getEnv) unaryPreDefName unfoldThmSuffix
   prependError m!"Cannot derive {name} from {unaryEqName}" do
   withOptions (tactic.hygienic.set · false) do
     lambdaTelescope preDef.value fun xs body => do

src/Lean/Elab/Print.lean

@@ -23,47 +23,57 @@ private def levelParamsToMessageData (levelParams : List Name) : MessageData :=
     return m ++ "}"
 
 private def mkHeader (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (safety : DefinitionSafety) (sig : Bool := true) : CommandElabM MessageData := do
-  let m : MessageData :=
-    match (← getReducibilityStatus id) with
-    | ReducibilityStatus.irreducible => "@[irreducible] "
-    | ReducibilityStatus.reducible => "@[reducible] "
-    | ReducibilityStatus.semireducible => ""
-  let m :=
-    m ++
-    match safety with
-    | DefinitionSafety.unsafe  => "unsafe "
-    | DefinitionSafety.partial => "partial "
-    | DefinitionSafety.safe    => ""
-  let m := if isProtected (← getEnv) id then m ++ "protected " else m
-  let (m, id) := match privateToUserName? id with
-    | some id => (m ++ "private ", id)
-    | none    => (m, id)
+  let mut attrs := #[]
+  match (← getReducibilityStatus id) with
+  | ReducibilityStatus.irreducible =>   attrs := attrs.push m!"irreducible"
+  | ReducibilityStatus.reducible =>     attrs := attrs.push m!"reducible"
+  | ReducibilityStatus.semireducible => pure ()
+
+  let mut m : MessageData := m!""
+  unless attrs.isEmpty do
+    m := m ++ "@[" ++ MessageData.joinSep attrs.toList ", " ++ "] "
+
+  match safety with
+  | DefinitionSafety.unsafe  => m := m ++ "unsafe "
+  | DefinitionSafety.partial => m := m ++ "partial "
+  | DefinitionSafety.safe    => pure ()
+
+  if isProtected (← getEnv) id then
+    m := m ++ "protected "
+
+  let id' ← match privateToUserName? id with
+    | some id' =>
+      m := m ++ "private "
+      pure id'
+    | none =>
+      pure id
+
   if sig then
-    return m!"{m}{kind} {id}{levelParamsToMessageData levelParams} : {type}"
+    return m!"{m}{kind} {id'}{levelParamsToMessageData levelParams} : {type}"
   else
     return m!"{m}{kind}"
 
-private def mkHeader' (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (isUnsafe : Bool) (sig : Bool := true) : CommandElabM MessageData :=
-  mkHeader kind id levelParams type (if isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe) (sig := sig)
-
 private def mkOmittedMsg : Option Expr → MessageData
   | none   => "<not imported>"
   | some e => e
 
-private def printDefLike (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (value? : Option Expr) (safety := DefinitionSafety.safe) : CommandElabM Unit := do
-  let m ← mkHeader kind id levelParams type safety
-  let m := m ++ " :=" ++ Format.line ++ mkOmittedMsg value?
-  logInfo m
+private def printAxiomLike (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (safety : DefinitionSafety) : CommandElabM Unit := do
+  logInfo (← mkHeader kind id levelParams type safety)
 
-private def printAxiomLike (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (isUnsafe := false) : CommandElabM Unit := do
-  logInfo (← mkHeader' kind id levelParams type isUnsafe)
+private def printDefLike (sigOnly : Bool) (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (value? : Option Expr) (safety := DefinitionSafety.safe) : CommandElabM Unit := do
+  if sigOnly then
+    printAxiomLike kind id levelParams type safety
+  else
+    let m ← mkHeader kind id levelParams type safety
+    let m := m ++ " :=" ++ Format.line ++ mkOmittedMsg value?
+    logInfo m
 
 private def printQuot (id : Name) (levelParams : List Name) (type : Expr) : CommandElabM Unit := do
-  printAxiomLike "Quotient primitive" id levelParams type
+  printAxiomLike "Quotient primitive" id levelParams type (safety := DefinitionSafety.safe)
 
 private def printInduct (id : Name) (levelParams : List Name) (numParams : Nat) (type : Expr)
     (ctors : List Name) (isUnsafe : Bool) : CommandElabM Unit := do
-  let mut m ← mkHeader' "inductive" id levelParams type isUnsafe
+  let mut m ← mkHeader "inductive" id levelParams type (if isUnsafe then .unsafe else .safe)
   m := m ++ Format.line ++ "number of parameters: " ++ toString numParams
   m := m ++ Format.line ++ "constructors:"
   for ctor in ctors do
@@ -89,7 +99,7 @@ private partial def printStructure (id : Name) (levelParams : List Name) (numPar
     (isUnsafe : Bool) : CommandElabM Unit := do
   let env ← getEnv
   let kind := if isClass env id then "class" else "structure"
-  let header ← mkHeader' kind id levelParams type isUnsafe (sig := false)
+  let header ← mkHeader kind id levelParams type (if isUnsafe then .unsafe else .safe) (sig := false)
   let levels := levelParams.map Level.param
   liftTermElabM <| forallTelescope (← getConstInfo id).type fun params _ =>
     let s := Expr.const id levels
@@ -158,20 +168,20 @@ private partial def printStructure (id : Name) (levelParams : List Name) (numPar
       withOptions (fun opts => opts.set pp.proofs.name false) do
         logInfo m
 
-private def printIdCore (id : Name) : CommandElabM Unit := do
+private def printIdCore (sigOnly : Bool) (id : Name) : CommandElabM Unit := do
   let env ← getEnv
   match env.find? id with
   | ConstantInfo.axiomInfo { levelParams := us, type := t, isUnsafe := u, .. } =>
     match getOriginalConstKind? env id with
-    | some .defn => printDefLike "def" id us t none (if u then .unsafe else .safe)
-    | some .thm => printDefLike "theorem" id us t none (if u then .unsafe else .safe)
-    | _  => printAxiomLike "axiom" id us t u
-  | ConstantInfo.defnInfo  { levelParams := us, type := t, value := v, safety := s, .. } => printDefLike "def" id us t v s
-  | ConstantInfo.thmInfo  { levelParams := us, type := t, value := v, .. } => printDefLike "theorem" id us t v
-  | ConstantInfo.opaqueInfo  { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "opaque" id us t u
+    | some .defn => printDefLike sigOnly "def" id us t none (if u then .unsafe else .safe)
+    | some .thm => printDefLike sigOnly "theorem" id us t none (if u then .unsafe else .safe)
+    | _  => printAxiomLike "axiom" id us t (if u then .unsafe else .safe)
+  | ConstantInfo.defnInfo  { levelParams := us, type := t, value := v, safety := s, .. } => printDefLike sigOnly "def" id us t v s
+  | ConstantInfo.thmInfo  { levelParams := us, type := t, value := v, .. } => printDefLike sigOnly "theorem" id us t v
+  | ConstantInfo.opaqueInfo  { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "opaque" id us t (if u then .unsafe else .safe)
   | ConstantInfo.quotInfo  { levelParams := us, type := t, .. } => printQuot id us t
-  | ConstantInfo.ctorInfo { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "constructor" id us t u
-  | ConstantInfo.recInfo { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "recursor" id us t u
+  | ConstantInfo.ctorInfo { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "constructor" id us t (if u then .unsafe else .safe)
+  | ConstantInfo.recInfo { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "recursor" id us t (if u then .unsafe else .safe)
   | ConstantInfo.inductInfo { levelParams := us, numParams, type := t, ctors, isUnsafe := u, .. } =>
     if isStructure env id then
       printStructure id us numParams t ctors[0]! u
@@ -182,13 +192,23 @@ private def printIdCore (id : Name) : CommandElabM Unit := do
 private def printId (id : Syntax) : CommandElabM Unit := do
   addCompletionInfo <| CompletionInfo.id id id.getId (danglingDot := false) {} none
   let cs ← liftCoreM <| realizeGlobalConstWithInfos id
-  cs.forM printIdCore
+  cs.forM (printIdCore (sigOnly := false) ·)
 
 @[builtin_command_elab «print»] def elabPrint : CommandElab
   | `(#print%$tk $id:ident) => withRef tk <| printId id
   | `(#print%$tk $s:str)    => logInfoAt tk s.getString
   | _                       => throwError "invalid #print command"
 
+private def printIdSig (id : Syntax) : CommandElabM Unit := do
+  addCompletionInfo <| CompletionInfo.id id id.getId (danglingDot := false) {} none
+  let cs ← liftCoreM <| realizeGlobalConstWithInfos id
+  cs.forM (printIdCore (sigOnly := true) ·)
+
+@[builtin_command_elab «printSig»] def elabPrintSig : CommandElab := fun stx =>
+  withRef stx[0] do
+    let id := stx[2]
+    printIdSig id
+
 private def printAxiomsOf (constName : Name) : CommandElabM Unit := do
   let axioms ← collectAxioms constName
   if axioms.isEmpty then

src/Lean/Elab/SyntheticMVars.lean

@@ -9,6 +9,7 @@ import Lean.Util.NumObjs
 import Lean.Util.ForEachExpr
 import Lean.Util.OccursCheck
 import Lean.Elab.Tactic.Basic
+import Lean.Meta.AbstractNestedProofs
 
 namespace Lean.Elab.Term
 open Tactic (TacticM evalTactic getUnsolvedGoals withTacticInfoContext)
@@ -215,7 +216,7 @@ def reportStuckSyntheticMVar (mvarId : MVarId) (ignoreStuckTC := false) : TermEl
     | .typeClass extraErrorMsg? =>
       let extraErrorMsg := extraMsgToMsg extraErrorMsg?
       unless ignoreStuckTC do
-         mvarId.withContext do
+        mvarId.withContext do
           let mvarDecl ← getMVarDecl mvarId
           unless (← MonadLog.hasErrors) do
             throwError "typeclass instance problem is stuck, it is often due to metavariables{indentExpr mvarDecl.type}{extraErrorMsg}"
@@ -226,6 +227,11 @@ def reportStuckSyntheticMVar (mvarId : MVarId) (ignoreStuckTC := false) : TermEl
         else
           throwTypeMismatchError header expectedType (← inferType e) e f?
             m!"failed to create type class instance for{indentExpr (← getMVarDecl mvarId).type}"
+    | .tactic (ctx := savedContext) (delayOnMVars := true) .. =>
+      withSavedContext savedContext do
+        mvarId.withContext do
+          let mvarDecl ← getMVarDecl mvarId
+          throwError "tactic execution is stuck, goal contains metavariables{indentExpr mvarDecl.type}"
     | _ => unreachable! -- TODO handle other cases.
 
 /--
@@ -341,12 +347,20 @@ mutual
   If `report := false`, then `runTactic` will not capture exceptions nor will report unsolved goals. Unsolved goals become exceptions.
   -/
   partial def runTactic (mvarId : MVarId) (tacticCode : Syntax) (kind : TacticMVarKind) (report := true) : TermElabM Unit := withoutAutoBoundImplicit do
+    let wasExporting := (← getEnv).isExporting
     -- exit exporting context if entering proof
-    let isExporting ← pure (← getEnv).isExporting <&&> do
+    let isNoLongerExporting ← pure wasExporting <&&> do
       mvarId.withContext do
-        return !(← isProp (← mvarId.getType))
-    withExporting (isExporting := isExporting) do
+        isProp (← mvarId.getType)
     instantiateMVarDeclMVars mvarId
+    -- When exiting exporting context, use fresh mvar for running tactics and abstract it into an
+    -- aux theorem in the end so that we cannot leak references to private decls into the exporting
+    -- context.
+    let mut mvarId' := mvarId
+    if isNoLongerExporting then
+      let mvarDecl ← getMVarDecl mvarId
+      mvarId' := (← mkFreshExprMVarAt mvarDecl.lctx mvarDecl.localInstances mvarDecl.type mvarDecl.kind).mvarId!
+    withExporting (isExporting := wasExporting && !isNoLongerExporting) do
     /-
     TODO: consider using `runPendingTacticsAt` at `mvarId` local context and target type.
     Issue #1380 demonstrates that the goal may still contain pending metavariables.
@@ -362,7 +376,7 @@ mutual
     in more complicated scenarios.
     -/
     tryCatchRuntimeEx
-      (do let remainingGoals ← withInfoHole mvarId <| Tactic.run mvarId <| kind.maybeWithoutRecovery do
+      (do let remainingGoals ← withInfoHole mvarId <| Tactic.run mvarId' <| kind.maybeWithoutRecovery do
             withTacticInfoContext tacticCode do
               -- also put an info node on the `by` keyword specifically -- the token may be `canonical` and thus shown in the info
               -- view even though it is synthetic while a node like `tacticCode` never is (#1990)
@@ -377,12 +391,19 @@ mutual
               kind.logError tacticCode
               reportUnsolvedGoals remainingGoals
             else
-              throwError "unsolved goals\n{goalsToMessageData remainingGoals}")
+              throwError "unsolved goals\n{goalsToMessageData remainingGoals}"
+          if isNoLongerExporting then
+            let mut e ← instantiateExprMVars (.mvar mvarId')
+            if !e.isFVar then
+              e ← mvarId'.withContext do
+                withExporting (isExporting := wasExporting) do
+                  abstractProof e
+            mvarId.assign e)
       fun ex => do
         if report then
           kind.logError tacticCode
         if report && (← read).errToSorry then
-          for mvarId in (← getMVars (mkMVar mvarId)) do
+          for mvarId in (← getMVars (mkMVar mvarId')) do
             mvarId.admit
           logException ex
         else
@@ -408,9 +429,9 @@ mutual
       return false
     -- NOTE: actual processing at `synthesizeSyntheticMVarsAux`
     | .postponed savedContext => resumePostponed savedContext mvarSyntheticDecl.stx mvarId postponeOnError
-    | .tactic tacticCode savedContext kind =>
+    | .tactic tacticCode savedContext kind delayOnMVars =>
       withSavedContext savedContext do
-        if runTactics then
+        if runTactics && !(delayOnMVars && (← mvarId.getType >>= instantiateExprMVars).hasExprMVar) then
           runTactic mvarId tacticCode kind
           return true
         else

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

@@ -355,6 +355,9 @@ builtin_initialize
 builtin_initialize
   registerReservedNameAction fun name => do
     let .str p s := name | return false
+    unless s == enumToBitVecSuffix ||
+           s == eqIffEnumToBitVecEqSuffix ||
+           s == enumToBitVecLeSuffix do return false
     if ← isEnumType p then
       if s == enumToBitVecSuffix then
         discard <| MetaM.run' (getEnumToBitVecFor p)

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

@@ -652,18 +652,18 @@ builtin_simproc [bv_normalize] bv_extract_concat
   let some start ← getNatValue? startExpr | return .continue
   let some len ← getNatValue? lenExpr | return .continue
   let some rhsWidth ← getNatValue? rhsWidthExpr | return .continue
-  if start + len < rhsWidth then
+  if start + len ≤ rhsWidth then
     let expr := mkApp4 (mkConst ``BitVec.extractLsb') rhsWidthExpr startExpr lenExpr rhsExpr
     let proof :=
       mkApp7
-        (mkConst ``BitVec.extractLsb'_append_eq_of_lt)
+        (mkConst ``BitVec.extractLsb'_append_eq_of_add_le)
         lhsWidthExpr
         rhsWidthExpr
         lhsExpr
         rhsExpr
         startExpr
         lenExpr
-        (← mkDecideProof (← mkLt (toExpr (start + len)) rhsWidthExpr))
+        (← mkDecideProof (← mkLe (toExpr (start + len)) rhsWidthExpr))
     return .visit { expr := expr, proof? := some proof }
   else if rhsWidth ≤ start then
     let expr := mkApp4 (mkConst ``BitVec.extractLsb') lhsWidthExpr (toExpr (start - rhsWidth)) lenExpr lhsExpr

src/Lean/Elab/Tactic/Grind.lean

@@ -86,7 +86,7 @@ def elabGrindParams (params : Grind.Params) (ps :  TSyntaxArray ``Parser.Tactic.
       | .intro =>
         if let some info ← Grind.isCasesAttrPredicateCandidate? declName false then
           for ctor in info.ctors do
-            params ← withRef p <| addEMatchTheorem params ctor .default
+            params ← withRef p <| addEMatchTheorem params ctor (.default false)
         else
           throwError "invalid use of `intro` modifier, `{declName}` is not an inductive predicate"
       | .ext =>
@@ -98,9 +98,9 @@ def elabGrindParams (params : Grind.Params) (ps :  TSyntaxArray ``Parser.Tactic.
             -- If it is an inductive predicate,
             -- we also add the constructors (intro rules) as E-matching rules
             for ctor in info.ctors do
-              params ← withRef p <| addEMatchTheorem params ctor .default
+              params ← withRef p <| addEMatchTheorem params ctor (.default false)
         else
-          params ← withRef p <| addEMatchTheorem params declName .default
+          params ← withRef p <| addEMatchTheorem params declName (.default false)
     | _ => throwError "unexpected `grind` parameter{indentD p}"
   return params
 where
@@ -108,15 +108,16 @@ where
     let info ← getConstInfo declName
     match info with
     | .thmInfo _ | .axiomInfo _ | .ctorInfo _ =>
-      if kind == .eqBoth then
-        let params := { params with extra := params.extra.push (← Grind.mkEMatchTheoremForDecl declName .eqLhs) }
-        return { params with extra := params.extra.push (← Grind.mkEMatchTheoremForDecl declName .eqRhs) }
-      else
+      match kind with
+      | .eqBoth gen =>
+        let params := { params with extra := params.extra.push (← Grind.mkEMatchTheoremForDecl declName (.eqLhs gen)) }
+        return { params with extra := params.extra.push (← Grind.mkEMatchTheoremForDecl declName (.eqRhs gen)) }
+      | _ =>
         return { params with extra := params.extra.push (← Grind.mkEMatchTheoremForDecl declName kind) }
     | .defnInfo _ =>
       if (← isReducible declName) then
         throwError "`{declName}` is a reducible definition, `grind` automatically unfolds them"
-      if kind != .eqLhs && kind != .default then
+      if !kind.isEqLhs && !kind.isDefault then
         throwError "invalid `grind` parameter, `{declName}` is a definition, the only acceptable (and redundant) modifier is '='"
       let some thms ← Grind.mkEMatchEqTheoremsForDef? declName
         | throwError "failed to generate equation theorems for `{declName}`"
@@ -223,16 +224,21 @@ def mkGrindOnly
       else
         let decl : Ident := mkIdent (← unresolveNameGlobalAvoidingLocals declName)
         let param ← match kind with
-          | .eqLhs     => `(Parser.Tactic.grindParam| = $decl)
-          | .eqRhs     => `(Parser.Tactic.grindParam| =_ $decl)
-          | .eqBoth    => `(Parser.Tactic.grindParam| _=_ $decl)
-          | .eqBwd     => `(Parser.Tactic.grindParam| ←= $decl)
-          | .bwd       => `(Parser.Tactic.grindParam| ← $decl)
-          | .fwd       => `(Parser.Tactic.grindParam| → $decl)
-          | .leftRight => `(Parser.Tactic.grindParam| => $decl)
-          | .rightLeft => `(Parser.Tactic.grindParam| <= $decl)
-          | .user      => `(Parser.Tactic.grindParam| usr $decl)
-          | .default   => `(Parser.Tactic.grindParam| $decl:ident)
+          | .eqLhs false   => `(Parser.Tactic.grindParam| = $decl:ident)
+          | .eqLhs true    => `(Parser.Tactic.grindParam| = gen $decl:ident)
+          | .eqRhs false   => `(Parser.Tactic.grindParam| =_ $decl:ident)
+          | .eqRhs true    => `(Parser.Tactic.grindParam| =_ gen $decl:ident)
+          | .eqBoth false  => `(Parser.Tactic.grindParam| _=_ $decl:ident)
+          | .eqBoth true   => `(Parser.Tactic.grindParam| _=_ gen $decl:ident)
+          | .eqBwd         => `(Parser.Tactic.grindParam| ←= $decl:ident)
+          | .bwd false     => `(Parser.Tactic.grindParam| ← $decl:ident)
+          | .bwd true      => `(Parser.Tactic.grindParam| ← gen $decl:ident)
+          | .fwd           => `(Parser.Tactic.grindParam| → $decl:ident)
+          | .leftRight     => `(Parser.Tactic.grindParam| => $decl:ident)
+          | .rightLeft     => `(Parser.Tactic.grindParam| <= $decl:ident)
+          | .user          => `(Parser.Tactic.grindParam| usr $decl:ident)
+          | .default false => `(Parser.Tactic.grindParam| $decl:ident)
+          | .default true  => `(Parser.Tactic.grindParam| gen $decl:ident)
         params := params.push param
   for declName in trace.eagerCases.toList do
     unless Grind.isBuiltinEagerCases declName do

src/Lean/Elab/Tactic/Induction.lean

@@ -316,7 +316,7 @@ private def saveAltVarsInfo (altMVarId : MVarId) (altStx : Syntax) (fvarIds : Ar
 open Language in
 def evalAlts (elimInfo : ElimInfo) (alts : Array Alt) (optPreTac : Syntax) (altStxs? : Option (Array Syntax))
     (initialInfo : Info) (tacStx : Syntax)
-    (numEqs : Nat := 0) (numGeneralized : Nat := 0) (toClear : Array FVarId := #[])
+    (numEqs : Nat := 0) (generalized : Array FVarId := #[]) (toClear : Array FVarId := #[])
     (toTag : Array (Ident × FVarId) := #[]) : TacticM Unit := do
   let hasAlts := altStxs?.isSome
   if hasAlts then
@@ -421,9 +421,17 @@ where
       let mut (_, altMVarId) ← altMVarId.introN numFields
       let some (altMVarId', subst) ← Cases.unifyEqs? numEqs altMVarId {}
         | continue  -- alternative is not reachable
+      altMVarId.withContext do
+        for x in subst.domain do
+          if let .fvar y := subst.get x then
+            if let some decl ← x.findDecl? then
+              Elab.pushInfoLeaf (.ofFVarAliasInfo { id := y, baseId := x, userName := decl.userName })
       altMVarId ← if info.provesMotive then
-        (_, altMVarId) ← altMVarId'.introNP numGeneralized
-        pure altMVarId
+        let (generalized', altMVarId') ← altMVarId'.introNP generalized.size
+        altMVarId'.withContext do
+          for x in generalized, y in generalized' do
+            Elab.pushInfoLeaf (.ofFVarAliasInfo { id := y, baseId := x, userName := ← y.getUserName })
+        pure altMVarId'
       else
         pure altMVarId'
       for fvarId in toClear do
@@ -462,9 +470,17 @@ where
         throwError "Alternative '{altName}' is not needed"
     let some (altMVarId', subst) ← Cases.unifyEqs? numEqs altMVarId {}
       | unusedAlt
+    altMVarId.withContext do
+      for x in subst.domain do
+        if let .fvar y := subst.get x then
+          if let some decl ← x.findDecl? then
+            Elab.pushInfoLeaf (.ofFVarAliasInfo { id := y, baseId := x, userName := decl.userName })
     altMVarId ← if info.provesMotive then
-      (_, altMVarId) ← altMVarId'.introNP numGeneralized
-      pure altMVarId
+      let (generalized', altMVarId') ← altMVarId'.introNP generalized.size
+      altMVarId'.withContext do
+        for x in generalized, y in generalized' do
+          Elab.pushInfoLeaf (.ofFVarAliasInfo { id := y, baseId := x, userName := ← y.getUserName })
+      pure altMVarId'
     else
       pure altMVarId'
     for fvarId in toClear do
@@ -526,7 +542,7 @@ private def getUserGeneralizingFVarIds (stx : Syntax) : TacticM (Array FVarId) :
       getFVarIds vars
 
 -- process `generalizingVars` subterm of induction Syntax `stx`.
-private def generalizeVars (mvarId : MVarId) (stx : Syntax) (targets : Array Expr) : TacticM (Nat × MVarId) :=
+private def generalizeVars (mvarId : MVarId) (stx : Syntax) (targets : Array Expr) : TacticM (Array FVarId × MVarId) :=
   mvarId.withContext do
     let userFVarIds ← getUserGeneralizingFVarIds stx
     let forbidden ← mkGeneralizationForbiddenSet targets
@@ -539,7 +555,7 @@ private def generalizeVars (mvarId : MVarId) (stx : Syntax) (targets : Array Exp
       s := s.insert userFVarId
     let fvarIds ← sortFVarIds s.toArray
     let (fvarIds, mvarId') ← mvarId.revert fvarIds
-    return (fvarIds.size, mvarId')
+    return (fvarIds, mvarId')
 
 /--
 Given `inductionAlts` of the form
@@ -865,7 +881,7 @@ private def evalInductionCore (stx : Syntax) (elimInfo : ElimInfo) (targets : Ar
   mvarId.withContext do
     checkInductionTargets targets
     let targetFVarIds := targets.map (·.fvarId!)
-    let (n, mvarId) ← generalizeVars mvarId stx targets
+    let (generalized, mvarId) ← generalizeVars mvarId stx targets
     mvarId.withContext do
       let result ← withRef stx[1] do -- use target position as reference
         ElimApp.mkElimApp elimInfo targets tag
@@ -879,7 +895,7 @@ private def evalInductionCore (stx : Syntax) (elimInfo : ElimInfo) (targets : Ar
         let optPreTac := getOptPreTacOfOptInductionAlts optInductionAlts
         mvarId.assign result.elimApp
         ElimApp.evalAlts elimInfo result.alts optPreTac alts? initInfo stx[0]
-          (numGeneralized := n) (toClear := targetFVarIds) (toTag := toTag)
+          (generalized := generalized) (toClear := targetFVarIds) (toTag := toTag)
         appendGoals result.others.toList
 
 @[builtin_tactic Lean.Parser.Tactic.induction, builtin_incremental]

src/Lean/Elab/Tactic/Try.lean

@@ -610,7 +610,7 @@ private def setGrindParams (tac : TSyntax `tactic) (params : Array (TSyntax ``Pa
 /-- Given a set of declaration names, returns `grind` parameters of the form `= <declName>` -/
 private def mkGrindEqnParams (declNames : Array Name) : MetaM (Array (TSyntax ``Parser.Tactic.grindParam)) := do
   declNames.mapM fun declName => do
-    `(Parser.Tactic.grindParam| = $(← toIdent declName))
+    `(Parser.Tactic.grindParam| = $(← toIdent declName):ident)
 
 private def mkGrindStx (info : Try.Info) : MetaM (TSyntax `tactic) := do
   let grind ← `(tactic| grind?)

src/Lean/Elab/Term.lean

@@ -59,8 +59,13 @@ inductive SyntheticMVarKind where
   -/
   | coe (header? : Option String) (expectedType : Expr) (e : Expr) (f? : Option Expr)
       (mkErrorMsg? : Option (MVarId → Expr → Expr → MetaM MessageData))
-  /-- Use tactic to synthesize value for metavariable. -/
-  | tactic (tacticCode : Syntax) (ctx : SavedContext) (kind : TacticMVarKind)
+  /--
+  Use tactic to synthesize value for metavariable.
+
+  If `delayOnMVars` is true, the tactic will not be executed until the goal is free of unassigned
+  expr metavariables.
+  -/
+  | tactic (tacticCode : Syntax) (ctx : SavedContext) (kind : TacticMVarKind) (delayOnMVars := false)
   /-- Metavariable represents a hole whose elaboration has been postponed. -/
   | postponed (ctx : SavedContext)
   deriving Inhabited
@@ -172,7 +177,7 @@ structure State where
   Backtrackable state for the `TermElabM` monad.
 -/
 structure SavedState where
-  meta   : Meta.SavedState
+  «meta» : Meta.SavedState
   «elab» : State
   deriving Nonempty
 
@@ -195,7 +200,7 @@ structure State where
 -/
 structure Snapshot where
   core   : Core.State
-  meta   : Meta.State
+  «meta» : Meta.State
   term   : Term.State
   tactic : Tactic.State
   stx    : Syntax
@@ -347,7 +352,7 @@ instance : Inhabited (TermElabM α) where
   default := throw default
 
 protected def saveState : TermElabM SavedState :=
-  return { meta := (← Meta.saveState), «elab» := (← get) }
+  return { «meta» := (← Meta.saveState), «elab» := (← get) }
 
 def SavedState.restore (s : SavedState) (restoreInfo : Bool := false) : TermElabM Unit := do
   let traceState ← getTraceState -- We never backtrack trace message
@@ -382,10 +387,10 @@ def withRestoreOrSaveFull (reusableResult? : Option (α × SavedState))
       snap.new.resolve old.val.get
 
   let reusableResult? := reusableResult?.map (fun (val, state) => (val, state.meta))
-  let (a, meta) ← withReader ({ · with tacSnap? }) do
+  let (a, «meta») ← withReader ({ · with tacSnap? }) do
     controlAt MetaM fun runInBase => do
       Meta.withRestoreOrSaveFull reusableResult? <| runInBase act
-  return (a, { meta, «elab» := (← get) })
+  return (a, { «meta», «elab» := (← get) })
 
 instance : MonadBacktrack SavedState TermElabM where
   saveState      := Term.saveState
@@ -1263,14 +1268,15 @@ register_builtin_option debug.byAsSorry : Bool := {
 Creates a new metavariable of type `type` that will be synthesized using the tactic code.
 The `tacticCode` syntax is the full `by ..` syntax.
 -/
-def mkTacticMVar (type : Expr) (tacticCode : Syntax) (kind : TacticMVarKind) : TermElabM Expr := do
+def mkTacticMVar (type : Expr) (tacticCode : Syntax) (kind : TacticMVarKind)
+    (delayOnMVars := false) : TermElabM Expr := do
   if ← pure (debug.byAsSorry.get (← getOptions)) <&&> isProp type then
     withRef tacticCode <| mkLabeledSorry type false (unique := true)
   else
     let mvar ← mkFreshExprMVar type MetavarKind.syntheticOpaque
     let mvarId := mvar.mvarId!
     let ref ← getRef
-    registerSyntheticMVar ref mvarId <| SyntheticMVarKind.tactic tacticCode (← saveContext) kind
+    registerSyntheticMVar ref mvarId <| .tactic tacticCode (← saveContext) kind delayOnMVars
     return mvar
 
 /--

src/Lean/EnvExtension.lean

@@ -150,8 +150,10 @@ namespace MapDeclarationExtension
 def insert (ext : MapDeclarationExtension α) (env : Environment) (declName : Name) (val : α) : Environment :=
   have : Inhabited Environment := ⟨env⟩
   assert! env.getModuleIdxFor? declName |>.isNone -- See comment at `MapDeclarationExtension`
-  assert! env.asyncMayContain declName
-  ext.addEntry env (declName, val)
+  if !env.asyncMayContain declName then
+    panic! s!"MapDeclarationExtension.insert: cannot insert {declName} into {ext.name}, it is not contined in {env.asyncPrefix?}"
+  else
+    ext.addEntry env (declName, val)
 
 def find? [Inhabited α] (ext : MapDeclarationExtension α) (env : Environment) (declName : Name)
     (includeServer := false) : Option α :=

src/Lean/Environment.lean

@@ -585,6 +585,16 @@ private def VisibilityMap.const (a : α) : VisibilityMap α :=
 
 namespace Environment
 
+def header (env : Environment) : EnvironmentHeader :=
+  -- can be assumed to be in sync with `env.checked`; see `setMainModule`, the only modifier of the header
+  env.base.private.header
+
+def imports (env : Environment) : Array Import :=
+  env.header.imports
+
+def allImportedModuleNames (env : Environment) : Array Name :=
+  env.header.moduleNames
+
 private def asyncConsts (env : Environment) : AsyncConsts :=
   env.asyncConstsMap.get env
 
@@ -598,9 +608,12 @@ def ofKernelEnv (env : Kernel.Environment) : Environment :=
 def toKernelEnv (env : Environment) : Kernel.Environment :=
   env.checked.get
 
-/-- Updates `Environment.isExporting`. -/
+/-- Updates `env.isExporting`. Ignored if `env.header.isModule` is false. -/
 def setExporting (env : Environment) (isExporting : Bool) : Environment :=
-  { env with isExporting }
+  if !env.header.isModule || env.isExporting == isExporting then
+    env
+  else
+    { env with isExporting }
 
 /-- Consistently updates synchronous and (private) asynchronous parts of the environment without blocking. -/
 private def modifyCheckedAsync (env : Environment) (f : Kernel.Environment → Kernel.Environment) : Environment :=
@@ -663,11 +676,31 @@ def addDeclCore (env : Environment) (maxHeartbeats : USize) (decl : @& Declarati
     if let some n := decl.getTopLevelNames.find? (!ctx.mayContain ·) then
       throw <| .other s!"cannot add declaration {n} to environment as it is restricted to the \
         prefix {ctx.declPrefix}"
-  if doCheck then
+  let mut env ← if doCheck then
     addDeclCheck env maxHeartbeats decl cancelTk?
   else
     addDeclWithoutChecking env decl
 
+  -- Let the elaborator know about the new constants. This uses the same constant for both
+  -- visibility scopes but the caller can still customize the public one on the main elaboration
+  -- branch by use of `addConstAsync` as is the case for `Lean.addDecl`.
+  for n in decl.getNames do
+    let some info := env.checked.get.find? n | unreachable!
+    env := { env with asyncConstsMap.private := env.asyncConstsMap.private.add {
+      constInfo := .ofConstantInfo info
+      exts? := none
+      consts := .pure <| .mk (α := AsyncConsts) default
+    } }
+    -- TODO
+    if true /- !isPrivateName n-/ then
+      env := { env with asyncConstsMap.public := env.asyncConstsMap.public.add {
+        constInfo := .ofConstantInfo info
+        exts? := none
+        consts := .pure <| .mk (α := AsyncConsts) default
+      } }
+
+  return env
+
 @[inherit_doc Kernel.Environment.constants]
 def constants (env : Environment) : ConstMap :=
   env.toKernelEnv.constants
@@ -689,17 +722,6 @@ private def lakeAdd (env : Environment) (cinfo : ConstantInfo) : Environment :=
     })
   }
 
-/--
-Save an extra constant name that is used to populate `const2ModIdx` when we import
-.olean files. We use this feature to save in which module an auxiliary declaration
-created by the code generator has been created.
--/
-def addExtraName (env : Environment) (name : Name) : Environment :=
-  if env.constants.contains name then
-    env
-  else
-    env.modifyCheckedAsync fun env => { env with extraConstNames := env.extraConstNames.insert name }
-
 -- forward reference due to too many cyclic dependencies
 @[extern "lean_is_reserved_name"]
 private opaque isReservedName (env : Environment) (name : Name) : Bool
@@ -799,7 +821,9 @@ be triggered if any.
 -/
 def enableRealizationsForConst (env : Environment) (opts : Options) (c : Name) :
     BaseIO Environment := do
-  if env.findAsync? c |>.isNone then
+  -- Meta code working on a non-exported declaration should usually do so inside `withoutExporting`
+  -- but we're lenient here in case this call is the only one that needs the setting.
+  if env.setExporting false |>.findAsync? c |>.isNone then
     panic! s!"declaration {c} not found in environment"
     return env
   if let some asyncCtx := env.asyncCtx? then
@@ -913,6 +937,7 @@ structure AddConstAsyncResult where
   asyncEnv : Environment
   private constName : Name
   private kind : ConstantKind
+  private exportedKind? : Option ConstantKind
   private sigPromise : IO.Promise ConstantVal
   private constPromise : IO.Promise ConstPromiseVal
   private checkedEnvPromise : IO.Promise Kernel.Environment
@@ -945,9 +970,13 @@ Starts the asynchronous addition of a constant to the environment. The environme
 corresponding information has been added on the "async" environment branch and committed there; see
 the respective fields of `AddConstAsyncResult` as well as the [Environment Branches] note for more
 information.
+
+`exportedKind?` must be passed if the eventual kind of the constant in the exported constant map
+will differ from that of the private version. It must be `none` if the constant will not be
+exported.
 -/
 def addConstAsync (env : Environment) (constName : Name) (kind : ConstantKind)
-    (exportedKind := kind) (reportExts := true) (checkMayContain := true) :
+    (exportedKind? : Option ConstantKind := some kind) (reportExts := true) (checkMayContain := true) :
     IO AddConstAsyncResult := do
   if checkMayContain then
     if let some ctx := env.asyncCtx? then
@@ -976,7 +1005,7 @@ def addConstAsync (env : Environment) (constName : Name) (kind : ConstantKind)
       | some v => .mk v.nestedConsts.private
       | none   => .mk (α := AsyncConsts) default
   }
-  let exportedAsyncConst := { privateAsyncConst with
+  let exportedAsyncConst? := exportedKind?.map fun exportedKind => { privateAsyncConst with
     constInfo := { privateAsyncConst.constInfo with
       kind := exportedKind
       constInfo := constPromise.result?.map (sync := true) fun
@@ -988,11 +1017,12 @@ def addConstAsync (env : Environment) (constName : Name) (kind : ConstantKind)
       | none   => .mk (α := AsyncConsts) default
   }
   return {
-    constName, kind
+    constName, kind, exportedKind?
     mainEnv := { env with
       asyncConstsMap := {
         «private» := env.asyncConstsMap.private.add privateAsyncConst
-        «public»  := env.asyncConstsMap.public.add exportedAsyncConst
+        «public»  := exportedAsyncConst?.map (env.asyncConstsMap.public.add ·)
+          |>.getD env.asyncConstsMap.public
       }
       checked := checkedEnvPromise.result?.bind (sync := true) fun
         | some kenv => .pure kenv
@@ -1024,6 +1054,7 @@ given environment. The declaration name and kind must match the original values
 def AddConstAsyncResult.commitConst (res : AddConstAsyncResult) (env : Environment)
     (info? : Option ConstantInfo := none) (exportedInfo? : Option ConstantInfo := none) :
     IO Unit := do
+  -- Make sure to access the non-exported version here
   let info ← match info? <|> (env.setExporting false).find? res.constName with
     | some info => pure info
     | none =>
@@ -1037,10 +1068,13 @@ def AddConstAsyncResult.commitConst (res : AddConstAsyncResult) (env : Environme
     throw <| .userError s!"AddConstAsyncResult.commitConst: constant has level params {info.levelParams} but expected {sig.levelParams}"
   if sig.type != info.type then
     throw <| .userError s!"AddConstAsyncResult.commitConst: constant has type {info.type} but expected {sig.type}"
+  let mut exportedInfo? := exportedInfo?
   if let some exportedInfo := exportedInfo? then
     if exportedInfo.toConstantVal != info.toConstantVal then
       -- may want to add more details if necessary
       throw <| .userError s!"AddConstAsyncResult.commitConst: exported constant has different signature"
+  else if res.exportedKind?.isNone then
+    exportedInfo? := some info  -- avoid `find?` call, ultimately unused
   res.constPromise.resolve {
     privateConstInfo := info
     exportedConstInfo := (exportedInfo? <|> (env.setExporting true).find? res.constName).getD info
@@ -1080,15 +1114,18 @@ not block.
 def containsOnBranch (env : Environment) (n : Name) : Bool :=
   (env.asyncConsts.find? n |>.isSome) || (env.base.get env).constants.contains n
 
-def header (env : Environment) : EnvironmentHeader :=
-  -- can be assumed to be in sync with `env.checked`; see `setMainModule`, the only modifier of the header
-  env.base.private.header
-
-def imports (env : Environment) : Array Import :=
-  env.header.imports
-
-def allImportedModuleNames (env : Environment) : Array Name :=
-  env.header.moduleNames
+/--
+Save an extra constant name that is used to populate `const2ModIdx` when we import
+.olean files. We use this feature to save in which module an auxiliary declaration
+created by the code generator has been created.
+-/
+def addExtraName (env : Environment) (name : Name) : Environment :=
+  -- Private definitions are not exported but may still have relevant IR for other modules.
+  -- TODO: restrict to relevant defs that are `meta`/inlining-relevant/...
+  if env.setExporting true |>.contains name then
+    env
+  else
+    env.modifyCheckedAsync fun env => { env with extraConstNames := env.extraConstNames.insert name }
 
 def setMainModule (env : Environment) (m : Name) : Environment := Id.run do
   let env := env.modifyCheckedAsync ({ · with
@@ -2118,6 +2155,7 @@ def displayStats (env : Environment) : IO Unit := do
   IO.println ("direct imports:                        " ++ toString env.header.imports);
   IO.println ("number of imported modules:            " ++ toString env.header.regions.size);
   IO.println ("number of memory-mapped modules:       " ++ toString (env.header.regions.filter (·.isMemoryMapped) |>.size));
+  IO.println ("number of imported consts:             " ++ toString env.constants.map₁.size);
   IO.println ("number of buckets for imported consts: " ++ toString env.constants.numBuckets);
   IO.println ("trust level:                           " ++ toString env.header.trustLevel);
   IO.println ("number of extensions:                  " ++ toString env.base.private.extensions.size);
@@ -2375,8 +2413,7 @@ Sets `Environment.isExporting` to the given value while executing `x`. No-op if
 def withExporting [Monad m] [MonadEnv m] [MonadFinally m] [MonadOptions m] (x : m α)
     (isExporting := true) : m α := do
   let old := (← getEnv).isExporting
-  let isModule := (← getEnv).header.isModule
-  modifyEnv (·.setExporting (isExporting && isModule))
+  modifyEnv (·.setExporting isExporting)
   try
     x
   finally

src/Lean/Message.lean

@@ -349,17 +349,14 @@ def andList (xs : List MessageData) : MessageData :=
 Produces a labeled note that can be appended to an error message.
 -/
 def note (note : MessageData) : MessageData :=
-  -- Note: we do not use the built-in string coercion because it can prevent proper line breaks
-  .tagged `note <| .compose (.ofFormat .line) <| .compose (.ofFormat .line) <|
-    .compose "Note: " note
+  Format.line ++ Format.line ++ "Note: " ++ note
 
 /--
 Produces a labeled hint without an associated code action (non-monadic variant of
 `MessageData.hint`).
 -/
 def hint' (hint : MessageData) : MessageData :=
-  .tagged `hint <| .compose (.ofFormat .line) <| .compose (.ofFormat .line) <|
-    .compose "Hint: " hint
+  Format.line ++ Format.line ++ "Hint: " ++ hint
 
 instance : Coe (List MessageData) MessageData := ⟨ofList⟩
 instance : Coe (List Expr) MessageData := ⟨fun es => ofList <| es.map ofExpr⟩

src/Lean/Meta/AbstractNestedProofs.lean

@@ -9,6 +9,19 @@ import Lean.Meta.Closure
 import Lean.Meta.Transform
 
 namespace Lean.Meta
+
+/-- Abstracts the given proof into an auxiliary theorem, suitably pre-processing its type. -/
+def abstractProof [Monad m] [MonadLiftT MetaM m] [MonadEnv m] [MonadOptions m] [MonadFinally m]
+    (proof : Expr) (cache := true) (postprocessType : Expr → m Expr := pure) : m Expr := do
+  let type ← withoutExporting do inferType proof
+  let type ← (Core.betaReduce type : MetaM _)
+  let type ← zetaReduce type
+  let type ← postprocessType type
+  /- We turn on zetaDelta-expansion to make sure we don't need to perform an expensive `check` step to
+    identify which let-decls can be abstracted. If we design a more efficient test, we can avoid the eager zetaDelta expansion step.
+    In a benchmark created by @selsam, The extra `check` step was a bottleneck. -/
+  mkAuxTheorem (cache := cache) type proof (zetaDelta := true)
+
 namespace AbstractNestedProofs
 
 def getLambdaBody (e : Expr) : Expr :=
@@ -53,8 +66,9 @@ partial def visit (e : Expr) : M Expr := do
         lctx := lctx.modifyLocalDecl xFVarId fun _ => localDecl
       withLCtx lctx localInstances k
     checkCache { val := e : ExprStructEq } fun _ => do
-      if (← isNonTrivialProof e) then
-        mkAuxLemma e
+      if (← withoutExporting do isNonTrivialProof e) then
+        /- Ensure proofs nested in type are also abstracted -/
+        abstractProof e (← read).cache visit
       else match e with
         | .lam ..      => lambdaLetTelescope e fun xs b => visitBinders xs do mkLambdaFVars xs (← visit b) (usedLetOnly := false)
         | .letE ..     => lambdaLetTelescope e fun xs b => visitBinders xs do mkLambdaFVars xs (← visit b) (usedLetOnly := false)
@@ -63,18 +77,6 @@ partial def visit (e : Expr) : M Expr := do
         | .proj _ _ b  => return e.updateProj! (← visit b)
         | .app ..      => e.withApp fun f args => return mkAppN (← visit f) (← args.mapM visit)
         | _            => pure e
-where
-  mkAuxLemma (e : Expr) : M Expr := do
-    let ctx ← read
-    let type ← inferType e
-    let type ← Core.betaReduce type
-    let type ← zetaReduce type
-    /- Ensure proofs nested in type are also abstracted -/
-    let type ← visit type
-    /- We turn on zetaDelta-expansion to make sure we don't need to perform an expensive `check` step to
-      identify which let-decls can be abstracted. If we design a more efficient test, we can avoid the eager zetaDelta expansion step.
-      It a benchmark created by @selsam, The extra `check` step was a bottleneck. -/
-    mkAuxTheorem (cache := ctx.cache) type e (zetaDelta := true)
 
 end AbstractNestedProofs
 

src/Lean/Meta/Basic.lean

@@ -427,7 +427,7 @@ structure State where
 -/
 structure SavedState where
   core        : Core.SavedState
-  meta        : State
+  «meta»      : State
   deriving Nonempty
 
 register_builtin_option maxSynthPendingDepth : Nat := {
@@ -555,7 +555,7 @@ instance : AddMessageContext MetaM where
   addMessageContext := addMessageContextFull
 
 protected def saveState : MetaM SavedState :=
-  return { core := (← Core.saveState), meta := (← get) }
+  return { core := (← Core.saveState), «meta» := (← get) }
 
 /-- Restore backtrackable parts of the state. -/
 def SavedState.restore (b : SavedState) : MetaM Unit := do
@@ -570,7 +570,7 @@ def withRestoreOrSaveFull (reusableResult? : Option (α × SavedState)) (act : M
   let reusableResult? := reusableResult?.map (fun (val, state) => (val, state.core))
   let (a, core) ← controlAt CoreM fun runInBase => do
     Core.withRestoreOrSaveFull reusableResult? <| runInBase act
-  return (a, { core, meta := (← get) })
+  return (a, { core, «meta» := (← get) })
 
 instance : MonadBacktrack SavedState MetaM where
   saveState      := Meta.saveState
@@ -2392,7 +2392,10 @@ where
         let _ : MonadExceptOf _ MetaM := MonadAlwaysExcept.except
         observing do
           realize
-          if !(← getEnv).contains constName then
+          -- Meta code working on a non-exported declaration should usually do so inside
+          -- `withoutExporting` but we're lenient here in case this call is the only one that needs
+          -- the setting.
+          if !((← getEnv).setExporting false).contains constName then
             throwError "Lean.Meta.realizeConst: {constName} was not added to the environment")
         <* addTraceAsMessages
     let res? ← act |>.run' |>.run coreCtx { env } |>.toBaseIO