sort tests

.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.sha }}
+          key: ${{ matrix.name }}-build-v3-${{ github.event.pull_request.head.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@v10 # https://github.com/marketplace/actions/download-workflow-artifact
+        uses: dawidd6/action-download-artifact@v9 # https://github.com/marketplace/actions/download-workflow-artifact
         with:
           run_id: ${{ github.event.workflow_run.id }}
           path: artifacts

src/Init/Control/Lawful.lean

@@ -9,4 +9,3 @@ prelude
 import Init.Control.Lawful.Basic
 import Init.Control.Lawful.Instances
 import Init.Control.Lawful.Lemmas
-import Init.Control.Lawful.MonadLift

src/Init/Control/Lawful/MonadLift.lean

@@ -1,11 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Paul Reichert
--/
-module
-
-prelude
-import Init.Control.Lawful.MonadLift.Basic
-import Init.Control.Lawful.MonadLift.Lemmas
-import Init.Control.Lawful.MonadLift.Instances

src/Init/Control/Lawful/MonadLift/Basic.lean

@@ -1,52 +0,0 @@
-/-
-Copyright (c) 2025 Quang Dao. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Quang Dao
--/
-module
-
-prelude
-import Init.Control.Basic
-
-/-!
-# LawfulMonadLift and LawfulMonadLiftT
-
-This module provides classes asserting that `MonadLift` and `MonadLiftT` are lawful, which means
-that `monadLift` is compatible with `pure` and `bind`.
--/
-
-section MonadLift
-
-/-- The `MonadLift` typeclass only contains the lifting operation. `LawfulMonadLift` further
-  asserts that lifting commutes with `pure` and `bind`:
-```
-monadLift (pure a) = pure a
-monadLift (ma >>= f) = monadLift ma >>= monadLift ∘ f
-```
--/
-class LawfulMonadLift (m : semiOutParam (Type u → Type v)) (n : Type u → Type w)
-    [Monad m] [Monad n] [inst : MonadLift m n] : Prop where
-  /-- Lifting preserves `pure` -/
-  monadLift_pure {α : Type u} (a : α) : inst.monadLift (pure a) = pure a
-  /-- Lifting preserves `bind` -/
-  monadLift_bind {α β : Type u} (ma : m α) (f : α → m β) :
-    inst.monadLift (ma >>= f) = inst.monadLift ma >>= (fun x => inst.monadLift (f x))
-
-/-- The `MonadLiftT` typeclass only contains the transitive lifting operation.
-  `LawfulMonadLiftT` further asserts that lifting commutes with `pure` and `bind`:
-```
-monadLift (pure a) = pure a
-monadLift (ma >>= f) = monadLift ma >>= monadLift ∘ f
-```
--/
-class LawfulMonadLiftT (m : Type u → Type v) (n : Type u → Type w) [Monad m] [Monad n]
-    [inst : MonadLiftT m n] : Prop where
-  /-- Lifting preserves `pure` -/
-  monadLift_pure {α : Type u} (a : α) : inst.monadLift (pure a) = pure a
-  /-- Lifting preserves `bind` -/
-  monadLift_bind {α β : Type u} (ma : m α) (f : α → m β) :
-    inst.monadLift (ma >>= f) = monadLift ma >>= (fun x => monadLift (f x))
-
-export LawfulMonadLiftT (monadLift_pure monadLift_bind)
-
-end MonadLift

src/Init/Control/Lawful/MonadLift/Instances.lean

@@ -1,137 +0,0 @@
-/-
-Copyright (c) 2025 Quang Dao. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Quang Dao, Paul Reichert
--/
-module
-
-prelude
-import all Init.Control.Option
-import all Init.Control.Except
-import all Init.Control.ExceptCps
-import all Init.Control.StateRef
-import all Init.Control.StateCps
-import Init.Control.Lawful.MonadLift.Lemmas
-import Init.Control.Lawful.Instances
-
-universe u v w x
-
-variable {m : Type u → Type v} {n : Type u → Type w} {o : Type u → Type x}
-
-variable (m n o) in
-instance [Monad m] [Monad n] [Monad o] [MonadLift n o] [MonadLiftT m n]
-    [LawfulMonadLift n o] [LawfulMonadLiftT m n] : LawfulMonadLiftT m o where
-  monadLift_pure := fun a => by
-    simp only [monadLift, LawfulMonadLift.monadLift_pure, liftM_pure]
-  monadLift_bind := fun ma f => by
-    simp only [monadLift, LawfulMonadLift.monadLift_bind, liftM_bind]
-
-variable (m) in
-instance [Monad m] : LawfulMonadLiftT m m where
-  monadLift_pure _ := rfl
-  monadLift_bind _ _ := rfl
-
-namespace StateT
-
-variable [Monad m] [LawfulMonad m]
-
-instance {σ : Type u} : LawfulMonadLift m (StateT σ m) where
-  monadLift_pure _ := by ext; simp [MonadLift.monadLift]
-  monadLift_bind _ _ := by ext; simp [MonadLift.monadLift]
-
-end StateT
-
-namespace ReaderT
-
-variable [Monad m]
-
-instance {ρ : Type u} : LawfulMonadLift m (ReaderT ρ m) where
-  monadLift_pure _ := rfl
-  monadLift_bind _ _ := rfl
-
-end ReaderT
-
-namespace OptionT
-
-variable [Monad m] [LawfulMonad m]
-
-@[simp]
-theorem lift_pure {α : Type u} (a : α) : OptionT.lift (pure a : m α) = pure a := by
-  simp only [OptionT.lift, OptionT.mk, bind_pure_comp, map_pure, pure, OptionT.pure]
-
-@[simp]
-theorem lift_bind {α β : Type u} (ma : m α) (f : α → m β) :
-    OptionT.lift (ma >>= f) = OptionT.lift ma >>= (fun a => OptionT.lift (f a)) := by
-  simp only [instMonad, OptionT.bind, OptionT.mk, OptionT.lift, bind_pure_comp, bind_map_left,
-    map_bind]
-
-instance : LawfulMonadLift m (OptionT m) where
-  monadLift_pure := lift_pure
-  monadLift_bind := lift_bind
-
-end OptionT
-
-namespace ExceptT
-
-variable [Monad m] [LawfulMonad m]
-
-@[simp]
-theorem lift_bind {α β ε : Type u} (ma : m α) (f : α → m β) :
-    ExceptT.lift (ε := ε) (ma >>= f) = ExceptT.lift ma >>= (fun a => ExceptT.lift (f a)) := by
-  simp only [instMonad, ExceptT.bind, mk, ExceptT.lift, bind_map_left, ExceptT.bindCont, map_bind]
-
-instance : LawfulMonadLift m (ExceptT ε m) where
-  monadLift_pure := lift_pure
-  monadLift_bind := lift_bind
-
-instance : LawfulMonadLift (Except ε) (ExceptT ε m) where
-  monadLift_pure _ := by
-    simp only [MonadLift.monadLift, mk, pure, Except.pure, ExceptT.pure]
-  monadLift_bind ma _ := by
-    simp only [instMonad, ExceptT.bind, mk, MonadLift.monadLift, pure_bind, ExceptT.bindCont,
-      Except.instMonad, Except.bind]
-    rcases ma with _ | _ <;> simp
-
-end ExceptT
-
-namespace StateRefT'
-
-instance {ω σ : Type} {m : Type → Type} [Monad m] : LawfulMonadLift m (StateRefT' ω σ m) where
-  monadLift_pure _ := by
-    simp only [MonadLift.monadLift, pure]
-    unfold StateRefT'.lift ReaderT.pure
-    simp only
-  monadLift_bind _ _ := by
-    simp only [MonadLift.monadLift, bind]
-    unfold StateRefT'.lift ReaderT.bind
-    simp only
-
-end StateRefT'
-
-namespace StateCpsT
-
-instance {σ : Type u} [Monad m] [LawfulMonad m] : LawfulMonadLift m (StateCpsT σ m) where
-  monadLift_pure _ := by
-    simp only [MonadLift.monadLift, pure]
-    unfold StateCpsT.lift
-    simp only [pure_bind]
-  monadLift_bind _ _ := by
-    simp only [MonadLift.monadLift, bind]
-    unfold StateCpsT.lift
-    simp only [bind_assoc]
-
-end StateCpsT
-
-namespace ExceptCpsT
-
-instance {ε : Type u} [Monad m] [LawfulMonad m] : LawfulMonadLift m (ExceptCpsT ε m) where
-  monadLift_pure _ := by
-    simp only [MonadLift.monadLift, pure]
-    unfold ExceptCpsT.lift
-    simp only [pure_bind]
-  monadLift_bind _ _ := by
-    simp only [MonadLift.monadLift, bind]
-    unfold ExceptCpsT.lift
-    simp only [bind_assoc]
-
-end ExceptCpsT

src/Init/Control/Lawful/MonadLift/Lemmas.lean

@@ -1,63 +0,0 @@
-/-
-Copyright (c) 2025 Quang Dao. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Quang Dao
--/
-module
-
-prelude
-import Init.Control.Lawful.Basic
-import Init.Control.Lawful.MonadLift.Basic
-
-universe u v w
-
-variable {m : Type u → Type v} {n : Type u → Type w} [Monad m] [Monad n] [MonadLiftT m n]
-  [LawfulMonadLiftT m n] {α β : Type u}
-
-theorem monadLift_map [LawfulMonad m] [LawfulMonad n] (f : α → β) (ma : m α) :
-    monadLift (f <$> ma) = f <$> (monadLift ma : n α) := by
-  rw [← bind_pure_comp, ← bind_pure_comp, monadLift_bind]
-  simp only [bind_pure_comp, monadLift_pure]
-
-theorem monadLift_seq [LawfulMonad m] [LawfulMonad n] (mf : m (α → β)) (ma : m α) :
-    monadLift (mf <*> ma) = monadLift mf <*> (monadLift ma : n α) := by
-  simp only [seq_eq_bind, monadLift_map, monadLift_bind]
-
-theorem monadLift_seqLeft [LawfulMonad m] [LawfulMonad n] (x : m α) (y : m β) :
-    monadLift (x <* y) = (monadLift x : n α) <* (monadLift y : n β) := by
-  simp only [seqLeft_eq, monadLift_map, monadLift_seq]
-
-theorem monadLift_seqRight [LawfulMonad m] [LawfulMonad n] (x : m α) (y : m β) :
-    monadLift (x *> y) = (monadLift x : n α) *> (monadLift y : n β) := by
-  simp only [seqRight_eq, monadLift_map, monadLift_seq]
-
-/-! We duplicate the theorems for `monadLift` to `liftM` since `rw` matches on syntax only. -/
-
-@[simp]
-theorem liftM_pure (a : α) : liftM (pure a : m α) = pure (f := n) a :=
-  monadLift_pure _
-
-@[simp]
-theorem liftM_bind (ma : m α) (f : α → m β) :
-    liftM (n := n) (ma >>= f) = liftM ma >>= (fun a => liftM (f a)) :=
-  monadLift_bind _ _
-
-@[simp]
-theorem liftM_map [LawfulMonad m] [LawfulMonad n] (f : α → β) (ma : m α) :
-    liftM (f <$> ma) = f <$> (liftM ma : n α) :=
-  monadLift_map _ _
-
-@[simp]
-theorem liftM_seq [LawfulMonad m] [LawfulMonad n] (mf : m (α → β)) (ma : m α) :
-    liftM (mf <*> ma) = liftM mf <*> (liftM ma : n α) :=
-  monadLift_seq _ _
-
-@[simp]
-theorem liftM_seqLeft [LawfulMonad m] [LawfulMonad n] (x : m α) (y : m β) :
-    liftM (x <* y) = (liftM x : n α) <* (liftM y : n β) :=
-  monadLift_seqLeft _ _
-
-@[simp]
-theorem liftM_seqRight [LawfulMonad m] [LawfulMonad n] (x : m α) (y : m β) :
-    liftM (x *> y) = (liftM x : n α) *> (liftM y : n β) :=
-  monadLift_seqRight _ _

src/Init/Core.lean

@@ -95,8 +95,7 @@ structure Thunk (α : Type u) : Type u where
   -/
   mk ::
   /-- Extract the getter function out of a thunk. Use `Thunk.get` instead. -/
-  -- The field is public so as to allow computation through it.
-  fn : Unit → α
+  private fn : Unit → α
 
 attribute [extern "lean_mk_thunk"] Thunk.mk
 
@@ -118,10 +117,6 @@ 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 {xs : Array α} (w : 0 < n) : (replicate n xs).back (by simpa using w) = xs := by
+@[simp] theorem back_replicate (w : 0 < n) : (replicate n a).back (by simpa using w) = a := by
   simp [back_eq_getElem]
 
 @[deprecated back_replicate (since := "2025-03-18")]

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 {f : Nat → α → β} {xs : Array α} {i : Nat} {h : i < xs.size} {a : α} :
+@[simp] theorem mapIdx_set {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/BEq.lean

@@ -27,7 +27,7 @@ class EquivBEq (α) [BEq α] : Prop extends PartialEquivBEq α, ReflBEq α
 theorem BEq.symm [BEq α] [PartialEquivBEq α] {a b : α} : a == b → b == a :=
   PartialEquivBEq.symm
 
-theorem BEq.comm [BEq α] [PartialEquivBEq α] {a b : α} : (a == b) = (b == a) :=
+@[grind] theorem BEq.comm [BEq α] [PartialEquivBEq α] {a b : α} : (a == b) = (b == a) :=
   Bool.eq_iff_iff.2 ⟨BEq.symm, BEq.symm⟩
 
 theorem bne_comm [BEq α] [PartialEquivBEq α] {a b : α} : (a != b) = (b != a) := by

src/Init/Data/BitVec/Lemmas.lean

@@ -3179,7 +3179,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 {x : BitVec w} : (concat x b)[0] = b := by
+@[simp] theorem getElem_concat_zero : (concat x b)[0] = b := by
   simp [getElem_concat]
 
 theorem getLsbD_concat_zero : (concat x b).getLsbD 0 = b := by

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, by exact mlt h⟩
+  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(a + b) % n, 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, by exact mlt h⟩
+  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(a * b) % n, 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, by exact mlt h⟩
+  | ⟨a, h⟩, ⟨b, _⟩ => ⟨((n - b) + a) % n, 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, by exact mlt h⟩
+  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(Nat.land a b) % n, mlt h⟩
 
 /--
 Bitwise or.
 -/
 def lor : Fin n → Fin n → Fin n
-  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(Nat.lor a b) % n, by exact mlt h⟩
+  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(Nat.lor a b) % n, mlt h⟩
 
 /--
 Bitwise xor (“exclusive or”).
 -/
 def xor : Fin n → Fin n → Fin n
-  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(Nat.xor a b) % n, by exact mlt h⟩
+  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(Nat.xor a b) % n, 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, by exact mlt h⟩
+  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(a <<< b) % n, 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, by exact mlt h⟩
+  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(a >>> b) % n, mlt h⟩
 
 instance : Add (Fin n) where
   add := Fin.add

src/Init/Data/Fin/Fold.lean

@@ -184,9 +184,8 @@ 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
-    try  -- TODO: block can be deleted after bootstrapping
-      funext
-      simp [foldrM_loop_zero]
+    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

@@ -142,36 +142,17 @@ private structure WorkItem where
   indent : Int
   activeTags : Nat
 
-/--
-A directive indicating whether a given work group is able to be flattened.
-
-- `allow` indicates that the group is allowed to be flattened; its argument is `true` if
-  there is sufficient space for it to be flattened (and so it should be), or `false` if not.
-- `disallow` means that this group should not be flattened irrespective of space concerns.
-  This is used at levels of a `Format` outside of any flattening groups. It is necessary to track
-  this so that, after a hard line break, we know whether to try to flatten the next line.
--/
-inductive FlattenAllowability where
-  | allow (fits : Bool)
-  | disallow
-  deriving BEq
-
-/-- Whether the given directive indicates that flattening should occur. -/
-def FlattenAllowability.shouldFlatten : FlattenAllowability → Bool
-  | allow true => true
-  | _ => false
-
 private structure WorkGroup where
-  fla   : FlattenAllowability
-  flb   : FlattenBehavior
-  items : List WorkItem
+  flatten : Bool
+  flb     : FlattenBehavior
+  items   : List WorkItem
 
 private partial def spaceUptoLine' : List WorkGroup → Nat → Nat → SpaceResult
   |   [],                         _,   _ => {}
   |   { items := [],    .. }::gs, col, w => spaceUptoLine' gs col w
   | g@{ items := i::is, .. }::gs, col, w =>
     merge w
-      (spaceUptoLine i.f g.fla.shouldFlatten (w + col - i.indent) w)
+      (spaceUptoLine i.f g.flatten (w + col - i.indent) w)
       (spaceUptoLine' ({ g with items := is }::gs) col)
 
 /-- A monad in which we can pretty-print `Format` objects. -/
@@ -188,11 +169,11 @@ open MonadPrettyFormat
 private def pushGroup (flb : FlattenBehavior) (items : List WorkItem) (gs : List WorkGroup) (w : Nat) [Monad m] [MonadPrettyFormat m] : m (List WorkGroup) := do
   let k  ← currColumn
   -- Flatten group if it + the remainder (gs) fits in the remaining space. For `fill`, measure only up to the next (ungrouped) line break.
-  let g  := { fla := .allow (flb == FlattenBehavior.allOrNone), flb := flb, items := items : WorkGroup }
+  let g  := { flatten := flb == FlattenBehavior.allOrNone, flb := flb, items := items : WorkGroup }
   let r  := spaceUptoLine' [g] k (w-k)
   let r' := merge (w-k) r (spaceUptoLine' gs k)
   -- Prevent flattening if any item contains a hard line break, except within `fill` if it is ungrouped (=> unflattened)
-  return { g with fla := .allow (!r.foundFlattenedHardLine && r'.space <= w-k) }::gs
+  return { g with flatten := !r.foundFlattenedHardLine && r'.space <= w-k }::gs
 
 private partial def be (w : Nat) [Monad m] [MonadPrettyFormat m] : List WorkGroup → m Unit
   | []                           => pure ()
@@ -219,15 +200,11 @@ private partial def be (w : Nat) [Monad m] [MonadPrettyFormat m] : List WorkGrou
         pushNewline i.indent.toNat
         let is := { i with f := text (s.extract (s.next p) s.endPos) }::is
         -- after a hard line break, re-evaluate whether to flatten the remaining group
-        -- note that we shouldn't start flattening after a hard break outside a group
-        if g.fla == .disallow then
-          be w (gs' is)
-        else
-          pushGroup g.flb is gs w >>= be w
+        pushGroup g.flb is gs w >>= be w
     | line =>
       match g.flb with
       | FlattenBehavior.allOrNone =>
-        if g.fla.shouldFlatten then
+        if g.flatten then
           -- flatten line = text " "
           pushOutput " "
           endTags i.activeTags
@@ -243,10 +220,10 @@ private partial def be (w : Nat) [Monad m] [MonadPrettyFormat m] : List WorkGrou
           endTags i.activeTags
           pushGroup FlattenBehavior.fill is gs w >>= be w
         -- if preceding fill item fit in a single line, try to fit next one too
-        if g.fla.shouldFlatten then
+        if g.flatten then
           let gs'@(g'::_) ← pushGroup FlattenBehavior.fill is gs (w - " ".length)
             | panic "unreachable"
-          if g'.fla.shouldFlatten then
+          if g'.flatten then
             pushOutput " "
             endTags i.activeTags
             be w gs'  -- TODO: use `return`
@@ -255,7 +232,7 @@ private partial def be (w : Nat) [Monad m] [MonadPrettyFormat m] : List WorkGrou
         else
           breakHere
     | align force =>
-      if g.fla.shouldFlatten && !force then
+      if g.flatten && !force then
         -- flatten (align false) = nil
         endTags i.activeTags
         be w (gs' is)
@@ -270,7 +247,7 @@ private partial def be (w : Nat) [Monad m] [MonadPrettyFormat m] : List WorkGrou
           endTags i.activeTags
           be w (gs' is)
     | group f flb =>
-      if g.fla.shouldFlatten then
+      if g.flatten then
         -- flatten (group f) = flatten f
         be w (gs' ({ i with f }::is))
       else
@@ -279,7 +256,7 @@ private partial def be (w : Nat) [Monad m] [MonadPrettyFormat m] : List WorkGrou
 /-- Render the given `f : Format` with a line width of `w`.
 `indent` is the starting amount to indent each line by. -/
 def prettyM (f : Format) (w : Nat) (indent : Nat := 0) [Monad m] [MonadPrettyFormat m] : m Unit :=
-  be w [{ flb := FlattenBehavior.allOrNone, fla := .disallow, items := [{ f := f, indent, activeTags := 0 }]}]
+  be w [{ flb := FlattenBehavior.allOrNone, flatten := false, items := [{ f := f, indent, activeTags := 0 }]}]
 
 /-- Create a format `l ++ f ++ r` with a flatten group.
 FlattenBehaviour is `allOrNone`; for `fill` use `bracketFill`. -/
@@ -317,7 +294,7 @@ private structure State where
   out    : String := ""
   column : Nat    := 0
 
-private instance : MonadPrettyFormat (StateM State) where
+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"]
-def decNonneg (m : @& Int) : Decidable (NonNeg m) :=
+private 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/Basic.lean

@@ -2096,7 +2096,7 @@ where
   | 0,   acc => acc
   | n+1, acc => loop n (n::acc)
 
-@[simp, grind =] theorem range_zero : range 0 = [] := rfl
+@[simp] theorem range_zero : range 0 = [] := rfl
 
 /-! ### range' -/
 

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 {l : List α} : Pairwise R l ↔
+theorem pairwise_iff_getElem : 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₂ : List α} : l₁ <:+ l₂ ↔
+theorem suffix_iff_getElem? : 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₂ : List α} : l₁ <:+: l₂ ↔
+theorem infix_iff_getElem? : 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,7 +211,6 @@ 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
@@ -269,8 +268,6 @@ 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/Range.lean

@@ -142,8 +142,6 @@ theorem range'_eq_cons_iff : range' s n = a :: xs ↔ s = a ∧ 0 < n ∧ xs = r
 
 /-! ### range -/
 
-@[simp, grind =] theorem range_one : range 1 = [0] := rfl
-
 theorem range_loop_range' : ∀ s n, range.loop s (range' s n) = range' 0 (n + s)
   | 0, _ => rfl
   | s + 1, n => by rw [← Nat.add_assoc, Nat.add_right_comm n s 1]; exact range_loop_range' s (n + 1)

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 (n := n) ⟨l.1.reverse, by simpa using l.2⟩).2.1, by simp; omega⟩ := by
+    (splitRevInTwo' l).1 = ⟨(splitInTwo ⟨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 (n := n) ⟨l.1.reverse, by simpa using l.2⟩).1.1.reverse, by simp; omega⟩ := by
+    (splitRevInTwo' l).2 = ⟨(splitInTwo ⟨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,8 +932,7 @@ 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₂ : List α} :
-    l₁ <+: l₂ ↔ ∀ i (h : i < l₁.length), l₂[i]? = some l₁[i] := by
+theorem prefix_iff_getElem? : 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,10 +1767,8 @@ 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)) <| 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⟩⟩
+  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⟩⟩)
 
 /-! ### 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} := private
+  rfl {x} :=
     match x with
     | some _ => BEq.rfl (α := α)
     | none => rfl

src/Init/Data/Option/Lemmas.lean

@@ -1163,11 +1163,8 @@ end ite
 
 /-! ### pbind -/
 
-@[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 pbind_none : pbind none f = none := rfl
+@[simp, grind] theorem pbind_some : pbind (some a) f = f a rfl := 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
@@ -1230,18 +1227,12 @@ theorem get_pbind {o : Option α} {f : (a : α) → o = some a → Option β} {h
 
 /-! ### pmap -/
 
-@[simp] theorem pmap_none {p : α → Prop} {f : ∀ (a : α), p a → β} {h} :
+@[simp, grind] theorem pmap_none {p : α → Prop} {f : ∀ (a : α), p a → β} {h} :
     pmap f none h = none := rfl
 
-@[simp] theorem pmap_some {p : α → Prop} {f : ∀ (a : α), p a → β} {h} :
+@[simp, grind] 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
@@ -1324,11 +1315,8 @@ theorem get_pmap {p : α → Bool} {f : (x : α) → p x → β} {o : Option α}
 
 /-! ### pelim -/
 
-@[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, 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_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
 
-def reprFast (n : Nat) : String :=
+private 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 {h : n = m} {xs : Vector α n} {a b : α} :
+@[simp] theorem replace_cast {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,15 +313,13 @@ 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. -/
--- We still keep it public for reduction purposes
-def get?Internal : (as : List α) → (i : Nat) → Option α
+private 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. -/
--- We still keep it public for reduction purposes
-def get!Internal [Inhabited α] : (as : List α) → (i : Nat) → α
+private def get!Internal [Inhabited α] : (as : List α) → (i : Nat) → α
   | a::_,  0   => a
   | _::as, n+1 => get!Internal as n
   | _,     _   => panic! "invalid index"

src/Init/Grind/Lemmas.lean

@@ -89,12 +89,6 @@ theorem beq_eq_true_of_eq {α : Type u} {_ : BEq α} {_ : LawfulBEq α} {a b :
 theorem beq_eq_false_of_diseq {α : Type u} {_ : BEq α} {_ : LawfulBEq α} {a b : α} (h : ¬ a = b) : (a == b) = false := by
   simp[*]
 
-theorem eq_of_beq_eq_true {α : Type u} {_ : BEq α} {_ : LawfulBEq α} {a b : α} (h : (a == b) = true) : a = b := by
-  simp [beq_iff_eq.mp h]
-
-theorem ne_of_beq_eq_false {α : Type u} {_ : BEq α} {_ : LawfulBEq α} {a b : α} (h : (a == b) = false) : (a = b) = False := by
-  simp [beq_eq_false_iff_ne.mp h]
-
 /-! Bool.and -/
 
 theorem Bool.and_eq_of_eq_true_left {a b : Bool} (h : a = true) : (a && b) = b := by simp [h]

src/Init/Grind/Tactics.lean

@@ -8,57 +8,6 @@ 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.
@@ -66,13 +15,12 @@ Reset all `grind` attributes. This command is intended for testing purposes only
 syntax (name := resetGrindAttrs) "reset_grind_attrs%" : command
 
 namespace Attr
-syntax grindGen    := &"gen "
-syntax grindEq     := "= " (grindGen)?
-syntax grindEqBoth := atomic("_" "=" "_ ") (grindGen)?
-syntax grindEqRhs  := atomic("=" "_ ") (grindGen)?
+syntax grindEq     := "= "
+syntax grindEqBoth := atomic("_" "=" "_ ")
+syntax grindEqRhs  := atomic("=" "_ ")
 syntax grindEqBwd  := atomic("←" "= ") <|> atomic("<-" "= ")
-syntax grindBwd    := ("← " <|> "<- ") (grindGen)?
-syntax grindFwd    := "→ " <|> "-> "
+syntax grindBwd    := "← " <|> "-> "
+syntax grindFwd    := "→ " <|> "<- "
 syntax grindRL     := "⇐ " <|> "<= "
 syntax grindLR     := "⇒ " <|> "=> "
 syntax grindUsr    := &"usr "
@@ -80,10 +28,7 @@ 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 <|> grindGen
+syntax grindMod := grindEqBoth <|> grindEqRhs <|> grindEq <|> grindEqBwd <|> grindBwd <|> grindFwd <|> grindRL <|> grindLR <|> grindUsr <|> grindCasesEager <|> grindCases <|> grindIntro <|> grindExt
 syntax (name := grind) "grind" (grindMod)? : attr
 syntax (name := grind?) "grind?" (grindMod)? : attr
 end Attr
@@ -177,7 +122,7 @@ structure Config where
   /--
   When `true` (default: `false`), uses procedure for handling equalities over commutative rings.
   -/
-  ring := true
+  ring := false
   ringSteps := 10000
   /--
   When `true` (default: `false`), the commutative ring procedure in `grind` constructs stepwise

src/Init/Grind/Util.lean

@@ -32,6 +32,55 @@ 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,7 +8,6 @@ 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
@@ -1204,8 +1203,7 @@ def quoteNameMk : Name → Term
   | .num n i => Syntax.mkCApp ``Name.mkNum #[quoteNameMk n, quote i]
 
 instance : Quote Name `term where
-  quote n := private
-    match getEscapedNameParts? [] n with
+  quote n := match getEscapedNameParts? [] n with
     | some ss => ⟨mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit ("`" ++ ".".intercalate ss)]⟩
     | none    => ⟨quoteNameMk n⟩
 
@@ -1218,7 +1216,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 := private quoteList
+  quote := quoteList
 
 private def quoteArray [Quote α `term] (xs : Array α) : Term :=
   if xs.size <= 8 then
@@ -1235,7 +1233,7 @@ where
   decreasing_by decreasing_trivial_pre_omega
 
 instance [Quote α `term] : Quote (Array α) `term where
-  quote := private quoteArray
+  quote := 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 "notMem" for "∉" in [«term_∉_»]
+recommended_spelling "not_mem" 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 maximum. The resulting type
+the minimal level, it takes a further level parameter and occupies their minimum. 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,12 +2500,8 @@ 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 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
+def Char.ofNatAux (n : @& Nat) (h : n.isValidChar) : Char :=
+  { val := ⟨BitVec.ofNatLT n (isValidChar_UInt32 h)⟩, valid := h }
 
 /--
 Converts a `Nat` into a `Char`. If the `Nat` does not encode a valid Unicode scalar value, `'\0'` is
@@ -4096,13 +4092,8 @@ 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 (`.`).
@@ -4187,35 +4178,35 @@ abbrev mkSimple (s : String) : Name :=
   .str .anonymous s
 
 /-- Make name `s₁` -/
-@[expose, reducible] def mkStr1 (s₁ : String) : Name :=
+@[reducible] def mkStr1 (s₁ : String) : Name :=
   .str .anonymous s₁
 
 /-- Make name `s₁.s₂` -/
-@[expose, reducible] def mkStr2 (s₁ s₂ : String) : Name :=
+@[reducible] def mkStr2 (s₁ s₂ : String) : Name :=
   .str (.str .anonymous s₁) s₂
 
 /-- Make name `s₁.s₂.s₃` -/
-@[expose, reducible] def mkStr3 (s₁ s₂ s₃ : String) : Name :=
+@[reducible] def mkStr3 (s₁ s₂ s₃ : String) : Name :=
   .str (.str (.str .anonymous s₁) s₂) s₃
 
 /-- Make name `s₁.s₂.s₃.s₄` -/
-@[expose, reducible] def mkStr4 (s₁ s₂ s₃ s₄ : String) : Name :=
+@[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₅` -/
-@[expose, reducible] def mkStr5 (s₁ s₂ s₃ s₄ s₅ : String) : Name :=
+@[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₆` -/
-@[expose, reducible] def mkStr6 (s₁ s₂ s₃ s₄ s₅ s₆ : String) : Name :=
+@[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₇` -/
-@[expose, reducible] def mkStr7 (s₁ s₂ s₃ s₄ s₅ s₆ s₇ : String) : Name :=
+@[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₈` -/
-@[expose, reducible] def mkStr8 (s₁ s₂ s₃ s₄ s₅ s₆ s₇ s₈ : String) : Name :=
+@[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. -/
@@ -4464,7 +4455,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.
 -/
-@[expose] def SyntaxNodeKinds := List SyntaxNodeKind
+def SyntaxNodeKinds := List SyntaxNodeKind
 
 /--
 Typed syntax, which tracks the potential kinds of the `Syntax` it contains.
@@ -5149,13 +5140,11 @@ end Syntax
 namespace Macro
 
 /-- References -/
--- TODO: make private again and make Nonempty instance no_expose instead after bootstrapping
-opaque MethodsRefPointed : NonemptyType.{0}
+private opaque MethodsRefPointed : NonemptyType.{0}
 
-set_option linter.missingDocs false in
-@[expose] def MethodsRef : Type := MethodsRefPointed.type
+private def MethodsRef : Type := MethodsRefPointed.type
 
-instance : Nonempty MethodsRef := MethodsRefPointed.property
+private instance : Nonempty MethodsRef := MethodsRefPointed.property
 
 /-- The read-only context for the `MacroM` monad. -/
 structure Context where

src/Init/System/IO.lean

@@ -1014,10 +1014,7 @@ inductive FileType where
   | dir
   /-- Ordinary files that have contents and are not directories. -/
   | file
-  /--
-  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.
-  -/
+  /-- Symbolic links that are pointers to other named files. -/
   | symlink
   /-- Files that are neither ordinary files, directories, or symbolic links. -/
   | other
@@ -1039,8 +1036,7 @@ instance : LE SystemTime := leOfOrd
 /--
 File metadata.
 
-The metadata for a file can be accessed with `System.FilePath.metadata`/
-`System.FilePath.symlinkMetadata`.
+The metadata for a file can be accessed with `System.FilePath.metadata`.
 -/
 structure Metadata where
   --permissions : ...
@@ -1070,22 +1066,14 @@ is not a directory.
 opaque readDir : @& FilePath → IO (Array IO.FS.DirEntry)
 
 /--
-Returns metadata for the indicated file, following symlinks. Throws an exception if the file does
-not exist or the metadata cannot be accessed.
+Returns metadata for the indicated file. 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
 
 /--
-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.
+Checks whether the indicated path can be read and is a directory.
 -/
 def isDir (p : FilePath) : BaseIO Bool := do
   match (← p.metadata.toBaseIO) with
@@ -1093,8 +1081,7 @@ def isDir (p : FilePath) : BaseIO Bool := do
   | Except.error _ => return false
 
 /--
-Checks whether the indicated path points to a file that exists. This function will traverse
-symlinks.
+Checks whether the indicated path points to a file that exists.
 -/
 def pathExists (p : FilePath) : BaseIO Bool :=
   return (← p.metadata.toBaseIO).toBool
@@ -1256,14 +1243,11 @@ 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.
-Symlinks are deleted but not followed. 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.
+  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
-    -- Do not follow symlinks
-    if (← ent.path.symlinkMetadata).type == .dir then
+    if (← ent.path.isDir : Bool) then
       removeDirAll ent.path
     else
       removeFile ent.path
@@ -1484,9 +1468,7 @@ 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 s!"process '{args.cmd}' exited with code {out.exitCode}\
-      \nstderr:\
-      \n{out.stderr}"
+    throw <| IO.userError <| "process '" ++ args.cmd ++ "' exited with code " ++ toString out.exitCode
   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] def mkPanicMessage (modName : String) (line col : Nat) (msg : String) : String :=
+@[noinline] private 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] def mkPanicMessageWithDecl (modName : String) (declName : String) (line col : Nat) (msg : String) : String :=
+@[noinline, expose] private 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,8 +157,14 @@ end Subrelation
 namespace InvImage
 variable {α : Sort u} {β : Sort v} {r : β → β → Prop}
 
-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)
+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` for `WellFounded.fix`
 def accessible {a : α} (f : α → β) (ac : Acc r (f a)) : Acc (InvImage r f) a :=

src/Lean/AddDecl.lean

@@ -108,22 +108,17 @@ def addDecl (decl : Declaration) : CoreM Unit := do
     | .axiomDecl ax => pure (ax.name, .axiomInfo ax, .axiom)
     | _ => return (← addSynchronously)
 
-  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
+  -- preserve original constant kind in extension if different from exported one
+  if exportedInfo?.isSome then
+    modifyEnv (privateConstKindsExt.insert · name kind)
 
   -- 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))
+    (exportedKind := exportedInfo?.map (.ofConstantInfo) |>.getD kind)
   -- report preliminary constant info immediately
-  async.commitConst async.asyncEnv (some info) (exportedInfo? <|> info)
+  async.commitConst async.asyncEnv (some info) exportedInfo?
   setEnv async.mainEnv
   let cancelTk ← IO.CancelToken.new
   let checkAct ← Core.wrapAsyncAsSnapshot (cancelTk? := cancelTk) fun _ => do

src/Lean/Compiler/ImplementedByAttr.lean

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

src/Lean/Compiler/LCNF/ExtractClosed.lean

@@ -63,7 +63,7 @@ partial def shouldExtractLetValue (isRoot : Bool) (v : LetValue) : M Bool := do
   | .lit (.nat v) =>
     -- The old compiler's implementation used the runtime's `is_scalar` function, which
     -- introduces a dependency on the architecture used by the compiler.
-    return !isRoot || v >= Nat.pow 2 63
+    return v >= Nat.pow 2 63
   | .lit _ | .erased => return !isRoot
   | .const name _ args =>
     if (← read).sccDecls.any (·.name == name) then

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

@@ -331,8 +331,7 @@ 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)]),
-  -- 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.
+  (``Nat.mul,    Folder.first #[Folder.mkBinary Nat.mul, Folder.leftRightNeutral 1, Folder.leftRightAnnihilator 0 0, Folder.mulShift ``Nat.shiftLeft (Nat.pow 2) Nat.log2]),
   (``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,13 +32,10 @@ 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' =>
-    /- 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)
+  | .const declName us args' => return .const declName us (args' ++ args)
   | .erased => return .erased
   | .proj .. | .lit .. => failure
 

src/Lean/Compiler/LCNF/Specialize.lean

@@ -80,13 +80,6 @@ def isGround [TraverseFVar α] (e : α) : SpecializeM Bool := do
   let fvarId := decl.fvarId
   withReader (fun { scope, ground, declName } => { declName, scope := scope.insert fvarId, ground := if grd then ground.insert fvarId else ground }) x
 
-@[inline] def withFunDecl (decl : FunDecl) (x : SpecializeM α) : SpecializeM α := do
-  let ctx ← read
-  let grd := allFVar (x := decl.value) fun fvarId =>
-    !(ctx.scope.contains fvarId) || ctx.ground.contains fvarId
-  let fvarId := decl.fvarId
-  withReader (fun { scope, ground, declName } => { declName, scope := scope.insert fvarId, ground := if grd then ground.insert fvarId else ground }) x
-
 namespace Collector
 /-!
 # Dependency collector for the code specialization function.
@@ -268,12 +261,8 @@ def getRemainingArgs (paramsInfo : Array SpecParamInfo) (args : Array Arg) : Arr
       result := result.push arg
   return result ++ args[paramsInfo.size:]
 
-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
+def paramsToVarSet (params : Array Param) : FVarIdSet :=
+  params.foldl (fun r p => r.insert p.fvarId) {}
 
 mutual
   /--
@@ -309,7 +298,7 @@ mutual
       specDecl.saveBase
       let specDecl ← specDecl.simp {}
       let specDecl ← specDecl.simp { etaPoly := true, inlinePartial := true, implementedBy := true }
-      let ground ← paramsToGroundVars specDecl.params
+      let ground := paramsToVarSet specDecl.params
       let value ← withReader (fun _ => { declName := specDecl.name, ground }) do
          withParams specDecl.params <| specDecl.value.mapCodeM visitCode
       let specDecl := { specDecl with value }
@@ -328,11 +317,7 @@ mutual
         decl ← decl.updateValue value
       let k ← withLetDecl decl <| visitCode k
       return code.updateLet! decl k
-    | .fun decl k =>
-      let decl ← visitFunDecl decl
-      let k ← withFunDecl decl <| visitCode k
-      return code.updateFun! decl k
-    | .jp decl k =>
+    | .fun decl k | .jp decl k =>
       let decl ← visitFunDecl decl
       let k ← withFVar decl.fvarId <| visitCode k
       return code.updateFun! decl k
@@ -356,7 +341,7 @@ def main (decl : Decl) : SpecializeM Decl := do
 end Specialize
 
 partial def Decl.specialize (decl : Decl) : CompilerM (Array Decl) := do
-  let ground ← Specialize.paramsToGroundVars decl.params
+  let ground := Specialize.paramsToVarSet 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 : FVarIdHashSet := {}
+  typeParams : FVarIdSet := {}
   noncomputableVars : FVarIdMap Name := {}
 
 abbrev ToMonoM := StateRefT ToMonoM.State CompilerM
 
 def Param.toMono (param : Param) : ToMonoM Param := do
   if isTypeFormerType param.type then
-    modify fun s => { s with typeParams := s.typeParams.insert param.fvarId }
+    modify fun { typeParams, .. } => { typeParams := typeParams.insert param.fvarId }
   param.update (← toMonoType param.type)
 
 def isTrivialConstructorApp? (declName : Name) (args : Array Arg) : ToMonoM (Option LetValue) := do

src/Lean/Elab/App.lean

@@ -1191,12 +1191,6 @@ 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
@@ -1512,19 +1506,15 @@ where
     let resultTypeFn := resultType.cleanupAnnotations.getAppFn
     try
       tryPostponeIfMVar resultTypeFn
-      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}"
+      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}"
     catch
       | ex@(.error ..) =>
         match (← unfoldDefinition? resultType) with

src/Lean/Elab/BuiltinCommand.lean

@@ -546,9 +546,4 @@ 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 (isolateStderr := Core.stderrAsMessages.get (← getOptions)) do
+  let (output, exOrRes) ← IO.FS.withIsolatedStreams 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,10 +155,7 @@ private def getMVarFromUserName (ident : Syntax) : MetaM Expr := do
 @[builtin_term_elab byTactic] def elabByTactic : TermElab := fun stx expectedType? => do
   match expectedType? with
   | some expectedType =>
-    -- `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)
+    mkTacticMVar expectedType stx .term
   | none =>
     tryPostpone
     throwError ("invalid 'by' tactic, expected type has not been provided")
@@ -375,10 +372,7 @@ private opaque evalFilePath (stx : Syntax) : TermElabM System.FilePath
       let name ← mkAuxDeclName `_private
       withoutExporting do
         let e ← elabTerm e expectedType?
-        -- 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
+        mkAuxDefinitionFor name e
     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₂))
-  `(def $(mkIdent auxFunName):ident $binders:bracketedBinder* : $type:term := $body:term
+  `(private 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
-    `(partial def $(mkIdent auxFunName):ident $binders:bracketedBinder* : UInt64 := $body:term)
+    `(private partial def $(mkIdent auxFunName):ident $binders:bracketedBinder* : UInt64 := $body:term)
   else
-    `(def $(mkIdent auxFunName):ident $binders:bracketedBinder* : UInt64 := $body:term)
+    `(private 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
-    `(partial def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Ordering := $body:term)
+    `(private partial def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Ordering := $body:term)
   else
-    `(def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Ordering := $body:term)
+    `(private 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
-    `(partial def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Format := $body:term)
+    `(private partial def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Format := $body:term)
   else
-    `(def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Format := $body:term)
+    `(private 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,9 +105,6 @@ 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`.
@@ -116,7 +113,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, ngen := info.ngen }
+      { env := info.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,7 +1069,6 @@ 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
@@ -1103,8 +1102,7 @@ where
     processDeriving headers
   elabAsync header view declId := do
     let env ← getEnv
-    let async ← env.addConstAsync declId.declName .thm
-      (exportedKind? := guard (!isPrivateName declId.declName) *> some .axiom)
+    let async ← env.addConstAsync declId.declName .thm (exportedKind := .axiom)
     setEnv async.mainEnv
 
     -- TODO: parallelize header elaboration as well? Would have to refactor auto implicits catch,
@@ -1165,16 +1163,14 @@ 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 :=
-      !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
+  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
     let headers := headers.map fun header =>
-      { header with modifiers.attrs := header.modifiers.attrs.filter (!·.name ∈ [`expose, `no_expose]) }
+      { header with modifiers.attrs := header.modifiers.attrs.filter (·.name != `expose) }
     for view in views, funFVar in funFVars do
       addLocalVarInfo view.declId funFVar
     let values ← try

src/Lean/Elab/MutualInductive.lean

@@ -952,7 +952,6 @@ 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 := mkEqnThmName declName (i+1)
+    let name := (Name.str declName eqnThmSuffixBase).appendIndexAfter (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 := mkEqnThmName baseName (i+1)
+    let name := (Name.str baseName eqnThmSuffixBase).appendIndexAfter (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,7 +9,6 @@ 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)
@@ -216,7 +215,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}"
@@ -227,11 +226,6 @@ 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.
 
 /--
@@ -348,18 +342,11 @@ mutual
   -/
   partial def runTactic (mvarId : MVarId) (tacticCode : Syntax) (kind : TacticMVarKind) (report := true) : TermElabM Unit := withoutAutoBoundImplicit do
     -- exit exporting context if entering proof
-    let isNoLongerExporting ← pure (← getEnv).isExporting <&&> do
+    let isExporting ← pure (← getEnv).isExporting <&&> do
       mvarId.withContext do
-        isProp (← mvarId.getType)
+        return !(← isProp (← mvarId.getType))
+    withExporting (isExporting := isExporting) do
     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.
@@ -375,7 +362,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)
@@ -390,18 +377,12 @@ mutual
               kind.logError tacticCode
               reportUnsolvedGoals remainingGoals
             else
-              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)
+              throwError "unsolved goals\n{goalsToMessageData remainingGoals}")
       fun ex => do
         if report then
           kind.logError tacticCode
         if report && (← read).errToSorry then
-          for mvarId in (← getMVars (mkMVar mvarId')) do
+          for mvarId in (← getMVars (mkMVar mvarId)) do
             mvarId.admit
           logException ex
         else
@@ -427,9 +408,9 @@ mutual
       return false
     -- NOTE: actual processing at `synthesizeSyntheticMVarsAux`
     | .postponed savedContext => resumePostponed savedContext mvarSyntheticDecl.stx mvarId postponeOnError
-    | .tactic tacticCode savedContext kind delayOnMVars =>
+    | .tactic tacticCode savedContext kind =>
       withSavedContext savedContext do
-        if runTactics && !(delayOnMVars && (← mvarId.getType >>= instantiateExprMVars).hasExprMVar) then
+        if runTactics then
           runTactic mvarId tacticCode kind
           return true
         else

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 false)
+            params ← withRef p <| addEMatchTheorem params ctor .default
         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 false)
+              params ← withRef p <| addEMatchTheorem params ctor .default
         else
-          params ← withRef p <| addEMatchTheorem params declName (.default false)
+          params ← withRef p <| addEMatchTheorem params declName .default
     | _ => throwError "unexpected `grind` parameter{indentD p}"
   return params
 where
@@ -108,16 +108,15 @@ where
     let info ← getConstInfo declName
     match info with
     | .thmInfo _ | .axiomInfo _ | .ctorInfo _ =>
-      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)) }
-      | _ =>
+      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
         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.isEqLhs && !kind.isDefault then
