chore: missing grind annotations for List/Array.modify

`@[grind local]` currently doesn't work as expected on theorems in
namespaces.

.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

@@ -3731,7 +3731,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 +4074,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 +4086,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 +4101,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 +4150,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]
 

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/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

@@ -2974,7 +2974,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 +2983,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 +3006,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 +3182,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 +3998,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 +4188,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 +5430,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/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/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/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

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/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

@@ -2965,7 +2965,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/GetElem.lean

@@ -313,13 +313,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/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/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

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

@@ -108,15 +108,20 @@ def addDecl (decl : Declaration) : CoreM Unit := do
     | .axiomDecl ax => pure (ax.name, .axiomInfo ax, .axiom)
     | _ => return (← addSynchronously)
 
-  -- 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

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/Simp/ConstantFold.lean

@@ -331,7 +331,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]),

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/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

src/Lean/CoreM.lean

@@ -709,8 +709,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/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/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/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/InfoTree/Main.lean

@@ -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 })

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

@@ -414,7 +414,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 := mkEqnThmName declName (i+1)
     thmNames := thmNames.push name
     -- determinism: `type` should be independent of the environment changes since `baseName` was
     -- added

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

@@ -73,7 +73,7 @@ def mkEqns (info : EqnInfo) : MetaM (Array Name) :=
   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 := mkEqnThmName baseName (i+1)
     thmNames := thmNames.push name
     -- determinism: `type` should be independent of the environment changes since `baseName` was
     -- added

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.
 
 /--
@@ -342,11 +348,18 @@ mutual
   -/
   partial def runTactic (mvarId : MVarId) (tacticCode : Syntax) (kind : TacticMVarKind) (report := true) : TermElabM Unit := withoutAutoBoundImplicit do
     -- exit exporting context if entering proof
-    let isExporting ← pure (← getEnv).isExporting <&&> do
+    let isNoLongerExporting ← pure (← getEnv).isExporting <&&> 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 := (← getEnv).isExporting && !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 +375,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 +390,18 @@ 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
+                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 +427,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/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
@@ -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/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 :=
@@ -689,17 +702,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 +801,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 +917,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 +950,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 +985,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 +997,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 +1034,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 +1048,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 +1094,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 +2135,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 +2393,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] (proof : Expr) (cache := true)
+    (postprocessType : Expr → m Expr := pure) : m Expr := do
+  let type ← 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 :=
@@ -54,7 +67,8 @@ partial def visit (e : Expr) : M Expr := do
       withLCtx lctx localInstances k
     checkCache { val := e : ExprStructEq } fun _ => do
       if (← isNonTrivialProof e) then
-        mkAuxLemma e
+        /- 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

@@ -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

src/Lean/Meta/Eqns.lean

@@ -62,6 +62,9 @@ def eqnThmSuffixBasePrefix := eqnThmSuffixBase ++ "_"
 def eqn1ThmSuffix := eqnThmSuffixBasePrefix ++ "1"
 example : eqn1ThmSuffix = "eq_1" := rfl
 
+def mkEqnThmName (declName : Name) (idx : Nat) : Name :=
+  Name.str declName eqnThmSuffixBase |>.appendIndexAfter idx
+
 /-- Returns `true` if `s` is of the form `eq_<idx>` -/
 def isEqnReservedNameSuffix (s : String) : Bool :=
   eqnThmSuffixBasePrefix.isPrefixOf s && (s.drop 3).isNat
@@ -86,7 +89,9 @@ builtin_initialize registerReservedNamePredicate fun env n =>
   match n with
   | .str p s =>
     (isEqnReservedNameSuffix s || s == unfoldThmSuffix || s == eqUnfoldThmSuffix)
-    && env.isSafeDefinition p
+    -- Make equation theorems accessible even when body should not be visible for compatibility.
+    -- TODO: Make them private instead.
+    && (env.setExporting false).isSafeDefinition p
     -- Remark: `f.match_<idx>.eq_<idx>` are handled separately in `Lean.Meta.Match.MatchEqs`.
     && !isMatcherCore env p
   | _ => false
