feat: more functions in the bytearray parser and move .eof out

.github/workflows/ci.yml

@@ -363,7 +363,7 @@ jobs:
         with:
           path: artifacts
       - name: Release
-        uses: softprops/action-gh-release@72f2c25fcb47643c292f7107632f7a47c1df5cd8
+        uses: softprops/action-gh-release@da05d552573ad5aba039eaac05058a918a7bf631
         with:
           files: artifacts/*/*
           fail_on_unmatched_files: true
@@ -407,7 +407,7 @@ jobs:
           echo -e "\n*Full commit log*\n" >> diff.md
           git log --oneline "$last_tag"..HEAD | sed 's/^/* /' >> diff.md
       - name: Release Nightly
-        uses: softprops/action-gh-release@72f2c25fcb47643c292f7107632f7a47c1df5cd8
+        uses: softprops/action-gh-release@da05d552573ad5aba039eaac05058a918a7bf631
         with:
           body_path: diff.md
           prerelease: true

.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@v11 # https://github.com/marketplace/actions/download-workflow-artifact
+        uses: dawidd6/action-download-artifact@v10 # https://github.com/marketplace/actions/download-workflow-artifact
         with:
           run_id: ${{ github.event.workflow_run.id }}
           path: artifacts
@@ -71,7 +71,7 @@ jobs:
           GH_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
       - name: Release (short format)
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        uses: softprops/action-gh-release@72f2c25fcb47643c292f7107632f7a47c1df5cd8
+        uses: softprops/action-gh-release@da05d552573ad5aba039eaac05058a918a7bf631
         with:
           name: Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }}
           # There are coredumps files here as well, but all in deeper subdirectories.
@@ -86,7 +86,7 @@ jobs:
 
       - name: Release (SHA-suffixed format)
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        uses: softprops/action-gh-release@72f2c25fcb47643c292f7107632f7a47c1df5cd8
+        uses: softprops/action-gh-release@da05d552573ad5aba039eaac05058a918a7bf631
         with:
           name: Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }} (${{ steps.workflow-info.outputs.sourceHeadSha }})
           # There are coredumps files here as well, but all in deeper subdirectories.
@@ -151,7 +151,7 @@ jobs:
 
       - name: 'Setup jq'
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        uses: dcarbone/install-jq-action@v3.2.0
+        uses: dcarbone/install-jq-action@v3.1.1
 
       # Check that the most recently nightly coincides with 'git merge-base HEAD master'
       - name: Check merge-base and nightly-testing-YYYY-MM-DD for Mathlib/Batteries

src/Init/Data/Array/Basic.lean

@@ -180,7 +180,7 @@ in-place when the reference to the array is unique.
 
 This avoids overhead due to unboxing a `Nat` used as an index.
 -/
-@[extern "lean_array_uset", expose]
+@[extern "lean_array_uset"]
 def uset (xs : Array α) (i : USize) (v : α) (h : i.toNat < xs.size) : Array α :=
   xs.set i.toNat v h
 
@@ -1024,7 +1024,7 @@ The optional parameters `start` and `stop` control the region of the array to wh
 applied. Iteration proceeds from `start` (inclusive) to `stop` (exclusive), so `f` is not invoked
 unless `start < stop`. By default, the entire array is used.
 -/
-@[inline, expose]
+@[inline]
 protected def forM {α : Type u} {m : Type v → Type w} [Monad m] (f : α → m PUnit) (as : Array α) (start := 0) (stop := as.size) : m PUnit :=
   as.foldlM (fun _ => f) ⟨⟩ start stop
 

src/Init/Data/Array/Find.lean

@@ -387,7 +387,7 @@ theorem find?_eq_some_iff_getElem {xs : Array α} {p : α → Bool} {b : α} :
 /-! ### findIdx -/
 
 @[grind =]
-theorem findIdx_empty : findIdx p #[] = 0 := by simp
+theorem findIdx_empty : findIdx p #[] = 0 := rfl
 
 @[grind =]
 theorem findIdx_singleton {a : α} {p : α → Bool} :

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

@@ -26,9 +26,9 @@ namespace Array
 @[simp, grind =] theorem le_toList [LT α] {xs ys : Array α} : xs.toList ≤ ys.toList ↔ xs ≤ ys := Iff.rfl
 
 protected theorem not_lt_iff_ge [LT α] {xs ys : Array α} : ¬ xs < ys ↔ ys ≤ xs := Iff.rfl
-protected theorem not_le_iff_gt [LT α] {xs ys : Array α} :
+protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] {xs ys : Array α} :
     ¬ xs ≤ ys ↔ ys < xs :=
-  Classical.not_not
+  Decidable.not_not
 
 @[simp] theorem lex_empty [BEq α] {lt : α → α → Bool} {xs : Array α} : xs.lex #[] lt = false := by
   simp [lex]
@@ -94,7 +94,7 @@ instance [LT α] [Trans (· < · : α → α → Prop) (· < ·) (· < ·)] :
     Trans (· < · : Array α → Array α → Prop) (· < ·) (· < ·) where
   trans h₁ h₂ := Array.lt_trans h₁ h₂
 
-protected theorem lt_of_le_of_lt [LT α]
+protected theorem lt_of_le_of_lt [DecidableEq α] [LT α] [DecidableLT α]
     [i₀ : Std.Irrefl (· < · : α → α → Prop)]
     [i₁ : Std.Asymm (· < · : α → α → Prop)]
     [i₂ : Std.Antisymm (¬ · < · : α → α → Prop)]
@@ -102,7 +102,7 @@ protected theorem lt_of_le_of_lt [LT α]
     {xs ys zs : Array α} (h₁ : xs ≤ ys) (h₂ : ys < zs) : xs < zs :=
   List.lt_of_le_of_lt h₁ h₂
 
-protected theorem le_trans [LT α]
+protected theorem le_trans [DecidableEq α] [LT α] [DecidableLT α]
     [Std.Irrefl (· < · : α → α → Prop)]
     [Std.Asymm (· < · : α → α → Prop)]
     [Std.Antisymm (¬ · < · : α → α → Prop)]
@@ -110,7 +110,7 @@ protected theorem le_trans [LT α]
     {xs ys zs : Array α} (h₁ : xs ≤ ys) (h₂ : ys ≤ zs) : xs ≤ zs :=
   fun h₃ => h₁ (Array.lt_of_le_of_lt h₂ h₃)
 
-instance [LT α]
+instance [DecidableEq α] [LT α] [DecidableLT α]
     [Std.Irrefl (· < · : α → α → Prop)]
     [Std.Asymm (· < · : α → α → Prop)]
     [Std.Antisymm (¬ · < · : α → α → Prop)]
@@ -122,34 +122,34 @@ protected theorem lt_asymm [LT α]
     [i : Std.Asymm (· < · : α → α → Prop)]
     {xs ys : Array α} (h : xs < ys) : ¬ ys < xs := List.lt_asymm h
 
-instance [LT α]
+instance [DecidableEq α] [LT α] [DecidableLT α]
     [Std.Asymm (· < · : α → α → Prop)] :
     Std.Asymm (· < · : Array α → Array α → Prop) where
   asymm _ _ := Array.lt_asymm
 
-protected theorem le_total [LT α]
+protected theorem le_total [DecidableEq α] [LT α] [DecidableLT α]
     [i : Std.Total (¬ · < · : α → α → Prop)] (xs ys : Array α) : xs ≤ ys ∨ ys ≤ xs :=
   List.le_total xs.toList ys.toList
 
 @[simp] protected theorem not_lt [LT α]
     {xs ys : Array α} : ¬ xs < ys ↔ ys ≤ xs := Iff.rfl
 
-@[simp] protected theorem not_le [LT α]
-    {xs ys : Array α} : ¬ ys ≤ xs ↔ xs < ys := Classical.not_not
+@[simp] protected theorem not_le [DecidableEq α] [LT α] [DecidableLT α]
+    {xs ys : Array α} : ¬ ys ≤ xs ↔ xs < ys := Decidable.not_not
 
-protected theorem le_of_lt [LT α]
+protected theorem le_of_lt [DecidableEq α] [LT α] [DecidableLT α]
     [i : Std.Total (¬ · < · : α → α → Prop)]
     {xs ys : Array α} (h : xs < ys) : xs ≤ ys :=
   List.le_of_lt h
 
-protected theorem le_iff_lt_or_eq [LT α]
+protected theorem le_iff_lt_or_eq [DecidableEq α] [LT α] [DecidableLT α]
     [Std.Irrefl (· < · : α → α → Prop)]
     [Std.Antisymm (¬ · < · : α → α → Prop)]
     [Std.Total (¬ · < · : α → α → Prop)]
     {xs ys : Array α} : xs ≤ ys ↔ xs < ys ∨ xs = ys := by
   simpa using List.le_iff_lt_or_eq (l₁ := xs.toList) (l₂ := ys.toList)
 
-instance [LT α]
+instance [DecidableEq α] [LT α] [DecidableLT α]
     [Std.Total (¬ · < · : α → α → Prop)] :
     Std.Total (· ≤ · : Array α → Array α → Prop) where
   total := Array.le_total
@@ -218,7 +218,7 @@ theorem lex_eq_false_iff_exists [BEq α] [PartialEquivBEq α] (lt : α → α
   cases l₂
   simp_all [List.lex_eq_false_iff_exists]
 
-protected theorem lt_iff_exists [LT α] {xs ys : Array α} :
+protected theorem lt_iff_exists [DecidableEq α] [LT α] [DecidableLT α] {xs ys : Array α} :
     xs < ys ↔
       (xs = ys.take xs.size ∧ xs.size < ys.size) ∨
         (∃ (i : Nat) (h₁ : i < xs.size) (h₂ : i < ys.size),
@@ -228,7 +228,7 @@ protected theorem lt_iff_exists [LT α] {xs ys : Array α} :
   cases ys
   simp [List.lt_iff_exists]
 
-protected theorem le_iff_exists [LT α]
+protected theorem le_iff_exists [DecidableEq α] [LT α] [DecidableLT α]
     [Std.Irrefl (· < · : α → α → Prop)]
     [Std.Asymm (· < · : α → α → Prop)]
     [Std.Antisymm (¬ · < · : α → α → Prop)] {xs ys : Array α} :
@@ -248,7 +248,7 @@ theorem append_left_lt [LT α] {xs ys zs : Array α} (h : ys < zs) :
   cases zs
   simpa using List.append_left_lt h
 
-theorem append_left_le [LT α]
+theorem append_left_le [DecidableEq α] [LT α] [DecidableLT α]
     [Std.Irrefl (· < · : α → α → Prop)]
     [Std.Asymm (· < · : α → α → Prop)]
     [Std.Antisymm (¬ · < · : α → α → Prop)]
@@ -272,7 +272,7 @@ protected theorem map_lt [LT α] [LT β]
   cases ys
   simpa using List.map_lt w h
 
-protected theorem map_le [LT α] [LT β]
+protected theorem map_le [DecidableEq α] [LT α] [DecidableLT α] [DecidableEq β] [LT β] [DecidableLT β]
     [Std.Irrefl (· < · : α → α → Prop)]
     [Std.Asymm (· < · : α → α → Prop)]
     [Std.Antisymm (¬ · < · : α → α → Prop)]

src/Init/Data/Fin/Fold.lean

@@ -185,9 +185,7 @@ theorem foldrM_loop [Monad m] [LawfulMonad m] (f : Fin (n+1) → α → m α) (x
   | zero =>
     rw [foldrM_loop_zero, foldrM_loop_succ, pure_bind]
     conv => rhs; rw [←bind_pure (f 0 x)]
-    congr
-    funext
-    rw [foldrM_loop_zero]
+    rfl
   | succ i ih =>
     rw [foldrM_loop_succ, foldrM_loop_succ, bind_assoc]
     congr; funext; exact ih ..

src/Init/Data/Iterators/Combinators/Monadic/Attach.lean

@@ -98,12 +98,12 @@ instance Attach.instIteratorCollectPartial {α β : Type w} {m : Type w → Type
   .defaultImplementation
 
 instance Attach.instIteratorLoop {α β : Type w} {m : Type w → Type w'} [Monad m]
-    {n : Type x → Type x'} [Monad n] {P : β → Prop} [Iterator α m β] :
+    [Monad n] {P : β → Prop} [Iterator α m β] [MonadLiftT m n] :
     IteratorLoop (Attach α m P) m n :=
   .defaultImplementation
 
 instance Attach.instIteratorLoopPartial {α β : Type w} {m : Type w → Type w'} [Monad m]
-    {n : Type x → Type x'} [Monad n] {P : β → Prop} [Iterator α m β] :
+    [Monad n] {P : β → Prop} [Iterator α m β] [MonadLiftT m n] :
     IteratorLoopPartial (Attach α m P) m n :=
   .defaultImplementation
 

src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean

@@ -231,14 +231,14 @@ instance {α β γ : Type w} {m : Type w → Type w'}
   .defaultImplementation
 
 instance FilterMap.instIteratorLoop {α β γ : Type w} {m : Type w → Type w'}
-    {n : Type w → Type w''} {o : Type x → Type x'}
+    {n : Type w → Type w''} {o : Type w → Type w'''}
     [Monad n] [Monad o] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α}
     {f : β → PostconditionT n (Option γ)} [Finite α m] :
     IteratorLoop (FilterMap α m n lift f) n o :=
   .defaultImplementation
 
 instance FilterMap.instIteratorLoopPartial {α β γ : Type w} {m : Type w → Type w'}
-    {n : Type w → Type w''} {o : Type x → Type x'}
+    {n : Type w → Type w''} {o : Type w → Type w'''}
     [Monad n] [Monad o] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α}
     {f : β → PostconditionT n (Option γ)} :
     IteratorLoopPartial (FilterMap α m n lift f) n o :=
@@ -274,14 +274,14 @@ instance Map.instIteratorCollectPartial {α β γ : Type w} {m : Type w → Type
       it.internalState.inner (m := m)
 
 instance Map.instIteratorLoop {α β γ : Type w} {m : Type w → Type w'}
-    {n : Type w → Type w''} {o : Type x → Type x'} [Monad n] [Monad o] [Iterator α m β]
+    {n : Type w → Type w''} {o : Type w → Type x} [Monad n] [Monad o] [Iterator α m β]
     {lift : ⦃α : Type w⦄ → m α → n α}
     {f : β → PostconditionT n γ} :
     IteratorLoop (Map α m n lift f) n o :=
   .defaultImplementation
 
 instance Map.instIteratorLoopPartial {α β γ : Type w} {m : Type w → Type w'}
-    {n : Type w → Type w''} {o : Type x → Type x'} [Monad n] [Monad o] [Iterator α m β]
+    {n : Type w → Type w''} {o : Type w → Type x} [Monad n] [Monad o] [Iterator α m β]
     {lift : ⦃α : Type w⦄ → m α → n α}
     {f : β → PostconditionT n γ} :
     IteratorLoopPartial (Map α m n lift f) n o :=

src/Init/Data/Iterators/Combinators/Monadic/ULift.lean

@@ -123,16 +123,15 @@ instance Types.ULiftIterator.instProductive [Iterator α m β] [Productive α m]
     Productive (ULiftIterator α m n β lift) n :=
   .of_productivenessRelation instProductivenessRelation
 
-instance Types.ULiftIterator.instIteratorLoop {o : Type x → Type x'} [Monad n] [Monad o]
-    [Iterator α m β] :
+instance Types.ULiftIterator.instIteratorLoop {o} [Monad n] [Monad o] [Iterator α m β] :
     IteratorLoop (ULiftIterator α m n β lift) n o :=
   .defaultImplementation
 
-instance Types.ULiftIterator.instIteratorLoopPartial {o : Type x → Type x'} [Monad n] [Monad o] [Iterator α m β] :
+instance Types.ULiftIterator.instIteratorLoopPartial {o} [Monad n] [Monad o] [Iterator α m β] :
     IteratorLoopPartial (ULiftIterator α m n β lift) n o :=
   .defaultImplementation
 
-instance Types.ULiftIterator.instIteratorCollect [Monad n] [Monad o] [Iterator α m β] :
+instance Types.ULiftIterator.instIteratorCollect {o} [Monad n] [Monad o] [Iterator α m β] :
     IteratorCollect (ULiftIterator α m n β lift) n o :=
   .defaultImplementation
 

src/Init/Data/Iterators/Consumers/Loop.lean

@@ -33,42 +33,32 @@ so this is not marked as `instance`. This way, more convenient instances can be
 or future library improvements will make it more comfortable.
 -/
 @[always_inline, inline]
-def Iter.instForIn' {α : Type w} {β : Type w} {n : Type x → Type x'} [Monad n]
+def Iter.instForIn' {α : Type w} {β : Type w} {n : Type w → Type w'} [Monad n]
     [Iterator α Id β] [Finite α Id] [IteratorLoop α Id n] :
     ForIn' n (Iter (α := α) β) β ⟨fun it out => it.IsPlausibleIndirectOutput out⟩ where
   forIn' it init f :=
-    IteratorLoop.finiteForIn' (fun _ _ f c => f c.run) |>.forIn' it.toIterM init
+    IteratorLoop.finiteForIn' (fun δ (c : Id δ) => pure c.run) |>.forIn' it.toIterM init
         fun out h acc =>
           f out (Iter.isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM.mpr h) acc
 
-instance (α : Type w) (β : Type w) (n : Type x → Type x') [Monad n]
+instance (α : Type w) (β : Type w) (n : Type w → Type w') [Monad n]
     [Iterator α Id β] [Finite α Id] [IteratorLoop α Id n] :
     ForIn n (Iter (α := α) β) β :=
   haveI : ForIn' n (Iter (α := α) β) β _ := Iter.instForIn'
   instForInOfForIn'
 
-@[always_inline, inline]
-def Iter.Partial.instForIn' {α : Type w} {β : Type w} {n : Type x → Type x'} [Monad n]
+instance (α : Type w) (β : Type w) (n : Type w → Type w') [Monad n]
     [Iterator α Id β] [IteratorLoopPartial α Id n] :
-    ForIn' n (Iter.Partial (α := α) β) β ⟨fun it out => it.it.IsPlausibleIndirectOutput out⟩ where
-  forIn' it init f :=
-    IteratorLoopPartial.forInPartial (α := α) (m := Id) (n := n) (fun _ _ f c => f c.run)
-      it.it.toIterM init
-      fun out h acc =>
-        f out (Iter.isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM.mpr h) acc
+    ForIn n (Iter.Partial (α := α) β) β where
+  forIn it init f :=
+    ForIn.forIn it.it.toIterM.allowNontermination init f
 
-instance (α : Type w) (β : Type w) (n : Type x → Type x') [Monad n]
-    [Iterator α Id β] [IteratorLoopPartial α Id n] :
-    ForIn n (Iter.Partial (α := α) β) β :=
-  haveI : ForIn' n (Iter.Partial (α := α) β) β _ := Iter.Partial.instForIn'
-  instForInOfForIn'
-
-instance {m : Type x → Type x'}
+instance {m : Type w → Type w'}
     {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id m] :
     ForM m (Iter (α := α) β) β where
   forM it f := forIn it PUnit.unit (fun out _ => do f out; return .yield .unit)
 
-instance {m : Type x → Type x'}
+instance {m : Type w → Type w'}
     {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoopPartial α Id m] :
     ForM m (Iter.Partial (α := α) β) β where
   forM it f := forIn it PUnit.unit (fun out _ => do f out; return .yield .unit)
@@ -85,8 +75,8 @@ number of steps. If the iterator is not finite or such an instance is not availa
 verify the behavior of the partial variant.
 -/
 @[always_inline, inline]
-def Iter.foldM {m : Type x → Type x'} [Monad m]
-    {α : Type w} {β : Type w} {γ : Type x} [Iterator α Id β] [Finite α Id]
+def Iter.foldM {m : Type w → Type w'} [Monad m]
+    {α : Type w} {β : Type w} {γ : Type w} [Iterator α Id β] [Finite α Id]
     [IteratorLoop α Id m] (f : γ → β → m γ)
     (init : γ) (it : Iter (α := α) β) : m γ :=
   ForIn.forIn it init (fun x acc => ForInStep.yield <$> f acc x)
@@ -101,8 +91,8 @@ This is a partial, potentially nonterminating, function. It is not possible to f
 its behavior. If the iterator has a `Finite` instance, consider using `IterM.foldM` instead.
 -/
 @[always_inline, inline]
-def Iter.Partial.foldM {m : Type x → Type x'} [Monad m]
-    {α : Type w} {β : Type w} {γ : Type x} [Iterator α Id β]
+def Iter.Partial.foldM {m : Type w → Type w'} [Monad m]
+    {α : Type w} {β : Type w} {γ : Type w} [Iterator α Id β]
     [IteratorLoopPartial α Id m] (f : γ → β → m γ)
     (init : γ) (it : Iter.Partial (α := α) β) : m γ :=
   ForIn.forIn it init (fun x acc => ForInStep.yield <$> f acc x)
@@ -119,7 +109,7 @@ number of steps. If the iterator is not finite or such an instance is not availa
 verify the behavior of the partial variant.
 -/
 @[always_inline, inline]
-def Iter.fold {α : Type w} {β : Type w} {γ : Type x} [Iterator α Id β] [Finite α Id]
+def Iter.fold {α : Type w} {β : Type w} {γ : Type w} [Iterator α Id β] [Finite α Id]
     [IteratorLoop α Id Id] (f : γ → β → γ)
     (init : γ) (it : Iter (α := α) β) : γ :=
   ForIn.forIn (m := Id) it init (fun x acc => ForInStep.yield (f acc x))
@@ -134,7 +124,7 @@ This is a partial, potentially nonterminating, function. It is not possible to f
 its behavior. If the iterator has a `Finite` instance, consider using `IterM.fold` instead.
 -/
 @[always_inline, inline]
-def Iter.Partial.fold {α : Type w} {β : Type w} {γ : Type x} [Iterator α Id β]
+def Iter.Partial.fold {α : Type w} {β : Type w} {γ : Type w} [Iterator α Id β]
     [IteratorLoopPartial α Id Id] (f : γ → β → γ)
     (init : γ) (it : Iter.Partial (α := α) β) : γ :=
   ForIn.forIn (m := Id) it init (fun x acc => ForInStep.yield (f acc x))

src/Init/Data/Iterators/Consumers/Monadic/Loop.lean

@@ -62,8 +62,8 @@ They can, however, assume that consumers that require an instance will work for
 provided by the standard library.
 -/
 class IteratorLoop (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β]
-    (n : Type x → Type x') where
-  forIn : ∀ (_liftBind : (γ : Type w) → (δ : Type x) → (γ → n δ) → m γ → n δ) (γ : Type x),
+    (n : Type w → Type w'') where
+  forIn : ∀ (_lift : (γ : Type w) → m γ → n γ) (γ : Type w),
       (plausible_forInStep : β → γ → ForInStep γ → Prop) →
       IteratorLoop.WellFounded α m plausible_forInStep →
       (it : IterM (α := α) m β) → γ →
@@ -79,8 +79,8 @@ They can, however, assume that consumers that require an instance will work for
 provided by the standard library.
 -/
 class IteratorLoopPartial (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β]
-    (n : Type x → Type x') where
-  forInPartial : ∀ (_liftBind : (γ : Type w) → (δ : Type x) → (γ → n δ) → m γ → n δ) {γ : Type x},
+    (n : Type w → Type w'') where
+  forInPartial : ∀ (_lift : (γ : Type w) → m γ → n γ) {γ : Type w},
       (it : IterM (α := α) m β) → γ →
       ((b : β) → it.IsPlausibleIndirectOutput b → (c : γ) → n (ForInStep γ)) → n γ
 
@@ -133,25 +133,27 @@ This is the loop implementation of the default instance `IteratorLoop.defaultImp
 @[specialize]
 def IterM.DefaultConsumers.forIn' {m : Type w → Type w'} {α : Type w} {β : Type w}
     [Iterator α m β]
-    {n : Type x → Type x'} [Monad n]
-    (lift : ∀ γ δ, (γ → n δ) → m γ → n δ) (γ : Type x)
+    {n : Type w → Type w''} [Monad n]
+    (lift : ∀ γ, m γ → n γ) (γ : Type w)
     (plausible_forInStep : β → γ → ForInStep γ → Prop)
     (wf : IteratorLoop.WellFounded α m plausible_forInStep)
     (it : IterM (α := α) m β) (init : γ)
     (P : β → Prop) (hP : ∀ b, it.IsPlausibleIndirectOutput b → P b)
     (f : (b : β) → P b → (c : γ) → n (Subtype (plausible_forInStep b c))) : n γ :=
   haveI : WellFounded _ := wf
-  (lift _ _ · it.step) fun
-      | .yield it' out h => do
-        match ← f out (hP _ <| .direct ⟨_, h⟩) init with
-        | ⟨.yield c, _⟩ =>
-          IterM.DefaultConsumers.forIn' lift _ plausible_forInStep wf it' c P
-            (fun _ h' => hP _ <| .indirect ⟨_, rfl, h⟩ h') f
-        | ⟨.done c, _⟩ => return c
-      | .skip it' h =>
-        IterM.DefaultConsumers.forIn' lift _ plausible_forInStep wf it' init P
-            (fun _ h' => hP _ <| .indirect ⟨_, rfl, h⟩ h') f
-      | .done _ => return init
+  letI : MonadLift m n := ⟨fun {γ} => lift γ⟩
+  do
+    match ← it.step with
+    | .yield it' out h =>
+      match ← f out (hP _ <| .direct ⟨_, h⟩) init with
+      | ⟨.yield c, _⟩ =>
+        IterM.DefaultConsumers.forIn' lift _ plausible_forInStep wf it' c P
+          (fun _ h' => hP _ <| .indirect ⟨_, rfl, h⟩ h') f
+      | ⟨.done c, _⟩ => return c
+    | .skip it' h =>
+      IterM.DefaultConsumers.forIn' lift _ plausible_forInStep wf it' init P
+          (fun _ h' => hP _ <| .indirect ⟨_, rfl, h⟩ h') f
+    | .done _ => return init
 termination_by IteratorLoop.WFRel.mk wf it init
 decreasing_by
   · exact Or.inl ⟨out, ‹_›, ‹_›⟩
@@ -163,7 +165,7 @@ It simply iterates through the iterator using `IterM.step`. For certain iterator
 implementations are possible and should be used instead.
 -/
 @[always_inline, inline]
-def IteratorLoop.defaultImplementation {α : Type w} {m : Type w → Type w'} {n : Type x → Type x'}
+def IteratorLoop.defaultImplementation {α : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
     [Monad n] [Iterator α m β] :
     IteratorLoop α m n where
   forIn lift γ Pl wf it init := IterM.DefaultConsumers.forIn' lift γ Pl wf it init _ (fun _ => id)
@@ -172,7 +174,7 @@ def IteratorLoop.defaultImplementation {α : Type w} {m : Type w → Type w'} {n
 Asserts that a given `IteratorLoop` instance is equal to `IteratorLoop.defaultImplementation`.
 (Even though equal, the given instance might be vastly more efficient.)
 -/
-class LawfulIteratorLoop (α : Type w) (m : Type w → Type w') (n : Type x → Type x')
+class LawfulIteratorLoop (α : Type w) (m : Type w → Type w') (n : Type w → Type w'')
     [Monad n] [Iterator α m β] [Finite α m] [i : IteratorLoop α m n] where
   lawful : i = .defaultImplementation
 
@@ -182,21 +184,23 @@ This is the loop implementation of the default instance `IteratorLoopPartial.def
 @[specialize]
 partial def IterM.DefaultConsumers.forInPartial {m : Type w → Type w'} {α : Type w} {β : Type w}
     [Iterator α m β]
-    {n : Type x → Type x'} [Monad n]
-    (lift : ∀ γ δ, (γ → n δ) → m γ → n δ) (γ : Type x)
+    {n : Type w → Type w''} [Monad n]
+    (lift : ∀ γ, m γ → n γ) (γ : Type w)
     (it : IterM (α := α) m β) (init : γ)
     (f : (b : β) → it.IsPlausibleIndirectOutput b → (c : γ) → n (ForInStep γ)) : n γ :=
-  (lift _ _ · it.step) fun
-      | .yield it' out h => do
-        match ← f out (.direct ⟨_, h⟩) init with
-        | .yield c =>
-          IterM.DefaultConsumers.forInPartial lift _ it' c
-            fun out h' acc => f out (.indirect ⟨_, rfl, h⟩ h') acc
-        | .done c => return c
-      | .skip it' h =>
-        IterM.DefaultConsumers.forInPartial lift _ it' init
+  letI : MonadLift m n := ⟨fun {γ} => lift γ⟩
+  do
+    match ← it.step with
+    | .yield it' out h =>
+      match ← f out (.direct ⟨_, h⟩) init with
+      | .yield c =>
+        IterM.DefaultConsumers.forInPartial lift _ it' c
           fun out h' acc => f out (.indirect ⟨_, rfl, h⟩ h') acc
-      | .done _ => return init
+      | .done c => return c
+    | .skip it' h =>
+      IterM.DefaultConsumers.forInPartial lift _ it' init
+        fun out h' acc => f out (.indirect ⟨_, rfl, h⟩ h') acc
+    | .done _ => return init
 
 /--
 This is the default implementation of the `IteratorLoopPartial` class.
@@ -205,11 +209,11 @@ implementations are possible and should be used instead.
 -/
 @[always_inline, inline]
 def IteratorLoopPartial.defaultImplementation {α : Type w} {m : Type w → Type w'}
-    {n : Type x → Type x'} [Monad m] [Monad n] [Iterator α m β] :
+    {n : Type w → Type w''} [Monad m] [Monad n] [Iterator α m β] :
     IteratorLoopPartial α m n where
   forInPartial lift := IterM.DefaultConsumers.forInPartial lift _
 
-instance (α : Type w) (m : Type w → Type w') (n : Type x → Type x')
+instance (α : Type w) (m : Type w → Type w') (n : Type w → Type w'')
     [Monad m] [Monad n] [Iterator α m β] [Finite α m] :
     letI : IteratorLoop α m n := .defaultImplementation
     LawfulIteratorLoop α m n :=
@@ -217,7 +221,7 @@ instance (α : Type w) (m : Type w → Type w') (n : Type x → Type x')
   ⟨rfl⟩
 
 theorem IteratorLoop.wellFounded_of_finite {m : Type w → Type w'}
-    {α β : Type w} {γ : Type x} [Iterator α m β] [Finite α m] :
+    {α β γ : Type w} [Iterator α m β] [Finite α m] :
     WellFounded α m (γ := γ) fun _ _ _ => True := by
   apply Subrelation.wf
     (r := InvImage IterM.TerminationMeasures.Finite.Rel (fun p => p.1.finitelyManySteps))
@@ -233,9 +237,9 @@ theorem IteratorLoop.wellFounded_of_finite {m : Type w → Type w'}
 This `ForIn'`-style loop construct traverses a finite iterator using an `IteratorLoop` instance.
 -/
 @[always_inline, inline]
-def IteratorLoop.finiteForIn' {m : Type w → Type w'} {n : Type x → Type x'}
+def IteratorLoop.finiteForIn' {m : Type w → Type w'} {n : Type w → Type w''}
     {α : Type w} {β : Type w} [Iterator α m β] [Finite α m] [IteratorLoop α m n]
-    (lift : ∀ γ δ, (γ → n δ) → m γ → n δ) :
+    (lift : ∀ γ, m γ → n γ) :
     ForIn' n (IterM (α := α) m β) β ⟨fun it out => it.IsPlausibleIndirectOutput out⟩ where
   forIn' {γ} [Monad n] it init f :=
     IteratorLoop.forIn (α := α) (m := m) lift γ (fun _ _ _ => True)
@@ -249,30 +253,23 @@ or future library improvements will make it more comfortable.
 -/
 @[always_inline, inline]
 def IterM.instForIn' {m : Type w → Type w'} {n : Type w → Type w''}
-    {α : Type w} {β : Type w} [Iterator α m β] [Finite α m] [IteratorLoop α m n] [Monad n]
+    {α : Type w} {β : Type w} [Iterator α m β] [Finite α m] [IteratorLoop α m n]
     [MonadLiftT m n] :
     ForIn' n (IterM (α := α) m β) β ⟨fun it out => it.IsPlausibleIndirectOutput out⟩ :=
-  IteratorLoop.finiteForIn' (fun _ _ f x => monadLift x >>= f)
+  IteratorLoop.finiteForIn' (fun _ => monadLift)
 
 instance {m : Type w → Type w'} {n : Type w → Type w''}
     {α : Type w} {β : Type w} [Iterator α m β] [Finite α m] [IteratorLoop α m n]
-    [MonadLiftT m n] [Monad n] :
+    [MonadLiftT m n] :
     ForIn n (IterM (α := α) m β) β :=
   haveI : ForIn' n (IterM (α := α) m β) β _ := IterM.instForIn'
   instForInOfForIn'
 
-@[always_inline, inline]
-def IterM.Partial.instForIn' {m : Type w → Type w'} {n : Type w → Type w''}
-    {α : Type w} {β : Type w} [Iterator α m β] [IteratorLoopPartial α m n] [MonadLiftT m n] [Monad n] :
-    ForIn' n (IterM.Partial (α := α) m β) β ⟨fun it out => it.it.IsPlausibleIndirectOutput out⟩ where
-  forIn' it init f := IteratorLoopPartial.forInPartial (α := α) (m := m) (n := n)
-      (fun _ _ f x => monadLift x >>= f) it.it init f
-
 instance {m : Type w → Type w'} {n : Type w → Type w''}
-    {α : Type w} {β : Type w} [Iterator α m β] [IteratorLoopPartial α m n] [MonadLiftT m n] [Monad n] :
-    ForIn n (IterM.Partial (α := α) m β) β :=
-  haveI : ForIn' n (IterM.Partial (α := α) m β) β _ := IterM.Partial.instForIn'
-  instForInOfForIn'
+    {α : Type w} {β : Type w} [Iterator α m β] [IteratorLoopPartial α m n] [MonadLiftT m n] :
+    ForIn' n (IterM.Partial (α := α) m β) β ⟨fun it out => it.it.IsPlausibleIndirectOutput out⟩ where
+  forIn' it init f :=
+    IteratorLoopPartial.forInPartial (α := α) (m := m) (fun _ => monadLift) it.it init f
 
 instance {m : Type w → Type w'} {n : Type w → Type w''}
     {α : Type w} {β : Type w} [Iterator α m β] [Finite α m] [IteratorLoop α m n]

src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean

@@ -16,30 +16,30 @@ public section
 namespace Std.Iterators
 
 theorem Iter.forIn'_eq {α β : Type w} [Iterator α Id β] [Finite α Id]
-    {m : Type x → Type x'} [Monad m] [IteratorLoop α Id m] [hl : LawfulIteratorLoop α Id m]
-    {γ : Type x} {it : Iter (α := α) β} {init : γ}
+    {m : Type w → Type w''} [Monad m] [IteratorLoop α Id m] [hl : LawfulIteratorLoop α Id m]
+    {γ : Type w} {it : Iter (α := α) β} {init : γ}
     {f : (b : β) → it.IsPlausibleIndirectOutput b → γ → m (ForInStep γ)} :
     letI : ForIn' m (Iter (α := α) β) β _ := Iter.instForIn'
     ForIn'.forIn' it init f =
-      IterM.DefaultConsumers.forIn' (fun _ _ f x => f x.run) γ (fun _ _ _ => True)
+      IterM.DefaultConsumers.forIn' (fun _ c => pure c.run) γ (fun _ _ _ => True)
         IteratorLoop.wellFounded_of_finite it.toIterM init _ (fun _ => id)
           (fun out h acc => (⟨·, .intro⟩) <$>
             f out (Iter.isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM.mpr h) acc) := by
   cases hl.lawful; rfl
 
 theorem Iter.forIn_eq {α β : Type w} [Iterator α Id β] [Finite α Id]
-    {m : Type x → Type x'} [Monad m] [IteratorLoop α Id m] [hl : LawfulIteratorLoop α Id m]
-    {γ : Type x} {it : Iter (α := α) β} {init : γ}
+    {m : Type w → Type w''} [Monad m] [IteratorLoop α Id m] [hl : LawfulIteratorLoop α Id m]
+    {γ : Type w} {it : Iter (α := α) β} {init : γ}
     {f : (b : β) → γ → m (ForInStep γ)} :
     ForIn.forIn it init f =
-      IterM.DefaultConsumers.forIn' (fun _ _ f c => f c.run) γ (fun _ _ _ => True)
+      IterM.DefaultConsumers.forIn' (fun _ c => pure c.run) γ (fun _ _ _ => True)
         IteratorLoop.wellFounded_of_finite it.toIterM init _ (fun _ => id)
           (fun out _ acc => (⟨·, .intro⟩) <$>
             f out acc) := by
   cases hl.lawful; rfl
 
 theorem Iter.forIn'_eq_forIn'_toIterM {α β : Type w} [Iterator α Id β]
-    [Finite α Id] {m : Type w → Type w'} [Monad m] [LawfulMonad m]
+    [Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m]
     [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
     {γ : Type w} {it : Iter (α := α) β} {init : γ}
     {f : (out : β) → _ → γ → m (ForInStep γ)} :
@@ -48,7 +48,7 @@ theorem Iter.forIn'_eq_forIn'_toIterM {α β : Type w} [Iterator α Id β]
       letI : ForIn' m (IterM (α := α) Id β) β _ := IterM.instForIn'
       ForIn'.forIn' it.toIterM init
         (fun out h acc => f out (isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM.mpr h) acc) := by
-  simp [ForIn'.forIn', Iter.instForIn', IterM.instForIn', monadLift]
+  rfl
 
 theorem Iter.forIn_eq_forIn_toIterM {α β : Type w} [Iterator α Id β]
     [Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m]
@@ -57,12 +57,12 @@ theorem Iter.forIn_eq_forIn_toIterM {α β : Type w} [Iterator α Id β]
     {f : β → γ → m (ForInStep γ)} :
     ForIn.forIn it init f =
       ForIn.forIn it.toIterM init f := by
-  simp [forIn_eq_forIn', forIn'_eq_forIn'_toIterM, -forIn'_eq_forIn]
+  rfl
 
 theorem Iter.forIn'_eq_match_step {α β : Type w} [Iterator α Id β]
-    [Finite α Id] {m : Type x → Type x''} [Monad m] [LawfulMonad m]
+    [Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m]
     [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
-    {γ : Type x} {it : Iter (α := α) β} {init : γ}
+    {γ : Type w} {it : Iter (α := α) β} {init : γ}
     {f : (out : β) → _ → γ → m (ForInStep γ)} :
     letI : ForIn' m (Iter (α := α) β) β _ := Iter.instForIn'
     ForIn'.forIn' it init f = (do
@@ -77,27 +77,20 @@ theorem Iter.forIn'_eq_match_step {α β : Type w} [Iterator α Id β]
           ForIn'.forIn' it' init
             fun out h' acc => f out (.indirect ⟨_, rfl, h⟩ h') acc
       | .done _ => return init) := by
-  simp only [forIn'_eq]
-  rw [IterM.DefaultConsumers.forIn'_eq_match_step]
-  simp only [bind_map_left, Iter.step]
-  cases it.toIterM.step.run using PlausibleIterStep.casesOn
-  · simp only [IterM.Step.toPure_yield, PlausibleIterStep.yield, toIter_toIterM, toIterM_toIter]
-    apply bind_congr
+  rw [Iter.forIn'_eq_forIn'_toIterM, @IterM.forIn'_eq_match_step, Iter.step]
+  simp only [liftM, monadLift, pure_bind]
+  generalize it.toIterM.step = step
+  cases step using PlausibleIterStep.casesOn
+  · apply bind_congr
     intro forInStep
-    cases forInStep
-    · simp
-    · simp only
-      apply IterM.DefaultConsumers.forIn'_eq_forIn'
-      intros; congr
-  · simp only
-    apply IterM.DefaultConsumers.forIn'_eq_forIn'
-    intros; congr
-  · simp
+    rfl
+  · rfl
+  · rfl
 
 theorem Iter.forIn_eq_match_step {α β : Type w} [Iterator α Id β]
-    [Finite α Id] {m : Type x → Type x'} [Monad m] [LawfulMonad m]
+    [Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m]
     [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
-    {γ : Type x} {it : Iter (α := α) β} {init : γ}
+    {γ : Type w} {it : Iter (α := α) β} {init : γ}
     {f : β → γ → m (ForInStep γ)} :
     ForIn.forIn it init f = (do
       match it.step with
@@ -107,15 +100,23 @@ theorem Iter.forIn_eq_match_step {α β : Type w} [Iterator α Id β]
         | .done c => return c
       | .skip it' _ => ForIn.forIn it' init f
       | .done _ => return init) := by
-  simp only [forIn_eq_forIn']
-  exact forIn'_eq_match_step
+  rw [Iter.forIn_eq_forIn_toIterM, @IterM.forIn_eq_match_step, Iter.step]
+  simp only [liftM, monadLift, pure_bind]
+  generalize it.toIterM.step = step
+  cases step using PlausibleIterStep.casesOn
+  · apply bind_congr
+    intro forInStep
+    rfl
+  · rfl
+  · rfl
 
-private theorem Iter.forIn'_toList.aux {ρ : Type u} {α : Type v} {γ : Type x} {m : Type x → Type x'}
+private theorem Iter.forIn'_toList.aux {ρ : Type u} {α : Type v} {γ : Type w} {m : Type w → Type w'}
     [Monad m] {_ : Membership α ρ} [ForIn' m ρ α inferInstance]
     {r s : ρ} {init : γ} {f : (a : α) → _ → γ → m (ForInStep γ)} (h : r = s) :
     forIn' r init f = forIn' s init (fun a h' acc => f a (h ▸ h') acc) := by
   cases h; rfl
 
+
 theorem Iter.isPlausibleStep_iff_step_eq {α β} [Iterator α Id β]
     [IteratorCollect α Id Id] [Finite α Id]
     [LawfulIteratorCollect α Id Id] [LawfulDeterministicIterator α Id]
@@ -184,11 +185,11 @@ theorem Iter.mem_toList_iff_isPlausibleIndirectOutput {α β} [Iterator α Id β
         simp [heq, IterStep.successor] at h₁
 
 theorem Iter.forIn'_toList {α β : Type w} [Iterator α Id β]
-    [Finite α Id] {m : Type x → Type x'} [Monad m] [LawfulMonad m]
+    [Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m]
     [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
     [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
     [LawfulDeterministicIterator α Id]
-    {γ : Type x} {it : Iter (α := α) β} {init : γ}
+    {γ : Type w} {it : Iter (α := α) β} {init : γ}
     {f : (out : β) → _ → γ → m (ForInStep γ)} :
     letI : ForIn' m (Iter (α := α) β) β _ := Iter.instForIn'
     ForIn'.forIn' it.toList init f = ForIn'.forIn' it init (fun out h acc => f out (Iter.mem_toList_iff_isPlausibleIndirectOutput.mpr h) acc) := by
@@ -218,11 +219,11 @@ theorem Iter.forIn'_toList {α β : Type w} [Iterator α Id β]
   · simp
 
 theorem Iter.forIn'_eq_forIn'_toList {α β : Type w} [Iterator α Id β]
-    [Finite α Id] {m : Type x → Type x'} [Monad m] [LawfulMonad m]
+    [Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m]
     [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
     [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
     [LawfulDeterministicIterator α Id]
-    {γ : Type x} {it : Iter (α := α) β} {init : γ}
+    {γ : Type w} {it : Iter (α := α) β} {init : γ}
     {f : (out : β) → _ → γ → m (ForInStep γ)} :
     letI : ForIn' m (Iter (α := α) β) β _ := Iter.instForIn'
     ForIn'.forIn' it init f = ForIn'.forIn' it.toList init (fun out h acc => f out (Iter.mem_toList_iff_isPlausibleIndirectOutput.mp h) acc) := by
@@ -230,10 +231,10 @@ theorem Iter.forIn'_eq_forIn'_toList {α β : Type w} [Iterator α Id β]
   congr
 
 theorem Iter.forIn_toList {α β : Type w} [Iterator α Id β]
-    [Finite α Id] {m : Type x → Type x'} [Monad m] [LawfulMonad m]
+    [Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m]
     [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
     [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
-    {γ : Type x} {it : Iter (α := α) β} {init : γ}
+    {γ : Type w} {it : Iter (α := α) β} {init : γ}
     {f : β → γ → m (ForInStep γ)} :
     ForIn.forIn it.toList init f = ForIn.forIn it init f := by
   rw [List.forIn_eq_foldlM]
@@ -249,14 +250,14 @@ theorem Iter.forIn_toList {α β : Type w} [Iterator α Id β]
     cases forInStep
     · induction it'.toList <;> simp [*]
     · simp only [ForIn.forIn] at ihy
-      simp [ihy h]
+      simp [ihy h, forIn_eq_forIn_toIterM]
   · rename_i it' h
     simp only [bind_pure_comp]
     rw [ihs h]
   · simp
 
-theorem Iter.foldM_eq_forIn {α β : Type w} {γ : Type x} [Iterator α Id β] [Finite α Id]
-    {m : Type x → Type x'} [Monad m] [IteratorLoop α Id m] {f : γ → β → m γ}
+theorem Iter.foldM_eq_forIn {α β γ : Type w} [Iterator α Id β] [Finite α Id] {m : Type w → Type w'}
+    [Monad m] [IteratorLoop α Id m] {f : γ → β → m γ}
     {init : γ} {it : Iter (α := α) β} :
     it.foldM (init := init) f = ForIn.forIn it init (fun x acc => ForInStep.yield <$> f acc x) :=
   (rfl)
@@ -265,19 +266,19 @@ theorem Iter.foldM_eq_foldM_toIterM {α β : Type w} [Iterator α Id β]
     [Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m]
     [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
     {γ : Type w} {it : Iter (α := α) β} {init : γ} {f : γ → β → m γ} :
-    it.foldM (init := init) f = it.toIterM.foldM (init := init) f := by
-  simp [foldM_eq_forIn, IterM.foldM_eq_forIn, forIn_eq_forIn_toIterM]
+    it.foldM (init := init) f = it.toIterM.foldM (init := init) f :=
+  (rfl)
 
-theorem Iter.forIn_yield_eq_foldM {α β : Type w} {γ : Type x} {δ : Type x} [Iterator α Id β]
-    [Finite α Id] {m : Type x → Type x'} [Monad m] [LawfulMonad m] [IteratorLoop α Id m]
+theorem Iter.forIn_yield_eq_foldM {α β γ δ : Type w} [Iterator α Id β]
+    [Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m] [IteratorLoop α Id m]
     [LawfulIteratorLoop α Id m] {f : β → γ → m δ} {g : β → γ → δ → γ} {init : γ}
     {it : Iter (α := α) β} :
-    ForIn.forIn (m := m) it init (fun c b => (fun d => .yield (g c b d)) <$> f c b) =
-      it.foldM (m := m) (fun b c => g c b <$> f c b) init := by
+    ForIn.forIn it init (fun c b => (fun d => .yield (g c b d)) <$> f c b) =
+      it.foldM (fun b c => g c b <$> f c b) init := by
   simp [Iter.foldM_eq_forIn]
 
-theorem Iter.foldM_eq_match_step {α β : Type w} {γ : Type x} [Iterator α Id β] [Finite α Id]
-    {m : Type x → Type x'} [Monad m] [LawfulMonad m] [IteratorLoop α Id m]
+theorem Iter.foldM_eq_match_step {α β γ : Type w} [Iterator α Id β] [Finite α Id]
+    {m : Type w → Type w'} [Monad m] [LawfulMonad m] [IteratorLoop α Id m]
     [LawfulIteratorLoop α Id m] {f : γ → β → m γ} {init : γ} {it : Iter (α := α) β} :
     it.foldM (init := init) f = (do
       match it.step with
@@ -288,19 +289,20 @@ theorem Iter.foldM_eq_match_step {α β : Type w} {γ : Type x} [Iterator α Id
   generalize it.step = step
   cases step using PlausibleIterStep.casesOn <;> simp [foldM_eq_forIn]
 
-theorem Iter.foldlM_toList {α β : Type w} {γ : Type x} [Iterator α Id β] [Finite α Id]
-    {m : Type x → Type x'} [Monad m] [LawfulMonad m] [IteratorLoop α Id m]
-    [LawfulIteratorLoop α Id m] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
-    {f : γ → β → m γ} {init : γ} {it : Iter (α := α) β} :
+theorem Iter.foldlM_toList {α β γ : Type w} [Iterator α Id β] [Finite α Id] {m : Type w → Type w'}
+    [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
+    [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
+    {f : γ → β → m γ}
+    {init : γ} {it : Iter (α := α) β} :
     it.toList.foldlM (init := init) f = it.foldM (init := init) f := by
   rw [Iter.foldM_eq_forIn, ← Iter.forIn_toList]
   simp only [List.forIn_yield_eq_foldlM, id_map']
 
 theorem IterM.forIn_eq_foldM {α β : Type w} [Iterator α Id β]
-    [Finite α Id] {m : Type x → Type x'} [Monad m] [LawfulMonad m]
+    [Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m]
     [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
     [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
-    {γ : Type x} {it : Iter (α := α) β} {init : γ}
+    {γ : Type w} {it : Iter (α := α) β} {init : γ}
     {f : β → γ → m (ForInStep γ)} :
     forIn it init f = ForInStep.value <$>
       it.foldM (fun c b => match c with
@@ -308,28 +310,31 @@ theorem IterM.forIn_eq_foldM {α β : Type w} [Iterator α Id β]
         | .done c => pure (.done c)) (ForInStep.yield init) := by
   simp only [← Iter.forIn_toList, List.forIn_eq_foldlM, ← Iter.foldlM_toList]; rfl
 
-theorem Iter.fold_eq_forIn {α β : Type w} {γ : Type x} [Iterator α Id β]
+theorem Iter.fold_eq_forIn {α β γ : Type w} [Iterator α Id β]
     [Finite α Id] [IteratorLoop α Id Id] {f : γ → β → γ} {init : γ} {it : Iter (α := α) β} :
     it.fold (init := init) f =
       (ForIn.forIn (m := Id) it init (fun x acc => pure (ForInStep.yield (f acc x)))).run := by
   rfl
 
-theorem Iter.fold_eq_foldM {α β : Type w} {γ : Type x} [Iterator α Id β]
-    [Finite α Id] [IteratorLoop α Id Id] {f : γ → β → γ} {init : γ} {it : Iter (α := α) β} :
+theorem Iter.fold_eq_foldM {α β γ : Type w} [Iterator α Id β]
+    [Finite α Id] [IteratorLoop α Id Id] {f : γ → β → γ} {init : γ}
+    {it : Iter (α := α) β} :
     it.fold (init := init) f = (it.foldM (m := Id) (init := init) (pure <| f · ·)).run := by
   simp [foldM_eq_forIn, fold_eq_forIn]
 
 @[simp]
-theorem Iter.forIn_pure_yield_eq_fold {α β : Type w} {γ : Type x} [Iterator α Id β]
-    [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {f : β → γ → γ} {init : γ}
+theorem Iter.forIn_pure_yield_eq_fold {α β γ : Type w} [Iterator α Id β]
+    [Finite α Id] [IteratorLoop α Id Id]
+    [LawfulIteratorLoop α Id Id] {f : β → γ → γ} {init : γ}
     {it : Iter (α := α) β} :
     ForIn.forIn (m := Id) it init (fun c b => pure (.yield (f c b))) =
       pure (it.fold (fun b c => f c b) init) := by
   simp only [fold_eq_forIn]
   rfl
 
-theorem Iter.fold_eq_match_step {α β : Type w} {γ : Type x} [Iterator α Id β] [Finite α Id]
-    [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {f : γ → β → γ} {init : γ} {it : Iter (α := α) β} :
+theorem Iter.fold_eq_match_step {α β γ : Type w} [Iterator α Id β] [Finite α Id]
+    [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
+    {f : γ → β → γ} {init : γ} {it : Iter (α := α) β} :
     it.fold (init := init) f = (match it.step with
       | .yield it' out _ => it'.fold (init := f init out) f
       | .skip it' _ => it'.fold (init := init) f
@@ -340,7 +345,7 @@ theorem Iter.fold_eq_match_step {α β : Type w} {γ : Type x} [Iterator α Id
   cases step using PlausibleIterStep.casesOn <;> simp
 
 @[simp]
-theorem Iter.foldl_toList {α β : Type w} {γ : Type x} [Iterator α Id β] [Finite α Id]
+theorem Iter.foldl_toList {α β γ : Type w} [Iterator α Id β] [Finite α Id]
     [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
     [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
     {f : γ → β → γ} {init : γ} {it : Iter (α := α) β} :

src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean

@@ -15,26 +15,28 @@ namespace Std.Iterators
 
 theorem IterM.DefaultConsumers.forIn'_eq_match_step {α β : Type w} {m : Type w → Type w'}
     [Iterator α m β]
-    {n : Type x → Type x'} [Monad n]
-    {lift : ∀ γ δ, (γ → n δ) → m γ → n δ} {γ : Type x}
+    {n : Type w → Type w''} [Monad n]
+    {lift : ∀ γ, m γ → n γ} {γ : Type w}
     {plausible_forInStep : β → γ → ForInStep γ → Prop}
     {wf : IteratorLoop.WellFounded α m plausible_forInStep}
     {it : IterM (α := α) m β} {init : γ}
-    {P hP} {f : (b : β) → P b → (c : γ) → n (Subtype (plausible_forInStep b c))} :
-    IterM.DefaultConsumers.forIn' lift γ plausible_forInStep wf it init P hP f =
-      (lift _ _ · it.step) (fun
-          | .yield it' out h => do
-            match ← f out (hP _ <| .direct ⟨_, h⟩) init with
-            | ⟨.yield c, _⟩ =>
-              IterM.DefaultConsumers.forIn' lift _ plausible_forInStep wf it' c P
-                (fun _ h' => hP _ <| .indirect ⟨_, rfl, h⟩ h') f
-            | ⟨.done c, _⟩ => return c
-          | .skip it' h =>
-            IterM.DefaultConsumers.forIn' lift _ plausible_forInStep wf it' init P
-              (fun _ h' => hP _ <| .indirect ⟨_, rfl, h⟩ h') f
-          | .done _ => return init) := by
+    {P hP}
+    {f : (b : β) → P b → (c : γ) → n (Subtype (plausible_forInStep b c))} :
+    IterM.DefaultConsumers.forIn' lift γ plausible_forInStep wf it init P hP f = (do
+      match ← lift _ it.step with
+      | .yield it' out h =>
+        match ← f out (hP _ <| .direct ⟨_, h⟩) init with
+        | ⟨.yield c, _⟩ =>
+          IterM.DefaultConsumers.forIn' lift _ plausible_forInStep wf it' c P
+            (fun _ h' => hP _ <| .indirect ⟨_, rfl, h⟩ h') f
+        | ⟨.done c, _⟩ => return c
+      | .skip it' h =>
+        IterM.DefaultConsumers.forIn' lift _ plausible_forInStep wf it' init P
+          (fun _ h' => hP _ <| .indirect ⟨_, rfl, h⟩ h') f
+      | .done _ => return init) := by
   rw [forIn']
-  congr; ext step
+  apply bind_congr
+  intro step
   cases step using PlausibleIterStep.casesOn <;> rfl
 
 theorem IterM.forIn'_eq {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m]
@@ -42,8 +44,7 @@ theorem IterM.forIn'_eq {α β : Type w} {m : Type w → Type w'} [Iterator α m
     [MonadLiftT m n] {γ : Type w} {it : IterM (α := α) m β} {init : γ}
     {f : (b : β) → it.IsPlausibleIndirectOutput b → γ → n (ForInStep γ)} :
     letI : ForIn' n (IterM (α := α) m β) β _ := IterM.instForIn'
-    ForIn'.forIn' it init f = IterM.DefaultConsumers.forIn' (n := n)
-        (fun _ _ f x => monadLift x >>= f) γ (fun _ _ _ => True)
+    ForIn'.forIn' it init f = IterM.DefaultConsumers.forIn' (fun _ => monadLift) γ (fun _ _ _ => True)
         IteratorLoop.wellFounded_of_finite it init _ (fun _ => id) ((⟨·, .intro⟩) <$> f · · ·) := by
   cases hl.lawful; rfl
 
@@ -51,15 +52,14 @@ theorem IterM.forIn_eq {α β : Type w} {m : Type w → Type w'} [Iterator α m
     {n : Type w → Type w''} [Monad n] [IteratorLoop α m n] [hl : LawfulIteratorLoop α m n]
     [MonadLiftT m n] {γ : Type w} {it : IterM (α := α) m β} {init : γ}
     {f : β → γ → n (ForInStep γ)} :
-    ForIn.forIn it init f = IterM.DefaultConsumers.forIn' (n := n)
-        (fun _ _ f x => monadLift x >>= f) γ (fun _ _ _ => True)
+    ForIn.forIn it init f = IterM.DefaultConsumers.forIn' (fun _ => monadLift) γ (fun _ _ _ => True)
         IteratorLoop.wellFounded_of_finite it init _ (fun _ => id) (fun out _ acc => (⟨·, .intro⟩) <$> f out acc) := by
   cases hl.lawful; rfl
 
 theorem IterM.DefaultConsumers.forIn'_eq_forIn' {m : Type w → Type w'} {α : Type w} {β : Type w}
     [Iterator α m β]
-    {n : Type x → Type x'} [Monad n]
-    {liftBind : ∀ γ δ, (γ → n δ) → m γ → n δ} {γ : Type x}
+    {n : Type w → Type w''} [Monad n]
+    {lift : ∀ γ, m γ → n γ} {γ : Type w}
     {Pl : β → γ → ForInStep γ → Prop}
     {wf : IteratorLoop.WellFounded α m Pl}
     {it : IterM (α := α) m β} {init : γ}
@@ -68,10 +68,11 @@ theorem IterM.DefaultConsumers.forIn'_eq_forIn' {m : Type w → Type w'} {α : T
     {f : (b : β) → P b → (c : γ) → n (Subtype (Pl b c))}
     {g : (b : β) → Q b → (c : γ) → n (Subtype (Pl b c))}
     (hfg : ∀ b c, (hPb : P b) → (hQb : Q b) → f b hPb c = g b hQb c) :
-    IterM.DefaultConsumers.forIn' liftBind γ Pl wf it init P hP f =
-      IterM.DefaultConsumers.forIn' liftBind γ Pl wf it init Q hQ g := by
+    IterM.DefaultConsumers.forIn' lift γ Pl wf it init P hP f =
+      IterM.DefaultConsumers.forIn' lift γ Pl wf it init Q hQ g := by
   rw [forIn', forIn']
-  congr; ext step
+  apply bind_congr
+  intro step
   split
   · congr
     · apply hfg
@@ -137,7 +138,8 @@ theorem IterM.forIn_eq_match_step {α β : Type w} {m : Type w → Type w'} [Ite
       | .skip it' _ => ForIn.forIn it' init f
       | .done _ => return init) := by
   simp only [forIn]
-  exact forIn'_eq_match_step
+  rw [forIn'_eq_match_step]
+  rfl
 
 theorem IterM.forM_eq_forIn {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
     [Finite α m] {n : Type w → Type w''} [Monad n] [LawfulMonad n]

src/Init/Data/List/BasicAux.lean

@@ -130,7 +130,7 @@ Safer alternatives include:
   * `List.head?`, which returns an `Option`, and
   * `List.headD`, which returns an explicitly-provided fallback value on empty lists.
 -/
-@[expose] def head! [Inhabited α] : List α → α
+def head! [Inhabited α] : List α → α
   | []   => panic! "empty list"
   | a::_ => a
 
@@ -362,13 +362,12 @@ theorem not_lex_antisymm [DecidableEq α] {r : α → α → Prop} [DecidableRel
         · exact h₁ (Lex.rel hba)
         · exact eq (antisymm _ _ hab hba)
 
-protected theorem le_antisymm [LT α]
+protected theorem le_antisymm [DecidableEq α] [LT α] [DecidableLT α]
     [i : Std.Antisymm (¬ · < · : α → α → Prop)]
     {as bs : List α} (h₁ : as ≤ bs) (h₂ : bs ≤ as) : as = bs :=
-  open Classical in
   not_lex_antisymm i.antisymm h₁ h₂
 
-instance [LT α]
+instance [DecidableEq α] [LT α] [DecidableLT α]
     [s : Std.Antisymm (¬ · < · : α → α → Prop)] :
     Std.Antisymm (· ≤ · : List α → List α → Prop) where
   antisymm _ _ h₁ h₂ := List.le_antisymm h₁ h₂

src/Init/Data/List/Lex.lean

@@ -22,9 +22,9 @@ namespace List
 @[simp] theorem not_lex_lt [LT α] {l₁ l₂ : List α} : ¬ Lex (· < ·) l₁ l₂ ↔ l₂ ≤ l₁ := Iff.rfl
 
 protected theorem not_lt_iff_ge [LT α] {l₁ l₂ : List α} : ¬ l₁ < l₂ ↔ l₂ ≤ l₁ := Iff.rfl
-protected theorem not_le_iff_gt [LT α] {l₁ l₂ : List α} :
+protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : List α} :
     ¬ l₁ ≤ l₂ ↔ l₂ < l₁ :=
-  Classical.not_not
+  Decidable.not_not
 
 theorem lex_irrefl {r : α → α → Prop} (irrefl : ∀ x, ¬r x x) (l : List α) : ¬Lex r l l := by
   induction l with
@@ -78,14 +78,13 @@ theorem not_cons_lex_cons_iff [DecidableEq α] [DecidableRel r] {a b} {l₁ l₂
     ¬ Lex r (a :: l₁) (b :: l₂) ↔ (¬ r a b ∧ a ≠ b) ∨ (¬ r a b ∧ ¬ Lex r l₁ l₂) := by
   rw [cons_lex_cons_iff, not_or, Decidable.not_and_iff_or_not, and_or_left]
 
-theorem cons_le_cons_iff [LT α]
+theorem cons_le_cons_iff [DecidableEq α] [LT α] [DecidableLT α]
     [i₀ : Std.Irrefl (· < · : α → α → Prop)]
     [i₁ : Std.Asymm (· < · : α → α → Prop)]
     [i₂ : Std.Antisymm (¬ · < · : α → α → Prop)]
     {a b} {l₁ l₂ : List α} :
     (a :: l₁) ≤ (b :: l₂) ↔ a < b ∨ a = b ∧ l₁ ≤ l₂ := by
   dsimp only [instLE, instLT, List.le, List.lt]
-  open Classical in
   simp only [not_cons_lex_cons_iff, ne_eq]
   constructor
   · rintro (⟨h₁, h₂⟩ | ⟨h₁, h₂⟩)
@@ -105,7 +104,7 @@ theorem cons_le_cons_iff [LT α]
     · right
       exact ⟨fun w => i₀.irrefl _ (h₁ ▸ w), h₂⟩
 
-theorem not_lt_of_cons_le_cons [LT α]
+theorem not_lt_of_cons_le_cons [DecidableEq α] [LT α] [DecidableLT α]
     [i₀ : Std.Irrefl (· < · : α → α → Prop)]
     [i₁ : Std.Asymm (· < · : α → α → Prop)]
     [i₂ : Std.Antisymm (¬ · < · : α → α → Prop)]
@@ -115,7 +114,7 @@ theorem not_lt_of_cons_le_cons [LT α]
   · exact i₁.asymm _ _ h
   · exact i₀.irrefl _
 
-theorem le_of_cons_le_cons [LT α]
+theorem le_of_cons_le_cons [DecidableEq α] [LT α] [DecidableLT α]
     [i₀ : Std.Irrefl (· < · : α → α → Prop)]
     [i₁ : Std.Asymm (· < · : α → α → Prop)]
     [i₂ : Std.Antisymm (¬ · < · : α → α → Prop)]
@@ -166,7 +165,7 @@ instance [LT α] [Trans (· < · : α → α → Prop) (· < ·) (· < ·)] :
 @[deprecated List.le_antisymm (since := "2024-12-13")]
 protected abbrev lt_antisymm := @List.le_antisymm
 
-protected theorem lt_of_le_of_lt [LT α]
+protected theorem lt_of_le_of_lt [DecidableEq α] [LT α] [DecidableLT α]
     [i₀ : Std.Irrefl (· < · : α → α → Prop)]
     [i₁ : Std.Asymm (· < · : α → α → Prop)]
     [i₂ : Std.Antisymm (¬ · < · : α → α → Prop)]
@@ -181,7 +180,7 @@ protected theorem lt_of_le_of_lt [LT α]
     | cons c l₁ =>
       apply Lex.rel
       replace h₁ := not_lt_of_cons_le_cons h₁
-      apply Classical.byContradiction
+      apply Decidable.byContradiction
       intro h₂
       have := i₃.trans h₁ h₂
       contradiction
@@ -194,9 +193,9 @@ protected theorem lt_of_le_of_lt [LT α]
       by_cases w₅ : a = c
       · subst w₅
         exact Lex.cons (ih (le_of_cons_le_cons h₁))
-      · exact Lex.rel (Classical.byContradiction fun w₆ => w₅ (i₂.antisymm _ _ w₄ w₆))
+      · exact Lex.rel (Decidable.byContradiction fun w₆ => w₅ (i₂.antisymm _ _ w₄ w₆))
 
-protected theorem le_trans [LT α]
+protected theorem le_trans [DecidableEq α] [LT α] [DecidableLT α]
     [Std.Irrefl (· < · : α → α → Prop)]
     [Std.Asymm (· < · : α → α → Prop)]
     [Std.Antisymm (¬ · < · : α → α → Prop)]
@@ -204,7 +203,7 @@ protected theorem le_trans [LT α]
     {l₁ l₂ l₃ : List α} (h₁ : l₁ ≤ l₂) (h₂ : l₂ ≤ l₃) : l₁ ≤ l₃ :=
   fun h₃ => h₁ (List.lt_of_le_of_lt h₂ h₃)
 
-instance [LT α]
+instance [DecidableEq α] [LT α] [DecidableLT α]
     [Std.Irrefl (· < · : α → α → Prop)]
     [Std.Asymm (· < · : α → α → Prop)]
     [Std.Antisymm (¬ · < · : α → α → Prop)]
@@ -232,9 +231,9 @@ instance [LT α] [Std.Asymm (· < · : α → α → Prop)] :
     Std.Asymm (· < · : List α → List α → Prop) where
   asymm _ _ := List.lt_asymm
 
-theorem not_lex_total {r : α → α → Prop}
+theorem not_lex_total [DecidableEq α] {r : α → α → Prop} [DecidableRel r]
     (h : ∀ x y : α, ¬ r x y ∨ ¬ r y x) (l₁ l₂ : List α) : ¬ Lex r l₁ l₂ ∨ ¬ Lex r l₂ l₁ := by
-  rw [Classical.or_iff_not_imp_left, Classical.not_not]
+  rw [Decidable.or_iff_not_imp_left, Decidable.not_not]
   intro w₁ w₂
   match l₁, l₂, w₁, w₂ with
   | nil, _ :: _, .nil, w₂ => simp at w₂
@@ -247,11 +246,11 @@ theorem not_lex_total {r : α → α → Prop}
   | _ :: l₁, _ :: l₂, .cons _, .cons _ =>
     obtain (_ | _) := not_lex_total h l₁ l₂ <;> contradiction
 
-protected theorem le_total [LT α]
+protected theorem le_total [DecidableEq α] [LT α] [DecidableLT α]
     [i : Std.Total (¬ · < · : α → α → Prop)] (l₁ l₂ : List α) : l₁ ≤ l₂ ∨ l₂ ≤ l₁ :=
   not_lex_total i.total l₂ l₁
 
-instance [LT α]
+instance [DecidableEq α] [LT α] [DecidableLT α]
     [Std.Total (¬ · < · : α → α → Prop)] :
     Std.Total (· ≤ · : List α → List α → Prop) where
   total := List.le_total
@@ -259,10 +258,10 @@ instance [LT α]
 @[simp] protected theorem not_lt [LT α]
     {l₁ l₂ : List α} : ¬ l₁ < l₂ ↔ l₂ ≤ l₁ := Iff.rfl
 
-@[simp] protected theorem not_le [LT α]
-    {l₁ l₂ : List α} : ¬ l₂ ≤ l₁ ↔ l₁ < l₂ := Classical.not_not
+@[simp] protected theorem not_le [DecidableEq α] [LT α] [DecidableLT α]
+    {l₁ l₂ : List α} : ¬ l₂ ≤ l₁ ↔ l₁ < l₂ := Decidable.not_not
 
-protected theorem le_of_lt [LT α]
+protected theorem le_of_lt [DecidableEq α] [LT α] [DecidableLT α]
     [i : Std.Total (¬ · < · : α → α → Prop)]
     {l₁ l₂ : List α} (h : l₁ < l₂) : l₁ ≤ l₂ := by
   obtain (h' | h') := List.le_total l₁ l₂
@@ -270,7 +269,7 @@ protected theorem le_of_lt [LT α]
   · exfalso
     exact h' h
 
-protected theorem le_iff_lt_or_eq [LT α]
+protected theorem le_iff_lt_or_eq [DecidableEq α] [LT α] [DecidableLT α]
     [Std.Irrefl (· < · : α → α → Prop)]
     [Std.Antisymm (¬ · < · : α → α → Prop)]
     [Std.Total (¬ · < · : α → α → Prop)]
@@ -281,7 +280,7 @@ protected theorem le_iff_lt_or_eq [LT α]
     · right
       apply List.le_antisymm h h'
     · left
-      exact Classical.not_not.mp h'
+      exact Decidable.not_not.mp h'
   · rintro (h | rfl)
     · exact List.le_of_lt h
     · exact List.le_refl l₁
@@ -446,17 +445,16 @@ theorem lex_eq_false_iff_exists [BEq α] [PartialEquivBEq α] (lt : α → α
               simpa using w₁ (j + 1) (by simpa)
             · simpa using w₂
 
-protected theorem lt_iff_exists [LT α] {l₁ l₂ : List α} :
+protected theorem lt_iff_exists [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : List α} :
     l₁ < l₂ ↔
       (l₁ = l₂.take l₁.length ∧ l₁.length < l₂.length) ∨
         (∃ (i : Nat) (h₁ : i < l₁.length) (h₂ : i < l₂.length),
           (∀ j, (hj : j < i) →
             l₁[j]'(Nat.lt_trans hj h₁) = l₂[j]'(Nat.lt_trans hj h₂)) ∧ l₁[i] < l₂[i]) := by
-  open Classical in
   rw [← lex_eq_true_iff_lt, lex_eq_true_iff_exists]
   simp
 
-protected theorem le_iff_exists [LT α]
+protected theorem le_iff_exists [DecidableEq α] [LT α] [DecidableLT α]
     [Std.Irrefl (· < · : α → α → Prop)]
     [Std.Asymm (· < · : α → α → Prop)]
     [Std.Antisymm (¬ · < · : α → α → Prop)] {l₁ l₂ : List α} :
@@ -465,7 +463,6 @@ protected theorem le_iff_exists [LT α]
         (∃ (i : Nat) (h₁ : i < l₁.length) (h₂ : i < l₂.length),
           (∀ j, (hj : j < i) →
             l₁[j]'(Nat.lt_trans hj h₁) = l₂[j]'(Nat.lt_trans hj h₂)) ∧ l₁[i] < l₂[i]) := by
-  open Classical in
   rw [← lex_eq_false_iff_ge, lex_eq_false_iff_exists]
   · simp only [isEqv_eq, beq_iff_eq, decide_eq_true_eq]
     simp only [eq_comm]
@@ -480,7 +477,7 @@ theorem append_left_lt [LT α] {l₁ l₂ l₃ : List α} (h : l₂ < l₃) :
   | nil => simp [h]
   | cons a l₁ ih => simp [cons_lt_cons_iff, ih]
 
-theorem append_left_le [LT α]
+theorem append_left_le [DecidableEq α] [LT α] [DecidableLT α]
     [Std.Irrefl (· < · : α → α → Prop)]
     [Std.Asymm (· < · : α → α → Prop)]
     [Std.Antisymm (¬ · < · : α → α → Prop)]
@@ -514,7 +511,7 @@ protected theorem map_lt [LT α] [LT β]
   | cons a l₁, cons b l₂, .rel h =>
     simp [cons_lt_cons_iff, w, h]
 
-protected theorem map_le [LT α] [LT β]
+protected theorem map_le [DecidableEq α] [LT α] [DecidableLT α] [DecidableEq β] [LT β] [DecidableLT β]
     [Std.Irrefl (· < · : α → α → Prop)]
     [Std.Asymm (· < · : α → α → Prop)]
     [Std.Antisymm (¬ · < · : α → α → Prop)]

src/Init/Data/Ord.lean

@@ -247,12 +247,12 @@ theorem isEq_eq_beq_eq : ∀ {o : Ordering}, o.isEq = (o == .eq) := by decide
 theorem isNe_eq_not_beq_eq : ∀ {o : Ordering}, o.isNe = (!o == .eq) := by decide
 theorem isNe_eq_isLT_or_isGT : ∀ {o : Ordering}, o.isNe = (o.isLT || o.isGT) := by decide
 
-@[simp] theorem not_isLT_eq_isGE : ∀ {o : Ordering}, (!o.isLT) = o.isGE := by decide
-@[simp] theorem not_isLE_eq_isGT : ∀ {o : Ordering}, (!o.isLE) = o.isGT := by decide
-@[simp] theorem not_isGT_eq_isLE : ∀ {o : Ordering}, (!o.isGT) = o.isLE := by decide
-@[simp] theorem not_isGE_eq_isLT : ∀ {o : Ordering}, (!o.isGE) = o.isLT := by decide
-@[simp] theorem not_isNe_eq_isEq : ∀ {o : Ordering}, (!o.isNe) = o.isEq := by decide
-theorem not_isEq_eq_isNe : ∀ {o : Ordering}, (!o.isEq) = o.isNe := by decide
+@[simp] theorem not_isLT_eq_isGE : ∀ {o : Ordering}, !o.isLT = o.isGE := by decide
+@[simp] theorem not_isLE_eq_isGT : ∀ {o : Ordering}, !o.isLE = o.isGT := by decide
+@[simp] theorem not_isGT_eq_isLE : ∀ {o : Ordering}, !o.isGT = o.isLE := by decide
+@[simp] theorem not_isGE_eq_isLT : ∀ {o : Ordering}, !o.isGE = o.isLT := by decide
+@[simp] theorem not_isNe_eq_isEq : ∀ {o : Ordering}, !o.isNe = o.isEq := by decide
+theorem not_isEq_eq_isNe : ∀ {o : Ordering}, !o.isEq = o.isNe := by decide
 
 theorem ne_lt_iff_isGE : ∀ {o : Ordering}, ¬o = .lt ↔ o.isGE := by decide
 theorem ne_gt_iff_isLE : ∀ {o : Ordering}, ¬o = .gt ↔ o.isLE := by decide

src/Init/Data/Range/Polymorphic/RangeIterator.lean

@@ -111,20 +111,20 @@ theorem RangeIterator.step_eq_step {su} [UpwardEnumerable α] [SupportsUpperBoun
   simp [Iter.step, step_eq_monadicStep, Monadic.step_eq_step, IterM.Step.toPure]
 
 @[always_inline, inline]
-instance RangeIterator.instIteratorLoop {su} [UpwardEnumerable α] [SupportsUpperBound su α]
-    {n : Type v → Type w} [Monad n] :
+instance RepeatIterator.instIteratorLoop {su} [UpwardEnumerable α] [SupportsUpperBound su α]
+    {n : Type u → Type w} [Monad n] :
     IteratorLoop (RangeIterator su α) Id n :=
   .defaultImplementation
 
-instance RangeIterator.instIteratorLoopPartial {su} [UpwardEnumerable α] [SupportsUpperBound su α]
-    {n : Type v → Type w} [Monad n] : IteratorLoopPartial (RangeIterator su α) Id n :=
+instance RepeatIterator.instIteratorLoopPartial {su} [UpwardEnumerable α] [SupportsUpperBound su α]
+    {n : Type u → Type w} [Monad n] : IteratorLoopPartial (RangeIterator su α) Id n :=
   .defaultImplementation
 
-instance RangeIterator.instIteratorCollect {su} [UpwardEnumerable α] [SupportsUpperBound su α]
+instance RepeatIterator.instIteratorCollect {su} [UpwardEnumerable α] [SupportsUpperBound su α]
     {n : Type u → Type w} [Monad n] : IteratorCollect (RangeIterator su α) Id n :=
   .defaultImplementation
 
-instance RangeIterator.instIteratorCollectPartial {su} [UpwardEnumerable α] [SupportsUpperBound su α]
+instance RepeatIterator.instIteratorCollectPartial {su} [UpwardEnumerable α] [SupportsUpperBound su α]
     {n : Type u → Type w} [Monad n] : IteratorCollectPartial (RangeIterator su α) Id n :=
   .defaultImplementation
 

src/Init/Data/Vector/Lemmas.lean

@@ -1213,7 +1213,7 @@ theorem contains_iff [BEq α] [LawfulBEq α] {a : α} {as : Vector α n} :
 instance [BEq α] [LawfulBEq α] (a : α) (as : Vector α n) : Decidable (a ∈ as) :=
   decidable_of_decidable_of_iff contains_iff
 
-@[grind] theorem contains_empty [BEq α] : (#v[] : Vector α 0).contains a = false := by simp
+@[grind] theorem contains_empty [BEq α] : (#v[] : Vector α 0).contains a = false := rfl
 
 @[simp, grind] theorem contains_eq_mem [BEq α] [LawfulBEq α] {a : α} {as : Vector α n} :
     as.contains a = decide (a ∈ as) := by
@@ -2975,7 +2975,7 @@ variable [BEq α]
   rcases xs with ⟨xs, rfl⟩
   simp
 
-@[simp, grind] theorem replace_empty : (#v[] : Vector α 0).replace a b = #v[] := by simp
+@[simp, grind] theorem replace_empty : (#v[] : Vector α 0).replace a b = #v[] := by rfl
 
 @[grind] theorem replace_singleton {a b c : α} : #v[a].replace b c = #v[if a == b then c else a] := by
   simp

src/Init/Data/Vector/Lex.lean

@@ -28,9 +28,9 @@ namespace Vector
 @[simp] theorem le_toList [LT α] {xs ys : Vector α n} : xs.toList ≤ ys.toList ↔ xs ≤ ys := Iff.rfl
 
 protected theorem not_lt_iff_ge [LT α] {xs ys : Vector α n} : ¬ xs < ys ↔ ys ≤ xs := Iff.rfl
-protected theorem not_le_iff_gt [LT α] {xs ys : Vector α n} :
+protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] {xs ys : Vector α n} :
     ¬ xs ≤ ys ↔ ys < xs :=
-  Classical.not_not
+  Decidable.not_not
 
 @[simp] theorem mk_lt_mk [LT α] :
     Vector.mk (α := α) (n := n) data₁ size₁ < Vector.mk data₂ size₂ ↔ data₁ < data₂ := Iff.rfl
@@ -92,7 +92,7 @@ instance [LT α]
     Trans (· < · : Vector α n → Vector α n → Prop) (· < ·) (· < ·) where
   trans h₁ h₂ := Vector.lt_trans h₁ h₂
 
-protected theorem lt_of_le_of_lt [LT α]
+protected theorem lt_of_le_of_lt [DecidableEq α] [LT α] [DecidableLT α]
     [i₀ : Std.Irrefl (· < · : α → α → Prop)]
     [i₁ : Std.Asymm (· < · : α → α → Prop)]
     [i₂ : Std.Antisymm (¬ · < · : α → α → Prop)]
@@ -100,7 +100,7 @@ protected theorem lt_of_le_of_lt [LT α]
     {xs ys zs : Vector α n} (h₁ : xs ≤ ys) (h₂ : ys < zs) : xs < zs :=
   Array.lt_of_le_of_lt h₁ h₂
 
-protected theorem le_trans [LT α]
+protected theorem le_trans [DecidableEq α] [LT α] [DecidableLT α]
     [Std.Irrefl (· < · : α → α → Prop)]
     [Std.Asymm (· < · : α → α → Prop)]
     [Std.Antisymm (¬ · < · : α → α → Prop)]
@@ -108,7 +108,7 @@ protected theorem le_trans [LT α]
     {xs ys zs : Vector α n} (h₁ : xs ≤ ys) (h₂ : ys ≤ zs) : xs ≤ zs :=
   fun h₃ => h₁ (Vector.lt_of_le_of_lt h₂ h₃)
 
-instance [LT α]
+instance [DecidableEq α] [LT α] [DecidableLT α]
     [Std.Irrefl (· < · : α → α → Prop)]
     [Std.Asymm (· < · : α → α → Prop)]
     [Std.Antisymm (¬ · < · : α → α → Prop)]
@@ -120,16 +120,16 @@ protected theorem lt_asymm [LT α]
     [i : Std.Asymm (· < · : α → α → Prop)]
     {xs ys : Vector α n} (h : xs < ys) : ¬ ys < xs := Array.lt_asymm h
 
-instance [LT α]
+instance [DecidableEq α] [LT α] [DecidableLT α]
     [Std.Asymm (· < · : α → α → Prop)] :
     Std.Asymm (· < · : Vector α n → Vector α n → Prop) where
   asymm _ _ := Vector.lt_asymm
 
-protected theorem le_total [LT α]
+protected theorem le_total [DecidableEq α] [LT α] [DecidableLT α]
     [i : Std.Total (¬ · < · : α → α → Prop)] (xs ys : Vector α n) : xs ≤ ys ∨ ys ≤ xs :=
   Array.le_total _ _
 
-instance [LT α]
+instance [DecidableEq α] [LT α] [DecidableLT α]
     [Std.Total (¬ · < · : α → α → Prop)] :
     Std.Total (· ≤ · : Vector α n → Vector α n → Prop) where
   total := Vector.le_total
@@ -137,15 +137,15 @@ instance [LT α]
 @[simp] protected theorem not_lt [LT α]
     {xs ys : Vector α n} : ¬ xs < ys ↔ ys ≤ xs := Iff.rfl
 
-@[simp] protected theorem not_le [LT α]
-    {xs ys : Vector α n} : ¬ ys ≤ xs ↔ xs < ys := Classical.not_not
+@[simp] protected theorem not_le [DecidableEq α] [LT α] [DecidableLT α]
+    {xs ys : Vector α n} : ¬ ys ≤ xs ↔ xs < ys := Decidable.not_not
 
-protected theorem le_of_lt [LT α]
+protected theorem le_of_lt [DecidableEq α] [LT α] [DecidableLT α]
     [i : Std.Total (¬ · < · : α → α → Prop)]
     {xs ys : Vector α n} (h : xs < ys) : xs ≤ ys :=
   Array.le_of_lt h
 
-protected theorem le_iff_lt_or_eq [LT α]
+protected theorem le_iff_lt_or_eq [DecidableEq α] [LT α] [DecidableLT α]
     [Std.Irrefl (· < · : α → α → Prop)]
     [Std.Antisymm (¬ · < · : α → α → Prop)]
     [Std.Total (¬ · < · : α → α → Prop)]
@@ -210,14 +210,14 @@ theorem lex_eq_false_iff_exists [BEq α] [PartialEquivBEq α] (lt : α → α
   rcases ys with ⟨ys, n₂⟩
   simp_all [Array.lex_eq_false_iff_exists]
 
-protected theorem lt_iff_exists [LT α] {xs ys : Vector α n} :
+protected theorem lt_iff_exists [DecidableEq α] [LT α] [DecidableLT α] {xs ys : Vector α n} :
     xs < ys ↔
       (∃ (i : Nat) (h : i < n), (∀ j, (hj : j < i) → xs[j] = ys[j]) ∧ xs[i] < ys[i]) := by
   cases xs
   cases ys
   simp_all [Array.lt_iff_exists]
 
-protected theorem le_iff_exists [LT α]
+protected theorem le_iff_exists [DecidableEq α] [LT α] [DecidableLT α]
     [Std.Irrefl (· < · : α → α → Prop)]
     [Std.Asymm (· < · : α → α → Prop)]
     [Std.Antisymm (¬ · < · : α → α → Prop)] {xs ys : Vector α n} :
@@ -232,7 +232,7 @@ theorem append_left_lt [LT α] {xs : Vector α n} {ys ys' : Vector α m} (h : ys
     xs ++ ys < xs ++ ys' := by
   simpa using Array.append_left_lt h
 
-theorem append_left_le [LT α]
+theorem append_left_le [DecidableEq α] [LT α] [DecidableLT α]
     [Std.Irrefl (· < · : α → α → Prop)]
     [Std.Asymm (· < · : α → α → Prop)]
     [Std.Antisymm (¬ · < · : α → α → Prop)]
@@ -245,7 +245,7 @@ protected theorem map_lt [LT α] [LT β]
     map f xs < map f ys := by
   simpa using Array.map_lt w h
 
-protected theorem map_le [LT α] [LT β]
+protected theorem map_le [DecidableEq α] [LT α] [DecidableLT α] [DecidableEq β] [LT β] [DecidableLT β]
     [Std.Irrefl (· < · : α → α → Prop)]
     [Std.Asymm (· < · : α → α → Prop)]
     [Std.Antisymm (¬ · < · : α → α → Prop)]

src/Init/Grind/Ring/Field.lean

@@ -80,45 +80,6 @@ theorem inv_eq_zero_iff {a : α} : a⁻¹ = 0 ↔ a = 0 := by
 theorem zero_eq_inv_iff {a : α} : 0 = a⁻¹ ↔ 0 = a := by
   rw [eq_comm, inv_eq_zero_iff, eq_comm]
 
-theorem of_mul_eq_zero {a b : α} : a*b = 0 → a = 0 ∨ b = 0 := by
-  cases (Classical.em (a = 0)); simp [*, Semiring.zero_mul]
-  cases (Classical.em (b = 0)); simp [*, Semiring.mul_zero]
-  next h₁ h₂ =>
-  replace h₁ := Field.mul_inv_cancel h₁
-  replace h₂ := Field.mul_inv_cancel h₂
-  intro h
-  replace h := congrArg (· * b⁻¹ * a⁻¹) h; simp [Semiring.zero_mul] at h
-  rw [Semiring.mul_assoc, Semiring.mul_assoc, ← Semiring.mul_assoc b, h₂, Semiring.one_mul, h₁] at h
-  have := Field.zero_ne_one (α := α)
-  simp [h] at this
-
-theorem mul_inv (a b : α) : (a*b)⁻¹ = a⁻¹*b⁻¹ := by
-  cases (Classical.em (a = 0)); simp [*, Semiring.zero_mul, Field.inv_zero]
-  cases (Classical.em (b = 0)); simp [*, Semiring.mul_zero, Field.inv_zero]
-  cases (Classical.em (a*b = 0)); simp [*, Field.inv_zero]
-  next h => cases (of_mul_eq_zero h) <;> contradiction
-  next h₁ h₂ h₃ =>
-    replace h₁ := Field.inv_mul_cancel h₁
-    replace h₂ := Field.inv_mul_cancel h₂
-    replace h₃ := Field.mul_inv_cancel h₃
-    replace h₃ := congrArg (b⁻¹*a⁻¹* ·) h₃; simp at h₃
-    rw [Semiring.mul_assoc, Semiring.mul_assoc, ← Semiring.mul_assoc (a⁻¹), h₁, Semiring.one_mul,
-      ← Semiring.mul_assoc, h₂, Semiring.one_mul, Semiring.mul_one, CommRing.mul_comm (b⁻¹)] at h₃
-    assumption
-
-theorem of_pow_eq_zero (a : α) (n : Nat) : a^n = 0 → a = 0 := by
-  induction n
-  next => simp [Semiring.pow_zero]; intro h; have := zero_ne_one (α := α); exfalso; exact this h.symm
-  next n ih =>
-    simp [Semiring.pow_succ]; intro h
-    apply Classical.byContradiction
-    intro hne
-    have := Field.mul_inv_cancel hne
-    replace h := congrArg (· * a⁻¹) h; simp at h
-    rw [Semiring.mul_assoc, this, Semiring.mul_one, Semiring.zero_mul] at h
-    have := ih h
-    contradiction
-
 instance [IsCharP α 0] : NoNatZeroDivisors α := NoNatZeroDivisors.mk' <| by
   intro a b h w
   have := IsCharP.natCast_eq_zero_iff (α := α) 0 a

src/Init/Grind/Ring/Poly.lean

@@ -395,9 +395,7 @@ def Expr.toPoly : Expr → Poly
   | .neg a   => a.toPoly.mulConst (-1)
   | .sub a b => a.toPoly.combine (b.toPoly.mulConst (-1))
   | .pow a k =>
-    bif k == 0 then
-      .num 1
-    else  match a with
+    match a with
     | .num n => .num (n^k)
     | .var x => Poly.ofMon (.mult {x, k} .unit)
     | _ => a.toPoly.pow k
@@ -538,9 +536,7 @@ where
     | .neg a   => (go a).mulConstC (-1) c
     | .sub a b => (go a).combineC ((go b).mulConstC (-1) c) c
     | .pow a k =>
-      bif k == 0 then
-        .num 1
-      else match a with
+      match a with
       | .num n => .num ((n^k) % c)
       | .var x => Poly.ofMon (.mult {x, k} .unit)
       | _ => (go a).powC k c
@@ -806,7 +802,6 @@ theorem Expr.denote_toPoly {α} [CommRing α] (ctx : Context α) (e : Expr)
     <;> simp [denote, Poly.denote, Poly.denote_ofVar, Poly.denote_combine,
           Poly.denote_mul, Poly.denote_mulConst, Poly.denote_pow, intCast_pow, intCast_neg, intCast_one,
           neg_mul, one_mul, sub_eq_add_neg, denoteInt_eq, *]
-  next a k h => simp at h; simp [h, Semiring.pow_zero]
   next => simp [Poly.denote_ofMon, Mon.denote, Power.denote_eq, mul_one]
 
 theorem Expr.eq_of_toPoly_eq {α} [CommRing α] (ctx : Context α) (a b : Expr) (h : a.toPoly == b.toPoly) : a.denote ctx = b.denote ctx := by
@@ -1001,7 +996,6 @@ theorem Expr.denote_toPolyC {α c} [CommRing α] [IsCharP α c] (ctx : Context
   next => rw [IsCharP.intCast_emod]
   next => rw [intCast_neg, neg_mul, intCast_one, one_mul]
   next => rw [intCast_neg, neg_mul, intCast_one, one_mul, sub_eq_add_neg]
-  next a k h => simp at h; simp [h, Semiring.pow_zero, Ring.intCast_one]
   next => rw [IsCharP.intCast_emod, intCast_pow]
   next => simp [Poly.denote_ofMon, Mon.denote, Power.denote_eq, mul_one]
 

src/Init/Grind/Tactics.lean

@@ -86,8 +86,8 @@ syntax grindMod :=
     grindEqBoth <|> grindEqRhs <|> grindEq <|> grindEqBwd <|> grindBwd
     <|> grindFwd <|> grindRL <|> grindLR <|> grindUsr <|> grindCasesEager
     <|> grindCases <|> grindIntro <|> grindExt <|> grindGen
-syntax (name := grind) "grind" (ppSpace grindMod)? : attr
-syntax (name := grind?) "grind?" (ppSpace grindMod)? : attr
+syntax (name := grind) "grind" ppSpace (grindMod)? : attr
+syntax (name := grind?) "grind?" ppSpace (grindMod)? : attr
 end Attr
 end Lean.Parser
 
@@ -479,7 +479,7 @@ example (as : Array α) (lo hi i j : Nat) :
 syntax (name := grind)
   "grind" optConfig (&" only")?
   (" [" withoutPosition(grindParam,*) "]")?
-  (&" on_failure " term)? : tactic
+  ("on_failure " term)? : tactic
 
 /--
 `grind?` takes the same arguments as `grind`, but reports an equivalent call to `grind only`
@@ -489,6 +489,6 @@ theorems in a local invocation.
 syntax (name := grindTrace)
   "grind?" optConfig (&" only")?
   (" [" withoutPosition(grindParam,*) "]")?
-  (&" on_failure " term)? : tactic
+  ("on_failure " term)? : tactic
 
 end Lean.Parser.Tactic

src/Init/WF.lean

@@ -44,7 +44,8 @@ noncomputable abbrev Acc.ndrecOn.{u1, u2} {α : Sort u2} {r : α → α → Prop
 namespace Acc
 variable {α : Sort u} {r : α → α → Prop}
 
-theorem inv {x y : α} (h₁ : Acc r x) (h₂ : r y x) : Acc r y :=
+-- `def` for `WellFounded.fix`
+def inv {x y : α} (h₁ : Acc r x) (h₂ : r y x) : Acc r y :=
   h₁.recOn (fun _ ac₁ _ h₂ => ac₁ y h₂) h₂
 
 end Acc
@@ -77,8 +78,8 @@ class WellFoundedRelation (α : Sort u) where
   wf  : WellFounded rel
 
 namespace WellFounded
-
-theorem apply {α : Sort u} {r : α → α → Prop} (wf : WellFounded r) (a : α) : Acc r a :=
+-- `def` for `WellFounded.fix`
+def apply {α : Sort u} {r : α → α → Prop} (wf : WellFounded r) (a : α) : Acc r a :=
   wf.rec (fun p => p) a
 
 section
@@ -158,13 +159,15 @@ end Subrelation
 namespace InvImage
 variable {α : Sort u} {β : Sort v} {r : β → β → Prop}
 
-theorem accAux (f : α → β) {b : β} (ac : Acc r b) : (x : α) → f x = b → Acc (InvImage r f) x :=
+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)
 
-theorem accessible {a : α} (f : α → β) (ac : Acc r (f a)) : Acc (InvImage r f) a :=
+-- `def` for `WellFounded.fix`
+def accessible {a : α} (f : α → β) (ac : Acc r (f a)) : Acc (InvImage r f) a :=
   accAux f ac a rfl
 
-theorem wf (f : α → β) (h : WellFounded r) : WellFounded (InvImage r f) :=
+-- `def` for `WellFounded.fix`
+def wf (f : α → β) (h : WellFounded r) : WellFounded (InvImage r f) :=
   ⟨fun a => accessible f (apply h (f a))⟩
 end InvImage
 

src/Lean/AddDecl.lean

@@ -64,6 +64,12 @@ Checks whether the declaration was originally declared as a theorem; see also
 def wasOriginallyTheorem (env : Environment) (declName : Name) : Bool :=
   getOriginalConstKind? env declName |>.map (· matches .thm) |>.getD false
 
+private def looksLikeRelevantTheoremProofType (type : Expr) : Bool :=
+  if let .forallE _ _ type _ := type then
+    looksLikeRelevantTheoremProofType type
+  else
+    type.isAppOfArity ``WellFounded 2
+
 /-- If `warn.sorry` is set to true, then, so long as the message log does not already have any errors,
 declarations with `sorryAx` generate the "declaration uses 'sorry'" warning. -/
 register_builtin_option warn.sorry : Bool := {
@@ -83,7 +89,10 @@ def addDecl (decl : Declaration) : CoreM Unit := do
   let mut exportedInfo? := none
   let (name, info, kind) ← match decl with
     | .thmDecl thm =>
-      if (← getEnv).header.isModule then
+      let exportProof := !(← getEnv).header.isModule ||
+        -- TODO: this is horrible...
+        looksLikeRelevantTheoremProofType thm.type
+      if !exportProof then
         exportedInfo? := some <| .axiomInfo { thm with isUnsafe := false }
       pure (thm.name, .thmInfo thm, .thm)
     | .defnDecl defn | .mutualDefnDecl [defn] =>

src/Lean/Compiler/IR/ToIR.lean

@@ -208,47 +208,45 @@ partial def lowerLet (decl : LCNF.LetDecl) (k : LCNF.Code) : M FnBody := do
             return code
           else
             mkExpr (.fap name irArgs)
+        else if let some scalarType ← lowerEnumToScalarType? ctorVal.name then
+          assert! args.isEmpty
+          let var ← bindVar decl.fvarId
+          return .vdecl var scalarType (.lit (.num ctorVal.cidx)) (← lowerCode k)
         else
-          let type ← nameToIRType ctorVal.induct
-          if type.isScalar then
-            let var ← bindVar decl.fvarId
-            return .vdecl var type (.lit (.num ctorVal.cidx)) (← lowerCode k)
-          else
-            assert! type == .object
-            let ⟨ctorInfo, fields⟩ ← getCtorLayout name
-            let args := args.extract (start := ctorVal.numParams)
-            let objArgs : Array Arg ← do
-              let mut result : Array Arg := #[]
-              for i in [0:fields.size] do
-                match args[i]! with
-                | .fvar fvarId =>
-                  if let some (.var varId) := (← get).fvars[fvarId]? then
-                    if fields[i]! matches .object .. then
-                      result := result.push (.var varId)
-                | .type _ | .erased =>
+          let ⟨ctorInfo, fields⟩ ← getCtorLayout name
+          let args := args.extract (start := ctorVal.numParams)
+          let objArgs : Array Arg ← do
+            let mut result : Array Arg := #[]
+            for i in [0:fields.size] do
+              match args[i]! with
+              | .fvar fvarId =>
+                if let some (.var varId) := (← get).fvars[fvarId]? then
                   if fields[i]! matches .object .. then
-                    result := result.push .irrelevant
-              pure result
-            let objVar ← bindVar decl.fvarId
-            let rec lowerNonObjectFields (_ : Unit) : M FnBody :=
-              let rec loop (usizeCount : Nat) (i : Nat) : M FnBody := do
-                match args[i]? with
-                | some (.fvar fvarId) =>
-                  match (← get).fvars[fvarId]? with
-                  | some (.var varId) =>
-                    match fields[i]! with
-                    | .usize .. =>
-                      let k ← loop (usizeCount + 1) (i + 1)
-                      return .uset objVar (ctorInfo.size + usizeCount) varId k
-                    | .scalar _ offset argType =>
-                      let k ← loop usizeCount (i + 1)
-                      return .sset objVar (ctorInfo.size + ctorInfo.usize) offset varId argType k
-                    | .object .. | .irrelevant => loop usizeCount (i + 1)
-                  | _ => loop usizeCount (i + 1)
-                | some (.type _) | some .erased => loop usizeCount (i + 1)
-                | none => lowerCode k
-              loop 0 0
-            return .vdecl objVar type (.ctor ctorInfo objArgs) (← lowerNonObjectFields ())
+                    result := result.push (.var varId)
+              | .type _ | .erased =>
+                if fields[i]! matches .object .. then
+                  result := result.push .irrelevant
+            pure result
+          let objVar ← bindVar decl.fvarId
+          let rec lowerNonObjectFields (_ : Unit) : M FnBody :=
+            let rec loop (usizeCount : Nat) (i : Nat) : M FnBody := do
+              match args[i]? with
+              | some (.fvar fvarId) =>
+                match (← get).fvars[fvarId]? with
+                | some (.var varId) =>
+                  match fields[i]! with
+                  | .usize .. =>
+                    let k ← loop (usizeCount + 1) (i + 1)
+                    return .uset objVar (ctorInfo.size + usizeCount) varId k
+                  | .scalar _ offset argType =>
+                    let k ← loop usizeCount (i + 1)
+                    return .sset objVar (ctorInfo.size + ctorInfo.usize) offset varId argType k
+                  | .object .. | .irrelevant => loop usizeCount (i + 1)
+                | _ => loop usizeCount (i + 1)
+              | some (.type _) | some .erased => loop usizeCount (i + 1)
+              | none => lowerCode k
+            loop 0 0
+          return .vdecl objVar .object (.ctor ctorInfo objArgs) (← lowerNonObjectFields ())
       | some (.axiomInfo ..) =>
         if name == ``Quot.lcInv then
           match irArgs[2]! with

src/Lean/Compiler/IR/ToIRType.lean

@@ -15,19 +15,40 @@ namespace IR
 
 open Lean.Compiler (LCNF.CacheExtension LCNF.isTypeFormerType LCNF.toLCNFType LCNF.toMonoType)
 
-builtin_initialize irTypeExt : LCNF.CacheExtension Name IRType ←
+builtin_initialize scalarTypeExt : LCNF.CacheExtension Name (Option IRType) ←
   LCNF.CacheExtension.register
 
-def nameToIRType (name : Name) : CoreM IRType := do
-  match (← irTypeExt.find? name) with
-  | some type => return type
+def lowerEnumToScalarType? (name : Name) : CoreM (Option IRType) := do
+  match (← scalarTypeExt.find? name) with
+  | some info? => return info?
   | none =>
-    let type ← fillCache
-    irTypeExt.insert name type
-    return type
-where fillCache : CoreM IRType := do
+    let info? ← fillCache
+    scalarTypeExt.insert name info?
+    return info?
+where fillCache : CoreM (Option IRType) := do
+  let env ← Lean.getEnv
+  let some (.inductInfo inductiveVal) := env.find? name | return none
+  let ctorNames := inductiveVal.ctors
+  let numCtors := ctorNames.length
+  for ctorName in ctorNames do
+    let some (.ctorInfo ctorVal) := env.find? ctorName | panic! "expected valid constructor name"
+    if ctorVal.type.isForall then return none
+  return if numCtors == 1 then
+    none
+  else if numCtors < Nat.pow 2 8 then
+    some .uint8
+  else if numCtors < Nat.pow 2 16 then
+    some .uint16
+  else if numCtors < Nat.pow 2 32 then
+    some .uint32
+  else
+    none
+
+def toIRType (e : Lean.Expr) : CoreM IRType := do
+  match e with
+  | .const name .. =>
     match name with
-    | ``UInt8 => return .uint8
+    | ``UInt8 | ``Bool => return .uint8
     | ``UInt16 => return .uint16
     | ``UInt32 => return .uint32
     | ``UInt64 => return .uint64
@@ -35,42 +56,21 @@ where fillCache : CoreM IRType := do
     | ``Float => return .float
     | ``Float32 => return .float32
     | ``lcErased => return .irrelevant
-    | _ =>
-      let env ← Lean.getEnv
-      let some (.inductInfo inductiveVal) := env.find? name | return .object
-      let ctorNames := inductiveVal.ctors
-      let numCtors := ctorNames.length
-      for ctorName in ctorNames do
-        let some (.ctorInfo ctorInfo) := env.find? ctorName | unreachable!
-        let isRelevant ← Meta.MetaM.run' <|
-                         Meta.forallTelescopeReducing ctorInfo.type fun params _ => do
-          for field in params[ctorInfo.numParams...*] do
-            let fieldType ← field.fvarId!.getType
-            let lcnfFieldType ← LCNF.toLCNFType fieldType
-            let monoFieldType ← LCNF.toMonoType lcnfFieldType
-            if !monoFieldType.isErased then return true
-          return false
-        if isRelevant then return .object
-      return if numCtors == 1 then
-        .object
-      else if numCtors < Nat.pow 2 8 then
-        .uint8
-      else if numCtors < Nat.pow 2 16 then
-        .uint16
-      else if numCtors < Nat.pow 2 32 then
-        .uint32
-      else
-        .object
-
-def toIRType (type : Lean.Expr) : CoreM IRType := do
-  match type with
-  | .const name _ => nameToIRType name
-  | .app .. =>
+    | _ => nameToIRType name
+  | .app f _ =>
     -- All mono types are in headBeta form.
-    let .const name _ := type.getAppFn | unreachable!
-    nameToIRType name
+    if let .const name _ := f then
+      nameToIRType name
+    else
+      return .object
   | .forallE .. => return .object
-  | _ => unreachable!
+  | _ => panic! "invalid type"
+where
+  nameToIRType name := do
+    if let some scalarType ← lowerEnumToScalarType? name then
+      return scalarType
+    else
+      return .object
 
 inductive CtorFieldInfo where
   | irrelevant

src/Lean/CoreM.lean

@@ -718,14 +718,9 @@ where doCompile := do
     return
   let opts ← getOptions
   if compiler.enableNew.get opts then
-    withoutExporting do
-      let state ← Core.saveState
-      try
-        compileDeclsNew decls
-      catch e =>
-        state.restore
-        if logErrors then
-          throw e
+    withoutExporting
+      try compileDeclsNew decls catch e =>
+        if logErrors then throw e else return ()
   else
     let res ← withTraceNode `compiler (fun _ => return m!"compiling old: {decls}") do
       return compileDeclsOld (← getEnv) opts decls

src/Lean/Elab/BuiltinTerm.lean

@@ -374,7 +374,7 @@ private opaque evalFilePath (stx : Syntax) : TermElabM System.FilePath
     if (← getEnv).isExporting then
       let name ← mkAuxDeclName `_private
       withoutExporting do
-        let e ← elabTermAndSynthesize e expectedType?
+        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.

src/Lean/Elab/Deriving/Basic.lean

@@ -67,12 +67,11 @@ def DerivingHandler := (typeNames : Array Name) → CommandElabM Bool
 
 builtin_initialize derivingHandlersRef : IO.Ref (NameMap (List DerivingHandler)) ← IO.mkRef {}
 
-/--
-Registers a deriving handler for a class. This function should be called in an `initialize` block.
+/-- A `DerivingHandler` is called on the fully qualified names of all types it is running for
+as well as the syntax of a `with` argument, if present.
 
-A `DerivingHandler` is called on the fully qualified names of all types it is running for. For
-example, `deriving instance Foo for Bar, Baz` invokes ``fooHandler #[`Bar, `Baz]``.
--/
+For example, `deriving instance Foo with fooArgs for Bar, Baz` invokes
+``fooHandler #[`Bar, `Baz] `(fooArgs)``. -/
 def registerDerivingHandler (className : Name) (handler : DerivingHandler) : IO Unit := do
   unless (← initializing) do
     throw (IO.userError "failed to register deriving handler, it can only be registered during initialization")

src/Lean/Elab/Deriving/FromToJson.lean

@@ -166,9 +166,9 @@ def mkToJsonAuxFunction (ctx : Context) (i : Nat) : TermElabM Command := do
   if ctx.usePartial then
     let letDecls ← mkLocalInstanceLetDecls ctx ``ToJson header.argNames
     body ← mkLet letDecls body
-    `(partial def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Json := $body:term)
+    `(private partial def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Json := $body:term)
   else
-    `(def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Json := $body:term)
+    `(private def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Json := $body:term)
 
 def mkFromJsonBody (ctx : Context) (e : Expr) : TermElabM Term := do
   let indName := e.getAppFn.constName!
@@ -188,9 +188,9 @@ def mkFromJsonAuxFunction (ctx : Context) (i : Nat) : TermElabM Command := do
   if ctx.usePartial || indval.isRec then
     let letDecls ← mkLocalInstanceLetDecls ctx ``FromJson header.argNames
     body ← mkLet letDecls body
-    `(partial def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Except String $(← mkInductiveApp ctx.typeInfos[i]! header.argNames) := $body:term)
+    `(private partial def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Except String $(← mkInductiveApp ctx.typeInfos[i]! header.argNames) := $body:term)
   else
-    `(def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Except String $(← mkInductiveApp ctx.typeInfos[i]! header.argNames) := $body:term)
+    `(private def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Except String $(← mkInductiveApp ctx.typeInfos[i]! header.argNames) := $body:term)
 
 
 def mkToJsonMutualBlock (ctx : Context) : TermElabM Command := do

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
-    `(@[no_expose] partial def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Format := $body:term)
+    `(partial def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Format := $body:term)
   else
-    `(@[no_expose] def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Format := $body:term)
+    `(def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Format := $body:term)
 
 def mkMutualBlock (ctx : Context) : TermElabM Syntax := do
   let mut auxDefs := #[]

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

@@ -151,7 +151,7 @@ def partialFixpoint (preDefs : Array PreDefinition) : TermElabM Unit := do
 
     -- Adjust the body of each function to take the other functions as a
     -- (packed) parameter
-    let Fs ← withoutExporting do preDefs.mapIdxM fun funIdx preDef => do
+    let Fs ← preDefs.mapIdxM fun funIdx preDef => do
       let body ← fixedParamPerms.perms[funIdx]!.instantiateLambda preDef.value fixedArgs
       withLocalDeclD (← mkFreshUserName `f) packedType fun f => do
         let body' ← withoutModifyingEnv do
@@ -163,7 +163,7 @@ def partialFixpoint (preDefs : Array PreDefinition) : TermElabM Unit := do
     -- Construct and solve monotonicity goals for each function separately
     -- This way we preserve the user's parameter names as much as possible
     -- and can (later) use the user-specified per-function tactic
-    let hmonos ← withoutExporting do preDefs.mapIdxM fun i preDef => do
+    let hmonos ← preDefs.mapIdxM fun i preDef => do
       let type := types[i]!
       let F := Fs[i]!
       let inst ← toPartialOrder insts'[i]! type

src/Lean/Elab/Structure.lean

@@ -200,15 +200,12 @@ The structure constructor syntax is
 leading_parser try (declModifiers >> ident >> " :: ")
 ```
 -/
-private def expandCtor (structStx : Syntax) (structModifiers : Modifiers) (structDeclName : Name)
-    (forcePrivate : Bool) : TermElabM CtorView := do
+private def expandCtor (structStx : Syntax) (structModifiers : Modifiers) (structDeclName : Name) : TermElabM CtorView := do
   let useDefault := do
-    let visibility := if forcePrivate then .private else .regular
     let declName := structDeclName ++ defaultCtorName
-    let declName ← applyVisibility visibility declName
     let ref := structStx[1].mkSynthetic
     addDeclarationRangesFromSyntax declName ref
-    pure { ref, declId := ref, modifiers := { (default : Modifiers) with visibility }, declName }
+    pure { ref, declId := ref, modifiers := default, declName }
   if structStx[4].isNone then
     useDefault
   else
@@ -218,14 +215,12 @@ private def expandCtor (structStx : Syntax) (structModifiers : Modifiers) (struc
     else
       let ctor := optCtor[0]
       withRef ctor do
-      let mut ctorModifiers ← elabModifiers ctor[0]
+      let ctorModifiers ← elabModifiers ctor[0]
       checkValidCtorModifier ctorModifiers
       if ctorModifiers.isPrivate && structModifiers.isPrivate then
         throwError "invalid 'private' constructor in a 'private' structure"
       if ctorModifiers.isProtected && structModifiers.isPrivate then
         throwError "invalid 'protected' constructor in a 'private' structure"
-      if !ctorModifiers.isPrivate && forcePrivate then
-        throwError "invalid constructor visibility, must be private in presence of private fields"
       let name := ctor[1].getId
       let declName := structDeclName ++ name
       let declName ← applyVisibility ctorModifiers.visibility declName
@@ -382,10 +377,8 @@ def structureSyntaxToView (modifiers : Modifiers) (stx : Syntax) : TermElabM Str
       pure type?
   let parents ← expandParents exts
   let derivingClasses ← getOptDerivingClasses stx[5]
+  let ctor ← expandCtor stx modifiers declName
   let fields ← expandFields stx modifiers declName
-  -- Private fields imply a private constructor; in the module system only for back-compat
-  let ctor ← expandCtor (forcePrivate := (← getEnv).header.isModule && fields.any (·.modifiers.isPrivate))
-    stx modifiers declName
   fields.forM fun field => do
     if field.declName == ctor.declName then
       throwErrorAt field.ref "invalid field name '{field.name}', it is equal to structure constructor name"
@@ -946,15 +939,14 @@ private def elabFieldTypeValue (structParams : Array Expr) (view : StructFieldVi
       match view.default? with
       | none => return (none, paramInfoOverrides, none)
       | some (.optParam valStx) =>
-        withoutExporting (when := view.modifiers.isPrivate) do
-          Term.synthesizeSyntheticMVarsNoPostponing
-          let params ← Term.addAutoBoundImplicits params (view.nameId.getTailPos? (canonicalOnly := true))
-          let value ← Term.withoutAutoBoundImplicit <| Term.elabTerm valStx none
-          let value ← runStructElabM (init := state) <| solveParentMVars value
-          registerFailedToInferFieldType view.name (← inferType value) view.nameId
-          registerFailedToInferDefaultValue view.name value valStx
-          let value ← mkLambdaFVars params value
-          return (none, paramInfoOverrides, StructFieldDefault.optParam value)
+        Term.synthesizeSyntheticMVarsNoPostponing
+        let params ← Term.addAutoBoundImplicits params (view.nameId.getTailPos? (canonicalOnly := true))
+        let value ← Term.withoutAutoBoundImplicit <| Term.elabTerm valStx none
+        let value ← runStructElabM (init := state) <| solveParentMVars value
+        registerFailedToInferFieldType view.name (← inferType value) view.nameId
+        registerFailedToInferDefaultValue view.name value valStx
+        let value ← mkLambdaFVars params value
+        return (none, paramInfoOverrides, StructFieldDefault.optParam value)
       | some (.autoParam tacticStx) =>
         throwErrorAt tacticStx "invalid field declaration, type must be provided when auto-param tactic is used"
     | some typeStx =>
@@ -968,14 +960,13 @@ private def elabFieldTypeValue (structParams : Array Expr) (view : StructFieldVi
         let type ← mkForallFVars params type
         return (type, paramInfoOverrides, none)
       | some (.optParam valStx) =>
-        withoutExporting (when := view.modifiers.isPrivate) do
-          let value ← Term.withoutAutoBoundImplicit <| Term.elabTermEnsuringType valStx type
-          let value ← runStructElabM (init := state) <| solveParentMVars value
-          registerFailedToInferDefaultValue view.name value valStx
-          Term.synthesizeSyntheticMVarsNoPostponing
-          let type  ← mkForallFVars params type
-          let value ← mkLambdaFVars params value
-          return (type, paramInfoOverrides, StructFieldDefault.optParam value)
+        let value ← Term.withoutAutoBoundImplicit <| Term.elabTermEnsuringType valStx type
+        let value ← runStructElabM (init := state) <| solveParentMVars value
+        registerFailedToInferDefaultValue view.name value valStx
+        Term.synthesizeSyntheticMVarsNoPostponing
+        let type  ← mkForallFVars params type
+        let value ← mkLambdaFVars params value
+        return (type, paramInfoOverrides, StructFieldDefault.optParam value)
       | some (.autoParam tacticStx) =>
         let name := mkAutoParamFnOfProjFn view.declName
         discard <| Term.declareTacticSyntax tacticStx name
@@ -1297,8 +1288,7 @@ private def addDefaults (levelParams : List Name) (params : Array Expr) (replace
           (← mkDefinitionValInferrringUnsafe declName levelParams type value ReducibilityHints.abbrev)
     for fieldInfo in fieldInfos do
       if let some (.optParam value) := fieldInfo.default? then
-        withoutExporting (when := isPrivateName fieldInfo.declName) do
-          addDefault (mkDefaultFnOfProjFn fieldInfo.declName) value
+        addDefault (mkDefaultFnOfProjFn fieldInfo.declName) value
       else if let some (.optParam value) := fieldInfo.resolvedDefault? then
         addDefault (mkInheritedDefaultFnOfProjFn fieldInfo.declName) value
 

src/Lean/Environment.lean

@@ -2532,13 +2532,9 @@ def withExporting [Monad m] [MonadEnv m] [MonadFinally m] [MonadOptions m] (x :
   finally
     modifyEnv (·.setExporting old)
 
-/-- If `when` is true, sets `Environment.isExporting` to false while executing `x`. -/
-def withoutExporting [Monad m] [MonadEnv m] [MonadFinally m] [MonadOptions m] (x : m α)
-    (when : Bool := true) : m α :=
-  if when then
-    withExporting (isExporting := false) x
-  else
-    x
+/-- Sets `Environment.isExporting` to false while executing `x`. -/
+def withoutExporting [Monad m] [MonadEnv m] [MonadFinally m] [MonadOptions m] (x : m α) : m α :=
+  withExporting (isExporting := false) x
 
 /-- Constructs a DefinitionVal, inferring the `unsafe` field -/
 def mkDefinitionValInferrringUnsafe [Monad m] [MonadEnv m] (name : Name) (levelParams : List Name)

src/Lean/ErrorExplanation.lean

@@ -89,7 +89,7 @@ where
   upToWs (nonempty : Bool) : Parser String := fun it =>
     let it' := it.find fun c => c.isWhitespace
     if nonempty && it'.pos == it.pos then
-      .error it' "Expected a nonempty string"
+      .error it' (.other "Expected a nonempty string")
     else
       .success it' (it.extract it')
 
@@ -176,7 +176,7 @@ private abbrev ValidationM := Parsec ValidationState
 private def ValidationM.run (p : ValidationM α) (input : String) : Except (Nat × String) α :=
   match p (.ofSource input) with
   | .success _ res => Except.ok res
-  | .error s err  => Except.error (s.getLineNumber, err)
+  | .error s err  => Except.error (s.getLineNumber, toString err)
 
 /--
 Matches `p` as many times as possible, followed by EOF. If `p` cannot be matched prior to the end
@@ -286,7 +286,7 @@ where
   labelingExampleErrors {α} (header : String) (x : ValidationM α) : ValidationM α := fun s =>
     match x s with
     | res@(.success ..) => res
-    | .error s' msg => .error s' s!"Example '{header}' is malformed: {msg}"
+    | .error s' msg => .error s' (.other s!"Example '{header}' is malformed: {msg}")
 
   /--
   If `line` is a level-`level` header and, if `title?` is non-`none`, its title is `title?`,

src/Lean/Expr.lean

@@ -2198,9 +2198,6 @@ private def natSubFn : Expr :=
 private def natMulFn : Expr :=
   mkApp4 (mkConst ``HMul.hMul [0, 0, 0]) Nat.mkType Nat.mkType Nat.mkType Nat.mkInstHMul
 
-private def natPowFn : Expr :=
-  mkApp4 (mkConst ``HPow.hPow [0, 0, 0]) Nat.mkType Nat.mkType Nat.mkType Nat.mkInstHPow
-
 /-- Given `a : Nat`, returns `Nat.succ a` -/
 def mkNatSucc (a : Expr) : Expr :=
   mkApp (mkConst ``Nat.succ) a
@@ -2217,10 +2214,6 @@ def mkNatSub (a b : Expr) : Expr :=
 def mkNatMul (a b : Expr) : Expr :=
   mkApp2 natMulFn a b
 
-/-- Given `a b : Nat`, returns `a ^ b` -/
-def mkNatPow (a b : Expr) : Expr :=
-  mkApp2 natPowFn a b
-
 private def natLEPred : Expr :=
   mkApp2 (mkConst ``LE.le [0]) Nat.mkType Nat.mkInstLE
 

src/Lean/LocalContext.lean

@@ -522,7 +522,7 @@ partial def isSubPrefixOfAux (a₁ a₂ : PArray (Option LocalDecl)) (exceptFVar
 def isSubPrefixOf (lctx₁ lctx₂ : LocalContext) (exceptFVars : Array Expr := #[]) : Bool :=
   isSubPrefixOfAux lctx₁.decls lctx₂.decls exceptFVars 0 0
 
-@[inline] def mkBinding (isLambda : Bool) (lctx : LocalContext) (xs : Array Expr) (b : Expr) (usedLetOnly : Bool := true) (generalizeNondepLet := false) : Expr :=
+@[inline] def mkBinding (isLambda : Bool) (lctx : LocalContext) (xs : Array Expr) (b : Expr) (generalizeNondepLet := false) : Expr :=
   let b := b.abstract xs
   xs.size.foldRev (init := b) fun i _ b =>
     let x := xs[i]
@@ -538,7 +538,7 @@ def isSubPrefixOf (lctx₁ lctx₂ : LocalContext) (exceptFVars : Array Expr :=
     | some (.ldecl _ _ n ty val nondep _) =>
       if nondep && generalizeNondepLet then
         handleCDecl n ty .default
-      else if !usedLetOnly || b.hasLooseBVar 0 then
+      else if b.hasLooseBVar 0 then
         let ty  := ty.abstractRange i xs
         let val := val.abstractRange i xs
         mkLet n ty val b nondep
@@ -548,13 +548,13 @@ def isSubPrefixOf (lctx₁ lctx₂ : LocalContext) (exceptFVars : Array Expr :=
 
 /-- Creates the expression `fun x₁ .. xₙ => b` for free variables `xs = #[x₁, .., xₙ]`,
 suitably abstracting `b` and the types for each of the `xᵢ`. -/
-def mkLambda (lctx : LocalContext) (xs : Array Expr) (b : Expr) (usedLetOnly : Bool := true) (generalizeNondepLet := false) : Expr :=
-  mkBinding true lctx xs b usedLetOnly generalizeNondepLet
+def mkLambda (lctx : LocalContext) (xs : Array Expr) (b : Expr) (generalizeNondepLet := false) : Expr :=
+  mkBinding true lctx xs b generalizeNondepLet
 
 /-- Creates the expression `(x₁:α₁) → .. → (xₙ:αₙ) → b` for free variables `xs = #[x₁, .., xₙ]`,
 suitably abstracting `b` and the types for each of the `xᵢ`, `αᵢ`. -/
-def mkForall (lctx : LocalContext) (xs : Array Expr) (b : Expr) (usedLetOnly : Bool := true) (generalizeNondepLet := false) : Expr :=
-  mkBinding false lctx xs b usedLetOnly generalizeNondepLet
+def mkForall (lctx : LocalContext) (xs : Array Expr) (b : Expr) (generalizeNondepLet := false) : Expr :=
+  mkBinding false lctx xs b generalizeNondepLet
 
 @[inline] def anyM [Monad m] (lctx : LocalContext) (p : LocalDecl → m Bool) : m Bool :=
   lctx.decls.anyM fun d => match d with

src/Lean/Message.lean

@@ -618,9 +618,7 @@ actually rendered. Consider using this function in lazy message data to avoid un
 computation for messages that are not displayed.
 -/
 private def MessageData.formatLength (ctx : PPContext) (msg : MessageData) : BaseIO Nat := do
-  let { env, mctx, lctx, opts, currNamespace, openDecls } := ctx
-  -- Simulate the naming context that will be added to the actual message
-  let msg := MessageData.withNamingContext { currNamespace, openDecls } msg
+  let { env, mctx, lctx, opts, ..} := ctx
   let fmt ← msg.format (some { env, mctx, lctx, opts })
   return fmt.pretty.length
 

src/Lean/Meta/DecLevel.lean

@@ -70,9 +70,6 @@ def decLevel (u : Level) : MetaM Level := do
 def getDecLevel (type : Expr) : MetaM Level := do
   decLevel (← getLevel type)
 
-def getDecLevel? (type : Expr) : MetaM (Option Level) := do
-  decLevel? (← getLevel type)
-
 builtin_initialize
   registerTraceClass `Meta.isLevelDefEq.step
 

src/Lean/Meta/SizeOf.lean

@@ -481,10 +481,10 @@ register_builtin_option genSizeOfSpec : Bool := {
 }
 
 def mkSizeOfInstances (typeName : Name) : MetaM Unit := do
-  let indInfo ← withoutExporting <| getConstInfoInduct typeName
-  withExporting (isExporting := !isPrivateName typeName && !indInfo.ctors.any isPrivateName) 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
       unless indInfo.isUnsafe do
         let (fns, recMap) ← mkSizeOfFns typeName
         for indTypeName in indInfo.all, fn in fns do

src/Lean/Meta/Tactic/AuxLemma.lean

@@ -10,15 +10,8 @@ import Lean.DefEqAttrib
 
 namespace Lean.Meta
 
-structure AuxLemmaKey where
-  type : Expr
-  -- When an aux lemma is created in a private context and thus has a private name, we must not
-  -- reuse it in an exported context.
-  isPrivate : Bool
-deriving BEq, Hashable
-
 structure AuxLemmas where
-  lemmas : PHashMap AuxLemmaKey (Name × List Name) := {}
+  lemmas : PHashMap Expr (Name × List Name) := {}
   deriving Inhabited
 
 builtin_initialize auxLemmasExt : EnvExtension AuxLemmas ←
@@ -39,7 +32,6 @@ def mkAuxLemma (levelParams : List Name) (type : Expr) (value : Expr) (kind? : O
     (cache := true) (inferRfl := false) : MetaM Name := do
   let env ← getEnv
   let s := auxLemmasExt.getState env
-  let key := { type, isPrivate := !env.isExporting }
   let mkNewAuxLemma := do
     let auxName ← mkAuxDeclName (kind := kind?.getD `_proof)
     let decl :=
@@ -59,17 +51,12 @@ def mkAuxLemma (levelParams : List Name) (type : Expr) (value : Expr) (kind? : O
     addDecl decl
     if inferRfl then
       inferDefEqAttr auxName
-    modifyEnv fun env => auxLemmasExt.modifyState env fun ⟨lemmas⟩ => ⟨lemmas.insert key (auxName, levelParams)⟩
+    modifyEnv fun env => auxLemmasExt.modifyState env fun ⟨lemmas⟩ => ⟨lemmas.insert type (auxName, levelParams)⟩
     return auxName
   if cache then
-    if let some (name, levelParams') := s.lemmas.find? key then
+    if let some (name, levelParams') := s.lemmas.find? type then
       if levelParams == levelParams' then
         return name
-    -- private contexts may reuse public matchers
-    if key.isPrivate then
-      if let some (name, levelParams') := s.lemmas.find? { key with isPrivate := false } then
-        if levelParams == levelParams' then
-          return name
   mkNewAuxLemma
 
 end Lean.Meta

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

@@ -12,4 +12,3 @@ import Lean.Meta.Tactic.Grind.Arith.Offset
 import Lean.Meta.Tactic.Grind.Arith.Cutsat
 import Lean.Meta.Tactic.Grind.Arith.CommRing
 import Lean.Meta.Tactic.Grind.Arith.Linear
-import Lean.Meta.Tactic.Grind.Arith.Simproc

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

@@ -9,7 +9,6 @@ import Lean.Meta.Tactic.Grind.Diseq
 import Lean.Meta.Tactic.Grind.Arith.ProofUtil
 import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
 import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
-import Lean.Meta.Tactic.Grind.Arith.CommRing.SafePoly
 import Lean.Meta.Tactic.Grind.Arith.CommRing.ToExpr
 
 namespace Lean.Meta.Grind.Arith.CommRing

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

@@ -1,114 +0,0 @@
-/-
-Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
-
-namespace Lean.Meta.Grind.Arith.CommRing
-
-/-!
-The polynomial functions at `Poly.lean` are used for constructing proofs-by-reflection,
-but they do not provide mechanisms for aborting expensive computations.
--/
-
-private def applyChar (a : Int) : RingM Int := do
-  if let some c ← nonzeroChar? then
-    return a % c
-  else
-    return a
-
-private def addConst (p : Poly) (k : Int) : RingM Poly := do
-  if let some c ← nonzeroChar? then return .addConstC p k c else return .addConst p k
-
-private def mulConst (k : Int) (p : Poly) : RingM Poly := do
-  if let some c ← nonzeroChar? then return .mulConstC k p c else return .mulConst k p
-
-private def mulMon (k : Int) (m : Mon) (p : Poly) : RingM Poly := do
-  if let some c ← nonzeroChar? then return .mulMonC k m p c else return .mulMon k m p
-
-private def combine (p₁ p₂ : Poly) : RingM Poly := withIncRecDepth do
-  match p₁, p₂ with
-  | .num k₁, .num k₂ => return .num (← applyChar (k₁ + k₂))
-  | .num k₁, .add k₂ m₂ p₂ => addConst (.add k₂ m₂ p₂) k₁
-  | .add k₁ m₁ p₁, .num k₂ => addConst (.add k₁ m₁ p₁) k₂
-  | .add k₁ m₁ p₁, .add k₂ m₂ p₂ =>
-    match m₁.grevlex m₂ with
-    | .eq =>
-      let k ← applyChar (k₁ + k₂)
-      bif k == 0 then
-        combine p₁ p₂
-      else
-        return .add k m₁ (← combine p₁ p₂)
-    | .gt => return .add k₁ m₁ (← combine p₁ (.add k₂ m₂ p₂))
-    | .lt => return .add k₂ m₂ (← combine (.add k₁ m₁ p₁) p₂)
-
-private def mul (p₁ : Poly) (p₂ : Poly) : RingM Poly :=
-  go p₁ (.num 0)
-where
-  go (p₁ : Poly) (acc : Poly) : RingM Poly :=  withIncRecDepth do
-    match p₁ with
-    | .num k => combine acc (← mulConst k p₂)
-    | .add k m p₁ =>
-      checkSystem "grind ring"
-      go p₁ (← combine acc (← mulMon k m p₂))
-
-private def pow (p : Poly) (k : Nat) : RingM Poly := withIncRecDepth do
-  match k with
-  | 0 => return .num 1
-  | 1 => return p
-  | 2 => mul p p
-  | k+3 => mul p (← pow p (k+2))
-
-private def toPoly (e : RingExpr) : RingM Poly := do
-  match e with
-  | .num n   => return .num (← applyChar n)
-  | .var x   => return .ofVar x
-  | .add a b => combine (← toPoly a) (← toPoly b)
-  | .mul a b => mul (← toPoly a) (← toPoly b)
-  | .neg a   => mulConst (-1) (← toPoly a)
-  | .sub a b => combine (← toPoly a) (← mulConst (-1) (← toPoly b))
-  | .pow a k =>
-    if k == 0 then
-      return .num 1
-    else match a with
-    | .num n => return .num (← applyChar (n^k))
-    | .var x => return .ofMon (.mult {x, k} .unit)
-    | _ => pow (← toPoly a) k
-
-/--
-Converts the given ring expression into a multivariate polynomial.
-If the ring has a nonzero characteristic, it is used during normalization.
--/
-abbrev _root_.Lean.Grind.CommRing.Expr.toPolyM (e : RingExpr) : RingM Poly := do
-  toPoly e
-
-abbrev _root_.Lean.Grind.CommRing.Poly.mulConstM (p : Poly) (k : Int) : RingM Poly :=
-  mulConst k p
-
-abbrev _root_.Lean.Grind.CommRing.Poly.mulMonM (p : Poly) (k : Int) (m : Mon) : RingM Poly :=
-  mulMon k m p
-
-abbrev _root_.Lean.Grind.CommRing.Poly.mulM (p₁ p₂ : Poly) : RingM Poly := do
-  mul p₁ p₂
-
-abbrev _root_.Lean.Grind.CommRing.Poly.combineM (p₁ p₂ : Poly) : RingM Poly :=
-  combine p₁ p₂
-
-def _root_.Lean.Grind.CommRing.Poly.spolM (p₁ p₂ : Poly) : RingM Grind.CommRing.SPolResult := do
-  match p₁, p₂ with
-  | .add k₁ m₁ p₁, .add k₂ m₂ p₂ =>
-    let m    := m₁.lcm m₂
-    let m₁   := m.div m₁
-    let m₂   := m.div m₂
-    let g    := Nat.gcd k₁.natAbs k₂.natAbs
-    let c₁   := k₂/g
-    let c₂   := -k₁/g
-    let p₁   ← mulMon c₁ m₁ p₁
-    let p₂   ← mulMon c₂ m₂ p₂
-    let spol ← combine p₁ p₂
-    return { spol, m₁, m₂, k₁ := c₁, k₂ := c₂ }
-  | _, _ => return {}
-
-end Lean.Meta.Grind.Arith.CommRing

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

@@ -172,6 +172,28 @@ def getCharInst : RingM (Expr × Nat) := do
 def isField : RingM Bool :=
   return (← getRing).fieldInst?.isSome
 
+/--
+Converts the given ring expression into a multivariate polynomial.
+If the ring has a nonzero characteristic, it is used during normalization.
+-/
+def _root_.Lean.Grind.CommRing.Expr.toPolyM (e : RingExpr) : RingM Poly := do
+  if let some c ← nonzeroChar? then return e.toPolyC c else return e.toPoly
+
+def _root_.Lean.Grind.CommRing.Poly.mulConstM (p : Poly) (k : Int) : RingM Poly :=
+  return p.mulConst' k (← nonzeroChar?)
+
+def _root_.Lean.Grind.CommRing.Poly.mulMonM (p : Poly) (k : Int) (m : Mon) : RingM Poly :=
+  return p.mulMon' k m (← nonzeroChar?)
+
+def _root_.Lean.Grind.CommRing.Poly.mulM (p₁ p₂ : Poly) : RingM Poly := do
+  if let some c ← nonzeroChar? then return p₁.mulC p₂ c else return p₁.mul p₂
+
+def _root_.Lean.Grind.CommRing.Poly.combineM (p₁ p₂ : Poly) : RingM Poly :=
+  return p₁.combine' p₂ (← nonzeroChar?)
+
+def _root_.Lean.Grind.CommRing.Poly.spolM (p₁ p₂ : Poly) : RingM Grind.CommRing.SPolResult := do
+  if let some c ← nonzeroChar? then return p₁.spol p₂ c else return p₁.spol p₂
+
 def isQueueEmpty : RingM Bool :=
   return (← getRing).queue.isEmpty
 

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

@@ -45,47 +45,9 @@ private def isForbiddenParent (parent? : Option Expr) : Bool :=
   else
     true
 
-partial def markVars (e : Expr) : LinearM Unit := do
-  match_expr e with
-  | HAdd.hAdd _ _ _ i a b =>
-    if isAddInst (← getStruct) i then markVars a; markVars b else markVar e
-  | HSub.hSub _ _ _ i a b => if isSubInst (← getStruct) i then markVars a; markVars b else markVar e
-  | HMul.hMul _ _ _ i a b =>
-    if isHMulInst (← getStruct) i then
-      if (← getIntValue? a).isSome then
-        return (← markVar b)
-    if isHMulNatInst (← getStruct) i then
-      if (← getNatValue? a).isSome then
-        return (← markVar b)
-    if isHomoMulInst (← getStruct) i then
-      if isNumeral a then
-        return (← markVar b)
-      else if isNumeral b then
-        return (← markVar a)
-      else
-        markVar a; markVar b; markVar e
-        return
-    markVar e
-  | HSMul.hSMul _ _ _ i a b =>
-    if isHSMulInst (← getStruct) i then
-      if (← getIntValue? a).isSome then
-        return (← markVar b)
-    if isHSMulNatInst (← getStruct) i then
-      if (← getNatValue? a).isSome then
-        return (← markVar b)
-    markVar e
-  | Neg.neg _ _ a => markVars a
-  | Zero.zero _ _ => return ()
-  | OfNat.ofNat _ _ _ => return ()
-  | _ => markVar e
-where
-  markVar (e : Expr) : LinearM Unit :=
-    discard <| mkVar e
-  isNumeral (e : Expr) : Bool :=
-    match_expr e with
-    | Neg.neg _ _ a => isNumeral a
-    | OfNat.ofNat _ n _ => isNatNum n
-    | _ => false
+def markVars (e : Expr) : LinearM Unit := do
+  -- TODO: avoid creation of auxiliary reified expression
+  discard <| reify? e (skipVar := true)
 
 def internalize (e : Expr) (parent? : Option Expr) : GoalM Unit := do
   unless (← getConfig).linarith do return ()

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

@@ -17,8 +17,6 @@ def isHMulInst (struct : Struct) (inst : Expr) : Bool :=
   isSameExpr struct.hmulFn.appArg! inst
 def isHMulNatInst (struct : Struct) (inst : Expr) : Bool :=
   isSameExpr struct.hmulNatFn.appArg! inst
-def isHomoMulInst (struct : Struct) (inst : Expr) : Bool :=
-  if let some homomulFn := struct.homomulFn? then isSameExpr homomulFn inst else false
 def isHSMulInst (struct : Struct) (inst : Expr) : Bool :=
   if let some smulFn := struct.hsmulFn? then isSameExpr smulFn.appArg! inst else false
 def isHSMulNatInst (struct : Struct) (inst : Expr) : Bool :=
@@ -110,4 +108,5 @@ where
       if (← isOfNatZero e) then return .zero else toVar e
     | _ => toVar e
 
+
 end  Lean.Meta.Grind.Arith.Linear

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

@@ -177,11 +177,6 @@ where
       return some one
     let one? ← getOne?
     let commRingInst? ← getInst? ``Grind.CommRing
-    let homomulFn? ← if commRingInst?.isSome then
-      let mulInst ← getBinHomoInst ``HMul
-      pure <| some (← internalizeFn <| mkApp4 (mkConst ``HMul.hMul [u, u, u]) type type type mulInst)
-    else
-      pure none
     let getOrderedRingInst? : GoalM (Option Expr) := do
       let some semiringInst := semiringInst? | return none
       let some preorderInst := preorderInst? | return none
@@ -202,7 +197,7 @@ where
     let struct : Struct := {
       id, type, u, intModuleInst, preorderInst?, orderedAddInst?, partialInst?, linearInst?, noNatDivInst?
       leFn?, ltFn?, addFn, subFn, negFn, hmulFn, hmulNatFn, hsmulFn?, hsmulNatFn?, zero, one?
-      ringInst?, commRingInst?, orderedRingInst?, charInst?, ringId?, fieldInst?, ofNatZero, homomulFn?
+      ringInst?, commRingInst?, orderedRingInst?, charInst?, ringId?, fieldInst?, ofNatZero
     }
     modify' fun s => { s with structs := s.structs.push struct }
     if let some one := one? then

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

@@ -123,7 +123,6 @@ structure Struct where
   hmulNatFn        : Expr
   hsmulFn?         : Option Expr
   hsmulNatFn?      : Option Expr
-  homomulFn?       : Option Expr -- homogeneous multiplication if structure is a ring
   subFn            : Expr
   negFn            : Expr
   /--

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

@@ -1,53 +0,0 @@
-/-
-Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Init.Grind.Ring.Basic
-import Init.Simproc
-import Lean.Meta.Tactic.Simp.Simproc
-
-namespace Lean.Meta.Grind.Arith
-
-private def mkSemiringThm (declName : Name) (α : Expr) : MetaM (Option Expr) := do
-  let some u ← getDecLevel? α | return none
-  let semiring := mkApp (mkConst ``Grind.Semiring [u]) α
-  let .some semiringInst ← trySynthInstance semiring | return none
-  return mkApp2 (mkConst declName [u]) α semiringInst
-
-/--
-Applies `a^(m+n) = a^m * a^n`, `a^0 = 1`, `a^1 = a`.
-
-We do normalize `a^0` and `a^1` when converting expressions into polynomials,
-but we need to normalize them here when for other preprocessing steps such as
-`a / b = a*b⁻¹`. If `b` is of the form `c^1`, it will be treated as an
-atom in the comm ring module.
--/
-builtin_simproc_decl expandPowAdd (_ ^ _) := fun e => do
-  let_expr HPow.hPow α nat α' _ a k := e | return .continue
-  let_expr Nat ← nat | return .continue
-  if let some k ← getNatValue? k then
-    if k == 0 then
-      unless (← isDefEq α α') do return .continue
-      let some h ← mkSemiringThm ``Grind.Semiring.pow_zero α | return .continue
-      let r ← mkNumeral α 1
-      return .done { expr := r, proof? := some (mkApp h a) }
-    else if k == 1 then
-      unless (← isDefEq α α') do return .continue
-      let some h ← mkSemiringThm ``Grind.Semiring.pow_one α | return .continue
-      return .done { expr := a, proof? := some (mkApp h a) }
-    else
-      return .continue
-  else
-    let_expr HAdd.hAdd _ _ _ _ m n := k | return .continue
-    unless (← isDefEq α α') do return .continue
-    let some h ← mkSemiringThm ``Grind.Semiring.pow_add α | return .continue
-    let pwFn := e.appFn!.appFn!
-    let r ← mkMul (mkApp2 pwFn a m) (mkApp2 pwFn a n)
-    return .visit { expr := r, proof? := some (mkApp3 h a m n) }
-
-def addSimproc (s : Simprocs) : CoreM Simprocs := do
-  s.add ``expandPowAdd (post := true)
-
-end Lean.Meta.Grind.Arith

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

@@ -40,21 +40,6 @@ def isOffsetPattern? (pat : Expr) : Option (Expr × Nat) := Id.run do
   let .lit (.natVal k) := k | none
   return some (pat, k)
 
-/--
-`detectOffsets` inverse.
-This function is used to expand `mkOffsetPattern` occurring in a constant pattern.
--/
-private def expandOffsetPatterns (pat : Expr) : CoreM Expr := do
-  let pre (e : Expr) := do
-    match e with
-    | .letE .. | .lam .. | .forallE .. => return .done e
-    | _ =>
-      let some (e, k) := isOffsetPattern? e
-        | return .continue e
-      if k == 0 then return .continue e
-      return .continue <| mkNatAdd e (mkNatLit k)
-  Core.transform pat (pre := pre)
-
 def mkEqBwdPattern (u : List Level) (α : Expr) (lhs rhs : Expr) : Expr :=
   mkApp3 (mkConst ``Grind.eqBwdPattern u) α lhs rhs
 
@@ -642,7 +627,7 @@ where
       if arg.hasMVar then
         pure dontCare
       else
-        return mkGroundPattern (← expandOffsetPatterns arg)
+        pure <| mkGroundPattern arg
     else match arg with
       | .bvar idx =>
         if inSupport && (← foundBVar idx) then

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

@@ -8,7 +8,6 @@ import Lean.Meta.Tactic.Simp.Simproc
 import Lean.Meta.Tactic.Grind.Simp
 import Lean.Meta.Tactic.Grind.MatchDiscrOnly
 import Lean.Meta.Tactic.Grind.MatchCond
-import Lean.Meta.Tactic.Grind.Arith.Simproc
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.List
 
 namespace Lean.Meta.Grind
@@ -67,7 +66,6 @@ protected def getSimprocs : MetaM (Array Simprocs) := do
   let s := s.erase ``List.reduceReplicate
   let s ← addSimpMatchDiscrsOnly s
   let s ← addPreMatchCondSimproc s
-  let s ← Arith.addSimproc s
   let s ← s.add ``simpBoolEq (post := false)
   return #[s]
 

src/Lean/Meta/Transform.lean

@@ -187,9 +187,6 @@ def zetaDeltaFVars (e : Expr) (fvars : Array FVarId) : MetaM Expr :=
 def unfoldDeclsFrom (biggerEnv : Environment) (e : Expr) : CoreM Expr := do
   withoutModifyingEnv do
     let env ← getEnv
-    -- There might have been nested proof abstractions, which yield private helper theoresms, so
-    -- make sure we can find them. They will later be re-abstracted again.
-    let biggerEnv := biggerEnv.setExporting false
     setEnv biggerEnv -- `e` has declarations from `biggerEnv` that are not in `env`
     let pre (e : Expr) : CoreM TransformStep := do
       let .const declName us := e | return .continue

src/Std/Data/DHashMap.lean

@@ -3,11 +3,7 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
-module
-
 prelude
-public import Std.Data.DHashMap.Basic
-public import Std.Data.DHashMap.Lemmas
-public import Std.Data.DHashMap.AdditionalOperations
-
-public section
+import Std.Data.DHashMap.Basic
+import Std.Data.DHashMap.Lemmas
+import Std.Data.DHashMap.AdditionalOperations

src/Std/Data/DHashMap/AdditionalOperations.lean

@@ -3,13 +3,9 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
-module
-
 prelude
-public import Std.Data.DHashMap.Internal.Raw
-public import Std.Data.DHashMap.Internal.WF
-
-public section
+import Std.Data.DHashMap.Internal.Raw
+import Std.Data.DHashMap.Internal.WF
 
 /-!
 # Additional dependent hash map operations

src/Std/Data/DHashMap/Basic.lean

@@ -3,12 +3,8 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
-module
-
 prelude
-public import all Std.Data.DHashMap.Raw
-
-public section
+import Std.Data.DHashMap.Raw
 
 /-!
 # Dependent hash maps

src/Std/Data/DHashMap/Internal/AssocList/Basic.lean

@@ -3,12 +3,8 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Mario Carneiro, Markus Himmel
 -/
-module
-
 prelude
-public import Init.NotationExtra
-
-public section
+import Init.NotationExtra
 
 /-!
 This is an internal implementation file of the hash map. Users of the hash map should not rely on

src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean

@@ -3,13 +3,9 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
-module
-
 prelude
-public import all Std.Data.DHashMap.Internal.AssocList.Basic
-public import Std.Data.Internal.List.Associative
-
-public section
+import Std.Data.DHashMap.Internal.AssocList.Basic
+import Std.Data.Internal.List.Associative
 
 /-!
 This is an internal implementation file of the hash map. Users of the hash map should not rely on
@@ -33,9 +29,9 @@ namespace Std.DHashMap.Internal.AssocList
 open Std.Internal.List
 open Std.Internal
 
-@[simp] theorem toList_nil : (nil : AssocList α β).toList = [] := (rfl)
+@[simp] theorem toList_nil : (nil : AssocList α β).toList = [] := rfl
 @[simp] theorem toList_cons {l : AssocList α β} {a : α} {b : β a} :
-    (l.cons a b).toList = ⟨a, b⟩ :: l.toList := (rfl)
+    (l.cons a b).toList = ⟨a, b⟩ :: l.toList := rfl
 
 @[simp]
 theorem foldl_eq {f : δ → (a : α) → β a → δ} {init : δ} {l : AssocList α β} :
@@ -85,8 +81,8 @@ theorem get_eq {β : Type v} [BEq α] {l : AssocList α (fun _ => β)} {a : α}
 theorem getCastD_eq [BEq α] [LawfulBEq α] {l : AssocList α β} {a : α} {fallback : β a} :
     l.getCastD a fallback = getValueCastD a l.toList fallback := by
   induction l
-  · simp [getCastD]
-  · simp_all [getCastD, List.getValueCastD, List.getValueCast?_cons,
+  · simp [getCastD, List.getValueCastD]
+  · simp_all [getCastD, List.getValueCastD, List.getValueCastD, List.getValueCast?_cons,
       apply_dite (fun x => Option.getD x fallback)]
 
 @[simp]

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

@@ -3,15 +3,11 @@ Copyright (c) 2018 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Mario Carneiro, Markus Himmel
 -/
-module
-
 prelude
-public import Init.Data.Array.Lemmas
-public import Std.Data.DHashMap.RawDef
-public import Std.Data.Internal.List.Defs
-public import Std.Data.DHashMap.Internal.Index
-
-public section
+import Init.Data.Array.Lemmas
+import Std.Data.DHashMap.RawDef
+import Std.Data.Internal.List.Defs
+import Std.Data.DHashMap.Internal.Index
 
 /-!
 This is an internal implementation file of the hash map. Users of the hash map should not rely on

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

@@ -3,14 +3,10 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
-module
-
 prelude
-public import Init.Data.Hashable
-public import Std.Data.Internal.List.Associative
-public import Std.Data.DHashMap.Internal.Defs
-
-public section
+import Init.Data.Hashable
+import Std.Data.Internal.List.Associative
+import Std.Data.DHashMap.Internal.Defs
 
 /-!
 This is an internal implementation file of the hash map. Users of the hash map should not rely on

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

@@ -3,13 +3,9 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
-module
-
 prelude
-public import Init.Data.UInt.Lemmas
-public import Init.Data.UInt.Bitwise
-
-public section
+import Init.Data.UInt.Lemmas
+import Init.Data.UInt.Bitwise
 
 /-!
 This is an internal implementation file of the hash map. Users of the hash map should not rely on
@@ -47,7 +43,7 @@ def scrambleHash (hash : UInt64) : UInt64 :=
 `sz` is an explicit parameter because having it inferred from `h` can lead to suboptimal IR,
 cf. https://github.com/leanprover/lean4/issues/4157
 -/
-@[irreducible, inline, expose] def mkIdx (sz : Nat) (h : 0 < sz) (hash : UInt64) :
+@[irreducible, inline] def mkIdx (sz : Nat) (h : 0 < sz) (hash : UInt64) :
     { u : USize // u.toNat < sz } :=
   ⟨(scrambleHash hash).toUSize &&& (USize.ofNat sz - 1), by
     -- This proof is a good test for our USize API

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

@@ -3,16 +3,11 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
-module
-
 prelude
-public import Init.Data.Array.TakeDrop
-public import Std.Data.DHashMap.Basic
-public import all Std.Data.DHashMap.Internal.Defs
-public import Std.Data.DHashMap.Internal.HashesTo
-public import Std.Data.DHashMap.Internal.AssocList.Lemmas
-
-public @[expose] section
+import Init.Data.Array.TakeDrop
+import Std.Data.DHashMap.Basic
+import Std.Data.DHashMap.Internal.HashesTo
+import Std.Data.DHashMap.Internal.AssocList.Lemmas
 
 /-!
 This is an internal implementation file of the hash map. Users of the hash map should not rely on
@@ -435,13 +430,13 @@ end
 
 theorem reinsertAux_eq [Hashable α] (data : { d : Array (AssocList α β) // 0 < d.size }) (a : α)
     (b : β a) :
-    (reinsertAux hash data a b).1 = updateBucket data.1 data.2 a (fun l => l.cons a b) := (rfl)
+    (reinsertAux hash data a b).1 = updateBucket data.1 data.2 a (fun l => l.cons a b) := rfl
 
 theorem get?_eq_get?ₘ [BEq α] [LawfulBEq α] [Hashable α] (m : Raw₀ α β) (a : α) :
-    get? m a = get?ₘ m a := (rfl)
+    get? m a = get?ₘ m a := rfl
 
 theorem get_eq_getₘ [BEq α] [LawfulBEq α] [Hashable α] (m : Raw₀ α β) (a : α) (h : m.contains a) :
-    get m a h = getₘ m a (by exact h) := (rfl)
+    get m a h = getₘ m a h := rfl
 
 theorem getD_eq_getDₘ [BEq α] [LawfulBEq α] [Hashable α] (m : Raw₀ α β) (a : α) (fallback : β a) :
     getD m a fallback = getDₘ m a fallback := by
@@ -452,10 +447,10 @@ theorem get!_eq_get!ₘ [BEq α] [LawfulBEq α] [Hashable α] (m : Raw₀ α β)
   simp [get!, get!ₘ, get?ₘ, List.getValueCast!_eq_getValueCast?, bucket]
 
 theorem getKey?_eq_getKey?ₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) :
-    getKey? m a = getKey?ₘ m a := (rfl)
+    getKey? m a = getKey?ₘ m a := rfl
 
 theorem getKey_eq_getKeyₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) (h : m.contains a) :
-    getKey m a h = getKeyₘ m a (by exact h) := (rfl)
+    getKey m a h = getKeyₘ m a h := rfl
 
 theorem getKeyD_eq_getKeyDₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a fallback : α) :
     getKeyD m a fallback = getKeyDₘ m a fallback := by
@@ -466,7 +461,7 @@ theorem getKey!_eq_getKey!ₘ [BEq α] [Hashable α] [Inhabited α] (m : Raw₀
   simp [getKey!, getKey!ₘ, getKey?ₘ, List.getKey!_eq_getKey?, bucket]
 
 theorem contains_eq_containsₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) :
-    m.contains a = m.containsₘ a := (rfl)
+    m.contains a = m.containsₘ a := rfl
 
 theorem insert_eq_insertₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) (b : β a) :
     m.insert a b = m.insertₘ a b := by
@@ -567,7 +562,7 @@ theorem containsThenInsertIfNew_eq_containsₘ [BEq α] [Hashable α] (m : Raw
   split <;> simp_all
 
 theorem insertIfNew_eq_insertIfNewₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) (b : β a) :
-    m.insertIfNew a b = m.insertIfNewₘ a b := (rfl)
+    m.insertIfNew a b = m.insertIfNewₘ a b := rfl
 
 theorem getThenInsertIfNew?_eq_insertIfNewₘ [BEq α] [Hashable α] [LawfulBEq α] (m : Raw₀ α β)
     (a : α) (b : β a) : (m.getThenInsertIfNew? a b).2 = m.insertIfNewₘ a b := by
@@ -592,13 +587,13 @@ theorem erase_eq_eraseₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) :
   · rfl
 
 theorem filterMap_eq_filterMapₘ (m : Raw₀ α β) (f : (a : α) → β a → Option (δ a)) :
-    m.filterMap f = m.filterMapₘ f := (rfl)
+    m.filterMap f = m.filterMapₘ f := rfl
 
 theorem map_eq_mapₘ (m : Raw₀ α β) (f : (a : α) → β a → δ a) :
-    m.map f = m.mapₘ f := (rfl)
+    m.map f = m.mapₘ f := rfl
 
 theorem filter_eq_filterₘ (m : Raw₀ α β) (f : (a : α) → β a → Bool) :
-    m.filter f = m.filterₘ f := (rfl)
+    m.filter f = m.filterₘ f := rfl
 
 theorem insertMany_eq_insertListₘ [BEq α] [Hashable α] (m : Raw₀ α β) (l : List ((a : α) × β a)) : insertMany m l = insertListₘ m l := by
   simp only [insertMany, Id.run_pure, pure_bind, List.forIn_pure_yield_eq_foldl]
@@ -618,10 +613,10 @@ section
 variable {β : Type v}
 
 theorem Const.get?_eq_get?ₘ [BEq α] [Hashable α] (m : Raw₀ α (fun _ => β)) (a : α) :
-    Const.get? m a = Const.get?ₘ m a := (rfl)
+    Const.get? m a = Const.get?ₘ m a := rfl
 
 theorem Const.get_eq_getₘ [BEq α] [Hashable α] (m : Raw₀ α (fun _ => β)) (a : α)
-    (h : m.contains a) : Const.get m a h = Const.getₘ m a (by exact h) := (rfl)
+    (h : m.contains a) : Const.get m a h = Const.getₘ m a h := rfl
 
 theorem Const.getD_eq_getDₘ [BEq α] [Hashable α] (m : Raw₀ α (fun _ => β)) (a : α) (fallback : β) :
     Const.getD m a fallback = Const.getDₘ m a fallback := by

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

@@ -3,12 +3,8 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
-module
-
 prelude
-public import all Std.Data.DHashMap.Basic
-
-public section
+import Std.Data.DHashMap.Basic
 
 /-!
 This is an internal implementation file of the hash map. Users of the hash map should not rely on
@@ -30,9 +26,9 @@ namespace Raw
 
 -- TODO: the next two lemmas need to be renamed, but there is a bootstrapping obstacle.
 
-theorem empty_eq {c : Nat} : (Raw.emptyWithCapacity c : Raw α β) = (Raw₀.emptyWithCapacity c).1 := (rfl)
+theorem empty_eq [BEq α] [Hashable α] {c : Nat} : (Raw.emptyWithCapacity c : Raw α β) = (Raw₀.emptyWithCapacity c).1 := rfl
 
-theorem emptyc_eq : (∅ : Raw α β) = Raw₀.emptyWithCapacity.1 := (rfl)
+theorem emptyc_eq [BEq α] [Hashable α] : (∅ : Raw α β) = Raw₀.emptyWithCapacity.1 := rfl
 
 theorem insert_eq [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {a : α} {b : β a} :
     m.insert a b = (Raw₀.insert ⟨m, h.size_buckets_pos⟩ a b).1 := by
@@ -80,7 +76,7 @@ theorem contains_eq [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {a : α} :
 
 theorem get_eq [BEq α] [Hashable α] [LawfulBEq α] {m : Raw α β} {a : α} {h : a ∈ m} :
     m.get a h = Raw₀.get ⟨m, by change dite .. = true at h; split at h <;> simp_all⟩ a
-      (by change dite .. = true at h; split at h <;> simp_all) := (rfl)
+      (by change dite .. = true at h; split at h <;> simp_all) := rfl
 
 theorem getD_eq [BEq α] [Hashable α] [LawfulBEq α] {m : Raw α β} (h : m.WF) {a : α}
     {fallback : β a} : m.getD a fallback = Raw₀.getD ⟨m, h.size_buckets_pos⟩ a fallback := by
@@ -96,7 +92,7 @@ theorem getKey?_eq [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {a : α} :
 
 theorem getKey_eq [BEq α] [Hashable α] {m : Raw α β} {a : α} {h : a ∈ m} :
     m.getKey a h = Raw₀.getKey ⟨m, by change dite .. = true at h; split at h <;> simp_all⟩ a
-      (by change dite .. = true at h; split at h <;> simp_all) := (rfl)
+      (by change dite .. = true at h; split at h <;> simp_all) := rfl
 
 theorem getKeyD_eq [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {a fallback : α} :
     m.getKeyD a fallback = Raw₀.getKeyD ⟨m, h.size_buckets_pos⟩ a fallback := by
@@ -172,7 +168,7 @@ theorem Const.get_eq [BEq α] [Hashable α] {m : Raw α (fun _ => β)} {a : α}
     Raw.Const.get m a h = Raw₀.Const.get
       ⟨m, by change dite .. = true at h; split at h <;> simp_all⟩ a
       (by change dite .. = true at h; split at h <;> simp_all) :=
-  (rfl)
+  rfl
 
 theorem Const.getD_eq [BEq α] [Hashable α] {m : Raw α (fun _ => β)} (h : m.WF) {a : α}
     {fallback : β} : Raw.Const.getD m a fallback =

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

@@ -3,16 +3,8 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
-module
-
 prelude
-import all Std.Data.Internal.List.Associative
-import all Std.Data.DHashMap.Internal.Defs
-public import Std.Data.DHashMap.Internal.WF
-import all Std.Data.DHashMap.Raw
-meta import all Std.Data.DHashMap.Basic
-
-public section
+import Std.Data.DHashMap.Internal.WF
 
 /-!
 This is an internal implementation file of the hash map. Users of the hash map should not rely on
@@ -81,7 +73,7 @@ namespace Raw₀
 variable (m : Raw₀ α β)
 
 @[simp]
-theorem size_emptyWithCapacity {c} : (emptyWithCapacity c : Raw₀ α β).1.size = 0 := (rfl)
+theorem size_emptyWithCapacity {c} : (emptyWithCapacity c : Raw₀ α β).1.size = 0 := rfl
 
 set_option linter.missingDocs false in
 @[deprecated size_emptyWithCapacity (since := "2025-03-12")]

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

@@ -3,18 +3,10 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
-module
-
 prelude
-import all Std.Data.Internal.List.Associative
-import all Std.Data.DHashMap.Raw
-public import Std.Data.DHashMap.Basic
-import all Std.Data.DHashMap.Internal.Defs
-public import Std.Data.DHashMap.Internal.Model
-import all Std.Data.DHashMap.Internal.AssocList.Basic
-public import Std.Data.DHashMap.Internal.AssocList.Lemmas
-
-public section
+import Std.Data.DHashMap.Basic
+import Std.Data.DHashMap.Internal.Model
+import Std.Data.DHashMap.Internal.AssocList.Lemmas
 
 /-!
 This is an internal implementation file of the hash map. Users of the hash map should not rely on
@@ -77,7 +69,7 @@ theorem isEmpty_eq_isEmpty [BEq α] [Hashable α] {m : Raw α β} (h : Raw.WFImp
     Nat.beq_eq_true_eq]
 
 theorem fold_eq {l : Raw α β} {f : γ → (a : α) → β a → γ} {init : γ} :
-    l.fold f init = l.buckets.foldl (fun acc l => l.foldl f acc) init := (rfl)
+    l.fold f init = l.buckets.foldl (fun acc l => l.foldl f acc) init := rfl
 
 theorem fold_cons_apply {l : Raw α β} {acc : List γ} (f : (a : α) → β a → γ) :
     l.fold (fun acc k v => f k v :: acc) acc =
@@ -419,7 +411,7 @@ theorem getKey?_eq_getKey? [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable
 
 theorem getKeyₘ_eq_getKey [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β}
     (hm : Raw.WFImp m.1) {a : α} {h : m.contains a} :
-    m.getKeyₘ a (by exact h) = List.getKey a (toListModel m.1.buckets) (contains_eq_containsKey hm ▸ h) :=
+    m.getKeyₘ a h = List.getKey a (toListModel m.1.buckets) (contains_eq_containsKey hm ▸ h) :=
   apply_bucket_with_proof hm a AssocList.getKey List.getKey AssocList.getKey_eq
     List.getKey_of_perm List.getKey_append_of_containsKey_eq_false
 

src/Std/Data/DHashMap/Lemmas.lean

@@ -3,15 +3,10 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
-module
-
 prelude
-public import Std.Data.DHashMap.Internal.Raw
-public import Std.Data.DHashMap.Internal.RawLemmas
-import all Std.Data.DHashMap.Basic
-public import all Std.Data.DHashMap.AdditionalOperations
-
-public section
+import Std.Data.DHashMap.Internal.Raw
+import Std.Data.DHashMap.Internal.RawLemmas
+import Std.Data.DHashMap.AdditionalOperations
 
 /-!
 # Dependent hash map lemmas
@@ -157,7 +152,7 @@ set_option linter.missingDocs false in
 @[deprecated size_empty (since := "2025-03-12")]
 abbrev size_emptyc := @size_empty
 
-theorem isEmpty_eq_size_eq_zero : m.isEmpty = (m.size == 0) := (rfl)
+theorem isEmpty_eq_size_eq_zero : m.isEmpty = (m.size == 0) := rfl
 
 @[grind =] theorem size_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
     (m.insert k v).size = if k ∈ m then m.size else m.size + 1 :=
@@ -1341,7 +1336,7 @@ theorem fold_eq_foldl_toList {f : δ → (a : α) → β → δ} {init : δ} :
   Raw₀.Const.fold_eq_foldl_toList ⟨m.1, m.2.size_buckets_pos⟩
 
 theorem forM_eq_forMUncurried [Monad m'] [LawfulMonad m'] {f : α → β → m' PUnit} :
-    DHashMap.forM f m = forMUncurried (fun a => f a.1 a.2) m := (rfl)
+    DHashMap.forM f m = forMUncurried (fun a => f a.1 a.2) m := rfl
 
 theorem forMUncurried_eq_forM_toList [Monad m'] [LawfulMonad m'] {f : α × β → m' PUnit} :
     Const.forMUncurried f m = (Const.toList m).forM f :=
@@ -1357,7 +1352,7 @@ theorem forM_eq_forM_toList [Monad m'] [LawfulMonad m'] {f : α → β → m' PU
 
 theorem forIn_eq_forInUncurried [Monad m'] [LawfulMonad m']
     {f : α → β → δ → m' (ForInStep δ)} {init : δ} :
-    DHashMap.forIn f init m = forInUncurried (fun a b => f a.1 a.2 b) init m := (rfl)
+    DHashMap.forIn f init m = forInUncurried (fun a b => f a.1 a.2 b) init m := rfl
 
 theorem forInUncurried_eq_forIn_toList [Monad m'] [LawfulMonad m']
     {f : α × β → δ → m' (ForInStep δ)} {init : δ} :
@@ -2021,7 +2016,7 @@ theorem ofList_singleton {k : α} {v : β k} :
   ext <| congrArg Subtype.val (Raw₀.insertMany_emptyWithCapacity_list_cons (α := α))
 
 theorem ofList_eq_insertMany_empty {l : List ((a : α) × β a)} :
-    ofList l = insertMany (∅ : DHashMap α β) l := (rfl)
+    ofList l = insertMany (∅ : DHashMap α β) l := rfl
 
 @[simp, grind =]
 theorem contains_ofList [EquivBEq α] [LawfulHashable α]
@@ -2170,7 +2165,7 @@ theorem ofList_singleton {k : α} {v : β} :
   ext <| congrArg Subtype.val (Raw₀.Const.insertMany_emptyWithCapacity_list_cons (α:= α))
 
 theorem ofList_eq_insertMany_empty {l : List (α × β)} :
-    ofList l = insertMany (∅ : DHashMap α (fun _ => β)) l := (rfl)
+    ofList l = insertMany (∅ : DHashMap α (fun _ => β)) l := rfl
 
 @[simp, grind =]
 theorem contains_ofList [EquivBEq α] [LawfulHashable α]

src/Std/Data/DHashMap/Raw.lean

@@ -3,14 +3,10 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
-module
-
 prelude
-public import Init.Data.BEq
-public import Init.Data.Hashable
-public import Std.Data.DHashMap.Internal.Defs
-
-public section
+import Init.Data.BEq
+import Init.Data.Hashable
+import Std.Data.DHashMap.Internal.Defs
 
 /-!
 # Dependent hash maps with unbundled well-formedness invariant

src/Std/Data/DHashMap/RawDef.lean

@@ -3,12 +3,8 @@ Copyright (c) 2018 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Mario Carneiro, Markus Himmel
 -/
-module
-
 prelude
-public import Std.Data.DHashMap.Internal.AssocList.Basic
-
-public section
+import Std.Data.DHashMap.Internal.AssocList.Basic
 
 /-!
 # Definition of `DHashMap.Raw`

src/Std/Data/DHashMap/RawLemmas.lean

@@ -3,14 +3,9 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
-module
-
 prelude
-public import Std.Data.DHashMap.Internal.Raw
-public import Std.Data.DHashMap.Internal.RawLemmas
-public import all Std.Data.DHashMap.Raw
-
-public section
+import Std.Data.DHashMap.Internal.Raw
+import Std.Data.DHashMap.Internal.RawLemmas
 
 /-!
 # Dependent hash map lemmas
@@ -1415,7 +1410,7 @@ theorem fold_eq_foldl_toList (h : m.WF) {f : δ → (a : α) → β → δ} {ini
 omit [BEq α] [Hashable α] in
 theorem forM_eq_forMUncurried [Monad m'] [LawfulMonad m']
     {f : α → β → m' PUnit} :
-    Raw.forM f m = Const.forMUncurried (fun a => f a.1 a.2) m := (rfl)
+    Raw.forM f m = Const.forMUncurried (fun a => f a.1 a.2) m := rfl
 
 theorem forMUncurried_eq_forM_toList [Monad m'] [LawfulMonad m'] (h : m.WF)
     {f : α × β → m' PUnit} :
@@ -1434,7 +1429,7 @@ omit [BEq α] [Hashable α] in
 @[simp]
 theorem forIn_eq_forInUncurried [Monad m'] [LawfulMonad m']
     {f : α → β → δ → m' (ForInStep δ)} {init : δ} :
-    forIn f init m = forInUncurried (fun a b => f a.1 a.2 b) init m := (rfl)
+    forIn f init m = forInUncurried (fun a b => f a.1 a.2 b) init m := rfl
 
 theorem forInUncurried_eq_forIn_toList [Monad m'] [LawfulMonad m'] (h : m.WF)
     {f : α × β → δ → m' (ForInStep δ)} {init : δ} :
@@ -2131,7 +2126,7 @@ theorem ofList_singleton {k : α} {v : β k} :
   rw [Raw₀.insertMany_emptyWithCapacity_list_cons]
 
 theorem ofList_eq_insertMany_empty {l : List ((a : α) × (β a))} :
-    ofList l = insertMany (∅ : Raw α β) l := (rfl)
+    ofList l = insertMany (∅ : Raw α β) l := rfl
 
 @[simp, grind =]
 theorem contains_ofList [EquivBEq α] [LawfulHashable α]
@@ -2283,7 +2278,7 @@ theorem ofList_singleton {k : α} {v : β} :
   rw [Raw₀.Const.insertMany_emptyWithCapacity_list_cons]
 
 theorem ofList_eq_insertMany_empty {l : List (α × β)} :
-    ofList l = insertMany (∅ : Raw α (fun _ => β)) l := (rfl)
+    ofList l = insertMany (∅ : Raw α (fun _ => β)) l := rfl
 
 @[simp, grind =]
 theorem contains_ofList [EquivBEq α] [LawfulHashable α]

src/Std/Data/Internal/List/Associative.lean

@@ -3,20 +3,16 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
-module
-
 prelude
-public import Init.Data.BEq
-public import Init.Data.Nat.Simproc
-public import Init.Data.Option.Attach
-public import Init.Data.List.Perm
-public import Init.Data.List.Find
-public import Init.Data.List.MinMax
-public import Init.Data.List.Monadic
-public import all Std.Data.Internal.List.Defs
-public import Std.Classes.Ord.Basic
-
-public section
+import Init.Data.BEq
+import Init.Data.Nat.Simproc
+import Init.Data.Option.Attach
+import Init.Data.List.Perm
+import Init.Data.List.Find
+import Init.Data.List.MinMax
+import Init.Data.List.Monadic
+import Std.Data.Internal.List.Defs
+import Std.Classes.Ord.Basic
 
 /-!
 This is an internal implementation file of the hash map. Users of the hash map should not rely on
@@ -27,6 +23,7 @@ File contents: Verification of associative lists
 
 set_option linter.missingDocs true
 set_option autoImplicit false
+set_option Elab.async false
 
 universe u v w w'
 
@@ -52,9 +49,9 @@ def getEntry? [BEq α] (a : α) : List ((a : α) × β a) → Option ((a : α)
   | ⟨k, v⟩ :: l => bif k == a then some ⟨k, v⟩ else getEntry? a l
 
 @[simp] theorem getEntry?_nil [BEq α] {a : α} :
-    getEntry? a ([] : List ((a : α) × β a)) = none := (rfl)
+    getEntry? a ([] : List ((a : α) × β a)) = none := rfl
 theorem getEntry?_cons [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} :
-    getEntry? a (⟨k, v⟩ :: l) = bif k == a then some ⟨k, v⟩ else getEntry? a l := (rfl)
+    getEntry? a (⟨k, v⟩ :: l) = bif k == a then some ⟨k, v⟩ else getEntry? a l := rfl
 
 theorem getEntry?_eq_find [BEq α] {k : α} {l : List ((a : α) × β a)} :
     getEntry? k l = l.find? (·.1 == k) := by
@@ -146,7 +143,7 @@ section
 variable {β : Type v}
 
 /-- Internal implementation detail of the hash map -/
-@[expose] def getValue? [BEq α] (a : α) : List ((_ : α) × β) → Option β
+def getValue? [BEq α] (a : α) : List ((_ : α) × β) → Option β
   | [] => none
   | ⟨k, v⟩ :: l => bif k == a then some v else getValue? a l
 
@@ -187,7 +184,7 @@ theorem isEmpty_eq_false_iff_exists_isSome_getValue? [BEq α] [ReflBEq α] {l :
 end
 
 /-- Internal implementation detail of the hash map -/
-@[expose] def getValueCast? [BEq α] [LawfulBEq α] (a : α) : List ((a : α) × β a) → Option (β a)
+def getValueCast? [BEq α] [LawfulBEq α] (a : α) : List ((a : α) × β a) → Option (β a)
   | [] => none
   | ⟨k, v⟩ :: l => if h : k == a then some (cast (congrArg β (eq_of_beq h)) v)
       else getValueCast? a l
@@ -255,7 +252,7 @@ private theorem Option.dmap_eq_some {o : Option α} {f : (a : α) → (o = some
 
 end
 
-private theorem getValueCast?_eq_getEntry? [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} :
+theorem getValueCast?_eq_getEntry? [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} :
     getValueCast? a l = Option.dmap (getEntry? a l)
       (fun p h => cast (congrArg β (eq_of_beq (beq_of_getEntry?_eq_some h))) p.2) := by
   induction l using assoc_induction
@@ -279,9 +276,9 @@ def containsKey [BEq α] (a : α) : List ((a : α) × β a) → Bool
   | ⟨k, _⟩ :: l => k == a || containsKey a l
 
 @[simp] theorem containsKey_nil [BEq α] {a : α} :
-    containsKey a ([] : List ((a : α) × β a)) = false := (rfl)
+    containsKey a ([] : List ((a : α) × β a)) = false := rfl
 @[simp] theorem containsKey_cons [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} :
-    containsKey a (⟨k, v⟩ :: l) = (k == a || containsKey a l) := (rfl)
+    containsKey a (⟨k, v⟩ :: l) = (k == a || containsKey a l) := rfl
 
 theorem containsKey_cons_eq_false [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} :
     (containsKey a (⟨k, v⟩ :: l) = false) ↔ ((k == a) = false) ∧ (containsKey a l = false) := by
@@ -333,9 +330,9 @@ theorem containsKey_eq_contains_map_fst [BEq α] [PartialEquivBEq α] {l : List
     simp only [List.map_cons, List.contains_cons]
     rw [BEq.comm]
 
-@[simp] theorem keys_nil : keys ([] : List ((a : α) × β a)) = [] := (rfl)
+@[simp] theorem keys_nil : keys ([] : List ((a : α) × β a)) = [] := rfl
 @[simp] theorem keys_cons {l : List ((a : α) × β a)} {k : α} {v : β k} :
-    keys (⟨k, v⟩ :: l) = k :: keys l := (rfl)
+    keys (⟨k, v⟩ :: l) = k :: keys l := rfl
 
 theorem length_keys_eq_length (l : List ((a : α) × β a)) : (keys l).length = l.length := by
   induction l using assoc_induction <;> simp_all
@@ -545,7 +542,7 @@ theorem getValue?_eq_some_getValue [BEq α] {l : List ((_ : α) × β)} {a : α}
   simp [getValue]
 
 theorem getValue_cons_of_beq [BEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} (h : k == a) :
-    getValue a (⟨k, v⟩ :: l) (containsKey_cons_of_beq h) = v := by
+    getValue a (⟨k, v⟩ :: l) (containsKey_cons_of_beq (k := k) (v := v) h) = v := by
   simp [getValue, getValue?_cons_of_true h]
 
 @[simp]
@@ -652,15 +649,15 @@ theorem getValue_eq_getValueCast {β : Type v} [BEq α] [LawfulBEq α] {l : List
   · simp_all [getValue_cons, getValueCast_cons]
 
 /-- Internal implementation detail of the hash map -/
-@[expose] def getValueCastD [BEq α] [LawfulBEq α] (a : α) (l : List ((a : α) × β a)) (fallback : β a) : β a :=
+def getValueCastD [BEq α] [LawfulBEq α] (a : α) (l : List ((a : α) × β a)) (fallback : β a) : β a :=
   (getValueCast? a l).getD fallback
 
 @[simp]
 theorem getValueCastD_nil [BEq α] [LawfulBEq α] {a : α} {fallback : β a} :
-  getValueCastD a ([] : List ((a : α) × β a)) fallback = fallback := (rfl)
+  getValueCastD a ([] : List ((a : α) × β a)) fallback = fallback := rfl
 
 theorem getValueCastD_eq_getValueCast? [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α}
-    {fallback : β a} : getValueCastD a l fallback = (getValueCast? a l).getD fallback := (rfl)
+    {fallback : β a} : getValueCastD a l fallback = (getValueCast? a l).getD fallback := rfl
 
 theorem getValueCastD_eq_fallback [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α}
     {fallback : β a} (h : containsKey a l = false) : getValueCastD a l fallback = fallback := by
@@ -679,16 +676,16 @@ theorem getValueCast?_eq_some_getValueCastD [BEq α] [LawfulBEq α] {l : List ((
   rw [getValueCast?_eq_some_getValueCast h, getValueCast_eq_getValueCastD]
 
 /-- Internal implementation detail of the hash map -/
-@[expose] def getValueCast! [BEq α] [LawfulBEq α] (a : α) [Inhabited (β a)] (l : List ((a : α) × β a)) :
+def getValueCast! [BEq α] [LawfulBEq α] (a : α) [Inhabited (β a)] (l : List ((a : α) × β a)) :
     β a :=
   (getValueCast? a l).get!
 
 @[simp]
 theorem getValueCast!_nil [BEq α] [LawfulBEq α] {a : α} [Inhabited (β a)] :
-    getValueCast! a ([] : List ((a : α) × β a)) = default := (rfl)
+    getValueCast! a ([] : List ((a : α) × β a)) = default := rfl
 
 theorem getValueCast!_eq_getValueCast? [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α}
-    [Inhabited (β a)] : getValueCast! a l = (getValueCast? a l).get! := (rfl)
+    [Inhabited (β a)] : getValueCast! a l = (getValueCast? a l).get! := rfl
 
 theorem getValueCast!_eq_default [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α}
     [Inhabited (β a)] (h : containsKey a l = false) : getValueCast! a l = default := by
@@ -706,22 +703,22 @@ theorem getValueCast?_eq_some_getValueCast! [BEq α] [LawfulBEq α] {l : List ((
   rw [getValueCast?_eq_some_getValueCast h, getValueCast_eq_getValueCast!]
 
 theorem getValueCast!_eq_getValueCastD_default [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)}
-    {a : α} [Inhabited (β a)] : getValueCast! a l = getValueCastD a l default := (rfl)
+    {a : α} [Inhabited (β a)] : getValueCast! a l = getValueCastD a l default := rfl
 
 section
 
 variable {β : Type v}
 
 /-- Internal implementation detail of the hash map -/
-@[expose] def getValueD [BEq α] (a : α) (l : List ((_ : α) × β)) (fallback : β) : β :=
+def getValueD [BEq α] (a : α) (l : List ((_ : α) × β)) (fallback : β) : β :=
   (getValue? a l).getD fallback
 
 @[simp]
 theorem getValueD_nil [BEq α] {a : α} {fallback : β} :
-    getValueD a ([] : List ((_ : α) × β)) fallback = fallback := (rfl)
+    getValueD a ([] : List ((_ : α) × β)) fallback = fallback := rfl
 
 theorem getValueD_eq_getValue? [BEq α] {l : List ((_ : α) × β)} {a : α} {fallback : β} :
-    getValueD a l fallback = (getValue? a l).getD fallback := (rfl)
+    getValueD a l fallback = (getValue? a l).getD fallback := rfl
 
 theorem getValueD_eq_fallback [BEq α] {l : List ((_ : α) × β)} {a : α} {fallback : β}
     (h : containsKey a l = false) : getValueD a l fallback = fallback := by
@@ -745,15 +742,15 @@ theorem getValueD_congr [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)
   simp only [getValueD_eq_getValue?, getValue?_congr hab]
 
 /-- Internal implementation detail of the hash map -/
-@[expose] def getValue! [BEq α] [Inhabited β] (a : α) (l : List ((_ : α) × β)) : β :=
+def getValue! [BEq α] [Inhabited β] (a : α) (l : List ((_ : α) × β)) : β :=
   (getValue? a l).get!
 
 @[simp]
 theorem getValue!_nil [BEq α] [Inhabited β] {a : α} :
-    getValue! a ([] : List ((_ : α) × β)) = default := (rfl)
+    getValue! a ([] : List ((_ : α) × β)) = default := rfl
 
 theorem getValue!_eq_getValue? [BEq α] [Inhabited β] {l : List ((_ : α) × β)} {a : α} :
-    getValue! a l = (getValue? a l).get! := (rfl)
+    getValue! a l = (getValue? a l).get! := rfl
 
 theorem getValue!_eq_default [BEq α] [Inhabited β] {l : List ((_ : α) × β)} {a : α}
     (h : containsKey a l = false) : getValue! a l = default := by
@@ -777,7 +774,7 @@ theorem getValue!_congr [BEq α] [PartialEquivBEq α] [Inhabited β] {l : List (
   simp only [getValue!_eq_getValue?, getValue?_congr hab]
 
 theorem getValue!_eq_getValueD_default [BEq α] [Inhabited β] {l : List ((_ : α) × β)} {a : α} :
-    getValue! a l = getValueD a l default := (rfl)
+    getValue! a l = getValueD a l default := rfl
 
 end
 
@@ -787,10 +784,10 @@ def getKey? [BEq α] (a : α) : List ((a : α) × β a) → Option α
   | ⟨k, _⟩ :: l => bif k == a then some k else getKey? a l
 
 @[simp] theorem getKey?_nil [BEq α] {a : α} :
-    getKey? a ([] : List ((a : α) × β a)) = none := (rfl)
+    getKey? a ([] : List ((a : α) × β a)) = none := rfl
 
 @[simp] theorem getKey?_cons [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} :
-    getKey? a (⟨k, v⟩ :: l) = bif k == a then some k else getKey? a l := (rfl)
+    getKey? a (⟨k, v⟩ :: l) = bif k == a then some k else getKey? a l := rfl
 
 theorem getKey?_cons_of_true [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h : k == a) :
     getKey? a (⟨k, v⟩ :: l) = some k := by
@@ -972,15 +969,15 @@ theorem forall_mem_keys_iff_forall_containsKey_getKey [BEq α] [EquivBEq α] {l
         · exact h
 
 /-- Internal implementation detail of the hash map -/
-@[expose] def getKeyD [BEq α] (a : α) (l : List ((a : α) × β a)) (fallback : α) : α :=
+def getKeyD [BEq α] (a : α) (l : List ((a : α) × β a)) (fallback : α) : α :=
   (getKey? a l).getD fallback
 
 @[simp]
 theorem getKeyD_nil [BEq α] {a fallback : α} :
-  getKeyD a ([] : List ((a : α) × β a)) fallback = fallback := (rfl)
+  getKeyD a ([] : List ((a : α) × β a)) fallback = fallback := rfl
 
 theorem getKeyD_eq_getKey? [BEq α] {l : List ((a : α) × β a)} {a fallback : α} :
-  getKeyD a l fallback = (getKey? a l).getD fallback := (rfl)
+  getKeyD a l fallback = (getKey? a l).getD fallback := rfl
 
 theorem getKeyD_eq_fallback [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {a fallback : α}
     (h : containsKey a l = false) : getKeyD a l fallback = fallback := by
@@ -1008,15 +1005,15 @@ theorem getKey?_eq_some_getKeyD [BEq α] [EquivBEq α] {l : List ((a : α) × β
   rw [getKey?_eq_some_getKey h, getKey_eq_getKeyD]
 
 /-- Internal implementation detail of the hash map -/
-@[expose] def getKey! [BEq α] [Inhabited α] (a : α) (l : List ((a : α) × β a)) : α :=
+def getKey! [BEq α] [Inhabited α] (a : α) (l : List ((a : α) × β a)) : α :=
   (getKey? a l).get!
 
 @[simp]
 theorem getKey!_nil [BEq α] [Inhabited α] {a : α} :
-    getKey! a ([] : List ((a : α) × β a)) = default := (rfl)
+    getKey! a ([] : List ((a : α) × β a)) = default := rfl
 
 theorem getKey!_eq_getKey? [BEq α] [Inhabited α] {l : List ((a : α) × β a)} {a : α} :
-    getKey! a l = (getKey? a l).get! := (rfl)
+    getKey! a l = (getKey? a l).get! := rfl
 
 theorem getKey!_eq_default [BEq α] [Inhabited α] {l : List ((a : α) × β a)} {a : α}
     (h : containsKey a l = false) : getKey! a l = default := by
@@ -1043,7 +1040,7 @@ theorem getKey?_eq_some_getKey! [BEq α] [Inhabited α] {l : List ((a : α) ×
   rw [getKey?_eq_some_getKey h, getKey_eq_getKey!]
 
 theorem getKey!_eq_getKeyD_default [BEq α] [EquivBEq α] [Inhabited α] {l : List ((a : α) × β a)}
-    {a : α} : getKey! a l = getKeyD a l default := (rfl)
+    {a : α} : getKey! a l = getKeyD a l default := rfl
 
 theorem getEntry?_eq_getValueCast? [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)}
     {a : α} : getEntry? a l = (getValueCast? a l).map (fun v => ⟨a, v⟩) := by
@@ -1076,10 +1073,10 @@ def replaceEntry [BEq α] (k : α) (v : β k) : List ((a : α) × β a) → List
   | [] => []
   | ⟨k', v'⟩ :: l => bif k' == k then ⟨k, v⟩ :: l else ⟨k', v'⟩ :: replaceEntry k v l
 
-@[simp] theorem replaceEntry_nil [BEq α] {k : α} {v : β k} : replaceEntry k v [] = [] := (rfl)
+@[simp] theorem replaceEntry_nil [BEq α] {k : α} {v : β k} : replaceEntry k v [] = [] := rfl
 theorem replaceEntry_cons [BEq α] {l : List ((a : α) × β a)} {k k' : α} {v : β k} {v' : β k'} :
     replaceEntry k v (⟨k', v'⟩ :: l) =
-      bif k' == k then ⟨k, v⟩ :: l else ⟨k', v'⟩ :: replaceEntry k v l := (rfl)
+      bif k' == k then ⟨k, v⟩ :: l else ⟨k', v'⟩ :: replaceEntry k v l := rfl
 
 theorem replaceEntry_cons_of_true [BEq α] {l : List ((a : α) × β a)} {k k' : α} {v : β k}
     {v' : β k'} (h : k' == k) : replaceEntry k v (⟨k', v'⟩ :: l) = ⟨k, v⟩ :: l := by
@@ -1259,10 +1256,10 @@ def eraseKey [BEq α] (k : α) : List ((a : α) × β a) → List ((a : α) ×
   | [] => []
   | ⟨k', v'⟩ :: l => bif k' == k then l else ⟨k', v'⟩ :: eraseKey k l
 
-@[simp] theorem eraseKey_nil [BEq α] {k : α} : eraseKey k ([] : List ((a : α) × β a)) = [] := (rfl)
+@[simp] theorem eraseKey_nil [BEq α] {k : α} : eraseKey k ([] : List ((a : α) × β a)) = [] := rfl
 
 theorem eraseKey_cons [BEq α] {l : List ((a : α) × β a)} {k k' : α} {v' : β k'} :
-    eraseKey k (⟨k', v'⟩ :: l) = bif k' == k then l else ⟨k', v'⟩ :: eraseKey k l := (rfl)
+    eraseKey k (⟨k', v'⟩ :: l) = bif k' == k then l else ⟨k', v'⟩ :: eraseKey k l := rfl
 
 theorem eraseKey_cons_of_beq [BEq α] {l : List ((a : α) × β a)} {k k' : α} {v' : β k'}
     (h : k' == k) : eraseKey k (⟨k', v'⟩ :: l) = l :=
@@ -1871,12 +1868,12 @@ theorem keys_filter [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {f : (
       (List.filter (fun x => f x.1 (getValueCast x.1 l (mem_keys_iff_contains.mp x.2)))
         (keys l).attach).unattach := by
   induction l using assoc_induction with
-  | nil => simp [keys]
+  | nil => simp
   | cons k v tl ih =>
     rw [List.filter_cons]
     specialize ih hl.tail
     replace hl := hl.containsKey_eq_false
-    simp only [keys, List.attach_cons, getValueCast_cons, ↓reduceDIte, cast_eq,
+    simp only [keys_cons, List.attach_cons, getValueCast_cons, ↓reduceDIte, cast_eq,
       List.filter_cons, BEq.rfl, List.filter_map, Function.comp_def]
     have (x : { x // x ∈ keys tl }) : (k == x.val) = False := eq_false <| by
       intro h
@@ -1893,12 +1890,12 @@ theorem Const.keys_filter [BEq α] [EquivBEq α] {β : Type v}
       (List.filter (fun x => f x.1 (getValue x.1 l (containsKey_of_mem_keys x.2)))
         (keys l).attach).unattach := by
   induction l using assoc_induction with
-  | nil => simp [keys]
+  | nil => simp
   | cons k v tl ih =>
     rw [List.filter_cons]
     specialize ih hl.tail
     replace hl := hl.containsKey_eq_false
-    simp only [keys, List.attach_cons, getValue_cons, ↓reduceDIte,
+    simp only [keys_cons, List.attach_cons, getValue_cons, ↓reduceDIte, 
       List.filter_cons, BEq.rfl, List.filter_map, Function.comp_def]
     have (x : { x // x ∈ keys tl }) : (k == x.val) = False := eq_false <| by
       intro h
@@ -3416,7 +3413,7 @@ theorem length_insertListIfNewUnit [BEq α] [EquivBEq α]
     rw [ih]
     · rw [length_insertEntryIfNew]
       specialize distinct_both hd
-      simp only [List.contains_cons, BEq.rfl, Bool.true_or,
+      simp only [List.contains_cons, BEq.rfl, Bool.true_or, 
         ] at distinct_both
       cases eq : containsKey hd l with
       | true => simp [eq] at distinct_both
@@ -3427,7 +3424,7 @@ theorem length_insertListIfNewUnit [BEq α] [EquivBEq α]
     · simp only [pairwise_cons] at distinct_toInsert
       apply And.right distinct_toInsert
     · intro a
-      simp only [List.contains_cons,
+      simp only [List.contains_cons, 
         ] at distinct_both
       rw [containsKey_insertEntryIfNew]
       simp only [Bool.or_eq_true]
@@ -3549,8 +3546,7 @@ theorem alterKey_cons_perm {k : α} {f : Option (β k) → Option (β k)} {k' :
   by_cases hk' : k' == k
   · simp only [hk', ↓reduceDIte]
     rw [getValueCast?_cons_of_true hk', eraseKey_cons_of_beq hk']
-    simp only [insertEntry_cons_of_beq hk']
-    rfl
+    simp [insertEntry_cons_of_beq hk']
   · simp only [hk', Bool.false_eq_true, ↓reduceDIte]
     rw [Bool.not_eq_true] at hk'
     rw [getValueCast?_cons_of_false hk', eraseKey_cons_of_false hk', alterKey]
@@ -3588,7 +3584,7 @@ theorem alterKey_append_of_containsKey_right_eq_false {a : α} {f : Option (β a
 theorem alterKey_nil {a : α} {f : Option (β a) → Option (β a)} :
     alterKey a f [] = match f none with
 | none => []
-| some b => [⟨a, b⟩] := (rfl)
+| some b => [⟨a, b⟩] := rfl
 
 theorem containsKey_alterKey_self {a : α} {f : Option (β a) → Option (β a)}
     {l : List ((a : α) × β a)} (hl : DistinctKeys l) :
@@ -3835,8 +3831,7 @@ theorem alterKey_cons_perm {k : α} {f : Option β → Option β} {k' : α} {v'
   by_cases hk' : k' == k
   · simp only [hk']
     rw [getValue?_cons_of_true hk', eraseKey_cons_of_beq hk']
-    simp only [insertEntry_cons_of_beq hk']
-    rfl
+    simp [insertEntry_cons_of_beq hk']
   · simp only [hk', Bool.false_eq_true]
     rw [Bool.not_eq_true] at hk'
     rw [getValue?_cons_of_false hk', eraseKey_cons_of_false hk', alterKey]
@@ -3874,7 +3869,7 @@ theorem alterKey_append_of_containsKey_right_eq_false {a : α} {f : Option β
 theorem alterKey_nil {a : α} {f : Option β → Option β} :
     alterKey a f [] = match f none with
 | none => []
-| some b => [⟨a, b⟩] := (rfl)
+| some b => [⟨a, b⟩] := rfl
 
 theorem containsKey_alterKey_self [EquivBEq α] {a : α} {f : Option β → Option β}
     {l : List ((_ : α) × β)} (hl : DistinctKeys l) :
@@ -3974,7 +3969,7 @@ theorem getValue!_alterKey [EquivBEq α] {k k' : α} [Inhabited β] {f : Option
         (f (getValue? k l)).get!
       else
         getValue! k' l := by
-  simp only [hl, getValue!_eq_getValue?, getValue?_alterKey,
+  simp only [hl, getValue!_eq_getValue?, getValue?_alterKey, 
     apply_ite Option.get!]
 
 theorem getValueD_alterKey [EquivBEq α] {k k' : α} {fallback : β} {f : Option β → Option β}
@@ -3984,7 +3979,7 @@ theorem getValueD_alterKey [EquivBEq α] {k k' : α} {fallback : β} {f : Option
         f (getValue? k l) |>.getD fallback
       else
         getValueD k' l fallback := by
-  simp only [hl, getValueD_eq_getValue?, getValue?_alterKey,
+  simp only [hl, getValueD_eq_getValue?, getValue?_alterKey, 
     apply_ite (Option.getD · fallback)]
 
 theorem getKey?_alterKey [EquivBEq α] {k k' : α} {f : Option β → Option β} (l : List ((_ : α) × β))
@@ -4418,31 +4413,31 @@ end Modify
 
 section FilterMap
 
-private theorem Option.dmap_bind {α β γ : Type _} (x : Option α) (f : α → Option β)
+theorem Option.dmap_bind {α β γ : Type _} (x : Option α) (f : α → Option β)
     (g : (a : β) → x.bind f = some a → γ) :
     Option.dmap (x.bind f) g =
       x.pbind (fun a h => Option.dmap (f a) (fun b h' => g b (h ▸ h'.symm ▸ rfl))) := by
   cases x <;> rfl
 
-private theorem Option.bind_dmap_left {α β γ : Type _} (x : Option α)
+theorem Option.bind_dmap_left {α β γ : Type _} (x : Option α)
     (f : (a : α) → x = some a → β) (g : β → Option γ) :
     (Option.dmap x f).bind g = x.pbind (fun a h => g (f a h)) := by
   cases x <;> rfl
 
-private theorem Option.dmap_map {α β γ : Type _} (x : Option α) (f : α → β)
+theorem Option.dmap_map {α β γ : Type _} (x : Option α) (f : α → β)
     (g : (a : β) → x.map f = some a → γ) :
     Option.dmap (x.map f) g = Option.dmap x (fun a h => g (f a) (h ▸ rfl)) := by
   cases x <;> rfl
 
-private theorem Option.map_dmap {α β γ : Type _} (x : Option α)
+theorem Option.map_dmap {α β γ : Type _} (x : Option α)
     (f : (a : α) → x = some a → β) (g : β → γ) :
     (x.dmap f).map g = Option.dmap x (fun a h => g (f a h)) := by
   cases x <;> rfl
 
-private theorem Option.dmap_id {α : Type _} (x : Option α) : Option.dmap x (fun a _ => a) = x := by
+theorem Option.dmap_id {α : Type _} (x : Option α) : Option.dmap x (fun a _ => a) = x := by
   cases x <;> rfl
 
-private theorem Option.dmap_ite {α β : Type _} (p : Prop) [Decidable p] (t e : Option α)
+theorem Option.dmap_ite {α β : Type _} (p : Prop) [Decidable p] (t e : Option α)
     (f : (a : α) → (if p then t else e) = some a → β) :
     Option.dmap (if p then t else e) f =
       if h : p then Option.dmap t (fun a h' => f a (if_pos h ▸ h'))
@@ -4453,7 +4448,7 @@ private theorem Option.dmap_ite {α β : Type _} (p : Prop) [Decidable p] (t e :
   · rename_i h
     simp only
 
-private theorem Option.get_dmap {α β : Type _} {x : Option α} {f : (a : α) → x = some a → β} (h) :
+theorem Option.get_dmap {α β : Type _} {x : Option α} {f : (a : α) → x = some a → β} (h) :
     (Option.dmap x f).get h =
       f (x.get (isSome_dmap.symm.trans h)) (Option.eq_some_of_isSome _) := by
   cases x <;> trivial
@@ -4467,16 +4462,16 @@ theorem Sigma.snd_congr {x x' : (a : α) × β a} (h : x = x') :
     x.snd = cast (congrArg (β ·.fst) h.symm) x'.snd := by
   cases h; rfl
 
-private theorem Option.pmap_eq_dmap {α β : Type _} {p : α → Prop} {x : Option α}
+theorem Option.pmap_eq_dmap {α β : Type _} {p : α → Prop} {x : Option α}
     {f : (a : α) → p a → β} (h : ∀ a ∈ x, p a) :
     x.pmap f h = Option.dmap x (fun a h' => f a (h a h')) := by
   cases x <;> rfl
 
-private theorem Option.dmap_eq_map {α β : Type _} {x : Option α} {f : α → β} :
+theorem Option.dmap_eq_map {α β : Type _} {x : Option α} {f : α → β} :
     Option.dmap x (fun a _ => f a) = x.map f := by
   cases x <;> rfl
 
-private theorem Option.any_dmap {α β : Type _} {x : Option α}
+theorem Option.any_dmap {α β : Type _} {x : Option α}
     {f : (a : α) → x = some a → β} {p : β → Bool} :
     (x.dmap f).any p = x.attach.any (fun ⟨a, h⟩ => p (f a h)) := by
   cases x <;> rfl
@@ -5018,7 +5013,7 @@ theorem length_filter_eq_length_iff [BEq α] [LawfulBEq α] {f : (a : α) → β
     {l : List ((a : α) × β a)} (distinct : DistinctKeys l) :
     (l.filter fun p => f p.1 p.2).length = l.length ↔
       ∀ (a : α) (h : containsKey a l), (f a (getValueCast a l h)) = true := by
-  simp [← List.filterMap_eq_filter,
+  simp [← List.filterMap_eq_filter, 
     forall_mem_iff_forall_contains_getValueCast (p := fun a b => f a b = true) distinct]
 
 theorem length_filter_key_eq_length_iff [BEq α] [EquivBEq α] {f : α → Bool}
@@ -5210,7 +5205,7 @@ theorem getValue?_filter {β : Type v} [BEq α] [EquivBEq α]
     getValue? k (l.filter fun p => (f p.1 p.2)) =
       (getValue? k l).pfilter (fun v h =>
         f (getKey k l (containsKey_eq_isSome_getValue?.trans (Option.isSome_of_eq_some h))) v) := by
-  simp only [getValue?_eq_getEntry?, distinct, getEntry?_filter,
+  simp only [getValue?_eq_getEntry?, distinct, getEntry?_filter, 
     Option.pfilter_eq_pbind_ite, ← Option.bind_guard, Option.guard_def,
     Option.pbind_map, Option.map_bind, Function.comp_def, apply_ite,
     Option.map_some, Option.map_none]
@@ -5385,14 +5380,14 @@ theorem length_filter_eq_length_iff {β : Type v} [BEq α] [EquivBEq α]
     {f : (_ : α) → β → Bool} {l : List ((_ : α) × β)} (distinct : DistinctKeys l) :
     (l.filter fun p => (f p.1 p.2)).length = l.length ↔
       ∀ (a : α) (h : containsKey a l), (f (getKey a l h) (getValue a l h)) = true := by
-  simp [← List.filterMap_eq_filter, Option.guard,
+  simp [← List.filterMap_eq_filter, Option.guard, 
     forall_mem_iff_forall_contains_getKey_getValue (p := fun a b => f a b = true) distinct]
 
 theorem length_filter_key_eq_length_iff {β : Type v} [BEq α] [EquivBEq α]
     {f : (_ : α) → Bool} {l : List ((_ : α) × β)} (distinct : DistinctKeys l) :
     (l.filter fun p => f p.1).length = l.length ↔
       ∀ (a : α) (h : containsKey a l), f (getKey a l h)  = true := by
-  simp [← List.filterMap_eq_filter,
+  simp [← List.filterMap_eq_filter, 
     forall_mem_iff_forall_contains_getKey_getValue (p := fun a b => f a = true) distinct]
 
 theorem isEmpty_filterMap_eq_true [BEq α] [EquivBEq α] {β : Type v} {γ : Type w}
@@ -5466,7 +5461,7 @@ private theorem leSigmaOfOrd_total [Ord α] [OrientedOrd α] (a b : (a : α) ×
 private local instance minSigmaOfOrd [Ord α] : Min ((a : α) × β a) where
   min a b := if compare a.1 b.1 |>.isLE then a else b
 
-private theorem min_def [Ord α] {p q : (a : α) × β a} :
+theorem min_def [Ord α] {p q : (a : α) × β a} :
     min p q = if compare p.1 q.1 |>.isLE then p else q :=
   rfl
 
@@ -5505,14 +5500,14 @@ theorem DistinctKeys.eq_of_mem_of_beq [BEq α] [EquivBEq α] {a b : (a : α) ×
     · simp [BEq.symm_false <| hd.1 a.1 <| fst_mem_keys_of_mem ‹_›] at he
     · exact ih ‹_› hd.2
 
-private theorem min_eq_or [Ord α] {p q : (a : α) × β a} : min p q = p ∨ min p q = q := by
+theorem min_eq_or [Ord α] {p q : (a : α) × β a} : min p q = p ∨ min p q = q := by
   rw [min_def]
   split <;> simp
 
-private theorem min_eq_left [Ord α] {p q : (a : α) × β a} (h : compare p.1 q.1 |>.isLE) : min p q = p := by
+theorem min_eq_left [Ord α] {p q : (a : α) × β a} (h : compare p.1 q.1 |>.isLE) : min p q = p := by
   simp [min_def, h]
 
-private theorem min_eq_left_of_lt [Ord α] {p q : (a : α) × β a} (h : compare p.1 q.1 = .lt) : min p q = p :=
+theorem min_eq_left_of_lt [Ord α] {p q : (a : α) × β a} (h : compare p.1 q.1 = .lt) : min p q = p :=
   min_eq_left (Ordering.isLE_of_eq_lt h)
 
 theorem minEntry?_eq_head? [Ord α] {l : List ((a : α) × β a)}
@@ -5523,7 +5518,7 @@ theorem minEntry?_eq_head? [Ord α] {l : List ((a : α) × β a)}
 theorem minEntry?_nil [Ord α] : minEntry? ([] : List ((a : α) × β a)) = none := by
   simp [minEntry?, List.min?]
 
-private theorem minEntry?_cons [Ord α] [TransOrd α] (e : (a : α) × β a) (l : List ((a : α) × β a)) :
+theorem minEntry?_cons [Ord α] [TransOrd α] (e : (a : α) × β a) (l : List ((a : α) × β a)) :
     minEntry? (e :: l) = some (match minEntry? l with
     | none => e
     | some w => min e w) := by
@@ -5536,7 +5531,7 @@ theorem isSome_minEntry?_of_isEmpty_eq_false [Ord α] {l : List ((a : α) × β
   · simp_all
   · simp [minEntry?, List.min?]
 
-private theorem le_min_iff [Ord α] [TransOrd α] {a b c : (a : α) × β a} :
+theorem le_min_iff [Ord α] [TransOrd α] {a b c : (a : α) × β a} :
     a ≤ min b c ↔ a ≤ b ∧ a ≤ c := by
   simp only [min_def]
   split
@@ -5637,7 +5632,7 @@ theorem isSome_minKey?_iff_isEmpty_eq_false [Ord α] {l : List ((a : α) × β a
     (minKey? l).isSome ↔ l.isEmpty = false := by
   simp [isSome_minKey?_eq_not_isEmpty]
 
-private theorem min_apply [Ord α] {e₁ e₂ : (a : α) × β a} {f : (a : α) × β a → (a : α) × β a}
+theorem min_apply [Ord α] {e₁ e₂ : (a : α) × β a} {f : (a : α) × β a → (a : α) × β a}
     (hf : compare e₁.1 e₂.1 = compare (f e₁).1 (f e₂).1) :
    min (f e₁) (f e₂) = f (min e₁ e₂) := by
   simp only [min_def, hf, apply_ite f]
@@ -6075,7 +6070,7 @@ theorem minKey_of_perm [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l l' :
 theorem minKey_eq_get_minKey? [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
     {l : List ((a : α) × β a)} {he} :
     minKey l he = (minKey? l |>.get (by simp [isSome_minKey?_eq_not_isEmpty, he])) :=
-  (rfl)
+  rfl
 
 theorem minKey?_eq_some_minKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
     {l : List ((a : α) × β a)} {he} :
@@ -6240,7 +6235,7 @@ theorem minKey_alterKey_eq_self [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α
 end Const
 
 /-- Returns the smallest key in an associative list or panics if the list is empty. -/
-@[expose] def minKey! [Ord α] [Inhabited α] (xs : List ((a : α) × β a)) : α :=
+def minKey! [Ord α] [Inhabited α] (xs : List ((a : α) × β a)) : α :=
   minKey? xs |>.get!
 
 theorem minKey!_of_perm [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
@@ -6445,7 +6440,7 @@ theorem minKeyD_of_perm [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
 theorem minKeyD_eq_getD_minKey? [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
     {l : List ((a : α) × β a)} {fallback} :
     minKeyD l fallback = (minKey? l).getD fallback :=
-  (rfl)
+  rfl
 
 theorem minKey_eq_minKeyD [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
     {l : List ((a : α) × β a)} {he fallback} :
@@ -6924,7 +6919,7 @@ theorem maxKey_of_perm [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l l' :
 theorem maxKey_eq_get_maxKey? [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
     {l : List ((a : α) × β a)} {he} :
     maxKey l he = (maxKey? l |>.get (by simp [isSome_maxKey?_eq_not_isEmpty, he])) :=
-  (rfl)
+  rfl
 
 theorem maxKey?_eq_some_maxKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
     {l : List ((a : α) × β a)} {he} :

src/Std/Data/Internal/List/Defs.lean

@@ -3,12 +3,8 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
-module
-
 prelude
-public import Init.BinderPredicates
-
-public section
+import Init.BinderPredicates
 
 /-!
 This is an internal implementation file of the hash map. Users of the hash map should not rely on

src/Std/Data/Iterators/Combinators/Monadic/Drop.lean

@@ -150,19 +150,19 @@ instance Drop.instProductive [Iterator α m β] [Monad m] [Productive α m] :
     Productive (Drop α m β) m :=
   Productive.of_productivenessRelation instProductivenessRelation
 
-instance Drop.instIteratorCollect {n : Type w → Type w'} [Monad m] [Monad n] [Iterator α m β] [Finite α m] :
+instance Drop.instIteratorCollect [Monad m] [Monad n] [Iterator α m β] [Finite α m] :
     IteratorCollect (Drop α m β) m n :=
   .defaultImplementation
 
-instance Drop.instIteratorCollectPartial {n : Type w → Type w'} [Monad m] [Monad n] [Iterator α m β] :
+instance Drop.instIteratorCollectPartial [Monad m] [Monad n] [Iterator α m β] :
     IteratorCollectPartial (Drop α m β) m n :=
   .defaultImplementation
 
-instance Drop.instIteratorLoop {n : Type x → Type x'} [Monad m] [Monad n] [Iterator α m β] :
+instance Drop.instIteratorLoop [Monad m] [Monad n] [Iterator α m β] :
     IteratorLoop (Drop α m β) m n :=
   .defaultImplementation
 
-instance Drop.instIteratorLoopPartial {n : Type x → Type x'} [Monad m] [Monad n] [Iterator α m β] :
+instance Drop.instIteratorLoopPartial [Monad m] [Monad n] [Iterator α m β] :
     IteratorLoopPartial (Drop α m β) m n :=
   .defaultImplementation
 

src/Std/Data/Iterators/Combinators/Monadic/Take.lean

@@ -17,7 +17,7 @@ This module provides the iterator combinator `IterM.take`.
 
 namespace Std.Iterators
 
-variable {α : Type w} {m : Type w → Type w'} {β : Type w}
+variable {α : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {β : Type w}
 
 /--
 The internal state of the `IterM.take` iterator combinator.
@@ -130,15 +130,16 @@ instance Take.instFinite [Monad m] [Iterator α m β] [Productive α m] :
     Finite (Take α m β) m :=
   Finite.of_finitenessRelation instFinitenessRelation
 
-instance Take.instIteratorCollect {n : Type w → Type w'} [Monad m] [Monad n] [Iterator α m β] :
+instance Take.instIteratorCollect [Monad m] [Monad n] [Iterator α m β] :
     IteratorCollect (Take α m β) m n :=
   .defaultImplementation
 
-instance Take.instIteratorCollectPartial {n : Type w → Type w'} [Monad m] [Monad n] [Iterator α m β] :
+instance Take.instIteratorCollectPartial [Monad m] [Monad n] [Iterator α m β] :
     IteratorCollectPartial (Take α m β) m n :=
   .defaultImplementation
 
-instance Take.instIteratorLoop {n : Type x → Type x'} [Monad m] [Monad n] [Iterator α m β] :
+instance Take.instIteratorLoop [Monad m] [Monad n] [Iterator α m β]
+    [MonadLiftT m n] :
     IteratorLoop (Take α m β) m n :=
   .defaultImplementation
 

src/Std/Data/Iterators/Combinators/Monadic/TakeWhile.lean

@@ -31,7 +31,7 @@ Several variants of this combinator are provided:
 
 namespace Std.Iterators
 
-variable {α : Type w} {m : Type w → Type w'} {β : Type w}
+variable {α : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {β : Type w}
 
 /--
 Internal state of the `takeWhile` combinator. Do not depend on its internals.
@@ -233,12 +233,12 @@ instance TakeWhile.instIteratorCollectPartial [Monad m] [Monad n] [Iterator α m
   .defaultImplementation
 
 instance TakeWhile.instIteratorLoop [Monad m] [Monad n] [Iterator α m β]
-    [IteratorLoop α m n] :
+    [IteratorLoop α m n] [MonadLiftT m n] :
     IteratorLoop (TakeWhile α m β P) m n :=
   .defaultImplementation
 
 instance TakeWhile.instIteratorForPartial [Monad m] [Monad n] [Iterator α m β]
-    [IteratorLoopPartial α m n] {P} :
+    [IteratorLoopPartial α m n] [MonadLiftT m n] {P} :
     IteratorLoopPartial (TakeWhile α m β P) m n :=
   .defaultImplementation
 

src/Std/Data/Iterators/Lemmas/Producers/Empty.lean

@@ -39,7 +39,7 @@ theorem Iter.toArray_empty {β} :
 theorem Iter.forIn_empty {m β γ} [Monad m] [LawfulMonad m]
     {init : γ} {f} :
     ForIn.forIn (m := m) (Iter.empty β) init f = pure init := by
-  simp [Iter.forIn_eq_match_step]
+  simp [Iter.forIn_eq_forIn_toIterM]
 
 @[simp]
 theorem Iter.foldM_empty {m β γ} [Monad m] [LawfulMonad m]

src/Std/Data/Iterators/Producers/Monadic/Array.lean

@@ -110,23 +110,19 @@ instance [Pure m] : Finite (ArrayIterator α) m :=
   Finite.of_finitenessRelation ArrayIterator.finitenessRelation
 
 @[always_inline, inline]
-instance {α : Type w} [Monad m] {n : Type w → Type w''} [Monad n] :
-    IteratorCollect (ArrayIterator α) m n :=
+instance {α : Type w} [Monad m] [Monad n] : IteratorCollect (ArrayIterator α) m n :=
   .defaultImplementation
 
 @[always_inline, inline]
-instance {α : Type w} [Monad m] {n : Type w → Type w''} [Monad n] :
-    IteratorCollectPartial (ArrayIterator α) m n :=
+instance {α : Type w} [Monad m] [Monad n] : IteratorCollectPartial (ArrayIterator α) m n :=
   .defaultImplementation
 
 @[always_inline, inline]
-instance {α : Type w} [Monad m] {n : Type x → Type x'} [Monad n] :
-    IteratorLoop (ArrayIterator α) m n :=
+instance {α : Type w} [Monad m] [Monad n] : IteratorLoop (ArrayIterator α) m n :=
   .defaultImplementation
 
 @[always_inline, inline]
-instance {α : Type w} [Monad m] {n : Type x → Type x'} [Monad n] :
-    IteratorLoopPartial (ArrayIterator α) m n :=
+instance {α : Type w} [Monad m] [Monad n] : IteratorLoopPartial (ArrayIterator α) m n :=
   .defaultImplementation
 
 @[always_inline, inline]

src/Std/Data/Iterators/Producers/Monadic/Empty.lean

@@ -62,11 +62,11 @@ instance Empty.instIteratorCollectPartial {n : Type w → Type w''} [Monad m] [M
     IteratorCollectPartial (Empty m β) m n :=
   .defaultImplementation
 
-instance Empty.instIteratorLoop {n : Type x → Type x'} [Monad m] [Monad n] :
+instance Empty.instIteratorLoop {n : Type w → Type w''} [Monad m] [Monad n] :
     IteratorLoop (Empty m β) m n :=
   .defaultImplementation
 
-instance Empty.instIteratorLoopPartial {n : Type x → Type x'} [Monad m] [Monad n] :
+instance Empty.instIteratorLoopPartial {n : Type w → Type w''} [Monad m] [Monad n] :
     IteratorLoopPartial (Empty m β) m n :=
   .defaultImplementation
 

src/Std/Data/Iterators/Producers/Monadic/List.lean

@@ -17,7 +17,7 @@ This module provides an iterator for lists that is accessible via `List.iterM`.
 
 namespace Std.Iterators
 
-variable {α : Type w} {m : Type w → Type w'}
+variable {α : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
 
 /--
 The underlying state of a list iterator. Its contents are internal and should
@@ -59,23 +59,19 @@ instance [Pure m] : Finite (ListIterator α) m :=
   Finite.of_finitenessRelation ListIterator.finitenessRelation
 
 @[always_inline, inline]
-instance {α : Type w} [Monad m] {n : Type w → Type w''} [Monad n] :
-    IteratorCollect (ListIterator α) m n :=
+instance {α : Type w} [Monad m] [Monad n] : IteratorCollect (ListIterator α) m n :=
   .defaultImplementation
 
 @[always_inline, inline]
-instance {α : Type w} [Monad m] {n : Type w → Type w''} [Monad n] :
-    IteratorCollectPartial (ListIterator α) m n :=
+instance {α : Type w} [Monad m] [Monad n] : IteratorCollectPartial (ListIterator α) m n :=
   .defaultImplementation
 
 @[always_inline, inline]
-instance {α : Type w} [Monad m] {n : Type x → Type x'} [Monad n] :
-    IteratorLoop (ListIterator α) m n :=
+instance {α : Type w} [Monad m] [Monad n] : IteratorLoop (ListIterator α) m n :=
   .defaultImplementation
 
 @[always_inline, inline]
-instance {α : Type w} [Monad m] {n : Type x → Type x'} [Monad n] :
-    IteratorLoopPartial (ListIterator α) m n :=
+instance {α : Type w} [Monad m] [Monad n] : IteratorLoopPartial (ListIterator α) m n :=
   .defaultImplementation
 
 @[always_inline, inline]

src/Std/Internal/Parsec/Basic.lean

@@ -1,24 +1,47 @@
 /-
 Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Author: Dany Fabian, Henrik Böving
+Author: Dany Fabian, Henrik Böving, Sofia Rodrigues
 -/
+module
+
 prelude
-import Init.NotationExtra
-import Init.Data.ToString.Macro
+public import Init.NotationExtra
+public import Init.Data.ToString.Macro
 
-namespace Std.Internal
+public section
 
+namespace Std
+namespace Internal
 namespace Parsec
 
+/--
+Error type for the `ParseResult`. It separates `eof` from the rest of the errors in order to
+improve the error handling for this case in parsers that can receive incomplete data and then reparse it.
+-/
+inductive Error where
+  | eof
+  | other (s : String)
+  deriving Repr
+
+instance : ToString Error where
+  toString
+    | .eof => "unexpected end of input"
+    | .other s => s
+
+/--
+The result of parsing some string.
+-/
 inductive ParseResult (α : Type) (ι : Type) where
   | success (pos : ι) (res : α)
-  | error (pos : ι) (err : String)
+  | error (pos : ι) (err : Error)
   deriving Repr
 
 end Parsec
 
-def Parsec (ι : Type) (α : Type) : Type := ι → Parsec.ParseResult α ι
+@[expose]
+def Parsec (ι : Type) (α : Type) : Type :=
+  ι → Parsec.ParseResult α ι
 
 namespace Parsec
 
@@ -34,26 +57,21 @@ variable {α : Type} {ι : Type} {elem : Type} {idx : Type}
 variable [DecidableEq idx] [DecidableEq elem] [Input ι elem idx]
 
 instance : Inhabited (Parsec ι α) where
-  default := fun it => .error it ""
+  default := fun it => ParseResult.error it (.other "")
 
 @[always_inline, inline]
 protected def pure (a : α) : Parsec ι α := fun it =>
   .success it a
 
 @[always_inline, inline]
-def bind {α β : Type} (f : Parsec ι α) (g : α → Parsec ι β) : Parsec ι β := fun it =>
+protected def bind {α β : Type} (f : Parsec ι α) (g : α → Parsec ι β) : Parsec ι β := fun it =>
   match f it with
   | .success rem a => g a rem
   | .error pos msg => .error pos msg
 
-@[always_inline]
-instance : Monad (Parsec ι) where
-  pure := Parsec.pure
-  bind := Parsec.bind
-
 @[always_inline, inline]
 def fail (msg : String) : Parsec ι α := fun it =>
-  .error it msg
+  .error it (.other msg)
 
 @[inline]
 def tryCatch (p : Parsec ι α) (csuccess : α → Parsec ι β) (cerror : Unit → Parsec ι β)
@@ -64,6 +82,11 @@ def tryCatch (p : Parsec ι α) (csuccess : α → Parsec ι β) (cerror : Unit
     -- We assume that it.s never changes as the `Parsec` monad only modifies `it.pos`.
     if Input.pos it = Input.pos rem then cerror () rem else .error rem err
 
+@[always_inline]
+instance : Monad (Parsec ι) where
+  pure := Parsec.pure
+  bind := Parsec.bind
+
 @[always_inline, inline]
 def orElse (p : Parsec ι α) (q : Unit → Parsec ι α) : Parsec ι α :=
   tryCatch p pure q
@@ -79,12 +102,10 @@ instance : Alternative (Parsec ι) where
   failure := fail ""
   orElse := orElse
 
-def expectedEndOfInput := "expected end of input"
-
 @[inline]
 def eof : Parsec ι Unit := fun it =>
   if Input.hasNext it then
-    .error it expectedEndOfInput
+    .error it .eof
   else
     .success it ()
 
@@ -102,8 +123,9 @@ def many (p : Parsec ι α) : Parsec ι <| Array α := manyCore p #[]
 @[inline]
 def many1 (p : Parsec ι α) : Parsec ι <| Array α := do manyCore p #[← p]
 
-def unexpectedEndOfInput := "unexpected end of input"
-
+/--
+Gets the next input element.
+-/
 @[inline]
 def any : Parsec ι elem := fun it =>
   if h : Input.hasNext it then
@@ -111,19 +133,28 @@ def any : Parsec ι elem := fun it =>
     let it' := Input.next' it h
     .success it' c
   else
-    .error it unexpectedEndOfInput
+    .error it .eof
 
+/--
+Checks if the next input element matches some condition.
+-/
 @[inline]
 def satisfy (p : elem → Bool) : Parsec ι elem := attempt do
   let c ← any
   if p c then return c else fail "condition not satisfied"
 
+/--
+Fails if `p` succeeds, otherwise succeeds without consuming input.
+-/
 @[inline]
 def notFollowedBy (p : Parsec ι α) : Parsec ι Unit := fun it =>
   match p it with
-  | .success _ _ => .error it ""
+  | .success _ _ => .error it (.other "")
   | .error _ _ => .success it ()
 
+/--
+Peeks at the next element, returns `some` if exists else `none`, does not consume input.
+-/
 @[inline]
 def peek? : Parsec ι (Option elem) := fun it =>
   if h : Input.hasNext it then
@@ -131,13 +162,32 @@ def peek? : Parsec ι (Option elem) := fun it =>
   else
     .success it none
 
+/--
+Peeks at the next element, returns `some elem` if it satisfies `p`, else `none`. Does not consume input.
+-/
+@[inline]
+def peekWhen? (p : elem → Bool) : Parsec ι (Option elem) := do
+  let some data ← peek?
+    | return none
+
+  if p data then
+    return some data
+  else
+    return none
+
+/--
+Peeks at the next element, errors on EOF, does not consume input.
+-/
 @[inline]
 def peek! : Parsec ι elem := fun it =>
   if h : Input.hasNext it then
     .success it (Input.curr' it h)
   else
-    .error it unexpectedEndOfInput
+    .error it .eof
 
+/--
+Peeks at the next element or returns a default if at EOF, does not consume input.
+-/
 @[inline]
 def peekD (default : elem) : Parsec ι elem := fun it =>
   if h : Input.hasNext it then
@@ -145,23 +195,37 @@ def peekD (default : elem) : Parsec ι elem := fun it =>
   else
     .success it default
 
+/--
+Consumes one element if available, otherwise errors on EOF.
+-/
 @[inline]
 def skip : Parsec ι Unit := fun it =>
   if h : Input.hasNext it then
     .success (Input.next' it h) ()
   else
-    .error it unexpectedEndOfInput
+    .error it .eof
 
+/--
+Parses zero or more chars with `p`, accumulates into a string.
+-/
 @[specialize]
 partial def manyCharsCore (p : Parsec ι Char) (acc : String) : Parsec ι String :=
   tryCatch p (manyCharsCore p <| acc.push ·) (fun _ => pure acc)
 
+/--
+Parses zero or more chars with `p` into a string.
+-/
 @[inline]
-def manyChars (p : Parsec ι Char) : Parsec ι String := manyCharsCore p ""
+def manyChars (p : Parsec ι Char) : Parsec ι String := do
+  manyCharsCore p ""
 
+/--
+Parses one or more chars with `p` into a string, errors if none.
+-/
 @[inline]
-def many1Chars (p : Parsec ι Char) : Parsec ι String := do manyCharsCore p (← p).toString
+def many1Chars (p : Parsec ι Char) : Parsec ι String := do
+  manyCharsCore p (← p).toString
 
 end Parsec
-
-end Std.Internal
+end Internal
+end Std

src/Std/Internal/Parsec/ByteArray.lean

@@ -3,12 +3,17 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
-prelude
-import Std.Internal.Parsec.Basic
-import Init.Data.ByteArray.Basic
-import Init.Data.String.Extra
+module
 
-namespace Std.Internal
+prelude
+public import Std.Internal.Parsec.Basic
+public import Init.Data.ByteArray.Basic
+public import Init.Data.String.Extra
+
+public section
+
+namespace Std
+namespace Internal
 namespace Parsec
 namespace ByteArray
 
@@ -22,27 +27,47 @@ instance : Input ByteArray.Iterator UInt8 Nat where
 
 abbrev Parser (α : Type) : Type := Parsec ByteArray.Iterator α
 
+/--
+Run a `Parser` on a `ByteArray`, returns either the result or an error string with offset.
+-/
 protected def Parser.run (p : Parser α) (arr : ByteArray) : Except String α :=
   match p arr.iter with
   | .success _ res => Except.ok res
-  | .error it err  => Except.error s!"offset {repr it.pos}: {err}"
+  | .error it (.other err)  => Except.error s!"offset {repr it.pos}: {err}"
+  | .error it .eof  => Except.error s!"offset {repr it.pos}: end of file"
 
+/--
+Parse a single byte equal to `b`, fails if different.
+-/
 @[inline]
 def pbyte (b : UInt8) : Parser UInt8 := attempt do
   if (← any) = b then pure b else fail s!"expected: '{b}'"
 
+/--
+Skip a single byte equal to `b`, fails if different.
+-/
 @[inline]
-def skipByte (b : UInt8) : Parser Unit := pbyte b *> pure ()
+def skipByte (b : UInt8) : Parser Unit :=
+  pbyte b *> pure ()
 
+/--
+Skip a sequence of bytes equal to the given `ByteArray`.
+-/
 def skipBytes (arr : ByteArray) : Parser Unit := do
   for b in arr do
     skipByte b
 
+/--
+Parse a string by matching its UTF-8 bytes, returns the string on success.
+-/
 @[inline]
 def pstring (s : String) : Parser String := do
   skipBytes s.toUTF8
   return s
 
+/--
+Skip a string by matching its UTF-8 bytes.
+-/
 @[inline]
 def skipString (s : String) : Parser Unit := pstring s *> pure ()
 
@@ -59,14 +84,24 @@ Skip a `Char` that can be represented in 1 byte. If `c` uses more than 1 byte it
 @[inline]
 def skipByteChar (c : Char) : Parser Unit := skipByte c.toUInt8
 
+/--
+Parse an ASCII digit `0-9` as a `Char`.
+-/
 @[inline]
 def digit : Parser Char := attempt do
   let b ← any
   if '0'.toUInt8 ≤ b ∧ b ≤ '9'.toUInt8 then return Char.ofUInt8 b else fail s!"digit expected"
 
+/--
+Convert a byte representing `'0'..'9'` to a `Nat`.
+-/
 @[inline]
-private def digitToNat (b : UInt8) : Nat := (b - '0'.toUInt8).toNat
+private def digitToNat (b : UInt8) : Nat :=
+  (b - '0'.toUInt8).toNat
 
+/--
+Parse zero or more ASCII digits into a `Nat`, continuing until non-digit or EOF.
+-/
 @[inline]
 private partial def digitsCore (acc : Nat) : Parser Nat := fun it =>
   /-
@@ -88,11 +123,17 @@ where
     else
       (acc, it)
 
+/--
+Parse one or more ASCII digits into a `Nat`.
+-/
 @[inline]
 def digits : Parser Nat := do
   let d ← digit
   digitsCore (digitToNat d.toUInt8)
 
+/--
+Parse a hex digit `0-9`, `a-f`, or `A-F` as a `Char`.
+-/
 @[inline]
 def hexDigit : Parser Char := attempt do
   let b ← any
@@ -100,6 +141,20 @@ def hexDigit : Parser Char := attempt do
    ∨ ('a'.toUInt8 ≤ b ∧ b ≤ 'f'.toUInt8)
    ∨ ('A'.toUInt8 ≤ b ∧ b ≤ 'F'.toUInt8) then return Char.ofUInt8 b else fail s!"hex digit expected"
 
+/--
+Parse an octal digit `0-7` as a `Char`.
+-/
+@[inline]
+def octDigit : Parser Char := attempt do
+  let b ← any
+  if '0'.toUInt8 ≤ b ∧ b ≤ '7'.toUInt8 then
+    return Char.ofUInt8 b
+  else
+    fail s!"octal digit expected"
+
+/--
+Parse an ASCII letter `a-z` or `A-Z` as a `Char`.
+-/
 @[inline]
 def asciiLetter : Parser Char := attempt do
   let b ← any
@@ -118,17 +173,65 @@ private partial def skipWs (it : ByteArray.Iterator) : ByteArray.Iterator :=
   else
    it
 
+/--
+Skip whitespace: tabs, newlines, carriage returns, and spaces.
+-/
 @[inline]
 def ws : Parser Unit := fun it =>
   .success (skipWs it) ()
 
+/--
+Parse `n` bytes from the input into a `ByteArray`, errors if not enough bytes.
+-/
 def take (n : Nat) : Parser ByteArray := fun it =>
   let subarr := it.array.extract it.idx (it.idx + n)
   if subarr.size != n then
-    .error it s!"expected: {n} bytes"
+    .error it .eof
   else
     .success (it.forward n) subarr
 
+/--
+Parses while a predicate is satisfied.
+-/
+@[inline]
+partial def takeWhile (pred : UInt8 → Bool) : Parser ByteArray :=
+  fun it =>
+    let rec findEnd (count : Nat) (iter : ByteArray.Iterator) : (Nat × ByteArray.Iterator) :=
+      if ¬iter.hasNext then (count, iter)
+      else if pred iter.curr then findEnd (count + 1) iter.next
+      else (count, iter)
+
+    let (length, newIt) := findEnd 0 it
+    .success newIt (it.array.extract it.idx (it.idx + length))
+
+/--
+Parses until a predicate is satisfied (exclusive).
+-/
+@[inline]
+def takeUntil (pred : UInt8 → Bool) : Parser ByteArray :=
+  takeWhile (fun b => ¬pred b)
+
+/--
+Skips while a predicate is satisfied.
+-/
+@[inline]
+partial def skipWhile (pred : UInt8 → Bool) : Parser Unit :=
+  fun it =>
+    let rec findEnd (count : Nat) (iter : ByteArray.Iterator) : ByteArray.Iterator :=
+      if ¬iter.hasNext then iter
+      else if pred iter.curr then findEnd (count + 1) iter.next
+      else iter
+
+    .success (findEnd 0 it) ()
+
+/--
+Skips until a predicate is satisfied.
+-/
+@[inline]
+def skipUntil (pred : UInt8 → Bool) : Parser Unit :=
+  skipWhile (fun b => ¬pred b)
+
 end ByteArray
 end Parsec
-end Std.Internal
+end Internal
+end Std

src/Std/Internal/Parsec/String.lean

@@ -3,8 +3,12 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Dany Fabian, Henrik Böving
 -/
+module
+
 prelude
-import Std.Internal.Parsec.Basic
+public import Std.Internal.Parsec.Basic
+
+public section
 
 namespace Std.Internal
 namespace Parsec
@@ -20,34 +24,55 @@ instance : Input String.Iterator Char String.Pos where
 
 abbrev Parser (α : Type) : Type := Parsec String.Iterator α
 
+/--
+Run a `Parser` on a `String`, returns either the result or an error string with offset.
+-/
 protected def Parser.run (p : Parser α) (s : String) : Except String α :=
   match p s.mkIterator with
   | .success _ res => Except.ok res
-  | .error it err  => Except.error s!"offset {repr it.i.byteIdx}: {err}"
+  | .error it (.other err)  => Except.error s!"offset {repr it.pos}: {err}"
+  | .error it .eof  => Except.error s!"offset {repr it.pos}: end of file"
 
-/-- Parses the given string. -/
+/--
+Parses the given string.
+-/
 def pstring (s : String) : Parser String := fun it =>
   let substr := it.extract (it.forward s.length)
   if substr = s then
     .success (it.forward s.length) substr
   else
-    .error it s!"expected: {s}"
+    .error it (.other s!"expected: {s}")
 
+/--
+Skips the given string.
+-/
 @[inline]
 def skipString (s : String) : Parser Unit := pstring s *> pure ()
 
+/--
+Parses the given char.
+-/
 @[inline]
 def pchar (c : Char) : Parser Char := attempt do
   if (← any) = c then pure c else fail s!"expected: '{c}'"
 
+/--
+Skips the given char.
+-/
 @[inline]
 def skipChar (c : Char) : Parser Unit := pchar c *> pure ()
 
+/--
+Parse an ASCII digit `0-9` as a `Char`.
+-/
 @[inline]
 def digit : Parser Char := attempt do
   let c ← any
   if '0' ≤ c ∧ c ≤ '9' then return c else fail s!"digit expected"
 
+/--
+Convert a byte representing `'0'..'9'` to a `Nat`.
+-/
 @[inline]
 private def digitToNat (b : Char) : Nat := b.toNat - '0'.toNat
 
@@ -72,11 +97,17 @@ where
     else
       (acc, it)
 
+/--
+Parse one or more ASCII digits into a `Nat`.
+-/
 @[inline]
 def digits : Parser Nat := do
   let d ← digit
   digitsCore (digitToNat d)
 
+/--
+Parse a hex digit `0-9`, `a-f`, or `A-F` as a `Char`.
+-/
 @[inline]
 def hexDigit : Parser Char := attempt do
   let c ← any
@@ -84,6 +115,9 @@ def hexDigit : Parser Char := attempt do
    ∨ ('a' ≤ c ∧ c ≤ 'f')
    ∨ ('A' ≤ c ∧ c ≤ 'F') then return c else fail s!"hex digit expected"
 
+/--
+Parse an ASCII letter `a-z` or `A-Z` as a `Char`.
+-/
 @[inline]
 def asciiLetter : Parser Char := attempt do
   let c ← any
@@ -99,14 +133,18 @@ private partial def skipWs (it : String.Iterator) : String.Iterator :=
   else
    it
 
+/--
+Skip whitespace: tabs, newlines, carriage returns, and spaces.
+-/
 @[inline]
 def ws : Parser Unit := fun it =>
   .success (skipWs it) ()
 
+
 def take (n : Nat) : Parser String := fun it =>
   let substr := it.extract (it.forward n)
   if substr.length != n then
-    .error it s!"expected: {n} codepoints"
+    .error it .eof
   else
     .success (it.forward n) substr
 

src/Std/Tactic/BVDecide/Normalize/Bool.lean

@@ -42,7 +42,7 @@ theorem if_eq_cond {b : Bool} {x y : α} : (if b = true then x else y) = (bif b
   rw [cond_eq_if]
 
 @[bv_normalize]
-theorem Bool.not_xor : ∀ (a b : Bool), (!(a ^^ b)) = (a == b) := by decide
+theorem Bool.not_xor : ∀ (a b : Bool), !(a ^^ b) = (a == b) := by decide
 
 @[bv_normalize]
 theorem Bool.not_beq_one : ∀ (a : BitVec 1), (!(a == 1#1)) = (a == 0#1) := by