+      if kind != .eqLhs && kind != .default 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}`"
@@ -224,21 +223,16 @@ def mkGrindOnly
       else
         let decl : Ident := mkIdent (← unresolveNameGlobalAvoidingLocals declName)
         let param ← match kind with
-          | .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)
+          | .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)
         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) (generalized : Array FVarId := #[]) (toClear : Array FVarId := #[])
+    (numEqs : Nat := 0) (numGeneralized : Nat := 0) (toClear : Array FVarId := #[])
     (toTag : Array (Ident × FVarId) := #[]) : TacticM Unit := do
   let hasAlts := altStxs?.isSome
   if hasAlts then
@@ -421,17 +421,9 @@ 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
-        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'
+        (_, altMVarId) ← altMVarId'.introNP numGeneralized
+        pure altMVarId
       else
         pure altMVarId'
       for fvarId in toClear do
@@ -470,17 +462,9 @@ 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
-      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'
+      (_, altMVarId) ← altMVarId'.introNP numGeneralized
+      pure altMVarId
     else
       pure altMVarId'
     for fvarId in toClear do
@@ -542,7 +526,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 (Array FVarId × MVarId) :=
+private def generalizeVars (mvarId : MVarId) (stx : Syntax) (targets : Array Expr) : TacticM (Nat × MVarId) :=
   mvarId.withContext do
     let userFVarIds ← getUserGeneralizingFVarIds stx
     let forbidden ← mkGeneralizationForbiddenSet targets
@@ -555,7 +539,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, mvarId')
+    return (fvarIds.size, mvarId')
 
 /--
 Given `inductionAlts` of the form
@@ -881,7 +865,7 @@ private def evalInductionCore (stx : Syntax) (elimInfo : ElimInfo) (targets : Ar
   mvarId.withContext do
     checkInductionTargets targets
     let targetFVarIds := targets.map (·.fvarId!)
-    let (generalized, mvarId) ← generalizeVars mvarId stx targets
+    let (n, mvarId) ← generalizeVars mvarId stx targets
     mvarId.withContext do
       let result ← withRef stx[1] do -- use target position as reference
         ElimApp.mkElimApp elimInfo targets tag
@@ -895,7 +879,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]
-          (generalized := generalized) (toClear := targetFVarIds) (toTag := toTag)
+          (numGeneralized := n) (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):ident)
+    `(Parser.Tactic.grindParam| = $(← toIdent declName))
 
 private def mkGrindStx (info : Try.Info) : MetaM (TSyntax `tactic) := do
   let grind ← `(tactic| grind?)

src/Lean/Elab/Term.lean

@@ -59,13 +59,8 @@ 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.
-
-  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)
+  /-- Use tactic to synthesize value for metavariable. -/
+  | tactic (tacticCode : Syntax) (ctx : SavedContext) (kind : TacticMVarKind)
   /-- Metavariable represents a hole whose elaboration has been postponed. -/
   | postponed (ctx : SavedContext)
   deriving Inhabited