@@ -190,7 +195,7 @@ private partial def alreadyGenerated? (declName : Name) : MetaM (Option (Array N
   let eq1 := Name.str declName eqn1ThmSuffix
   if env.contains eq1 then
     let rec loop (idx : Nat) (eqs : Array Name) : MetaM (Array Name) := do
-      let nextEq := declName ++ (`eq).appendIndexAfter idx
+      let nextEq := mkEqnThmName declName idx
       if env.contains nextEq then
         loop (idx+1) (eqs.push nextEq)
       else

src/Lean/Meta/Hint.lean

@@ -66,7 +66,10 @@ export default function ({ diff, range, suggestion }) {
       e('span', defStyle, comp.text)
   )
   const fullDiff = e('span',
-    { onClick, title: 'Apply suggestion', className: 'link pointer dim font-code', },
+    { onClick,
+      title: 'Apply suggestion',
+      className: 'link pointer dim font-code',
+      style: { display: 'inline-block', verticalAlign: 'text-top' } },
     spans)
   return fullDiff
 }"
@@ -74,85 +77,106 @@ export default function ({ diff, range, suggestion }) {
 /--
 Converts an array of diff actions into corresponding JSON interpretable by `tryThisDiffWidget`.
 -/
-private def mkDiffJson (ds : Array (Diff.Action × Char)) :=
-  -- Avoid cluttering the DOM by grouping "runs" of the same action
-  let unified : List (Diff.Action × List Char) := ds.foldr (init := []) fun
-    | (act, c), [] => [(act, [c])]
-    | (act, c), (act', cs) :: acc =>
-      if act == act' then
-        (act, c :: cs) :: acc
-      else
-        (act, [c]) :: (act', cs) :: acc
-  toJson <| unified.map fun
-    | (.insert, s) => json% { type: "insertion", text: $(String.mk s) }
-    | (.delete, s) => json% { type: "deletion", text: $(String.mk s) }
-    | (.skip  , s) => json% { type: "unchanged", text: $(String.mk s) }
+private def mkDiffJson (ds : Array (Diff.Action × String)) :=
+  toJson <| ds.map fun
+    | (.insert, s) => json% { type: "insertion", text: $s }
+    | (.delete, s) => json% { type: "deletion", text: $s }
+    | (.skip  , s) => json% { type: "unchanged", text: $s }
 
 /--
 Converts an array of diff actions into a Unicode string that visually depicts the diff.
 
 Note that this function does not return the string that results from applying the diff to some
-input; rather, it returns a string representation of the actions that the diff itself comprises, such as `b̵a̵c̲h̲e̲e̲rs̲`.
-
+input; rather, it returns a string representation of the actions that the diff itself comprises,
+such as `b̵a̵c̲h̲e̲e̲rs̲`.
 -/
-private def mkDiffString (ds : Array (Diff.Action × Char)) : String :=
+private def mkDiffString (ds : Array (Diff.Action × String)) : String :=
   let rangeStrs := ds.map fun
-    | (.insert, s) => String.mk [s, '\u0332'] -- U+0332 Combining Low Line
-    | (.delete, s) => String.mk [s, '\u0335'] -- U+0335 Combining Short Stroke Overlay
-    | (.skip  , s) => String.mk [s]
+    | (.insert, s) => String.mk (s.data.flatMap ([·, '\u0332'])) -- U+0332 Combining Low Line
+    | (.delete, s) => String.mk (s.data.flatMap ([·, '\u0335'])) -- U+0335 Combining Short Stroke Overlay
+    | (.skip  , s) => s
   rangeStrs.foldl (· ++ ·) ""
 
 /--
 A code action suggestion associated with a hint in a message.
 
 Refer to `TryThis.Suggestion`; this extends that structure with a `span?` field, allowing a single
-hint to suggest modifications at different locations. If `span?` is not specified, then the `ref`
-for the containing `Suggestions` value is used.
+hint to suggest modifications at different locations. If `span?` is not specified, then the syntax
+reference provided to `MessageData.hint` will be used.
 -/
-structure Suggestion extends TryThis.Suggestion where
+structure Suggestion extends toTryThisSuggestion : TryThis.Suggestion where
   span? : Option Syntax := none
 
 instance : Coe TryThis.SuggestionText Suggestion where
   coe t := { suggestion := t }
 
 instance : ToMessageData Suggestion where
-  toMessageData s := toMessageData s.toSuggestion
+  toMessageData s := toMessageData s.toTryThisSuggestion
 
 /--
-A collection of code action suggestions to be included in a hint in a diagnostic message.
+Produces a diff that splits either on characters, tokens, or not at all, depending on the edit
+distance between the arguments.
 
-Contains the following fields:
-* `ref`: the syntax location for the code action suggestions. Will be overridden by the `span?`
-  field on any suggestions that specify it.
-* `suggestions`: the suggestions to display.
-* `codeActionPrefix?`: if specified, text to display in place of "Try this: " in the code action
-  label
+Guarantees that all actions in the output will be maximally grouped; that is, instead of returning
+`#[(.insert, "a"), (.insert, "b")]`, it will return `#[(.insert, "ab")]`.
 -/
-structure Suggestions where
-  ref : Syntax
-  suggestions : Array Suggestion
-  codeActionPrefix? : Option String := none
+partial def readableDiff (s s' : String) : Array (Diff.Action × String) :=
+  -- TODO: add additional diff granularities
+  let minLength := min s.length s'.length
+  -- The coefficient on this value can be tuned:
+  let maxCharDiffDistance := minLength
+
+  let charDiff := Diff.diff (splitChars s) (splitChars s')
+  -- Note: this is just a rough heuristic, since the diff has no notion of substitution
+  let approxEditDistance := charDiff.filter (·.1 != .skip) |>.size
+  let preStrDiff := joinEdits charDiff
+  -- Given that `Diff.diff` returns a minimal diff, any length-≤3 diff can only have edits at the
+  -- front and back, or at a single interior point. This will always be fairly readable (and
+  -- splitting by a larger unit would likely only be worse). Otherwise, we should only use the
+  -- per-character diff if the edit distance isn't so large that it will be hard to read:
+  if preStrDiff.size ≤ 3 || approxEditDistance ≤ maxCharDiffDistance then
+    preStrDiff.map fun (act, cs) => (act, String.mk cs.toList)
+  else
+    #[(.delete, s), (.insert, s')]
+where
+  splitChars (s : String) : Array Char :=
+    s.toList.toArray
+
+  joinEdits {α} (ds : Array (Diff.Action × α)) : Array (Diff.Action × Array α) :=
+    ds.foldl (init := #[]) fun acc (act, c) =>
+      if h : acc.isEmpty then
+        #[(act, #[c])]
+      else
+        have : acc.size - 1 < acc.size := Nat.sub_one_lt <| mt Array.size_eq_zero_iff.mp <|
+          Array.isEmpty_eq_false_iff.mp (Bool.of_not_eq_true h)
+        let (act', cs) := acc[acc.size - 1]
+        if act == act' then
+          acc.set (acc.size - 1) (act, cs.push c)
+        else
+          acc.push (act, #[c])
 
 /--
 Creates message data corresponding to a `HintSuggestions` collection and adds the corresponding info
 leaf.
 -/
-def Suggestions.toHintMessage (suggestions : Suggestions) : CoreM MessageData := do
-  let { ref, codeActionPrefix?, suggestions } := suggestions
+def mkSuggestionsMessage (suggestions : Array Suggestion)
+    (ref : Syntax)
+    (codeActionPrefix? : Option String) : CoreM MessageData := do
   let mut msg := m!""
   for suggestion in suggestions do
     if let some range := (suggestion.span?.getD ref).getRange? then
-      let { info, suggestions := suggestionArr, range := lspRange } ← processSuggestions ref range
-        #[suggestion.toSuggestion] codeActionPrefix?
+      let { info, suggestions := suggestionArr, range := lspRange } ←
+        processSuggestions ref range #[suggestion.toTryThisSuggestion] codeActionPrefix?
       pushInfoLeaf info
+      -- The following access is safe because
+      -- `suggestionsArr = #[suggestion.toTryThisSuggestion].map ...` (see `processSuggestions`)
       let suggestionText := suggestionArr[0]!.2.1
       let map ← getFileMap
       let rangeContents := Substring.mk map.source range.start range.stop |>.toString
-      let split (s : String) := s.toList.toArray
-      let edits := Diff.diff (split rangeContents) (split suggestionText)
-      let diff := mkDiffJson edits
+      let edits := readableDiff rangeContents suggestionText
+      let diffJson := mkDiffJson edits
       let json := json% {
-        diff: $diff,
+        diff: $diffJson,
         suggestion: $suggestionText,
         range: $lspRange
       }
@@ -164,17 +188,31 @@ def Suggestions.toHintMessage (suggestions : Suggestions) : CoreM MessageData :=
           props := return json
         } (suggestion.messageData?.getD (mkDiffString edits))
       let widgetMsg := m!"{preInfo}{widget}{postInfo}"
-      let suggestionMsg := if suggestions.size == 1 then m!"\n{widgetMsg}" else m!"\n• {widgetMsg}"
+      let suggestionMsg := if suggestions.size == 1 then
+        m!"\n{widgetMsg}"
+      else
+        m!"\n" ++ MessageData.nest 2 m!"• {widgetMsg}"
       msg := msg ++ MessageData.nestD suggestionMsg
   return msg
 
 /--
-Appends a hint `hint` to `msg`. If `suggestions?` is non-`none`, will also append an inline
-suggestion widget.
+Creates a hint message with associated code action suggestions.
+
+To provide a hint without an associated code action, use `MessageData.hint'`.
+
+The arguments are as follows:
+* `hint`: the main message of the hint, which precedes its code action suggestions.
+* `suggestions`: the suggestions to display.
+* `ref?`: if specified, the syntax location for the code action suggestions; otherwise, default to
+  the syntax reference in the monadic state. Will be overridden by the `span?` field on any
+  suggestions that specify it.
+* `codeActionPrefix?`: if specified, text to display in place of "Try this: " in the code action
+  label
 -/
-def _root_.Lean.MessageData.hint (hint : MessageData) (suggestions? : Option Suggestions := none)
+def _root_.Lean.MessageData.hint (hint : MessageData)
+    (suggestions : Array Suggestion) (ref? : Option Syntax := none)
+    (codeActionPrefix? : Option String := none)
     : CoreM MessageData := do
-  let mut hintMsg := m!"\n\nHint: {hint}"
-  if let some suggestions := suggestions? then
-    hintMsg := hintMsg ++ (← suggestions.toHintMessage)
-  return .tagged `hint hintMsg
+  let ref := ref?.getD (← getRef)
+  let suggs ← mkSuggestionsMessage suggestions ref codeActionPrefix?
+  return .tagged `hint (m!"\n\nHint: " ++ hint ++ suggs)

src/Lean/Meta/Injective.lean

@@ -188,6 +188,7 @@ def mkInjectiveTheorems (declName : Name) : MetaM Unit := do
       -- See https://github.com/leanprover/lean4/issues/2188
       withLCtx {} {} do
       for ctor in info.ctors do
+        withExporting (isExporting := !isPrivateName ctor) do
         withTraceNode `Meta.injective (fun _ => return m!"{ctor}") do
           let ctorVal ← getConstInfoCtor ctor
           if ctorVal.numFields > 0 then

src/Lean/Meta/Match/Match.lean

@@ -797,7 +797,15 @@ register_builtin_option bootstrap.genMatcherCode : Bool := {
   descr := "disable code generation for auxiliary matcher function"
 }
 
-builtin_initialize matcherExt : EnvExtension (PHashMap (Expr × Bool) Name) ←
+private structure MatcherKey where
+  value     : Expr
+  compile   : Bool
+  -- When a matcher is created in a private context and thus may contain private references, we must
+  -- not reuse it in an exported context.
+  isPrivate : Bool
+deriving BEq, Hashable
+
+private builtin_initialize matcherExt : EnvExtension (PHashMap MatcherKey Name) ←
   registerEnvExtension (pure {}) (asyncMode := .local)  -- mere cache, keep it local
 
 /-- Similar to `mkAuxDefinition`, but uses the cache `matcherExt`.
@@ -809,7 +817,12 @@ def mkMatcherAuxDefinition (name : Name) (type : Expr) (value : Expr) : MetaM (E
   let env ← getEnv
   let mkMatcherConst name :=
     mkAppN (mkConst name result.levelArgs.toList) result.exprArgs
-  match (matcherExt.getState env).find? (result.value, compile) with
+  let key := { value := result.value, compile, isPrivate := env.header.isModule && isPrivateName name }
+  let mut nameNew? := (matcherExt.getState env).find? key
+  if nameNew?.isNone && key.isPrivate then
+    -- private contexts may reuse public matchers
+    nameNew? := (matcherExt.getState env).find? { key with isPrivate := false }
+  match nameNew? with
   | some nameNew => return (mkMatcherConst nameNew, none)
   | none =>
     let decl := Declaration.defnDecl (← mkDefinitionValInferrringUnsafe name result.levelParams.toList
@@ -819,7 +832,7 @@ def mkMatcherAuxDefinition (name : Name) (type : Expr) (value : Expr) : MetaM (E
       -- matcher bodies should always be exported, if not private anyway
       withExporting do
         addDecl decl
-      modifyEnv fun env => matcherExt.modifyState env fun s => s.insert (result.value, compile) name
+      modifyEnv fun env => matcherExt.modifyState env fun s => s.insert key name
       addMatcherInfo name mi
       setInlineAttribute name
       enableRealizationsForConst name

src/Lean/Meta/Match/MatchEqs.lean

@@ -762,7 +762,7 @@ where go baseName splitterName := withConfig (fun c => { c with etaStruct := .no
     let mut altArgMasks := #[] -- masks produced by `forallAltTelescope`
     for i in [:alts.size] do
       let altNumParams := matchInfo.altNumParams[i]!
-      let thmName := baseName ++ ((`eq).appendIndexAfter idx)
+      let thmName := mkEqnThmName baseName idx
       eqnNames := eqnNames.push thmName
       let (notAlt, splitterAltType, splitterAltNumParam, argMask) ←
           forallAltTelescope (← inferType alts[i]!) altNumParams numDiscrEqs

src/Lean/Meta/SizeOf.lean

@@ -420,6 +420,7 @@ where
 end SizeOfSpecNested
 
 private def mkSizeOfSpecTheorem (indInfo : InductiveVal) (sizeOfFns : Array Name) (recMap : NameMap Name) (ctorName : Name) : MetaM Unit := do
+  withExporting (isExporting := !isPrivateName ctorName) do
   let ctorInfo ← getConstInfoCtor ctorName
   let us := ctorInfo.levelParams.map mkLevelParam
   let simpAttr ← ofExcept <| getAttributeImpl (← getEnv) `simp
@@ -476,6 +477,7 @@ register_builtin_option genSizeOfSpec : Bool := {
 }
 
 def mkSizeOfInstances (typeName : Name) : MetaM Unit := do
+  withExporting (isExporting := !isPrivateName typeName) do
   if (← getEnv).contains ``SizeOf && genSizeOf.get (← getOptions) && !(← isInductivePredicate typeName) then
     withTraceNode `Meta.sizeOf (fun _ => return m!"{typeName}") do
       let indInfo ← getConstInfoInduct typeName

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

@@ -27,9 +27,19 @@ private def getType? (e : Expr) : Option Expr :=
 
 private def isForbiddenParent (parent? : Option Expr) : Bool :=
   if let some parent := parent? then
-    getType? parent |>.isSome
+    if getType? parent |>.isSome then
+      true
+    else
+      -- We also ignore the following parents.
+      -- Remark: `HDiv` should appear in `getType?` as soon as we add support for `Field`,
+      -- `LE.le` linear combinations
+      match_expr parent with
+      | LE.le _ _ _ _ => true
+      | HDiv.hDiv _ _ _ _ _ _ => true
+      | HMod.hMod _ _ _ _ _ _ => true
+      | _ => false
   else
-    false
+    true
 
 def internalize (e : Expr) (parent? : Option Expr) : GoalM Unit := do
   if !(← getConfig).ring && !(← getConfig).ringNull then return ()

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

@@ -51,15 +51,15 @@ partial def reify? (e : Expr) : RingM (Option RingExpr) := do
       if isPowInst (← getRing) i then return .pow (← go a) k else asVar e
     | Neg.neg _ i a =>
       if isNegInst (← getRing) i then return .neg (← go a) else asVar e
-    | IntCast.intCast _ i e =>
+    | IntCast.intCast _ i a =>
       if isIntCastInst (← getRing) i then
-        let some k ← getIntValue? e | toVar e
+        let some k ← getIntValue? a | toVar e
         return .num k
       else
         asVar e
-    | NatCast.natCast _ i e =>
+    | NatCast.natCast _ i a =>
       if isNatCastInst (← getRing) i then
-        let some k ← getNatValue? e | toVar e
+        let some k ← getNatValue? a | toVar e
         return .num k
       else
         asVar e

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

@@ -228,10 +228,10 @@ def EqCnstr.assertImpl (c : EqCnstr) : GoalM Unit := do
     { d, p, h := .ofEq x c : DvdCnstr }.assert
 
 private def exprAsPoly (a : Expr) : GoalM Poly := do
-  if let some var := (← get').varMap.find? { expr := a } then
-    return .add 1 var (.num 0)
-  else if let some k ← getIntValue? a then
+  if let some k ← getIntValue? a then
     return .num k
+  else if let some var := (← get').varMap.find? { expr := a } then
+    return .add 1 var (.num 0)
   else
     throwError "internal `grind` error, expression is not relevant to cutsat{indentExpr a}"
 
@@ -259,23 +259,6 @@ def processNewEqImpl (a b : Expr) : GoalM Unit := do
   | some .nat, some .nat => processNewNatEq a b
   | _, _ => return ()
 
-private def processNewIntLitEq (a ke : Expr) : GoalM Unit := do
-  let some k ← getIntValue? ke | return ()
-  let p₁ ← exprAsPoly a
-  let c ← if k == 0 then
-    pure { p := p₁, h := .core0 a ke : EqCnstr }
-  else
-    let p₂ ← exprAsPoly ke
-    let p := p₁.combine (p₂.mul (-1))
-    pure { p, h := .core a ke p₁ p₂ : EqCnstr }
-  c.assert
-
-@[export lean_process_cutsat_eq_lit]
-def processNewEqLitImpl (a ke : Expr) : GoalM Unit := do
-  match (← foreignTerm? a) with
-  | none => processNewIntLitEq a ke
-  | some .nat => processNewNatEq a ke
-
 private def processNewIntDiseq (a b : Expr) : GoalM Unit := do
   let p₁ ← exprAsPoly a
   let c ← if let some 0 ← getIntValue? b then
@@ -305,7 +288,7 @@ def processNewDiseqImpl (a b : Expr) : GoalM Unit := do
 
 /-- Different kinds of terms internalized by this module. -/
 private inductive SupportedTermKind where
-  | add | mul | num | div | mod | sub | natAbs | toNat
+  | add | mul | num | div | mod | sub | pow | natAbs | toNat
   deriving BEq
 
 private def getKindAndType? (e : Expr) : Option (SupportedTermKind × Expr) :=
@@ -315,6 +298,7 @@ private def getKindAndType? (e : Expr) : Option (SupportedTermKind × Expr) :=
   | HMul.hMul α _ _ _ _ _ => some (.mul, α)
   | HDiv.hDiv α _ _ _ _ _ => some (.div, α)
   | HMod.hMod α _ _ _ _ _ => some (.mod, α)
+  | HPow.hPow α _ _ _ _ _ => some (.pow, α)
   | OfNat.ofNat α _ _ => some (.num, α)
   | Neg.neg α _ a =>
     let_expr OfNat.ofNat _ _ _ := a | none
@@ -329,12 +313,14 @@ private def isForbiddenParent (parent? : Option Expr) (k : SupportedTermKind) :
   -- TODO: document `NatCast.natCast` case.
   -- Remark: we added it to prevent natCast_sub from being expanded twice.
   if declName == ``NatCast.natCast then return true
-  if k matches .div | .mod | .sub | .natAbs | .toNat then return false
+  if k matches .div | .mod | .sub | .pow | .natAbs | .toNat then return false
   if declName == ``HAdd.hAdd || declName == ``LE.le || declName == ``Dvd.dvd then return true
   match k with
   | .add => return false
   | .mul => return declName == ``HMul.hMul
-  | .num => return declName == ``HMul.hMul || declName == ``Eq
+  | .num =>
+    -- Recall that we don't want to internalize numerals occurring at terms such as `x^3`.
+    return declName == ``HMul.hMul || declName == ``HPow.hPow
   | _ => unreachable!
 
 private def internalizeInt (e : Expr) : GoalM Unit := do
@@ -413,7 +399,7 @@ Internalizes an integer (and `Nat`) expression. Here are the different cases tha
 
 - `a + b` when `parent?` is not `+`, `≤`, or `∣`
 - `k * a` when `k` is a numeral and `parent?` is not `+`, `*`, `≤`, `∣`
-- numerals when `parent?` is not `+`, `*`, `≤`, `∣`, `=`.
+- numerals when `parent?` is not `+`, `*`, `≤`, `∣`.
   Recall that we must internalize numerals to make sure we can propagate equalities
   back to the congruence closure module. Example: we have `f 5`, `f x`, `x - y = 3`, `y = 2`.
 -/
@@ -425,7 +411,6 @@ def internalize (e : Expr) (parent? : Option Expr) : GoalM Unit := do
     match k with
     | .div => propagateDiv e
     | .mod => propagateMod e
-    | .num => pure ()
     | _ => internalizeInt e
   else if type.isConstOf ``Nat then
     if (← hasForeignVar e) then return ()
@@ -434,7 +419,6 @@ def internalize (e : Expr) (parent? : Option Expr) : GoalM Unit := do
     | .sub => propagateNatSub e
     | .natAbs => propagateNatAbs e
     | .toNat => propagateToNat e
-    | .num => pure ()
     | _ => internalizeNat e
 
 end Lean.Meta.Grind.Arith.Cutsat

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

@@ -130,6 +130,7 @@ assert that `e` is nonnegative.
 -/
 def assertDenoteAsIntNonneg (e : Expr) : GoalM Unit := withIncRecDepth do
   if e.isAppOf ``NatCast.natCast then return ()
+  if e.isAppOf ``OfNat.ofNat then return () -- we don't want to propagate constraints such as `2 ≥ 0`
   let some rhs ← Int.OfNat.ofDenoteAsIntExpr? e |>.run | return ()
   let gen ← getGeneration e
   let ctx ← getForeignVars .nat
@@ -146,6 +147,7 @@ asserts that it is nonnegative.
 def assertNatCast (e : Expr) (x : Var) : GoalM Unit := do
   let_expr NatCast.natCast _ inst a := e | return ()
   let_expr instNatCastInt := inst | return ()
+  if a.isAppOf ``OfNat.ofNat then return () -- we don't want to propagate constraints such as `2 ≥ 0`
   if (← get').foreignDef.contains { expr := a } then return ()
   let n ← mkForeignVar a .nat
   let p := .add (-1) x (.num 0)

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

@@ -20,19 +20,24 @@ inductive AttrKind where
 /-- Return theorem kind for `stx` of the form `Attr.grindThmMod` -/
 def getAttrKindCore (stx : Syntax) : CoreM AttrKind := do
   match stx with
-  | `(Parser.Attr.grindMod| =) => return .ematch .eqLhs
+  | `(Parser.Attr.grindMod| =) => return .ematch (.eqLhs false)
+  | `(Parser.Attr.grindMod| = gen) => return .ematch (.eqLhs true)
   | `(Parser.Attr.grindMod| →)
   | `(Parser.Attr.grindMod| ->) => return .ematch .fwd
   | `(Parser.Attr.grindMod| ←)
-  | `(Parser.Attr.grindMod| <-) => return .ematch .bwd
-  | `(Parser.Attr.grindMod| =_) => return .ematch .eqRhs
-  | `(Parser.Attr.grindMod| _=_) => return .ematch .eqBoth
+  | `(Parser.Attr.grindMod| <-) => return .ematch (.bwd false)
+  | `(Parser.Attr.grindMod| <- gen) => return .ematch (.bwd true)
+  | `(Parser.Attr.grindMod| =_) => return .ematch (.eqRhs false)
+  | `(Parser.Attr.grindMod| =_ gen) => return .ematch (.eqRhs true)
+  | `(Parser.Attr.grindMod| _=_) => return .ematch (.eqBoth false)
+  | `(Parser.Attr.grindMod| _=_ gen) => return .ematch (.eqBoth true)
   | `(Parser.Attr.grindMod| ←=) => return .ematch .eqBwd
   | `(Parser.Attr.grindMod| ⇒)
   | `(Parser.Attr.grindMod| =>) => return .ematch .leftRight
   | `(Parser.Attr.grindMod| ⇐)
   | `(Parser.Attr.grindMod| <=) => return .ematch .rightLeft
   | `(Parser.Attr.grindMod| usr) => return .ematch .user
+  | `(Parser.Attr.grindMod| gen) => return .ematch (.default true)
   | `(Parser.Attr.grindMod| cases) => return .cases false
   | `(Parser.Attr.grindMod| cases eager) => return .cases true
   | `(Parser.Attr.grindMod| intro) => return .intro
@@ -87,7 +92,7 @@ private def registerGrindAttr (showInfo : Bool) : IO Unit :=
       | .intro =>
         if let some info ← isCasesAttrPredicateCandidate? declName false then
           for ctor in info.ctors do
-            addEMatchAttr ctor attrKind .default (showInfo := showInfo)
+            addEMatchAttr ctor attrKind (.default false) (showInfo := showInfo)
         else
           throwError "invalid `[grind intro]`, `{declName}` is not an inductive predicate"
       | .ext => addExtAttr declName attrKind
@@ -98,9 +103,9 @@ private def registerGrindAttr (showInfo : Bool) : IO Unit :=
             -- If it is an inductive predicate,
             -- we also add the constructors (intro rules) as E-matching rules
             for ctor in info.ctors do
-              addEMatchAttr ctor attrKind .default (showInfo := showInfo)
+              addEMatchAttr ctor attrKind (.default false) (showInfo := showInfo)
         else
-          addEMatchAttr declName attrKind .default (showInfo := showInfo)
+          addEMatchAttr declName attrKind (.default false) (showInfo := showInfo)
     erase := fun declName => MetaM.run' do
       if showInfo then
         throwError "`[grind?]` is a helper attribute for displaying inferred patterns, if you want to remove the attribute, consider using `[grind]` instead"

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

@@ -113,14 +113,6 @@ inductive PendingTheoryPropagation where
     none
   | /-- Propagate the equality `lhs = rhs`. -/
     eq (lhs rhs : Expr)
-  |
-    /--
-    Propagate the literal equality `lhs = lit`.
-    This is needed because some solvers do not internalize literal values.
-    Remark: we may remove this optimization in the future because it adds complexity
-    for a small performance gain.
-    -/
-    eqLit (lhs lit : Expr)
   | /-- Propagate the disequalities in `ps`. -/
     diseqs (ps : ParentSet)
 
@@ -153,25 +145,19 @@ private def checkCutsatEq (rhsRoot lhsRoot : ENode) : GoalM PendingTheoryPropaga
   | some lhsCutsat =>
     if let some rhsCutsat := rhsRoot.cutsat? then
       return .eq lhsCutsat rhsCutsat
-    else if isNum rhsRoot.self then
-      return .eqLit lhsCutsat rhsRoot.self
     else
       -- We have to retrieve the node because other fields have been updated
       let rhsRoot ← getENode rhsRoot.self
       setENode rhsRoot.self { rhsRoot with cutsat? := lhsCutsat }
       return .diseqs (← getParents rhsRoot.self)
   | none =>
-    if let some rhsCutsat := rhsRoot.cutsat? then
-      if isNum lhsRoot.self then
-        return .eqLit rhsCutsat lhsRoot.self
-      else
-        return .diseqs (← getParents lhsRoot.self)
+    if rhsRoot.cutsat?.isSome then
+      return .diseqs (← getParents lhsRoot.self)
     else
       return .none
 
 def propagateCutsat : PendingTheoryPropagation → GoalM Unit
   | .eq lhs rhs => Arith.Cutsat.processNewEq lhs rhs
-  | .eqLit lhs lit => Arith.Cutsat.processNewEqLit lhs lit
   | .diseqs ps => propagateCutsatDiseqs ps
   | .none => return ()
 

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

@@ -148,18 +148,61 @@ private def preprocessMatchCongrEqType (type : Expr) : MetaM Expr := do
     let resultType := mkAppN resultTypeFn (resultArgs.set! 1 lhsNew)
     mkForallFVars hs resultType
 
+/--
+A heuristic procedure for detecting generalized patterns.
+For example, given the theorem
+```
+theorem Option.pbind_some' {α β} {x : Option α} {a : α} {f : (a : α) → x = some a → Option β}
+  (h : x = some a) : pbind x f = f a h
+```
+In the current implementation, we support only occurrences in the resulting type.
+Thus, the following resulting type is generated for the example above:
+```
+pbind (Grind.genPattern h x (some a)) f = f a h
+```
+-/
+private def detectGeneralizedPatterns? (type : Expr) : MetaM Expr := do
+  forallTelescopeReducing type fun hs resultType => do
+    let isTarget? (lhs : Expr) (rhs : Expr) (s : FVarSubst) : Option (FVarId × Expr) := Id.run do
+      let .fvar fvarId := lhs | return none
+      if !hs.contains lhs then
+        return none -- It is a foreign free variable
+      if rhs.containsFVar fvarId then
+        return none -- It is not a generalization if `rhs` contains it
+      if s.contains fvarId then
+        return none -- Remark: may want to abort instead, it is probably not a generalization
+      let rhs := s.apply rhs
+      return some (fvarId, rhs)
+    let mut s : FVarSubst := {}
+    for h in hs do
+      match_expr (← inferType h) with
+      | f@Eq α lhs rhs =>
+        let some (fvarId, rhs) := isTarget? lhs rhs s | pure ()
+        s := s.insert fvarId <| mkGenPattern f.constLevels! α h lhs rhs
+      | f@HEq α lhs β rhs =>
+        let some (fvarId, rhs) := isTarget? lhs rhs s | pure ()
+        s := s.insert fvarId <| mkGenHEqPattern f.constLevels! α β h lhs rhs
+      | _ => pure ()
+    if s.isEmpty then
+      return type
+    let resultType' := s.apply resultType
+    if resultType' == resultType then
+      return type
+    mkForallFVars hs resultType'
+
 /--
 Given the proof for a proposition to be used as an E-matching theorem,
 infers its type, and preprocess it to identify generalized patterns.
 Recall that we infer these generalized patterns automatically for
 `match` congruence equations.
 -/
-private def inferEMatchProofType (proof : Expr) : MetaM Expr := do
+private def inferEMatchProofType (proof : Expr) (gen : Bool) : MetaM Expr := do
   let type ← inferType proof
   if (← isMatchCongrEqConst proof) then
     preprocessMatchCongrEqType type
+  else if gen then
+    detectGeneralizedPatterns? type
   else
-    -- TODO: implement support for to be implemented annotations
     return type
 
 -- Configuration for the `grind` normalizer. We want both `zetaDelta` and `zeta`
@@ -210,31 +253,53 @@ instance : Hashable Origin where
   hash a := hash a.key
 
 inductive EMatchTheoremKind where
-  | eqLhs | eqRhs | eqBoth | eqBwd | fwd | bwd | leftRight | rightLeft | default | user /- pattern specified using `grind_pattern` command -/
+  | eqLhs (gen : Bool)
+  | eqRhs (gen : Bool)
+  | eqBoth (gen : Bool)
+  | eqBwd
+  | fwd
+  | bwd (gen : Bool)
+  | leftRight
+  | rightLeft
+  | default (gen : Bool)
+  | user /- pattern specified using `grind_pattern` command -/
   deriving Inhabited, BEq, Repr, Hashable
 
+def EMatchTheoremKind.isEqLhs : EMatchTheoremKind → Bool
+  | .eqLhs _ => true
+  | _ => false
+
+def EMatchTheoremKind.isDefault : EMatchTheoremKind → Bool
+  | .default _ => true
+  | _ => false
+
 private def EMatchTheoremKind.toAttribute : EMatchTheoremKind → String
-  | .eqLhs     => "[grind =]"
-  | .eqRhs     => "[grind =_]"
-  | .eqBoth    => "[grind _=_]"
-  | .eqBwd     => "[grind ←=]"
-  | .fwd       => "[grind →]"
-  | .bwd       => "[grind ←]"
-  | .leftRight => "[grind =>]"
-  | .rightLeft => "[grind <=]"
-  | .default   => "[grind]"
-  | .user      => "[grind]"
+  | .eqLhs true     => "[grind = gen]"
+  | .eqLhs false    => "[grind =]"
+  | .eqRhs true     => "[grind =_ gen]"
+  | .eqRhs false    => "[grind =_]"
+  | .eqBoth false   => "[grind _=_]"
+  | .eqBoth true    => "[grind _=_ gen]"
+  | .eqBwd          => "[grind ←=]"
+  | .fwd            => "[grind →]"
+  | .bwd false      => "[grind ←]"
+  | .bwd true       => "[grind ← gen]"
+  | .leftRight      => "[grind =>]"
+  | .rightLeft      => "[grind <=]"
+  | .default false  => "[grind]"
+  | .default true   => "[grind gen]"
+  | .user           => "[grind]"
 
 private def EMatchTheoremKind.explainFailure : EMatchTheoremKind → String
-  | .eqLhs     => "failed to find pattern in the left-hand side of the theorem's conclusion"
-  | .eqRhs     => "failed to find pattern in the right-hand side of the theorem's conclusion"
-  | .eqBoth    => unreachable! -- eqBoth is a macro
+  | .eqLhs _   => "failed to find pattern in the left-hand side of the theorem's conclusion"
+  | .eqRhs _   => "failed to find pattern in the right-hand side of the theorem's conclusion"
+  | .eqBoth _  => unreachable! -- eqBoth is a macro
   | .eqBwd     => "failed to use theorem's conclusion as a pattern"
   | .fwd       => "failed to find patterns in the antecedents of the theorem"
-  | .bwd       => "failed to find patterns in the theorem's conclusion"
+  | .bwd _     => "failed to find patterns in the theorem's conclusion"
   | .leftRight => "failed to find patterns searching from left to right"
   | .rightLeft => "failed to find patterns searching from right to left"
-  | .default   => "failed to find patterns"
+  | .default _ => "failed to find patterns"
   | .user      => unreachable!
 
 /-- A theorem for heuristic instantiation based on E-matching. -/
@@ -440,6 +505,10 @@ structure State where
 abbrev M := StateRefT State MetaM
 
 private def saveSymbol (h : HeadIndex) : M Unit := do
+  if let .const declName := h then
+    if declName == ``Grind.genHEqPattern || declName == ``Grind.genPattern then
+      -- We do not save gadgets in the list of symbols.
+      return ()
   unless (← get).symbolSet.contains h do
     modify fun s => { s with symbols := s.symbols.push h, symbolSet := s.symbolSet.insert h }
 
@@ -747,8 +816,8 @@ Given a theorem with proof `proof` and type of the form `∀ (a_1 ... a_n), lhs
 creates an E-matching pattern for it using `addEMatchTheorem n [lhs]`
 If `normalizePattern` is true, it applies the `grind` simplification theorems and simprocs to the pattern.
 -/
-def mkEMatchEqTheoremCore (origin : Origin) (levelParams : Array Name) (proof : Expr) (normalizePattern : Bool) (useLhs : Bool) (showInfo := false) : MetaM EMatchTheorem := do
-  let (numParams, patterns) ← forallTelescopeReducing (← inferEMatchProofType proof) fun xs type => do
+def mkEMatchEqTheoremCore (origin : Origin) (levelParams : Array Name) (proof : Expr) (normalizePattern : Bool) (useLhs : Bool) (gen : Bool) (showInfo := false) : MetaM EMatchTheorem := do
+  let (numParams, patterns) ← forallTelescopeReducing (← inferEMatchProofType proof gen) fun xs type => do
     let (lhs, rhs) ← match_expr type with
       | Eq _ lhs rhs => pure (lhs, rhs)
       | Iff lhs rhs => pure (lhs, rhs)
@@ -760,10 +829,10 @@ def mkEMatchEqTheoremCore (origin : Origin) (levelParams : Array Name) (proof :
     trace[grind.debug.ematch.pattern] "mkEMatchEqTheoremCore: after preprocessing: {pat}, {← normalize pat normConfig}"
     let pats := splitWhileForbidden (pat.abstract xs)
     return (xs.size, pats)
-  mkEMatchTheoremCore origin levelParams numParams proof patterns (if useLhs then .eqLhs else .eqRhs) (showInfo := showInfo)
+  mkEMatchTheoremCore origin levelParams numParams proof patterns (if useLhs then .eqLhs gen else .eqRhs gen) (showInfo := showInfo)
 
 def mkEMatchEqBwdTheoremCore (origin : Origin) (levelParams : Array Name) (proof : Expr) (showInfo := false) : MetaM EMatchTheorem := do
-  let (numParams, patterns) ← forallTelescopeReducing (← inferEMatchProofType proof) fun xs type => do
+  let (numParams, patterns) ← forallTelescopeReducing (← inferEMatchProofType proof (gen := false)) fun xs type => do
     let_expr f@Eq α lhs rhs := type
       | throwError "invalid E-matching `←=` theorem, conclusion must be an equality{indentExpr type}"
     let pat ← preprocessPattern (mkEqBwdPattern f.constLevels! α lhs rhs)
@@ -777,8 +846,8 @@ creates an E-matching pattern for it using `addEMatchTheorem n [lhs]`
 If `normalizePattern` is true, it applies the `grind` simplification theorems and simprocs to the
 pattern.
 -/
-def mkEMatchEqTheorem (declName : Name) (normalizePattern := true) (useLhs : Bool := true) (showInfo := false) : MetaM EMatchTheorem := do
-  mkEMatchEqTheoremCore (.decl declName) #[] (← getProofFor declName) normalizePattern useLhs (showInfo := showInfo)
+def mkEMatchEqTheorem (declName : Name) (normalizePattern := true) (useLhs : Bool := true) (gen : Bool := false) (showInfo := false) : MetaM EMatchTheorem := do
+  mkEMatchEqTheoremCore (.decl declName) #[] (← getProofFor declName) normalizePattern useLhs gen (showInfo := showInfo)
 
 /--
 Adds an E-matching theorem to the environment.
@@ -956,6 +1025,15 @@ where
         return none
     | _ => return none
 
+def EMatchTheoremKind.gen : EMatchTheoremKind → Bool
+  | .eqLhs gen => gen
+  | .eqRhs gen => gen
+  | .eqBoth gen => gen
+  | .default gen => gen
+  | .bwd gen => gen
+  | .eqBwd | .fwd | .rightLeft
+  | .leftRight | .user => false
+
 /--
 Creates an E-match theorem using the given proof and kind.
 If `groundPatterns` is `true`, it accepts patterns without pattern variables. This is useful for
@@ -965,13 +1043,16 @@ since the theorem is already in the `grind` state and there is nothing to be ins
 def mkEMatchTheoremWithKind?
       (origin : Origin) (levelParams : Array Name) (proof : Expr) (kind : EMatchTheoremKind)
       (groundPatterns := true) (showInfo := false) : MetaM (Option EMatchTheorem) := do
-  if kind == .eqLhs then
-    return (← mkEMatchEqTheoremCore origin levelParams proof (normalizePattern := true) (useLhs := true) (showInfo := showInfo))
-  else if kind == .eqRhs then
-    return (← mkEMatchEqTheoremCore origin levelParams proof (normalizePattern := true) (useLhs := false) (showInfo := showInfo))
-  else if kind == .eqBwd then
+  match kind with
+  | .eqLhs gen =>
+    return (← mkEMatchEqTheoremCore origin levelParams proof (normalizePattern := true) (useLhs := true) (gen := gen) (showInfo := showInfo))
+  | .eqRhs gen =>
+    return (← mkEMatchEqTheoremCore origin levelParams proof (normalizePattern := true) (useLhs := false) (gen := gen) (showInfo := showInfo))
+  | .eqBwd =>
     return (← mkEMatchEqBwdTheoremCore origin levelParams proof (showInfo := showInfo))
-  let type ← inferEMatchProofType proof
+  | _ =>
+    pure ()
+  let type ← inferEMatchProofType proof kind.gen
   /-
   Remark: we should not use `forallTelescopeReducing` (with default reducibility) here
   because it may unfold a definition/abstraction, and then select a suboptimal pattern.
@@ -996,10 +1077,10 @@ def mkEMatchTheoremWithKind?
         if ps.isEmpty then
           throwError "invalid `grind` forward theorem, theorem `{← origin.pp}` does not have propositional hypotheses"
         pure ps
-      | .bwd => pure #[type]
+      | .bwd _ => pure #[type]
       | .leftRight => pure <| (← getPropTypes xs).push type
       | .rightLeft => pure <| #[type] ++ (← getPropTypes xs).reverse
-      | .default => pure <| #[type] ++ (← getPropTypes xs)
+      | .default _ => pure <| #[type] ++ (← getPropTypes xs)
       | _ => unreachable!
     go xs searchPlaces
 where
@@ -1032,7 +1113,7 @@ def mkEMatchEqTheoremsForDef? (declName : Name) (showInfo := false) : MetaM (Opt
 
 private def addGrindEqAttr (declName : Name) (attrKind : AttributeKind) (thmKind : EMatchTheoremKind) (useLhs := true) (showInfo := false) : MetaM Unit := do
   if wasOriginallyTheorem (← getEnv) declName then
-    ematchTheoremsExt.add (← mkEMatchEqTheorem declName (normalizePattern := true) (useLhs := useLhs) (showInfo := showInfo)) attrKind
+    ematchTheoremsExt.add (← mkEMatchEqTheorem declName (normalizePattern := true) (useLhs := useLhs) (gen := thmKind.gen) (showInfo := showInfo)) attrKind
   else if let some thms ← mkEMatchEqTheoremsForDef? declName (showInfo := showInfo) then
     unless useLhs do
       throwError "`{declName}` is a definition, you must only use the left-hand side for extracting patterns"
@@ -1057,14 +1138,15 @@ def EMatchTheorems.eraseDecl (s : EMatchTheorems) (declName : Name) : MetaM EMat
     return s.erase <| .decl declName
 
 def addEMatchAttr (declName : Name) (attrKind : AttributeKind) (thmKind : EMatchTheoremKind) (showInfo := false) : MetaM Unit := do
-  if thmKind == .eqLhs then
+  match thmKind with
+  | .eqLhs _ =>
     addGrindEqAttr declName attrKind thmKind (useLhs := true) (showInfo := showInfo)
-  else if thmKind == .eqRhs then
+  | .eqRhs _ =>
     addGrindEqAttr declName attrKind thmKind (useLhs := false) (showInfo := showInfo)
-  else if thmKind == .eqBoth then
+  | .eqBoth _ =>
     addGrindEqAttr declName attrKind thmKind (useLhs := true) (showInfo := showInfo)
     addGrindEqAttr declName attrKind thmKind (useLhs := false) (showInfo := showInfo)
-  else
+  | _ =>
     let info ← getConstInfo declName
     if !wasOriginallyTheorem (← getEnv) declName && !info.isCtor && !info.isAxiom then
       addGrindEqAttr declName attrKind thmKind (showInfo := showInfo)

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

@@ -78,7 +78,7 @@ private def addLocalEMatchTheorems (e : Expr) : GoalM Unit := do
   if let some thm ← mkEMatchTheoremWithKind'? origin proof .rightLeft then
     activateTheorem thm gen
   if (← get).ematch.newThms.size == size then
-    if let some thm ← mkEMatchTheoremWithKind'? origin proof .default then
+    if let some thm ← mkEMatchTheoremWithKind'? origin proof (.default false) then
       activateTheorem thm gen
   if (← get).ematch.newThms.size == size then
     reportIssue! "failed to create E-match local theorem for{indentExpr e}"

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

@@ -982,13 +982,6 @@ Notifies the cutsat module that `a = b` where
 @[extern "lean_process_cutsat_eq"] -- forward definition
 opaque Arith.Cutsat.processNewEq (a b : Expr) : GoalM Unit
 
-/--
-Notifies the cutsat module that `a = k` where
-`a` is term that has been internalized by this module, and `k` is a numeral.
--/
-@[extern "lean_process_cutsat_eq_lit"] -- forward definition
-opaque Arith.Cutsat.processNewEqLit (a k : Expr) : GoalM Unit
-
 /--
 Notifies the cutsat module that `a ≠ b` where
 `a` and `b` are terms that have been internalized by this module.
@@ -1064,8 +1057,6 @@ def markAsCutsatTerm (e : Expr) : GoalM Unit := do
   let root ← getRootENode e
   if let some e' := root.cutsat? then
     Arith.Cutsat.processNewEq e e'
-  else if isNum root.self && !isSameExpr e root.self then
-    Arith.Cutsat.processNewEqLit e root.self
   else
     setENode root.self { root with cutsat? := some e }
     propagateCutsatDiseqs (← getParents root.self)

src/Lean/Meta/Tactic/Try/Collect.lean

@@ -111,7 +111,7 @@ def saveLibSearchCandidates (e : Expr) : M Unit := do
     for (declName, declMod) in (← libSearchFindDecls e) do
       unless (← Grind.isEMatchTheorem declName) do
         let kind := match declMod with
-          | .none => .default
+          | .none => (.default false)
           | .mp => .leftRight
           | .mpr => .rightLeft
         modify fun s => { s with libSearchResults := s.libSearchResults.insert (declName, kind) }

src/Lean/Parser/Command.lean

@@ -523,6 +523,9 @@ declaration signatures.
 -/
 @[builtin_command_parser] def withExporting  := leading_parser
   "#with_exporting " >> commandParser
+/-- Debugging command: Prints the result of `Environment.dumpAsyncEnvState`. -/
+@[builtin_command_parser] def dumpAsyncEnvState := leading_parser
+  "#dump_async_env_state"
 @[builtin_command_parser] def «init_quot»    := leading_parser
   "init_quot"
 def optionValue := nonReservedSymbol "true" <|> nonReservedSymbol "false" <|> strLit <|> numLit

src/Lean/Util/Diff.lean

@@ -20,7 +20,7 @@ inductive Action where
   | delete
   /-- Leave the item in the source -/
   | skip
-deriving Repr, BEq, Hashable, Repr
+deriving Repr, BEq, Hashable, Inhabited
 
 instance : ToString Action where
   toString

src/Std/Data/DHashMap/Lemmas.lean

@@ -1158,7 +1158,7 @@ theorem distinct_keys [EquivBEq α] [LawfulHashable α] :
     m.keys.Pairwise (fun a b => (a == b) = false) :=
   Raw₀.distinct_keys ⟨m.1, m.2.size_buckets_pos⟩ m.2
 
-@[simp, grind =]
+@[simp, grind _=_]
 theorem map_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] :
     m.toList.map Sigma.fst = m.keys :=
   Raw₀.map_fst_toList_eq_keys ⟨m.1, m.2.size_buckets_pos⟩
@@ -1209,7 +1209,7 @@ namespace Const
 
 variable {β : Type v} {m : DHashMap α (fun _ => β)}
 
-@[simp, grind =]
+@[simp, grind _=_]
 theorem map_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] :
     (toList m).map Prod.fst = m.keys :=
   Raw₀.Const.map_fst_toList_eq_keys ⟨m.1, m.2.size_buckets_pos⟩

src/Std/Data/DHashMap/RawLemmas.lean

@@ -1226,7 +1226,7 @@ theorem distinct_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m.keys.Pairwise (fun a b => (a == b) = false) := by
   simp_to_raw using Raw₀.distinct_keys ⟨m, h.size_buckets_pos⟩ h
 
-@[simp, grind =]
+@[simp, grind _=_]
 theorem map_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m.toList.map Sigma.fst = m.keys := by
   apply Raw₀.map_fst_toList_eq_keys ⟨m, h.size_buckets_pos⟩
@@ -1277,7 +1277,7 @@ namespace Const
 
 variable {β : Type v} {m : Raw α (fun _ => β)}
 
-@[simp, grind =]
+@[simp, grind _=_]
 theorem map_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     (Raw.Const.toList m).map Prod.fst = m.keys := by
   apply Raw₀.Const.map_fst_toList_eq_keys ⟨m, h.size_buckets_pos⟩

src/Std/Data/DTreeMap/Lemmas.lean

@@ -1053,7 +1053,7 @@ theorem ordered_keys [TransCmp cmp] :
     t.keys.Pairwise (fun a b => cmp a b = .lt) :=
   Impl.ordered_keys t.wf
 
-@[simp, grind =]
+@[simp, grind _=_]
 theorem map_fst_toList_eq_keys :
     t.toList.map Sigma.fst = t.keys :=
   Impl.map_fst_toList_eq_keys
@@ -1098,7 +1098,7 @@ namespace Const
 
 variable {β : Type v} {t : DTreeMap α β cmp}
 
-@[simp, grind =]
+@[simp, grind _=_]
 theorem map_fst_toList_eq_keys :
     (toList t).map Prod.fst = t.keys :=
   Impl.Const.map_fst_toList_eq_keys

src/Std/Data/DTreeMap/Raw/Lemmas.lean

@@ -1063,7 +1063,7 @@ theorem ordered_keys [TransCmp cmp] (h : t.WF) :
     t.keys.Pairwise (fun a b => cmp a b = .lt) :=
   Impl.ordered_keys h.out
 
-@[simp, grind =]
+@[simp, grind _=_]
 theorem map_fst_toList_eq_keys :
     t.toList.map Sigma.fst = t.keys :=
   Impl.map_fst_toList_eq_keys
@@ -1108,7 +1108,7 @@ namespace Const
 
 variable {β : Type v} {t : Raw α β cmp}
 
-@[simp, grind =]
+@[simp, grind _=_]
 theorem map_fst_toList_eq_keys :
     (toList t).map Prod.fst = t.keys :=
   Impl.Const.map_fst_toList_eq_keys

src/Std/Data/HashMap/Lemmas.lean

@@ -854,7 +854,7 @@ theorem distinct_keys [EquivBEq α] [LawfulHashable α] :
     m.keys.Pairwise (fun a b => (a == b) = false) :=
   DHashMap.distinct_keys
 
-@[simp, grind =]
+@[simp, grind _=_]
 theorem map_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] :
     m.toList.map Prod.fst = m.keys :=
   DHashMap.Const.map_fst_toList_eq_keys

src/Std/Data/HashMap/RawLemmas.lean

@@ -869,7 +869,7 @@ theorem distinct_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m.keys.Pairwise (fun a b => (a == b) = false) :=
   DHashMap.Raw.distinct_keys h.out
 
-@[simp, grind =]
+@[simp, grind _=_]
 theorem map_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m.toList.map Prod.fst = m.keys :=
   DHashMap.Raw.Const.map_fst_toList_eq_keys h.out

src/Std/Data/TreeMap/Lemmas.lean

@@ -795,7 +795,7 @@ theorem ordered_keys [TransCmp cmp] :
     t.keys.Pairwise (fun a b => cmp a b = .lt) :=
   DTreeMap.ordered_keys
 
-@[simp, grind =]
+@[simp, grind _=_]
 theorem map_fst_toList_eq_keys :
     (toList t).map Prod.fst = t.keys :=
   DTreeMap.Const.map_fst_toList_eq_keys

src/Std/Data/TreeMap/Raw/Lemmas.lean

@@ -789,7 +789,7 @@ theorem ordered_keys [TransCmp cmp] (h : t.WF) :
     t.keys.Pairwise (fun a b => cmp a b = .lt) :=
   DTreeMap.Raw.ordered_keys h
 
-@[simp, grind =]
+@[simp, grind _=_]
 theorem map_fst_toList_eq_keys :
     (toList t).map Prod.fst = t.keys :=
   DTreeMap.Raw.Const.map_fst_toList_eq_keys

src/runtime/io.cpp

@@ -1039,11 +1039,7 @@ static obj_res timespec_to_obj(timespec const & ts) {
     return o;
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_metadata(b_obj_arg fname, obj_arg) {
-    struct stat st;
-    if (stat(string_cstr(fname), &st) != 0) {
-        return io_result_mk_error(decode_io_error(errno, fname));
-    }
+static obj_res metadata_core(struct stat const & st) {
     object * mdata = alloc_cnstr(0, 2, sizeof(uint64) + sizeof(uint8));
 #ifdef __APPLE__
     cnstr_set(mdata, 0, timespec_to_obj(st.st_atimespec));
@@ -1067,6 +1063,26 @@ extern "C" LEAN_EXPORT obj_res lean_io_metadata(b_obj_arg fname, obj_arg) {
     return io_result_mk_ok(mdata);
 }
 
+extern "C" LEAN_EXPORT obj_res lean_io_metadata(b_obj_arg fname, obj_arg) {
+    struct stat st;
+    if (stat(string_cstr(fname), &st) != 0) {
+        return io_result_mk_error(decode_io_error(errno, fname));
+    }
+    return metadata_core(st);
+}
+
+extern "C" LEAN_EXPORT obj_res lean_io_symlink_metadata(b_obj_arg fname, obj_arg) {
+#ifdef LEAN_WINDOWS
+    return lean_io_metadata(fname, io_mk_world());
+#else
+    struct stat st;
+    if (lstat(string_cstr(fname), &st) != 0) {
+        return io_result_mk_error(decode_io_error(errno, fname));
+    }
+    return metadata_core(st);
+#endif
+}
+
 extern "C" LEAN_EXPORT obj_res lean_io_create_dir(b_obj_arg p, obj_arg) {
 #ifdef LEAN_WINDOWS
     if (mkdir(string_cstr(p)) == 0) {