@@ -1268,15 +1263,14 @@ 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)
-    (delayOnMVars := false) : TermElabM Expr := do
+def mkTacticMVar (type : Expr) (tacticCode : Syntax) (kind : TacticMVarKind) : 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 <| .tactic tacticCode (← saveContext) kind delayOnMVars
+    registerSyntheticMVar ref mvarId <| SyntheticMVarKind.tactic tacticCode (← saveContext) kind
     return mvar
 
 /--

src/Lean/Environment.lean

@@ -585,16 +585,6 @@ 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
 
@@ -608,12 +598,9 @@ def ofKernelEnv (env : Kernel.Environment) : Environment :=
 def toKernelEnv (env : Environment) : Kernel.Environment :=
   env.checked.get
 
-/-- Updates `env.isExporting`. Ignored if `env.header.isModule` is false. -/
+/-- Updates `Environment.isExporting`. -/
 def setExporting (env : Environment) (isExporting : Bool) : Environment :=
-  if !env.header.isModule || env.isExporting == isExporting then
-    env
-  else
-    { env with isExporting }
+  { 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 :=
@@ -702,6 +689,17 @@ 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
@@ -801,9 +799,7 @@ be triggered if any.
 -/
 def enableRealizationsForConst (env : Environment) (opts : Options) (c : Name) :
     BaseIO Environment := do
-  -- 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
+  if env.findAsync? c |>.isNone then
     panic! s!"declaration {c} not found in environment"
     return env
   if let some asyncCtx := env.asyncCtx? then
@@ -917,7 +913,6 @@ 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
@@ -950,13 +945,9 @@ 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? : Option ConstantKind := some kind) (reportExts := true) (checkMayContain := true) :
+    (exportedKind := kind) (reportExts := true) (checkMayContain := true) :
     IO AddConstAsyncResult := do
   if checkMayContain then
     if let some ctx := env.asyncCtx? then
@@ -985,7 +976,7 @@ def addConstAsync (env : Environment) (constName : Name) (kind : ConstantKind)
       | some v => .mk v.nestedConsts.private
       | none   => .mk (α := AsyncConsts) default
   }
-  let exportedAsyncConst? := exportedKind?.map fun exportedKind => { privateAsyncConst with
+  let exportedAsyncConst := { privateAsyncConst with
     constInfo := { privateAsyncConst.constInfo with
       kind := exportedKind
       constInfo := constPromise.result?.map (sync := true) fun
@@ -997,12 +988,11 @@ def addConstAsync (env : Environment) (constName : Name) (kind : ConstantKind)
       | none   => .mk (α := AsyncConsts) default
   }
   return {
-    constName, kind, exportedKind?
+    constName, kind
     mainEnv := { env with
       asyncConstsMap := {
         «private» := env.asyncConstsMap.private.add privateAsyncConst
-        «public»  := exportedAsyncConst?.map (env.asyncConstsMap.public.add ·)
-          |>.getD env.asyncConstsMap.public
+        «public»  := env.asyncConstsMap.public.add exportedAsyncConst
       }
       checked := checkedEnvPromise.result?.bind (sync := true) fun
         | some kenv => .pure kenv
@@ -1034,7 +1024,6 @@ 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 =>
@@ -1048,13 +1037,10 @@ 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
@@ -1094,18 +1080,15 @@ not block.
 def containsOnBranch (env : Environment) (n : Name) : Bool :=
   (env.asyncConsts.find? n |>.isSome) || (env.base.get env).constants.contains n
 
-/--
-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 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
 
 def setMainModule (env : Environment) (m : Name) : Environment := Id.run do
   let env := env.modifyCheckedAsync ({ · with
@@ -2135,7 +2118,6 @@ 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);
@@ -2393,7 +2375,8 @@ 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
-  modifyEnv (·.setExporting isExporting)
+  let isModule := (← getEnv).header.isModule
+  modifyEnv (·.setExporting (isExporting && isModule))
   try
     x
   finally

src/Lean/Expr.lean

@@ -166,13 +166,32 @@ def BinderInfo.toUInt64 : BinderInfo → UInt64
   | .strictImplicit => 2
   | .instImplicit   => 3
 
-@[extern "lean_expr_mk_data"]
-opaque Expr.mkData (h : UInt64) (looseBVarRange : Nat := 0) (approxDepth : UInt32 := 0)
-    (hasFVar hasExprMVar hasLevelMVar hasLevelParam : Bool := false) : Expr.Data
+def Expr.mkData
+    (h : UInt64) (looseBVarRange : Nat := 0) (approxDepth : UInt32 := 0)
+    (hasFVar hasExprMVar hasLevelMVar hasLevelParam : Bool := false)
+    : Expr.Data :=
+  let approxDepth : UInt8 := if approxDepth > 255 then 255 else approxDepth.toUInt8
+  assert! (looseBVarRange ≤ Nat.pow 2 20 - 1)
+  let r : UInt64 :=
+      h.toUInt32.toUInt64 +
+      approxDepth.toUInt64.shiftLeft 32 +
+      hasFVar.toUInt64.shiftLeft 40 +
+      hasExprMVar.toUInt64.shiftLeft 41 +
+      hasLevelMVar.toUInt64.shiftLeft 42 +
+      hasLevelParam.toUInt64.shiftLeft 43 +
+      looseBVarRange.toUInt64.shiftLeft 44
+  r
 
 /-- Optimized version of `Expr.mkData` for applications. -/
-@[extern "lean_expr_mk_app_data"]
-opaque Expr.mkAppData (fData : Data) (aData : Data) : Data
+@[inline] def Expr.mkAppData (fData : Data) (aData : Data) : Data :=
+  let depth          := (max fData.approxDepth.toUInt16 aData.approxDepth.toUInt16) + 1
+  let approxDepth    := if depth > 255 then 255 else depth.toUInt8
+  let looseBVarRange := max fData.looseBVarRange aData.looseBVarRange
+  let hash           := mixHash fData aData
+  let fData : UInt64 := fData
+  let aData : UInt64 := aData
+  assert! (looseBVarRange ≤ (Nat.pow 2 20 - 1).toUInt32)
+  ((fData ||| aData) &&& ((15 : UInt64) <<< (40 : UInt64))) ||| hash.toUInt32.toUInt64 ||| (approxDepth.toUInt64 <<< (32 : UInt64)) ||| (looseBVarRange.toUInt64 <<< (44 : UInt64))
 
 @[inline] def Expr.mkDataForBinder (h : UInt64) (looseBVarRange : Nat) (approxDepth : UInt32) (hasFVar hasExprMVar hasLevelMVar hasLevelParam : Bool) : Expr.Data :=
   Expr.mkData h looseBVarRange approxDepth hasFVar hasExprMVar hasLevelMVar hasLevelParam

src/Lean/Language/Basic.lean

@@ -318,12 +318,12 @@ def SnapshotTree.getAll (s : SnapshotTree) : Array Snapshot :=
   Id.run <| s.foldM (pure <| ·.push ·) #[]
 
 /-- Returns a task that waits on all snapshots in the tree. -/
-partial def SnapshotTree.waitAll : SnapshotTree → BaseIO (Task Unit)
+def SnapshotTree.waitAll : SnapshotTree → BaseIO (Task Unit)
   | mk _ children => go children.toList
 where
   go : List (SnapshotTask SnapshotTree) → BaseIO (Task Unit)
     | [] => return .pure ()
-    | t::ts => BaseIO.bindTask (sync := true) t.task fun t => go (t.children.toList ++ ts)
+    | t::ts => BaseIO.bindTask t.task fun _ => go ts
 
 /-- Context of an input processing invocation. -/
 structure ProcessingContext extends Parser.InputContext

src/Lean/Level.lean

@@ -43,8 +43,11 @@ def Level.Data.hasMVar (c : Level.Data) : Bool :=
 def Level.Data.hasParam (c : Level.Data) : Bool :=
   ((c.shiftRight 33).land 1) == 1
 
-@[extern "lean_level_mk_data"]
-opaque Level.mkData (h : UInt64) (depth : Nat := 0) (hasMVar hasParam : Bool := false) : Level.Data
+def Level.mkData (h : UInt64) (depth : Nat := 0) (hasMVar hasParam : Bool := false) : Level.Data :=
+  if depth > Nat.pow 2 24 - 1 then panic! "universe level depth is too big"
+  else
+    let r : UInt64 := h.toUInt32.toUInt64 + hasMVar.toUInt64.shiftLeft 32 + hasParam.toUInt64.shiftLeft 33 + depth.toUInt64.shiftLeft 40
+    r
 
 instance : Repr Level.Data where
   reprPrec v prec := Id.run do

src/Lean/Message.lean

@@ -349,14 +349,17 @@ def andList (xs : List MessageData) : MessageData :=
 Produces a labeled note that can be appended to an error message.
 -/
 def note (note : MessageData) : MessageData :=
-  Format.line ++ Format.line ++ "Note: " ++ note
+  -- 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
 
 /--
 Produces a labeled hint without an associated code action (non-monadic variant of
 `MessageData.hint`).
 -/
 def hint' (hint : MessageData) : MessageData :=
-  Format.line ++ Format.line ++ "Hint: " ++ hint
+  .tagged `hint <| .compose (.ofFormat .line) <| .compose (.ofFormat .line) <|
+    .compose "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,19 +9,6 @@ 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 :=
@@ -67,8 +54,7 @@ partial def visit (e : Expr) : M Expr := do
       withLCtx lctx localInstances k
     checkCache { val := e : ExprStructEq } fun _ => do
       if (← isNonTrivialProof e) then
-        /- Ensure proofs nested in type are also abstracted -/
-        abstractProof e (← read).cache visit
+        mkAuxLemma e
       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)
@@ -77,6 +63,18 @@ 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,10 +2392,7 @@ where
         let _ : MonadExceptOf _ MetaM := MonadAlwaysExcept.except
         observing do
           realize
-          -- 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
+          if !(← getEnv).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,9 +62,6 @@ 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
@@ -89,9 +86,7 @@ builtin_initialize registerReservedNamePredicate fun env n =>
   match n with
   | .str p s =>
     (isEqnReservedNameSuffix s || s == unfoldThmSuffix || s == eqUnfoldThmSuffix)
-    -- Make equation theorems accessible even when body should not be visible for compatibility.
-    -- TODO: Make them private instead.
-    && (env.setExporting false).isSafeDefinition p
+    && env.isSafeDefinition p
     -- Remark: `f.match_<idx>.eq_<idx>` are handled separately in `Lean.Meta.Match.MatchEqs`.
     && !isMatcherCore env p
   | _ => false
@@ -195,7 +190,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 := mkEqnThmName declName idx
+      let nextEq := declName ++ (`eq).appendIndexAfter idx
       if env.contains nextEq then
         loop (idx+1) (eqs.push nextEq)
       else

src/Lean/Meta/Hint.lean

@@ -66,10 +66,7 @@ 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',
-      style: { display: 'inline-block', verticalAlign: 'text-top' } },
+    { onClick, title: 'Apply suggestion', className: 'link pointer dim font-code', },
     spans)
   return fullDiff
 }"
@@ -77,106 +74,85 @@ 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 × 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 }
+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) }
 
 /--
 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 × String)) : String :=
+private def mkDiffString (ds : Array (Diff.Action × Char)) : String :=
   let rangeStrs := ds.map fun
-    | (.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
+    | (.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]
   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 syntax
-reference provided to `MessageData.hint` will be used.
+hint to suggest modifications at different locations. If `span?` is not specified, then the `ref`
+for the containing `Suggestions` value is used.
 -/
-structure Suggestion extends toTryThisSuggestion : TryThis.Suggestion where
+structure Suggestion extends 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.toTryThisSuggestion
+  toMessageData s := toMessageData s.toSuggestion
 
 /--
-Produces a diff that splits either on characters, tokens, or not at all, depending on the edit
-distance between the arguments.
+A collection of code action suggestions to be included in a hint in a diagnostic message.
 
-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")]`.
+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
 -/
-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])
+structure Suggestions where
+  ref : Syntax
+  suggestions : Array Suggestion
+  codeActionPrefix? : Option String := none
 
 /--
 Creates message data corresponding to a `HintSuggestions` collection and adds the corresponding info
 leaf.
 -/
-def mkSuggestionsMessage (suggestions : Array Suggestion)
-    (ref : Syntax)
-    (codeActionPrefix? : Option String) : CoreM MessageData := do
+def Suggestions.toHintMessage (suggestions : Suggestions) : CoreM MessageData := do
+  let { ref, codeActionPrefix?, suggestions } := suggestions
   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.toTryThisSuggestion] codeActionPrefix?
+      let { info, suggestions := suggestionArr, range := lspRange } ← processSuggestions ref range
+        #[suggestion.toSuggestion] 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 edits := readableDiff rangeContents suggestionText
-      let diffJson := mkDiffJson edits
+      let split (s : String) := s.toList.toArray
+      let edits := Diff.diff (split rangeContents) (split suggestionText)
+      let diff := mkDiffJson edits
       let json := json% {
-        diff: $diffJson,
+        diff: $diff,
         suggestion: $suggestionText,
         range: $lspRange
       }
@@ -188,31 +164,17 @@ def mkSuggestionsMessage (suggestions : Array Suggestion)
           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" ++ MessageData.nest 2 m!"• {widgetMsg}"
+      let suggestionMsg := if suggestions.size == 1 then m!"\n{widgetMsg}" else m!"\n• {widgetMsg}"
       msg := msg ++ MessageData.nestD suggestionMsg
   return msg
 
 /--
-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
+Appends a hint `hint` to `msg`. If `suggestions?` is non-`none`, will also append an inline
+suggestion widget.
 -/
-def _root_.Lean.MessageData.hint (hint : MessageData)
-    (suggestions : Array Suggestion) (ref? : Option Syntax := none)
-    (codeActionPrefix? : Option String := none)
+def _root_.Lean.MessageData.hint (hint : MessageData) (suggestions? : Option Suggestions := none)
     : CoreM MessageData := do
-  let ref := ref?.getD (← getRef)
-  let suggs ← mkSuggestionsMessage suggestions ref codeActionPrefix?
-  return .tagged `hint (m!"\n\nHint: " ++ hint ++ suggs)
+  let mut hintMsg := m!"\n\nHint: {hint}"
+  if let some suggestions := suggestions? then
+    hintMsg := hintMsg ++ (← suggestions.toHintMessage)
+  return .tagged `hint hintMsg

src/Lean/Meta/Injective.lean

@@ -188,7 +188,6 @@ 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,15 +797,7 @@ register_builtin_option bootstrap.genMatcherCode : Bool := {
   descr := "disable code generation for auxiliary matcher function"
 }
 
-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) ←
+builtin_initialize matcherExt : EnvExtension (PHashMap (Expr × Bool) Name) ←
   registerEnvExtension (pure {}) (asyncMode := .local)  -- mere cache, keep it local
 
 /-- Similar to `mkAuxDefinition`, but uses the cache `matcherExt`.
@@ -817,12 +809,7 @@ def mkMatcherAuxDefinition (name : Name) (type : Expr) (value : Expr) : MetaM (E
   let env ← getEnv
   let mkMatcherConst name :=
     mkAppN (mkConst name result.levelArgs.toList) result.exprArgs
-  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
+  match (matcherExt.getState env).find? (result.value, compile) with
   | some nameNew => return (mkMatcherConst nameNew, none)
   | none =>
     let decl := Declaration.defnDecl (← mkDefinitionValInferrringUnsafe name result.levelParams.toList
@@ -832,7 +819,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 key name
+      modifyEnv fun env => matcherExt.modifyState env fun s => s.insert (result.value, compile) 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 := mkEqnThmName baseName idx
+      let thmName := baseName ++ ((`eq).appendIndexAfter idx)
       eqnNames := eqnNames.push thmName
       let (notAlt, splitterAltType, splitterAltNumParam, argMask) ←
           forallAltTelescope (← inferType alts[i]!) altNumParams numDiscrEqs

src/Lean/Meta/SizeOf.lean

@@ -420,7 +420,6 @@ 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
@@ -477,7 +476,6 @@ 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/AlphaShareCommon.lean

@@ -13,7 +13,7 @@ private def hashChild (e : Expr) : UInt64 :=
   | .bvar .. | .mvar .. | .const .. | .fvar .. | .sort .. | .lit .. =>
     hash e
   | .app .. | .letE .. | .forallE .. | .lam .. | .mdata .. | .proj .. =>
-    hashPtrExpr e
+    (unsafe ptrAddrUnsafe e).toUInt64
 
 private def alphaHash (e : Expr) : UInt64 :=
   match e with

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

@@ -27,19 +27,9 @@ private def getType? (e : Expr) : Option Expr :=
 
 private def isForbiddenParent (parent? : Option Expr) : Bool :=
   if let some parent := parent? then
-    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
+    getType? parent |>.isSome
   else
-    true
+    false
 
 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 a =>
+    | IntCast.intCast _ i e =>
       if isIntCastInst (← getRing) i then
-        let some k ← getIntValue? a | toVar e
+        let some k ← getIntValue? e | toVar e
         return .num k
       else
         asVar e
-    | NatCast.natCast _ i a =>
+    | NatCast.natCast _ i e =>
       if isNatCastInst (← getRing) i then
-        let some k ← getNatValue? a | toVar e
+        let some k ← getNatValue? e | 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 k ← getIntValue? a then
-    return .num k
-  else if let some var := (← get').varMap.find? { expr := a } then
+  if let some var := (← get').varMap.find? { expr := a } then
     return .add 1 var (.num 0)
+  else if let some k ← getIntValue? a then
+    return .num k
   else
     throwError "internal `grind` error, expression is not relevant to cutsat{indentExpr a}"
 
@@ -259,6 +259,23 @@ 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
@@ -288,7 +305,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 | pow | natAbs | toNat
+  | add | mul | num | div | mod | sub | natAbs | toNat
   deriving BEq
 
 private def getKindAndType? (e : Expr) : Option (SupportedTermKind × Expr) :=
@@ -298,7 +315,6 @@ 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
@@ -313,14 +329,12 @@ 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 | .pow | .natAbs | .toNat then return false
+  if k matches .div | .mod | .sub | .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 =>
-    -- Recall that we don't want to internalize numerals occurring at terms such as `x^3`.
-    return declName == ``HMul.hMul || declName == ``HPow.hPow
+  | .num => return declName == ``HMul.hMul || declName == ``Eq
   | _ => unreachable!
 
 private def internalizeInt (e : Expr) : GoalM Unit := do
@@ -399,7 +413,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`.
 -/
@@ -411,6 +425,7 @@ 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 ()
@@ -419,6 +434,7 @@ 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,7 +130,6 @@ 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
@@ -147,7 +146,6 @@ 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/Arith/Offset/Main.lean

@@ -339,7 +339,9 @@ def internalize (e : Expr) (parent? : Option Expr) : GoalM Unit := do
     if let some (b, k) := isNatOffset? e then
       internalizeTerm e b k
     else if let some k := isNatNum? e then
-      internalizeTerm e z k
+      -- core module has support for detecting equality between literals
+      unless isEqParent parent? do
+        internalizeTerm e z k
 
 @[export lean_process_new_offset_eq]
 def processNewEqImpl (a b : Expr) : GoalM Unit := do
@@ -351,6 +353,17 @@ def processNewEqImpl (a b : Expr) : GoalM Unit := do
     addEdge u v 0 <| mkApp3 (mkConst ``Grind.Nat.le_of_eq_1) a b h
     addEdge v u 0 <| mkApp3 (mkConst ``Grind.Nat.le_of_eq_2) a b h
 
+@[export lean_process_new_offset_eq_lit]
+def processNewEqLitImpl (a b : Expr) : GoalM Unit := do
+  unless isSameExpr a b do
+    trace[grind.offset.eq.to] "{a}, {b}"
+    let some k := isNatNum? b | unreachable!
+    let u ← getNodeId a
+    let z ← mkNode (← getNatZeroExpr)
+    let h ← mkEqProof a b
+    addEdge u z k <| mkApp3 (mkConst ``Grind.Nat.le_of_eq_1) a b h
+    addEdge z u (-k) <| mkApp3 (mkConst ``Grind.Nat.le_of_eq_2) a b h
+
 def traceDists : GoalM Unit := do
   let s ← get'
   for u in [:s.targets.size], es in s.targets.toArray do

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

@@ -20,24 +20,19 @@ 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 false)
-  | `(Parser.Attr.grindMod| = gen) => return .ematch (.eqLhs true)
+  | `(Parser.Attr.grindMod| =) => return .ematch .eqLhs
   | `(Parser.Attr.grindMod| →)
   | `(Parser.Attr.grindMod| ->) => return .ematch .fwd
   | `(Parser.Attr.grindMod| ←)
-  | `(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 .bwd
+  | `(Parser.Attr.grindMod| =_) => return .ematch .eqRhs
+  | `(Parser.Attr.grindMod| _=_) => return .ematch .eqBoth
   | `(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
@@ -92,7 +87,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 false) (showInfo := showInfo)
+            addEMatchAttr ctor attrKind .default (showInfo := showInfo)
         else
           throwError "invalid `[grind intro]`, `{declName}` is not an inductive predicate"
       | .ext => addExtAttr declName attrKind
@@ -103,9 +98,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 false) (showInfo := showInfo)
+              addEMatchAttr ctor attrKind .default (showInfo := showInfo)
         else
-          addEMatchAttr declName attrKind (.default false) (showInfo := showInfo)
+          addEMatchAttr declName attrKind .default (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,6 +113,14 @@ 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)
 
@@ -125,15 +133,22 @@ private def checkOffsetEq (rhsRoot lhsRoot : ENode) : GoalM PendingTheoryPropaga
   | some lhsOffset =>
     if let some rhsOffset := rhsRoot.offset? then
       return .eq lhsOffset rhsOffset
+    else if isNatNum rhsRoot.self then
+      return .eqLit lhsOffset 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 offset? := lhsOffset }
       return .none
-  | none => return .none
+  | none =>
+    if isNatNum lhsRoot.self then
+      if let some rhsOffset := rhsRoot.offset? then
+        return .eqLit rhsOffset lhsRoot.self
+    return .none
 
 def propagateOffset : PendingTheoryPropagation → GoalM Unit
   | .eq lhs rhs => Arith.Offset.processNewEq lhs rhs
+  | .eqLit lhs lit => Arith.Offset.processNewEqLit lhs lit
   | _ => return ()
 
 /--
@@ -145,19 +160,25 @@ 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 rhsRoot.cutsat?.isSome then
-      return .diseqs (← getParents lhsRoot.self)
+    if let some rhsCutsat := rhsRoot.cutsat? then
+      if isNum lhsRoot.self then
+        return .eqLit rhsCutsat lhsRoot.self
+      else
+        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,61 +148,18 @@ 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) (gen : Bool) : MetaM Expr := do
+private def inferEMatchProofType (proof : Expr) : 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`
@@ -253,53 +210,31 @@ instance : Hashable Origin where
   hash a := hash a.key
 
 inductive EMatchTheoremKind where
-  | 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 -/
+  | eqLhs | eqRhs | eqBoth | eqBwd | fwd | bwd | leftRight | rightLeft | default | 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 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]"
+  | .eqLhs     => "[grind =]"
+  | .eqRhs     => "[grind =_]"
+  | .eqBoth    => "[grind _=_]"
+  | .eqBwd     => "[grind ←=]"
+  | .fwd       => "[grind →]"
+  | .bwd       => "[grind ←]"
+  | .leftRight => "[grind =>]"
+  | .rightLeft => "[grind <=]"
+  | .default   => "[grind]"
+  | .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. -/
@@ -505,10 +440,6 @@ 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 }
 
@@ -816,8 +747,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) (gen : Bool) (showInfo := false) : MetaM EMatchTheorem := do
-  let (numParams, patterns) ← forallTelescopeReducing (← inferEMatchProofType proof gen) fun xs type => do
+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
     let (lhs, rhs) ← match_expr type with
       | Eq _ lhs rhs => pure (lhs, rhs)
       | Iff lhs rhs => pure (lhs, rhs)
@@ -829,10 +760,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 gen else .eqRhs gen) (showInfo := showInfo)
+  mkEMatchTheoremCore origin levelParams numParams proof patterns (if useLhs then .eqLhs else .eqRhs) (showInfo := showInfo)
 
 def mkEMatchEqBwdTheoremCore (origin : Origin) (levelParams : Array Name) (proof : Expr) (showInfo := false) : MetaM EMatchTheorem := do
-  let (numParams, patterns) ← forallTelescopeReducing (← inferEMatchProofType proof (gen := false)) fun xs type => do
+  let (numParams, patterns) ← forallTelescopeReducing (← inferEMatchProofType proof) 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)
@@ -846,8 +777,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) (gen : Bool := false) (showInfo := false) : MetaM EMatchTheorem := do
-  mkEMatchEqTheoremCore (.decl declName) #[] (← getProofFor declName) normalizePattern useLhs gen (showInfo := showInfo)
+def mkEMatchEqTheorem (declName : Name) (normalizePattern := true) (useLhs : Bool := true) (showInfo := false) : MetaM EMatchTheorem := do
+  mkEMatchEqTheoremCore (.decl declName) #[] (← getProofFor declName) normalizePattern useLhs (showInfo := showInfo)
 
 /--
 Adds an E-matching theorem to the environment.
@@ -1025,15 +956,6 @@ 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
@@ -1043,16 +965,13 @@ 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
-  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 =>
+  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
     return (← mkEMatchEqBwdTheoremCore origin levelParams proof (showInfo := showInfo))
-  | _ =>
-    pure ()
-  let type ← inferEMatchProofType proof kind.gen
+  let type ← inferEMatchProofType proof
   /-
   Remark: we should not use `forallTelescopeReducing` (with default reducibility) here
   because it may unfold a definition/abstraction, and then select a suboptimal pattern.
@@ -1077,10 +996,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
@@ -1113,7 +1032,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) (gen := thmKind.gen) (showInfo := showInfo)) attrKind
+    ematchTheoremsExt.add (← mkEMatchEqTheorem declName (normalizePattern := true) (useLhs := useLhs) (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"
@@ -1138,15 +1057,14 @@ 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
-  match thmKind with
-  | .eqLhs _ =>
+  if thmKind == .eqLhs then
     addGrindEqAttr declName attrKind thmKind (useLhs := true) (showInfo := showInfo)
-  | .eqRhs _ =>
+  else if thmKind == .eqRhs then
     addGrindEqAttr declName attrKind thmKind (useLhs := false) (showInfo := showInfo)
-  | .eqBoth _ =>
+  else if thmKind == .eqBoth then
     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/ENodeKey.lean

@@ -21,11 +21,8 @@ have been hash-consed, i.e., we have applied `shareCommon`.
 structure ENodeKey where
   expr : Expr
 
-abbrev hashPtrExpr (e : Expr) : UInt64 :=
-  unsafe (ptrAddrUnsafe e >>> 3).toUInt64
-
 instance : Hashable ENodeKey where
-  hash k := hashPtrExpr k.expr
+  hash k := unsafe (ptrAddrUnsafe k.expr).toUInt64
 
 instance : BEq ENodeKey where
   beq k₁ k₂ := isSameExpr k₁.expr k₂.expr

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 false) then
+    if let some thm ← mkEMatchTheoremWithKind'? origin proof .default 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/Internalize.lean

@@ -62,7 +62,7 @@ def isMorallyIff (e : Expr) : Bool :=
 private def checkAndAddSplitCandidate (e : Expr) : GoalM Unit := do
   match h : e with
   | .app .. =>
-    if (← getConfig).splitIte && (isIte e || isDIte e) then
+    if (← getConfig).splitIte && (e.isIte || e.isDIte) then
       addSplitCandidate (.default e)
       return ()
     if isMorallyIff e then
@@ -87,7 +87,7 @@ private def checkAndAddSplitCandidate (e : Expr) : GoalM Unit := do
       else if (← getConfig).splitIndPred then
         addSplitCandidate (.default e)
   | .fvar .. =>
-    let .const declName _ := (← whnf (← inferType e)).getAppFn | return ()
+    let .const declName _ := (← whnfD (← inferType e)).getAppFn | return ()
     if (← get).split.casesTypes.isSplit declName then
       addSplitCandidate (.default e)
   | .forallE _ d _ _ =>
@@ -201,7 +201,7 @@ these facts.
 -/
 private def propagateEtaStruct (a : Expr) (generation : Nat) : GoalM Unit := do
   unless (← getConfig).etaStruct do return ()
-  let aType ← whnf (← inferType a)
+  let aType ← whnfD (← inferType a)
   matchConstStructureLike aType.getAppFn (fun _ => return ()) fun inductVal us ctorVal => do
     unless a.isAppOf ctorVal.name do
       -- TODO: remove ctorVal.numFields after update stage0
@@ -215,9 +215,7 @@ private def propagateEtaStruct (a : Expr) (generation : Nat) : GoalM Unit := do
           ctorApp := mkApp ctorApp proj
         ctorApp ← preprocessLight ctorApp
         internalize ctorApp generation
-        let u ← getLevel aType
-        let expectedProp := mkApp3 (mkConst ``Eq [u]) aType a ctorApp
-        pushEq a ctorApp <| mkExpectedPropHint (mkApp2 (mkConst ``Eq.refl [u]) aType a) expectedProp
+        pushEq a ctorApp <| (← mkEqRefl a)
 
 /-- Returns `true` if we can ignore `ext` for functions occurring as arguments of a `declName`-application. -/
 private def extParentsToIgnore (declName : Name) : Bool :=
@@ -368,7 +366,6 @@ where
           let c := args[0]!
           internalizeImpl c generation e
           registerParent e c
-          pushEqTrue c <| mkApp2 (mkConst ``eq_true) c args[1]!
         else if f.isConstOf ``ite && args.size == 5 then
           let c := args[1]!
           internalizeImpl c generation e

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

@@ -173,25 +173,6 @@ builtin_grind_propagator propagateEqDown ↓Eq := fun e => do
       for thm in (← getExtTheorems α) do
         instantiateExtTheorem thm e
 
-private def getLawfulBEqInst? (u : List Level) (α : Expr) (binst : Expr) : MetaM (Option Expr) := do
-  let lawfulBEq := mkApp2 (mkConst ``LawfulBEq u) α binst
-  let .some linst ← trySynthInstance lawfulBEq | return none
-  return some linst
-
-/-
-Note about `BEq.beq`
-Given `a b : α` in a context where we have `[BEq α] [LawfulBEq α]`
-The normalizer (aka `simp`) fails to normalize `if a == b then ... else ...` to `if a = b then ... else ...` using
-```
-theorem beq_iff_eq [BEq α] [LawfulBEq α] {a b : α} : a == b ↔ a = b :=
-  ⟨eq_of_beq, beq_of_eq⟩
-```
-The main issue is that `ite_congr` requires that the resulting proposition to be decidable,
-and we don't have `[DecidableEq α]`. Thus, the normalization step fails.
-The following propagators for `BEq.beq` ensure `grind` does not assume this normalization
-rule has been applied.
--/
-
 builtin_grind_propagator propagateBEqUp ↑BEq.beq := fun e => do
   /-
   `grind` uses the normalization rule `Bool.beq_eq_decide_eq`, but it is only applicable if
@@ -200,27 +181,17 @@ builtin_grind_propagator propagateBEqUp ↑BEq.beq := fun e => do
   Thus, we have added this propagator as a backup.
   -/
   let_expr f@BEq.beq α binst a b := e | return ()
-  let u := f.constLevels!
   if (← isEqv a b) then
-    let some linst ← getLawfulBEqInst? u α binst | return ()
+    let u := f.constLevels!
+    let lawfulBEq := mkApp2 (mkConst ``LawfulBEq u) α binst
+    let .some linst ← trySynthInstance lawfulBEq | return ()
     pushEqBoolTrue e <| mkApp6 (mkConst ``Grind.beq_eq_true_of_eq u) α binst linst a b (← mkEqProof a b)
   else if let some h ← mkDiseqProof? a b then
-    let some linst ← getLawfulBEqInst? u α binst | return ()
+    let u := f.constLevels!
+    let lawfulBEq := mkApp2 (mkConst ``LawfulBEq u) α binst
+    let .some linst ← trySynthInstance lawfulBEq | return ()
     pushEqBoolFalse e <| mkApp6 (mkConst ``Grind.beq_eq_false_of_diseq u) α binst linst a b h
 
-builtin_grind_propagator propagateBEqDown ↓BEq.beq := fun e => do
-  /- See comment above -/
-  let_expr f@BEq.beq α binst a b := e | return ()
-  let u := f.constLevels!
-  if (← isEqBoolTrue e) then
-    let some linst ← getLawfulBEqInst? u α binst | return ()
-    pushEq a b <| mkApp6 (mkConst ``Grind.eq_of_beq_eq_true u) α binst linst a b (← mkEqProof e (← getBoolTrueExpr))
-  else if (← isEqBoolFalse e) then
-    let some linst ← getLawfulBEqInst? u α binst | return ()
-    let eq ← shareCommon (mkApp3 (mkConst ``Eq [u.head!.succ]) α a b)
-    internalize eq (← getGeneration a)
-    pushEqFalse eq <| mkApp6 (mkConst ``Grind.ne_of_beq_eq_false u) α binst linst a b (← mkEqProof e (← getBoolFalseExpr))
-
 /-- Propagates `EqMatch` downwards -/
 builtin_grind_propagator propagateEqMatchDown ↓Grind.EqMatch := fun e => do
   if (← isEqTrue e) then
@@ -240,73 +211,35 @@ builtin_grind_propagator propagateHEqUp ↑HEq := fun e => do
   if (← isEqv a b) then
     pushEqTrue e <| mkEqTrueCore e (← mkHEqProof a b)
 
-/--
-Helper function for propagating over-applied `ite` and `dite`-applications.
-`h` is a proof for the `e`'s prefix (of size `prefixSize`) that is equal to `rhs`.
-`args` contains all arguments of `e`.
-`prefixSize <= args.size`
--/
-private def applyCongrFun (e rhs : Expr) (h : Expr) (prefixSize : Nat) (args : Array Expr) : GoalM Unit := do
-  if prefixSize == args.size then
-    internalize rhs (← getGeneration e)
-    pushEq e rhs h
-  else
-    go rhs h prefixSize
-where
-  go (rhs : Expr) (h : Expr) (i : Nat) : GoalM Unit := do
-    if _h : i < args.size then
-      let arg := args[i]
-      let rhs' := mkApp rhs arg
-      let h' ← mkCongrFun h arg
-      go rhs' h' (i+1)
-    else
-      let rhs ← preprocessLight rhs
-      internalize rhs (← getGeneration e)
-      pushEq e rhs h
-
 /-- Propagates `ite` upwards -/
 builtin_grind_propagator propagateIte ↑ite := fun e => do
-  let numArgs := e.getAppNumArgs
-  if numArgs < 5 then return ()
-  let c := e.getArg! 1 numArgs
+  let_expr f@ite α c h a b := e | return ()
   if (← isEqTrue c) then
-    let f := e.getAppFn
-    let args := e.getAppArgs
-    let rhs := args[3]!
-    let h := mkApp (mkAppRange (mkConst ``ite_cond_eq_true f.constLevels!) 0 5 args) (← mkEqTrueProof c)
-    applyCongrFun e rhs h 5 args
+    internalize a (← getGeneration e)
+    pushEq e a <| mkApp6 (mkConst ``ite_cond_eq_true f.constLevels!) α c h a b (← mkEqTrueProof c)
   else if (← isEqFalse c) then
-    let f := e.getAppFn
-    let args := e.getAppArgs
-    let rhs := args[4]!
-    let h := mkApp (mkAppRange (mkConst ``ite_cond_eq_false f.constLevels!) 0 5 args) (← mkEqFalseProof c)
-    applyCongrFun e rhs h 5 args
+    internalize b (← getGeneration e)
+    pushEq e b <| mkApp6 (mkConst ``ite_cond_eq_false f.constLevels!) α c h a b (← mkEqFalseProof c)
 
 /-- Propagates `dite` upwards -/
 builtin_grind_propagator propagateDIte ↑dite := fun e => do
-  let numArgs := e.getAppNumArgs
-  if numArgs < 5 then return ()
-  let c := e.getArg! 1 numArgs
+  let_expr f@dite α c h a b := e | return ()
   if (← isEqTrue c) then
-    let f := e.getAppFn
-    let args := e.getAppArgs
-    let h₁ ← mkEqTrueProof c
-    let ah₁ := mkApp args[3]! (mkOfEqTrueCore c h₁)
-    let p ← preprocess ah₁
-    let r := p.expr
-    let h₂ ← p.getProof
-    let h := mkApp3 (mkAppRange (mkConst ``Grind.dite_cond_eq_true' f.constLevels!) 0 5 args) r h₁ h₂
-    applyCongrFun e r h 5 args
+     let h₁ ← mkEqTrueProof c
+     let ah₁ := mkApp a (mkOfEqTrueCore c h₁)
+     let p ← preprocess ah₁
+     let r := p.expr
+     let h₂ ← p.getProof
+     internalize r (← getGeneration e)
+     pushEq e r <| mkApp8 (mkConst ``Grind.dite_cond_eq_true' f.constLevels!) α c h a b r h₁ h₂
   else if (← isEqFalse c) then
-    let f := e.getAppFn
-    let args := e.getAppArgs
-    let h₁ ← mkEqFalseProof c
-    let bh₁ := mkApp args[4]! (mkOfEqFalseCore c h₁)
-    let p ← preprocess bh₁
-    let r := p.expr
-    let h₂ ← p.getProof
-    let h := mkApp3 (mkAppRange (mkConst ``Grind.dite_cond_eq_false' f.constLevels!) 0 5 args) r h₁ h₂
-    applyCongrFun e r h 5 args
+     let h₁ ← mkEqFalseProof c
+     let bh₁ := mkApp b (mkOfEqFalseCore c h₁)
+     let p ← preprocess bh₁
+     let r := p.expr
+     let h₂ ← p.getProof
+     internalize r (← getGeneration e)
+     pushEq e r <| mkApp8 (mkConst ``Grind.dite_cond_eq_false' f.constLevels!) α c h a b r h₁ h₂
 
 builtin_grind_propagator propagateDecideDown ↓decide := fun e => do
   let root ← getRootENode e

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

@@ -93,9 +93,9 @@ private def checkDefaultSplitStatus (e : Expr) : GoalM SplitStatus := do
       checkIffStatus e a b
     else
       return .ready 2
+  | ite _ c _ _ _ => checkIteCondStatus c
+  | dite _ c _ _ _ => checkIteCondStatus c
   | _ =>
-    if isIte e || isDIte e then
-      return (← checkIteCondStatus (e.getArg! 1))
     if (← isResolvedCaseSplit e) then
       trace_goal[grind.debug.split] "split resolved: {e}"
       return .resolved
@@ -215,6 +215,8 @@ private def mkGrindEM (c : Expr) :=
 private def mkCasesMajor (c : Expr) : GoalM Expr := do
   match_expr c with
   | And a b => return mkApp3 (mkConst ``Grind.or_of_and_eq_false) a b (← mkEqFalseProof c)
+  | ite _ c _ _ _ => return mkGrindEM c
+  | dite _ c _ _ _ => return mkGrindEM c
   | Eq _ a b =>
     if isMorallyIff c then
       if (← isEqTrue c) then
@@ -226,9 +228,7 @@ private def mkCasesMajor (c : Expr) : GoalM Expr := do
       return mkGrindEM c
   | Not e => return mkGrindEM e
   | _ =>
-    if isIte c || isDIte c then
-      return mkGrindEM (c.getArg! 1)
-    else if (← isEqTrue c) then
+    if (← isEqTrue c) then
       return mkOfEqTrueCore c (← mkEqTrueProof c)
     else
       return c

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

@@ -86,7 +86,7 @@ instance : BEq CongrTheoremCacheKey where
 
 -- We manually define `Hashable` because we want to use pointer equality.
 instance : Hashable CongrTheoremCacheKey where
-  hash a := mixHash (hashPtrExpr a.f) (hash a.numArgs)
+  hash a := mixHash (unsafe ptrAddrUnsafe a.f).toUInt64 (hash a.numArgs)
 
 structure EMatchTheoremTrace where
   origin : Origin
@@ -372,9 +372,9 @@ structure CongrKey (enodes : ENodeMap) where
 
 private def hashRoot (enodes : ENodeMap) (e : Expr) : UInt64 :=
   if let some node := enodes.find? { expr := e } then
-    hashPtrExpr node.root
+    unsafe (ptrAddrUnsafe node.root).toUInt64
   else
-    hashPtrExpr e
+    13
 
 private def hasSameRoot (enodes : ENodeMap) (a b : Expr) : Bool := Id.run do
   if isSameExpr a b then
@@ -461,9 +461,9 @@ structure PreInstance where
 
 instance : Hashable PreInstance where
   hash i := Id.run do
-    let mut r := hashPtrExpr i.proof
+    let mut r := unsafe (ptrAddrUnsafe i.proof >>> 3).toUInt64
     for v in i.assignment do
-      r := mixHash r (hashPtrExpr v)
+      r := mixHash r (unsafe (ptrAddrUnsafe v >>> 3).toUInt64)
     return r
 
 instance : BEq PreInstance where
@@ -957,6 +957,14 @@ Notifies the offset constraint module that `a = b` where
 @[extern "lean_process_new_offset_eq"] -- forward definition
 opaque Arith.Offset.processNewEq (a b : Expr) : GoalM Unit
 
+/--
+Notifies the offset constraint module that `a = k` where
+`a` is term that has been internalized by this module,
+and `k` is a numeral.
+-/
+@[extern "lean_process_new_offset_eq_lit"] -- forward definition
+opaque Arith.Offset.processNewEqLit (a k : Expr) : GoalM Unit
+
 /-- Returns `true` if `e` is a numeral and has type `Nat`. -/
 def isNatNum (e : Expr) : Bool := Id.run do
   let_expr OfNat.ofNat _ _ inst := e | false
@@ -972,6 +980,8 @@ def markAsOffsetTerm (e : Expr) : GoalM Unit := do
   let root ← getRootENode e
   if let some e' := root.offset? then
     Arith.Offset.processNewEq e e'
+  else if isNatNum root.self && !isSameExpr e root.self then
+    Arith.Offset.processNewEqLit e root.self
   else
     setENode root.self { root with offset? := some e }
 
@@ -982,6 +992,13 @@ 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.
@@ -1057,6 +1074,8 @@ 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/Grind/Util.lean

@@ -216,10 +216,4 @@ def replacePreMatchCond (e : Expr) : MetaM Simp.Result := do
     let e' ← Core.transform e (pre := pre)
     return { expr := e', proof? := mkExpectedPropHint (← mkEqRefl e') (← mkEq e e') }
 
-def isIte (e : Expr) :=
-  e.isAppOf ``ite && e.getAppNumArgs >= 5
-
-def isDIte (e : Expr) :=
-  e.isAppOf ``dite && e.getAppNumArgs >= 5
-
 end Lean.Meta.Grind

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 false)
+          | .none => .default
           | .mp => .leftRight
           | .mpr => .rightLeft
         modify fun s => { s with libSearchResults := s.libSearchResults.insert (declName, kind) }

src/Lean/Parser/Command.lean

@@ -523,9 +523,6 @@ 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, Inhabited
+deriving Repr, BEq, Hashable, Repr
 
 instance : ToString Action where
   toString

src/Std/Data/Internal/LawfulMonadLiftFunction.lean

@@ -1,74 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Paul Reichert
--/
-prelude
-import Init.Control.Basic
-import Init.Control.Lawful.Basic
-import Init.NotationExtra
-import Init.Control.Lawful.MonadLift
-
-/-!
-# Typeclass for lawfule monad lifting functions
-
-This module provides a typeclass `LawfulMonadLiftFunction f` that asserts that a function `f`
-mapping values from one monad to another monad commutes with `pure` and `bind`. This equivalent to
-the requirement that the `MonadLift(T)` instance induced by `f` admits a
-`LawfulMonadLift(T)` instance.
--/
-
-namespace Std.Internal
-
-class LawfulMonadLiftFunction {m : Type u → Type v} {n : Type u → Type w}
-    [Monad m] [Monad n] (lift : ⦃α : Type u⦄ → m α → n α) where
-  lift_pure {α : Type u} (a : α) : lift (pure a) = pure a
-  lift_bind {α β : Type u} (ma : m α) (f : α → m β) :
-    lift (ma >>= f) = lift ma >>= (fun x => lift (f x))
-
-instance {m : Type u → Type v} [Monad m] : LawfulMonadLiftFunction (fun ⦃α⦄ => (id : m α → m α)) where
-  lift_pure := by simp
-  lift_bind := by simp
-
-instance {m : Type u → Type v} [Monad m] {n : Type u → Type w} [Monad n] [MonadLiftT m n]
-    [LawfulMonadLiftT m n] :
-    LawfulMonadLiftFunction (fun ⦃α⦄ => (monadLift : m α → n α)) where
-  lift_pure := monadLift_pure
-  lift_bind := monadLift_bind
-
-variable {m : Type u → Type v} {n : Type u → Type w} [Monad m] [Monad n]
-    {lift : ⦃α : Type u⦄ → m α → n α}
-
-theorem LawfulMonadLiftFunction.lift_map [LawfulMonad m] [LawfulMonad n]
-    [LawfulMonadLiftFunction lift] (f : α → β) (ma : m α) :
-    lift (f <$> ma) = f <$> (lift ma : n α) := by
-  rw [← bind_pure_comp, ← bind_pure_comp, lift_bind (lift := lift)]
-  simp only [bind_pure_comp, lift_pure]
-
-theorem LawfulMonadLiftFunction.lift_seq [LawfulMonad m] [LawfulMonad n]
-    [LawfulMonadLiftFunction lift] (mf : m (α → β)) (ma : m α) :
-    lift (mf <*> ma) = lift mf <*> (lift ma : n α) := by
-  simp only [seq_eq_bind, lift_map, lift_bind]
-
-theorem LawfulMonadLiftFunction.lift_seqLeft [LawfulMonad m] [LawfulMonad n]
-    [LawfulMonadLiftFunction lift] (x : m α) (y : m β) :
-    lift (x <* y) = (lift x : n α) <* (lift y : n β) := by
-  simp only [seqLeft_eq, lift_map, lift_seq]
-
-theorem LawfulMonadLiftFunction.lift_seqRight [LawfulMonad m] [LawfulMonad n]
-    [LawfulMonadLiftFunction lift] (x : m α) (y : m β) :
-    lift (x *> y) = (lift x : n α) *> (lift y : n β) := by
-  simp only [seqRight_eq, lift_map, lift_seq]
-
-def instMonadLiftOfFunction {lift : ⦃α : Type u⦄ -> m α → n α} :
-    MonadLift m n where
-  monadLift := lift (α := _)
-
-instance [LawfulMonadLiftFunction lift] :
-    letI : MonadLift m n := ⟨lift (α := _)⟩
-    LawfulMonadLift m n :=
-  letI : MonadLift m n := ⟨lift (α := _)⟩
-  { monadLift_pure := LawfulMonadLiftFunction.lift_pure
-    monadLift_bind := LawfulMonadLiftFunction.lift_bind }
-
-end Std.Internal

src/Std/Data/Iterators.lean

@@ -7,10 +7,8 @@ prelude
 import Std.Data.Iterators.Basic
 import Std.Data.Iterators.Producers
 import Std.Data.Iterators.Consumers
-import Std.Data.Iterators.Combinators
-import Std.Data.Iterators.Lemmas
-import Std.Data.Iterators.PostConditionMonad
 import Std.Data.Iterators.Internal
+import Std.Data.Iterators.Lemmas
 
 /-!
 # Iterators

src/Std/Data/Iterators/Basic.lean

@@ -221,7 +221,7 @@ def PlausibleIterStep (IsPlausibleStep : IterStep α β → Prop) := Subtype IsP
 /--
 Match pattern for the `yield` case. See also `IterStep.yield`.
 -/
-@[match_pattern, simp]
+@[match_pattern]
 def PlausibleIterStep.yield {IsPlausibleStep : IterStep α β → Prop}
     (it' : α) (out : β) (h : IsPlausibleStep (.yield it' out)) :
     PlausibleIterStep IsPlausibleStep :=
@@ -230,7 +230,7 @@ def PlausibleIterStep.yield {IsPlausibleStep : IterStep α β → Prop}
 /--
 Match pattern for the `skip` case. See also `IterStep.skip`.
 -/
-@[match_pattern, simp]
+@[match_pattern]
 def PlausibleIterStep.skip {IsPlausibleStep : IterStep α β → Prop}
     (it' : α) (h : IsPlausibleStep (.skip it')) : PlausibleIterStep IsPlausibleStep :=
   ⟨.skip it', h⟩
@@ -238,7 +238,7 @@ def PlausibleIterStep.skip {IsPlausibleStep : IterStep α β → Prop}
 /--
 Match pattern for the `done` case. See also `IterStep.done`.
 -/
-@[match_pattern, simp]
+@[match_pattern]
 def PlausibleIterStep.done {IsPlausibleStep : IterStep α β → Prop}
     (h : IsPlausibleStep .done) : PlausibleIterStep IsPlausibleStep :=
   ⟨.done, h⟩

src/Std/Data/Iterators/Combinators.lean

@@ -1,12 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Paul Reichert
--/
-prelude
-import Std.Data.Iterators.Combinators.Monadic
-import Std.Data.Iterators.Combinators.Take
-import Std.Data.Iterators.Combinators.TakeWhile
-import Std.Data.Iterators.Combinators.DropWhile
-import Std.Data.Iterators.Combinators.FilterMap
-import Std.Data.Iterators.Combinators.Zip

src/Std/Data/Iterators/Combinators/DropWhile.lean

@@ -1,59 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Paul Reichert
--/
-prelude
-import Std.Data.Iterators.Combinators.Monadic.DropWhile
-
-namespace Std.Iterators
-
-/--
-Constructs intermediate states of an iterator created with the combinator `Iter.dropWhile`.
-When `it.dropWhile P` has stopped dropping elements, its new state cannot be created
-directly with `Iter.dropWhile` but only with `Intermediate.dropWhile`.
-
-`Intermediate.dropWhile` is meant to be used only for internally or for verification purposes.
--/
-@[always_inline, inline]
-def Iter.Intermediate.dropWhile (P : β → Bool) (dropping : Bool)
-    (it : Iter (α := α) β) :=
-  ((IterM.Intermediate.dropWhile P dropping it.toIterM).toIter : Iter β)
-
-/--
-Given an iterator `it` and a predicate `P`, `it.dropWhile P` is an iterator that
-emits the values emitted by `it` starting from the first value that is rejected by `P`.
-The elements before are dropped.
-
-In situations where `P` is monadic, use `dropWhileM` instead.
-
-**Marble diagram:**
-
-Assuming that the predicate `P` accepts `a` and `b` but rejects `c`:
-
-```text
-it               ---a----b---c--d-e--⊥
-it.dropWhile P   ------------c--d-e--⊥
-
-it               ---a----⊥
-it.dropWhile P   --------⊥
-```
-
-**Termination properties:**
-
-* `Finite` instance: only if `it` is finite
-* `Productive` instance: only if `it` is finite
-
-Depending on `P`, it is possible that `it.dropWhileM P` is productive although
-`it` is not. In this case, the `Productive` instance needs to be proved manually.
-
-**Performance:**
-
-This combinator calls `P` on each output of `it` until the predicate evaluates to false. After
-that, the combinator incurs an addictional O(1) cost for each value emitted by `it`.
--/
-@[always_inline, inline]
-def Iter.dropWhile {α : Type w} {β : Type w} (P : β → Bool) (it : Iter (α := α) β) :=
-  (it.toIterM.dropWhile P |>.toIter : Iter β)
-
-end Std.Iterators