fix: comment

This PR fixes the `grind` support for `Nat.ctorIdx`. Nat constructors
appear in `grind` as offsets or literals, and not as a node marked
`.constr`, so handle that case as well.

.github/workflows/check-stdlib-flags.yml

@@ -0,0 +1,57 @@
+name: Check stdlib_flags.h modifications
+
+on:
+  pull_request:
+    types: [opened, synchronize, reopened, labeled, unlabeled]
+
+jobs:
+  check-stdlib-flags:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Check if stdlib_flags.h was modified
+        uses: actions/github-script@v8
+        with:
+          script: |
+            // Get the list of files changed in this PR
+            const files = await github.paginate(
+              github.rest.pulls.listFiles,
+              {
+                owner: context.repo.owner,
+                repo: context.repo.repo,
+                pull_number: context.payload.pull_request.number,
+              }
+            );
+
+            // Check if stdlib_flags.h was modified
+            const stdlibFlagsModified = files.some(file =>
+              file.filename === 'src/stdlib_flags.h'
+            );
+
+            if (stdlibFlagsModified) {
+              console.log('src/stdlib_flags.h was modified in this PR');
+
+              // Check if the unlock label is present
+
+              const { data: pr } = await github.rest.pulls.get({
+                owner: context.repo.owner,
+                repo: context.repo.repo,
+                pull_number: context.issue.number,
+              });
+
+              const hasUnlockLabel = pr.labels.some(label =>
+                label.name === 'unlock-upstream-stdlib-flags'
+              );
+
+              if (!hasUnlockLabel) {
+                core.setFailed(
+                  'src/stdlib_flags.h was modified. This is likely a mistake. If you would like to change ' +
+                  'bootstrapping settings or request a stage0 update, you should modify stage0/src/stdlib_flags.h. ' +
+                  'If you really want to change src/stdlib_flags.h (which should be extremely rare), set the ' +
+                  'unlock-upstream-stdlib-flags label.'
+                );
+              } else {
+                console.log('Found unlock-upstream-stdlib-flags');
+              }
+            } else {
+              console.log('src/stdlib_flags.h was not modified');
+            }

.github/workflows/ci.yml

@@ -267,12 +267,14 @@ jobs:
                 "test": true,
                 // turn off custom allocator & symbolic functions to make LSAN do its magic
                 "CMAKE_PRESET": "sanitize",
-                // `StackOverflow*` correctly triggers ubsan
-                // `reverse-ffi` fails to link in sanitizers
+                // `StackOverflow*` correctly triggers ubsan.
+                // `reverse-ffi` fails to link in sanitizers.
                 // `interactive` and `async_select_channel` fail nondeterministically, would need to
-                // be investigated.
-                // 9366 is too close to timeout
-                "CTEST_OPTIONS": "-E 'StackOverflow|reverse-ffi|interactive|async_select_channel|9366'"
+                // be investigated..
+                // 9366 is too close to timeout.
+                // `bv_` sometimes times out calling into cadical even though we should be using the
+                // standard compile flags for it.
+                "CTEST_OPTIONS": "-E 'StackOverflow|reverse-ffi|interactive|async_select_channel|9366|run/bv_'"
               },
               {
                 "name": "macOS",

src/CMakeLists.txt

@@ -10,7 +10,7 @@ endif()
 include(ExternalProject)
 project(LEAN CXX C)
 set(LEAN_VERSION_MAJOR 4)
-set(LEAN_VERSION_MINOR 27)
+set(LEAN_VERSION_MINOR 28)
 set(LEAN_VERSION_PATCH 0)
 set(LEAN_VERSION_IS_RELEASE 0)  # This number is 1 in the release revision, and 0 otherwise.
 set(LEAN_SPECIAL_VERSION_DESC "" CACHE STRING "Additional version description like 'nightly-2018-03-11'")

src/Init/Data/Iterators/Basic.lean

@@ -77,8 +77,6 @@ public theorem Shrink.deflate_inj {α} {x y : α} :
   · rintro rfl
     rfl
 
-namespace Iterators
-
 -- It is not fruitful to move the following docstrings to verso right now because there are lots of
 -- forward references that cannot be realized nicely.
 set_option doc.verso false
@@ -124,6 +122,7 @@ def x := ([1, 2, 3].iterM IO : IterM IO Nat)
 -/
 @[ext]
 structure IterM {α : Type w} (m : Type w → Type w') (β : Type w) where
+  mk' ::
   /-- Internal implementation detail of the iterator. -/
   internalState : α
 
@@ -358,21 +357,27 @@ class Iterator (α : Type w) (m : Type w → Type w') (β : outParam (Type w)) w
 section Monadic
 
 /--
-Converts wraps the state of an iterator into an `IterM` object.
+Wraps the state of an iterator into an `IterM` object.
 -/
 @[always_inline, inline, expose]
-def toIterM {α : Type w} (it : α) (m : Type w → Type w') (β : Type w) :
+def IterM.mk {α : Type w} (it : α) (m : Type w → Type w') (β : Type w) :
     IterM (α := α) m β :=
   ⟨it⟩
 
+@[deprecated IterM.mk (since := "2025-12-01"), inline, expose]
+def Iterators.toIterM := @IterM.mk
+
 @[simp]
-theorem toIterM_internalState {α m β} (it : IterM (α := α) m β) :
-    toIterM it.internalState m β = it :=
+theorem IterM.mk_internalState {α m β} (it : IterM (α := α) m β) :
+    .mk it.internalState m β = it :=
   rfl
 
+@[deprecated IterM.mk_internalState (since := "2025-12-01")]
+def Iterators.toIterM_internalState := @IterM.mk_internalState
+
 @[simp]
 theorem internalState_toIterM {α m β} (it : α) :
-    (toIterM it m β).internalState = it :=
+    (IterM.mk it m β).internalState = it :=
   rfl
 
 /--
@@ -677,11 +682,11 @@ this means that the relation of plausible successors is well-founded.
 Given this typeclass, termination proofs for well-founded recursion over an iterator `it` can use
 `it.finitelyManySteps` as a termination measure.
 -/
-class Finite (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] : Prop where
+class Iterators.Finite (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] : Prop where
   /-- The relation of plausible successors is well-founded. -/
   wf : WellFounded (IterM.IsPlausibleSuccessorOf (α := α) (m := m))
 
-theorem Finite.wf_of_id {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] :
+theorem Iterators.Finite.wf_of_id {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] :
     WellFounded (Iter.IsPlausibleSuccessorOf (α := α)) := by
   simpa [Iter.isPlausibleSuccessorOf_eq_invImage] using InvImage.wf _ Finite.wf
 
@@ -703,10 +708,11 @@ def IterM.TerminationMeasures.Finite.Rel
     TerminationMeasures.Finite α m → TerminationMeasures.Finite α m → Prop :=
   Relation.TransGen <| InvImage IterM.IsPlausibleSuccessorOf IterM.TerminationMeasures.Finite.it
 
-instance {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
-    [Finite α m] : WellFoundedRelation (IterM.TerminationMeasures.Finite α m) where
+instance IterM.TerminationMeasures.instWellFoundedRelationFinite {α : Type w} {m : Type w → Type w'}
+    {β : Type w} [Iterator α m β] [Iterators.Finite α m] :
+    WellFoundedRelation (IterM.TerminationMeasures.Finite α m) where
   rel := IterM.TerminationMeasures.Finite.Rel
-  wf := by exact (InvImage.wf _ Finite.wf).transGen
+  wf := by exact (InvImage.wf _ Iterators.Finite.wf).transGen
 
 /--
 Termination measure to be used in well-founded recursive functions recursing over a finite iterator
@@ -714,7 +720,7 @@ Termination measure to be used in well-founded recursive functions recursing ove
 -/
 @[expose]
 def IterM.finitelyManySteps {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
-    [Finite α m] (it : IterM (α := α) m β) : IterM.TerminationMeasures.Finite α m :=
+    [Iterators.Finite α m] (it : IterM (α := α) m β) : IterM.TerminationMeasures.Finite α m :=
   ⟨it⟩
 
 /--
@@ -756,7 +762,7 @@ macro_rules | `(tactic| decreasing_trivial) => `(tactic|
   | fail)
 
 @[inherit_doc IterM.finitelyManySteps, expose]
-def Iter.finitelyManySteps {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id]
+def Iter.finitelyManySteps {α : Type w} {β : Type w} [Iterator α Id β] [Iterators.Finite α Id]
     (it : Iter (α := α) β) : IterM.TerminationMeasures.Finite α Id :=
   it.toIterM.finitelyManySteps
 
@@ -806,7 +812,7 @@ well-founded.
 Given this typeclass, termination proofs for well-founded recursion over an iterator `it` can use
 `it.finitelyManySkips` as a termination measure.
 -/
-class Productive (α m) {β} [Iterator α m β] : Prop where
+class Iterators.Productive (α m) {β} [Iterator α m β] : Prop where
   /-- The relation of plausible successors during skips is well-founded. -/
   wf : WellFounded (IterM.IsPlausibleSkipSuccessorOf (α := α) (m := m))
 
@@ -846,10 +852,11 @@ theorem IterM.TerminationMeasures.Finite.Rel.of_productive
     refine .trans ih ?_
     exact .single ⟨_, rfl, hab⟩
 
-instance {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
-    [Productive α m] : WellFoundedRelation (IterM.TerminationMeasures.Productive α m) where
+instance IterM.TerminationMeasures.instWellFoundedRelationProductive {α : Type w}
+    {m : Type w → Type w'} {β : Type w} [Iterator α m β] [Iterators.Productive α m] :
+    WellFoundedRelation (IterM.TerminationMeasures.Productive α m) where
   rel := IterM.TerminationMeasures.Productive.Rel
-  wf := by exact (InvImage.wf _ Productive.wf).transGen
+  wf := by exact (InvImage.wf _ Iterators.Productive.wf).transGen
 
 /--
 Termination measure to be used in well-founded recursive functions recursing over a productive
@@ -857,7 +864,7 @@ iterator (see also `Productive`).
 -/
 @[expose]
 def IterM.finitelyManySkips {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
-    [Productive α m] (it : IterM (α := α) m β) : IterM.TerminationMeasures.Productive α m :=
+    [Iterators.Productive α m] (it : IterM (α := α) m β) : IterM.TerminationMeasures.Productive α m :=
   ⟨it⟩
 
 /--
@@ -876,7 +883,7 @@ macro_rules | `(tactic| decreasing_trivial) => `(tactic|
     | fail)
 
 @[inherit_doc IterM.finitelyManySkips, expose]
-def Iter.finitelyManySkips {α : Type w} {β : Type w} [Iterator α Id β] [Productive α Id]
+def Iter.finitelyManySkips {α : Type w} {β : Type w} [Iterator α Id β] [Iterators.Productive α Id]
     (it : Iter (α := α) β) : IterM.TerminationMeasures.Productive α Id :=
   it.toIterM.finitelyManySkips
 
@@ -895,12 +902,13 @@ macro_rules | `(tactic| decreasing_trivial) => `(tactic|
     | exact Iter.TerminationMeasures.Productive.rel_of_skip ‹_›
     | fail)
 
-instance [Iterator α m β] [Finite α m] : Productive α m where
+instance Iterators.instProductiveOfFinte [Iterator α m β] [Iterators.Finite α m] :
+    Iterators.Productive α m where
   wf := by
     apply Subrelation.wf (r := IterM.IsPlausibleSuccessorOf)
     · intro it' it h
       exact IterM.isPlausibleSuccessorOf_of_skip h
-    · exact Finite.wf
+    · exact Iterators.Finite.wf
 
 end Productive
 
@@ -919,8 +927,4 @@ class LawfulDeterministicIterator (α : Type w) (m : Type w → Type w') [Iterat
     where
   isPlausibleStep_eq_eq : ∀ it : IterM (α := α) m β, ∃ step, it.IsPlausibleStep = (· = step)
 
-end Iterators
-
-export Iterators (Iter IterM)
-
 end Std

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

@@ -11,7 +11,8 @@ public import Init.Data.Iterators.Combinators.FilterMap
 
 public section
 
-namespace Std.Iterators
+namespace Std
+open Std.Iterators
 
 @[always_inline, inline, expose, inherit_doc IterM.attachWith]
 def Iter.attachWith {α β : Type w}
@@ -24,4 +25,4 @@ where finally
     simp only [← isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM]
     exact h
 
-end Std.Iterators
+end Std

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

@@ -30,7 +30,8 @@ Several variants of these combinators are provided:
   iterator, and particularly for specialized termination proofs. If possible, avoid this.
 -/
 
-namespace Std.Iterators
+namespace Std
+open Std.Iterators
 
 -- We cannot use `inherit_doc` because the docstring for `IterM` states that a `MonadLiftT` instance
 -- is needed.
@@ -305,4 +306,4 @@ def Iter.map {α : Type w} {β : Type w} {γ : Type w} [Iterator α Id β]
     (f : β → γ) (it : Iter (α := α) β) :=
   ((it.toIterM.map f).toIter : Iter γ)
 
-end Std.Iterators
+end Std

src/Init/Data/Iterators/Combinators/FlatMap.lean

@@ -24,7 +24,7 @@ and so on. In other words, {lit}`it` flattens the iterator of iterators obtained
 {lit}`f`.
 -/
 
-namespace Std.Iterators
+namespace Std
 
 @[always_inline, inherit_doc IterM.flatMapAfterM]
 public def Iter.flatMapAfterM {α : Type w} {β : Type w} {α₂ : Type w}
@@ -49,5 +49,3 @@ public def Iter.flatMap {α : Type w} {β : Type w} {α₂ : Type w}
     {γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ]
     (f : β → Iter (α := α₂) γ) (it : Iter (α := α) β) :=
   (it.flatMapAfter f none : Iter γ)
-
-end Std.Iterators

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

@@ -96,7 +96,7 @@ instance Attach.instIteratorLoop {α β : Type w} {m : Type w → Type w'} [Mona
     IteratorLoop (Attach α m P) m n :=
   .defaultImplementation
 
-end Types
+end Iterators.Types
 
 /--
 “Attaches” individual proofs to an iterator of values that satisfy a predicate `P`, returning an
@@ -111,7 +111,7 @@ iterator with values in the corresponding subtype `{ x // P x }`.
 def IterM.attachWith {α β : Type w} {m : Type w → Type w'} [Monad m]
     [Iterator α m β] (it : IterM (α := α) m β) (P : β → Prop)
     (h : ∀ out, it.IsPlausibleIndirectOutput out → P out) :
-    IterM (α := Types.Attach α m P) m { out : β // P out } :=
+    IterM (α := Iterators.Types.Attach α m P) m { out : β // P out } :=
   ⟨⟨it, h⟩⟩
 
-end Std.Iterators
+end Std

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

@@ -32,7 +32,9 @@ Several variants of these combinators are provided:
   iterator, and particularly for specialized termination proofs. If possible, avoid this.
 -/
 
-namespace Std.Iterators
+namespace Std
+
+namespace Iterators.Types
 
 /--
 Internal state of the `filterMap` combinator. Do not depend on its internals.
@@ -53,19 +55,23 @@ def Map (α : Type w) {β γ : Type w} (m : Type w → Type w') (n : Type w →
     (f : β → PostconditionT n γ) :=
   FilterMap α m n lift (fun b => PostconditionT.map some (f b))
 
+end Iterators.Types
+
+open Std.Iterators Std.Iterators.Types
+
 @[always_inline, inline, expose]
 def IterM.InternalCombinators.filterMap {α β γ : Type w} {m : Type w → Type w'}
     {n : Type w → Type w''} (lift : ⦃α : Type w⦄ → m α → n α)
     [Iterator α m β] (f : β → PostconditionT n (Option γ))
     (it : IterM (α := α) m β) : IterM (α := FilterMap α m n lift f) n γ :=
-  toIterM ⟨it⟩ n γ
+  .mk ⟨it⟩ n γ
 
 @[always_inline, inline, expose]
 def IterM.InternalCombinators.map {α β γ : Type w} {m : Type w → Type w'}
     {n : Type w → Type w''} [Monad n] (lift : ⦃α : Type w⦄ → m α → n α)
     [Iterator α m β] (f : β → PostconditionT n γ)
     (it : IterM (α := α) m β) : IterM (α := Map α m n lift f) n γ :=
-  toIterM ⟨it⟩ n γ
+  .mk ⟨it⟩ n γ
 
 /--
 *Note: This is a very general combinator that requires an advanced understanding of monads,
@@ -119,14 +125,16 @@ def IterM.filterMapWithPostcondition {α β γ : Type w} {m : Type w → Type w'
     (it : IterM (α := α) m β) : IterM (α := FilterMap α m n (fun ⦃_⦄ => monadLift) f) n γ :=
   IterM.InternalCombinators.filterMap (fun ⦃_⦄ => monadLift) f it
 
+namespace Iterators.Types
+
 /--
 `it.PlausibleStep step` is the proposition that `step` is a possible next step from the
 `filterMap` iterator `it`. This is mostly internally relevant, except if one needs to manually
 prove termination (`Finite` or `Productive` instances, for example) of a `filterMap` iterator.
 -/
-inductive FilterMap.PlausibleStep {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
-    {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n (Option γ)} [Iterator α m β]
-    (it : IterM (α := FilterMap α m n lift f) n γ) :
+inductive FilterMap.PlausibleStep {α β γ : Type w} {m : Type w → Type w'}
+    {n : Type w → Type w''} {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n (Option γ)}
+    [Iterator α m β] (it : IterM (α := FilterMap α m n lift f) n γ) :
     IterStep (IterM (α := FilterMap α m n lift f) n γ) γ → Prop where
   | yieldNone : ∀ {it' out},
       it.internalState.inner.IsPlausibleStep (.yield it' out) →
@@ -139,8 +147,8 @@ inductive FilterMap.PlausibleStep {α β γ : Type w} {m : Type w → Type w'} {
       PlausibleStep it (.skip (IterM.InternalCombinators.filterMap lift f it'))
   | done : it.internalState.inner.IsPlausibleStep .done → PlausibleStep it .done
 
-instance FilterMap.instIterator {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
-    {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n (Option γ)}
+instance FilterMap.instIterator {α β γ : Type w} {m : Type w → Type w'}
+    {n : Type w → Type w''} {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n (Option γ)}
     [Iterator α m β] [Monad n] :
     Iterator (FilterMap α m n lift f) n γ where
   IsPlausibleStep := FilterMap.PlausibleStep (m := m) (n := n)
@@ -155,9 +163,8 @@ instance FilterMap.instIterator {α β γ : Type w} {m : Type w → Type w'} {n
       | .skip it' h => pure <| .deflate <| .skip (it'.filterMapWithPostcondition f) (by exact .skip h)
       | .done h => pure <| .deflate <| .done (.done h)
 
-instance {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad n] [Iterator α m β]
-    {lift : ⦃α : Type w⦄ → m α → n α}
-    {f : β → PostconditionT n γ} :
+instance Map.instIterator {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad n]
+    [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n γ} :
     Iterator (Map α m n lift f) n γ :=
   inferInstanceAs <| Iterator (FilterMap α m n lift _) n γ
 
@@ -189,8 +196,8 @@ instance FilterMap.instFinite {α β γ : Type w} {m : Type w → Type w'}
   Finite.of_finitenessRelation FilterMap.instFinitenessRelation
 
 @[no_expose]
-instance {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad n] [Iterator α m β]
-    {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n γ} [Finite α m] :
+instance Map.instFinite {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad n]
+    [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n γ} [Finite α m] :
     Finite (Map α m n lift f) n :=
   Finite.of_finitenessRelation FilterMap.instFinitenessRelation
 
@@ -214,7 +221,7 @@ instance Map.instProductive {α β γ : Type w} {m : Type w → Type w'}
     Productive (Map α m n lift f) n :=
   Productive.of_productivenessRelation Map.instProductivenessRelation
 
-instance {α β γ : Type w} {m : Type w → Type w'}
+instance FilterMap.instIteratorCollect {α β γ : Type w} {m : Type w → Type w'}
     {n : Type w → Type w''} {o : Type w → Type x} [Monad n] [Monad o] [Iterator α m β]
     {lift : ⦃α : Type w⦄ → m α → n α}
     {f : β → PostconditionT n (Option γ)} :
@@ -252,6 +259,8 @@ instance Map.instIteratorLoop {α β γ : Type w} {m : Type w → Type w'}
     IteratorLoop (Map α m n lift f) n o :=
   .defaultImplementation
 
+end Iterators.Types
+
 /--
 *Note: This is a very general combinator that requires an advanced understanding of monads, dependent
 types and termination proofs. The variants `map` and `mapM` are easier to use and sufficient
@@ -571,4 +580,4 @@ def IterM.filter {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [M
     (f : β → Bool) (it : IterM (α := α) m β) :=
   (it.filterMap (fun b => if f b then some b else none) : IterM m β)
 
-end Std.Iterators
+end Std

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

@@ -22,11 +22,12 @@ and so on. In other words, `it` flattens the iterator of iterators obtained by m
 `f`.
 -/
 
-namespace Std.Iterators
+namespace Std
+open Iterators.Types
 
 /-- Internal implementation detail of the `flatMap` combinator -/
 @[ext, unbox]
-public structure Flatten (α α₂ β : Type w) (m) where
+public structure Iterators.Types.Flatten (α α₂ β : Type w) (m) where
   it₁ : IterM (α := α) m (IterM (α := α₂) m β)
   it₂ : Option (IterM (α := α₂) m β)
 
@@ -37,7 +38,7 @@ Internal iterator combinator that is used to implement all `flatMap` variants
 def IterM.flattenAfter {α α₂ β : Type w} {m : Type w → Type w'} [Monad m]
     [Iterator α m (IterM (α := α₂) m β)] [Iterator α₂ m β]
     (it₁ : IterM (α := α) m (IterM (α := α₂) m β)) (it₂ : Option (IterM (α := α₂) m β)) :=
-  (toIterM (α := Flatten α α₂ β m) ⟨it₁, it₂⟩ m β : IterM m β)
+  (.mk (α := Flatten α α₂ β m) ⟨it₁, it₂⟩ m β : IterM m β)
 
 /--
 Let `it₁` and `it₂` be iterators and `f` a monadic function mapping `it₁`'s outputs to iterators
@@ -201,23 +202,25 @@ public def IterM.flatMap {α : Type w} {β : Type w} {α₂ : Type w}
     (f : β → IterM (α := α₂) m γ) (it : IterM (α := α) m β) :=
   (it.flatMapAfter f none : IterM m γ)
 
+namespace Iterators.Types
+
 variable {α α₂ β : Type w} {m : Type w → Type w'}
 
 /-- The plausible-step predicate for `Flatten` iterators -/
 public inductive Flatten.IsPlausibleStep [Iterator α m (IterM (α := α₂) m β)] [Iterator α₂ m β] :
     (it : IterM (α := Flatten α α₂ β m) m β) → (step : IterStep (IterM (α := Flatten α α₂ β m) m β) β) → Prop where
   | outerYield : ∀ {it₁ it₁' it₂'}, it₁.IsPlausibleStep (.yield it₁' it₂') →
-      IsPlausibleStep (toIterM ⟨it₁, none⟩ m β) (.skip (toIterM ⟨it₁', some it₂'⟩ m β))
+      IsPlausibleStep (.mk ⟨it₁, none⟩ m β) (.skip (.mk ⟨it₁', some it₂'⟩ m β))
   | outerSkip : ∀ {it₁ it₁'}, it₁.IsPlausibleStep (.skip it₁') →
-      IsPlausibleStep (toIterM ⟨it₁, none⟩ m β) (.skip (toIterM ⟨it₁', none⟩ m β))
+      IsPlausibleStep (.mk ⟨it₁, none⟩ m β) (.skip (.mk ⟨it₁', none⟩ m β))
   | outerDone : ∀ {it₁}, it₁.IsPlausibleStep .done →
-      IsPlausibleStep (toIterM ⟨it₁, none⟩ m β) .done
+      IsPlausibleStep (.mk ⟨it₁, none⟩ m β) .done
   | innerYield : ∀ {it₁ it₂ it₂' b}, it₂.IsPlausibleStep (.yield it₂' b) →
-      IsPlausibleStep (toIterM ⟨it₁, some it₂⟩ m β) (.yield (toIterM ⟨it₁, some it₂'⟩ m β) b)
+      IsPlausibleStep (.mk ⟨it₁, some it₂⟩ m β) (.yield (.mk ⟨it₁, some it₂'⟩ m β) b)
   | innerSkip : ∀ {it₁ it₂ it₂'}, it₂.IsPlausibleStep (.skip it₂') →
-      IsPlausibleStep (toIterM ⟨it₁, some it₂⟩ m β) (.skip (toIterM ⟨it₁, some it₂'⟩ m β))
+      IsPlausibleStep (.mk ⟨it₁, some it₂⟩ m β) (.skip (.mk ⟨it₁, some it₂'⟩ m β))
   | innerDone : ∀ {it₁ it₂}, it₂.IsPlausibleStep .done →
-      IsPlausibleStep (toIterM ⟨it₁, some it₂⟩ m β) (.skip (toIterM ⟨it₁, none⟩ m β))
+      IsPlausibleStep (.mk ⟨it₁, some it₂⟩ m β) (.skip (.mk ⟨it₁, none⟩ m β))
 
 public instance Flatten.instIterator [Monad m] [Iterator α m (IterM (α := α₂) m β)] [Iterator α₂ m β] :
     Iterator (Flatten α α₂ β m) m β where
@@ -246,7 +249,7 @@ section Finite
 variable {α : Type w} {α₂ : Type w} {β : Type w} {m : Type w → Type w'}
 
 variable (α m β) in
-def Rel [Monad m] [Iterator α m (IterM (α := α₂) m β)] [Iterator α₂ m β] [Finite α m] [Finite α₂ m] :
+def Flatten.Rel [Monad m] [Iterator α m (IterM (α := α₂) m β)] [Iterator α₂ m β] [Finite α m] [Finite α₂ m] :
     IterM (α := Flatten α α₂ β m) m β → IterM (α := Flatten α α₂ β m) m β → Prop :=
   InvImage
     (Prod.Lex
@@ -271,7 +274,7 @@ theorem Flatten.rel_of_right₂ [Monad m] [Iterator α m (IterM (α := α₂) m
     Rel α β m ⟨it₁, none⟩ ⟨it₁, some it₂⟩ :=
   Prod.Lex.right _ True.intro
 
-instance [Monad m] [Iterator α m (IterM (α := α₂) m β)] [Iterator α₂ m β]
+def Flatten.instFinitenessRelation [Monad m] [Iterator α m (IterM (α := α₂) m β)] [Iterator α₂ m β]
     [Finite α m] [Finite α₂ m] :
     FinitenessRelation (Flatten α α₂ β m) m where
   rel := Rel α β m
@@ -299,9 +302,9 @@ instance [Monad m] [Iterator α m (IterM (α := α₂) m β)] [Iterator α₂ m
       apply Flatten.rel_of_right₂
 
 @[no_expose]
-public instance [Monad m] [Iterator α m (IterM (α := α₂) m β)] [Iterator α₂ m β]
+public instance Flatten.instFinite [Monad m] [Iterator α m (IterM (α := α₂) m β)] [Iterator α₂ m β]
     [Finite α m] [Finite α₂ m] : Finite (Flatten α α₂ β m) m :=
-  .of_finitenessRelation instFinitenessRelationFlattenOfIterMOfFinite
+  .of_finitenessRelation instFinitenessRelation
 
 end Finite
 
@@ -310,7 +313,7 @@ section Productive
 variable {α : Type w} {α₂ : Type w} {β : Type w} {m : Type w → Type w'}
 
 variable (α m β) in
-def ProductiveRel [Monad m] [Iterator α m (IterM (α := α₂) m β)] [Iterator α₂ m β] [Finite α m]
+def Flatten.ProductiveRel [Monad m] [Iterator α m (IterM (α := α₂) m β)] [Iterator α₂ m β] [Finite α m]
     [Productive α₂ m] :
     IterM (α := Flatten α α₂ β m) m β → IterM (α := Flatten α α₂ β m) m β → Prop :=
   InvImage
@@ -336,8 +339,8 @@ theorem Flatten.productiveRel_of_right₂ [Monad m] [Iterator α m (IterM (α :=
     ProductiveRel α β m ⟨it₁, none⟩ ⟨it₁, some it₂⟩ :=
   Prod.Lex.right _ True.intro
 
-instance [Monad m] [Iterator α m (IterM (α := α₂) m β)] [Iterator α₂ m β]
-    [Finite α m] [Productive α₂ m] :
+def Flatten.instProductivenessRelation [Monad m] [Iterator α m (IterM (α := α₂) m β)]
+    [Iterator α₂ m β] [Finite α m] [Productive α₂ m] :
     ProductivenessRelation (Flatten α α₂ β m) m where
   rel := ProductiveRel α β m
   wf := by
@@ -360,9 +363,9 @@ instance [Monad m] [Iterator α m (IterM (α := α₂) m β)] [Iterator α₂ m
       apply Flatten.productiveRel_of_right₂
 
 @[no_expose]
-public instance [Monad m] [Iterator α m (IterM (α := α₂) m β)] [Iterator α₂ m β]
+public def Flatten.instProductive [Monad m] [Iterator α m (IterM (α := α₂) m β)] [Iterator α₂ m β]
     [Finite α m] [Productive α₂ m] : Productive (Flatten α α₂ β m) m :=
-  .of_productivenessRelation instProductivenessRelationFlattenOfFiniteIterMOfProductive
+  .of_productivenessRelation instProductivenessRelation
 
 end Productive
 
@@ -374,4 +377,4 @@ public instance Flatten.instIteratorLoop [Monad m] [Monad n] [Iterator α m (Ite
     [Iterator α₂ m β] : IteratorLoop (Flatten α α₂ β m) m n :=
   .defaultImplementation
 
-end Std.Iterators
+end Std.Iterators.Types

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

@@ -17,7 +17,7 @@ public import Init.Data.Iterators.Internal.Termination
 This module provides the iterator combinator `IterM.take`.
 -/
 
-namespace Std.Iterators
+namespace Std
 
 variable {α : Type w} {m : Type w → Type w'} {β : Type w}
 
@@ -25,7 +25,7 @@ variable {α : Type w} {m : Type w → Type w'} {β : Type w}
 The internal state of the `IterM.take` iterator combinator.
 -/
 @[unbox]
-structure Take (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] where
+structure Iterators.Types.Take (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] where
   /--
   Internal implementation detail of the iterator library.
   Caution: For `take n`, `countdown` is `n + 1`.
@@ -40,6 +40,8 @@ structure Take (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α
   -/
   finite : countdown > 0 ∨ Finite α m
 
+open Std.Iterators Std.Iterators.Types
+
 /--
 Given an iterator `it` and a natural number `n`, `it.take n` is an iterator that outputs
 up to the first `n` of `it`'s values in order and then terminates.
@@ -65,7 +67,7 @@ This combinator incurs an additional O(1) cost with each output of `it`.
 -/
 @[always_inline, inline]
 def IterM.take [Iterator α m β] (n : Nat) (it : IterM (α := α) m β) :=
-  toIterM (Take.mk (n + 1) it (Or.inl <| Nat.zero_lt_succ _)) m β
+  IterM.mk (Take.mk (n + 1) it (Or.inl <| Nat.zero_lt_succ _)) m β
 
 /--
 This combinator is only useful for advanced use cases.
@@ -91,7 +93,7 @@ This combinator incurs an additional O(1) cost with each output of `it`.
 -/
 @[always_inline, inline]
 def IterM.toTake [Iterator α m β] [Finite α m] (it : IterM (α := α) m β) :=
-  toIterM (Take.mk 0 it (Or.inr inferInstance)) m β
+  IterM.mk (Take.mk 0 it (Or.inr inferInstance)) m β
 
 theorem IterM.take.surjective_of_zero_lt {α : Type w} {m : Type w → Type w'} {β : Type w}
     [Iterator α m β] (it : IterM (α := Take α m) m β) (h : 0 < it.internalState.countdown) :
@@ -100,6 +102,8 @@ theorem IterM.take.surjective_of_zero_lt {α : Type w} {m : Type w → Type w'}
   simp only [take, Nat.sub_add_cancel (m := 1) (n := it.internalState.countdown) (by omega)]
   rfl
 
+namespace Iterators.Types
+
 inductive Take.PlausibleStep [Iterator α m β] (it : IterM (α := Take α m) m β) :
     (step : IterStep (IterM (α := Take α m) m β) β) → Prop where
   | yield : ∀ {it' out}, it.internalState.inner.IsPlausibleStep (.yield it' out) →
@@ -212,4 +216,4 @@ instance Take.instIteratorLoop {n : Type x → Type x'} [Monad m] [Monad n] [Ite
     IteratorLoop (Take α m) m n :=
   .defaultImplementation
 
-end Std.Iterators
+end Std.Iterators.Types

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

@@ -11,11 +11,12 @@ public import Init.Data.Iterators.Consumers.Monadic
 
 public section
 
-namespace Std.Iterators
+namespace Std
 
 universe v u v' u'
 
 section ULiftT
+namespace Iterators
 
 /-- `ULiftT.{v, u}` shrinks a monad on `Type max u v` to a monad on `Type u`. -/
 @[expose]  -- for codegen
@@ -60,11 +61,14 @@ theorem ULiftT.run_map {n : Type max u v → Type v'} [Monad n] {α β : Type u}
     (f <$> x).run = x.run >>= (fun a => pure <| .up (f a.down)) :=
   (rfl)
 
+end Iterators
 end ULiftT
 
+namespace Iterators.Types
+
 /-- Internal state of the `uLift` iterator combinator. Do not depend on its internals. -/
 @[unbox]
-structure Types.ULiftIterator (α : Type u) (m : Type u → Type u') (n : Type max u v → Type v')
+structure ULiftIterator (α : Type u) (m : Type u → Type u') (n : Type max u v → Type v')
     (β : Type u) (lift : ∀ ⦃γ : Type u⦄, m γ → ULiftT n γ) : Type max u v where
   inner : IterM (α := α) m β
 
@@ -75,14 +79,14 @@ variable {α : Type u} {m : Type u → Type u'} {n : Type max u v → Type v'}
 Transforms a step of the base iterator into a step of the `uLift` iterator.
 -/
 @[always_inline, inline, expose]
-def Types.ULiftIterator.Monadic.modifyStep (step : IterStep (IterM (α := α) m β) β) :
+def ULiftIterator.Monadic.modifyStep (step : IterStep (IterM (α := α) m β) β) :
     IterStep (IterM (α := ULiftIterator.{v} α m n β lift) n (ULift.{v} β)) (ULift.{v} β) :=
   match step with
   | .yield it' out => .yield ⟨⟨it'⟩⟩ (.up out)
   | .skip it' => .skip ⟨⟨it'⟩⟩
   | .done => .done
 
-instance Types.ULiftIterator.instIterator [Iterator α m β] [Monad n] :
+instance ULiftIterator.instIterator [Iterator α m β] [Monad n] :
     Iterator (ULiftIterator α m n β lift) n (ULift β) where
   IsPlausibleStep it step :=
     ∃ step', it.internalState.inner.IsPlausibleStep step' ∧
@@ -93,7 +97,7 @@ instance Types.ULiftIterator.instIterator [Iterator α m β] [Monad n] :
   where finally
     case hp => exact ⟨step.inflate.val, step.inflate.property, rfl⟩
 
-def Types.ULiftIterator.instFinitenessRelation [Iterator α m β] [Finite α m] [Monad n] :
+private def ULiftIterator.instFinitenessRelation [Iterator α m β] [Finite α m] [Monad n] :
     FinitenessRelation (ULiftIterator α m n β lift) n where
   rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.inner.finitelyManySteps)
   wf := InvImage.wf _ WellFoundedRelation.wf
@@ -105,11 +109,11 @@ def Types.ULiftIterator.instFinitenessRelation [Iterator α m β] [Finite α m]
     · apply IterM.TerminationMeasures.Finite.rel_of_skip
       exact hp
 
-instance Types.ULiftIterator.instFinite [Iterator α m β] [Finite α m] [Monad n] :
+instance ULiftIterator.instFinite [Iterator α m β] [Finite α m] [Monad n] :
     Finite (ULiftIterator α m n β lift) n :=
   .of_finitenessRelation instFinitenessRelation
 
-def Types.ULiftIterator.instProductivenessRelation [Iterator α m β] [Productive α m] [Monad n] :
+private def ULiftIterator.instProductivenessRelation [Iterator α m β] [Productive α m] [Monad n] :
     ProductivenessRelation (ULiftIterator α m n β lift) n where
   rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.inner.finitelyManySkips)
   wf := InvImage.wf _ WellFoundedRelation.wf
@@ -119,19 +123,23 @@ def Types.ULiftIterator.instProductivenessRelation [Iterator α m β] [Productiv
     apply IterM.TerminationMeasures.Productive.rel_of_skip
     exact hp
 
-instance Types.ULiftIterator.instProductive [Iterator α m β] [Productive α m] [Monad n] :
+instance ULiftIterator.instProductive [Iterator α m β] [Productive α m] [Monad n] :
     Productive (ULiftIterator α m n β lift) n :=
   .of_productivenessRelation instProductivenessRelation
 
-instance Types.ULiftIterator.instIteratorLoop {o : Type x → Type x'} [Monad n] [Monad o]
+instance ULiftIterator.instIteratorLoop {o : Type x → Type x'} [Monad n] [Monad o]
     [Iterator α m β] :
     IteratorLoop (ULiftIterator α m n β lift) n o :=
   .defaultImplementation
 
-instance Types.ULiftIterator.instIteratorCollect [Monad n] [Monad o] [Iterator α m β] :
+instance ULiftIterator.instIteratorCollect [Monad n] [Monad o] [Iterator α m β] :
     IteratorCollect (ULiftIterator α m n β lift) n o :=
   .defaultImplementation
 
+end Iterators.Types
+
+open Std.Iterators Std.Iterators.Types
+
 /--
 Transforms an `m`-monadic iterator with values in `β` into an `n`-monadic iterator with
 values in `ULift β`. Requires a `MonadLift m (ULiftT n)` instance.
@@ -149,9 +157,9 @@ it.uLift n    ---.up a----.up b---.up c--.up d---⊥
 * `Productive`: only if the original iterator is productive
 -/
 @[always_inline, inline, expose]
-def IterM.uLift (it : IterM (α := α) m β) (n : Type max u v → Type v')
-    [lift : MonadLiftT m (ULiftT n)] :
-    IterM (α := Types.ULiftIterator α m n β (fun _ => lift.monadLift)) n (ULift β) :=
+def IterM.uLift {α β : Type u} {m : Type u → Type u'} (it : IterM (α := α) m β)
+    (n : Type max u v → Type v') [lift : MonadLiftT m (ULiftT n)] :
+    IterM (α := ULiftIterator α m n β (fun _ => lift.monadLift)) n (ULift β) :=
   ⟨⟨it⟩⟩
 
-end Std.Iterators
+end Std

src/Init/Data/Iterators/Combinators/Take.lean

@@ -10,7 +10,8 @@ public import Init.Data.Iterators.Combinators.Monadic.Take
 
 @[expose] public section
 
-namespace Std.Iterators
+namespace Std
+open Std.Iterators Std.Iterators.Types
 
 /--
 Given an iterator `it` and a natural number `n`, `it.take n` is an iterator that outputs
@@ -67,4 +68,4 @@ def Iter.toTake {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] (
     Iter (α := Take α Id) β :=
   it.toIterM.toTake.toIter
 
-end Std.Iterators
+end Std

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

@@ -10,7 +10,8 @@ public import Init.Data.Iterators.Combinators.Monadic.ULift
 
 public section
 
-namespace Std.Iterators
+namespace Std
+open Std.Iterators Std.Iterators.Types
 
 universe v u v' u'
 
@@ -20,10 +21,10 @@ variable {α : Type u} {β : Type u}
 Transforms a step of the base iterator into a step of the `uLift` iterator.
 -/
 @[always_inline, inline]
-def Types.ULiftIterator.modifyStep (step : IterStep (Iter (α := α) β) β) :
+def Iterators.Types.ULiftIterator.modifyStep (step : IterStep (Iter (α := α) β) β) :
     IterStep (Iter (α := ULiftIterator.{v} α Id Id β (fun _ => monadLift)) (ULift.{v} β))
       (ULift.{v} β) :=
-  (Monadic.modifyStep (step.mapIterator Iter.toIterM)).mapIterator IterM.toIter
+  (ULiftIterator.Monadic.modifyStep (step.mapIterator Iter.toIterM)).mapIterator IterM.toIter
 
 /--
 Transforms an iterator with values in `β` into one with values in `ULift β`.
@@ -48,4 +49,4 @@ def Iter.uLift (it : Iter (α := α) β) :
     Iter (α := Types.ULiftIterator.{v} α Id Id β (fun _ => monadLift)) (ULift β) :=
   (it.toIterM.uLift Id).toIter
 
-end Std.Iterators
+end Std

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

@@ -11,7 +11,8 @@ public import Init.Data.Iterators.Consumers.Monadic.Access
 
 @[expose] public section
 
-namespace Std.Iterators
+namespace Std
+open Std.Iterators
 
 /--
 If possible, takes `n` steps with the iterator `it` and
@@ -62,4 +63,4 @@ def Iter.atIdx? {α β} [Iterator α Id β] [Productive α Id] [IteratorAccess
   | .skip _ => none
   | .done => none
 
-end Std.Iterators
+end Std

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

@@ -25,7 +25,8 @@ Concretely, the following operations are provided:
 Some operations are implemented using the `IteratorCollect` type class.
 -/
 
-namespace Std.Iterators
+namespace Std
+open Std.Iterators
 
 /--
 Traverses the given iterator and stores the emitted values in an array.
@@ -131,4 +132,4 @@ def Iter.Total.toList {α : Type w} {β : Type w}
     List β :=
   it.it.toList
 
-end Std.Iterators
+end Std

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

@@ -26,7 +26,8 @@ function in every iteration. Concretely, the following operations are provided:
 These operations are implemented using the `IteratorLoop` type class.
 -/
 
-namespace Std.Iterators
+namespace Std
+open Std.Iterators
 
 /--
 A `ForIn'` instance for iterators. Its generic membership relation is not easy to use,
@@ -677,4 +678,4 @@ def Iter.Partial.size {α : Type w} {β : Type w} [Iterator α Id β] [IteratorL
     (it : Iter.Partial (α := α) β) : Nat :=
   it.it.count
 
-end Std.Iterators
+end Std

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

@@ -10,7 +10,8 @@ public import Init.Data.Iterators.Basic
 
 public section
 
-namespace Std.Iterators
+namespace Std
+open Std.Iterators
 
 /--
 `it.IsPlausibleNthOutputStep n step` is the proposition that according to the
@@ -105,4 +106,4 @@ def IterM.atIdx? [Iterator α m β] [IteratorAccess α m] [Monad m] (it : IterM
   | .skip _ => return none
   | .done => return none
 
-end Std.Iterators
+end Std

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

@@ -29,8 +29,8 @@ implementation is provided. The typeclass `LawfulIteratorCollect` asserts that a
 instance equals the default implementation.
 -/
 
-namespace Std.Iterators
-open Std.Internal
+namespace Std
+open Std.Internal Std.Iterators
 
 section Typeclasses
 
@@ -122,8 +122,8 @@ theorem LawfulIteratorCollect.toArrayMapped_eq {α β γ : Type w} {m : Type w
       IterM.DefaultConsumers.toArrayMapped lift f it (m := m) := by
   rw [lawful_toArrayMapped]; rfl
 
-instance (α β : Type w) (m : Type w → Type w') (n : Type w → Type w'') [Monad n]
-    [Iterator α m β] [Monad m] [Iterator α m β] [Finite α m] :
+instance instLawfulIteratorCollectDefaultImplementation (α β : Type w) (m : Type w → Type w')
+    (n : Type w → Type w'') [Monad n] [Iterator α m β] [Monad m] [Iterator α m β] [Finite α m] :
     haveI : IteratorCollect α m n := .defaultImplementation
     LawfulIteratorCollect α m n :=
   letI : IteratorCollect α m n := .defaultImplementation
@@ -246,4 +246,4 @@ def IterM.Total.toList {α : Type w} {m : Type w → Type w'} {β : Type w} [Mon
     m (List β) :=
   it.it.toList
 
-end Std.Iterators
+end Std

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

@@ -31,9 +31,9 @@ types of iterators. A default implementation is provided. The typeclass `LawfulI
 asserts that an `IteratorLoop` instance equals the default implementation.
 -/
 
-namespace Std.Iterators
+namespace Std
 
-open Std.Internal
+open Std.Internal Std.Iterators
 
 section Typeclasses
 
@@ -169,8 +169,8 @@ class LawfulIteratorLoop (α : Type w) (m : Type w → Type w') (n : Type x →
     i.forIn lift γ Pl it init f =
       IteratorLoop.defaultImplementation.forIn lift γ Pl it init f
 
-instance (α : Type w) (m : Type w → Type w') (n : Type x → Type x')
-    [Monad m] [Monad n] [Iterator α m β] [Finite α m] :
+instance instLawfulIteratorLoopDefaultImplementation (α : Type w) (m : Type w → Type w')
+    (n : Type x → Type x') [Monad m] [Monad n] [Iterator α m β] [Finite α m] :
     letI : IteratorLoop α m n := .defaultImplementation
     LawfulIteratorLoop α m n := by
   letI : IteratorLoop α m n := .defaultImplementation
@@ -212,7 +212,7 @@ def IterM.instForIn' {m : Type w → Type w'} {n : Type w → Type w''}
     ForIn' n (IterM (α := α) m β) β ⟨fun it out => it.IsPlausibleIndirectOutput out⟩ :=
   IteratorLoop.finiteForIn' (fun _ _ f x => monadLift x >>= f)
 
-instance {m : Type w → Type w'} {n : Type w → Type w''}
+instance IterM.instForInOfIteratorLoop {m : Type w → Type w'} {n : Type w → Type w''}
     {α : Type w} {β : Type w} [Iterator α m β] [IteratorLoop α m n]
     [MonadLiftT m n] [Monad n] :
     ForIn n (IterM (α := α) m β) β :=
@@ -233,7 +233,7 @@ def IterM.Total.instForIn' {m : Type w → Type w'} {n : Type w → Type w''}
     ForIn' n (IterM.Total (α := α) m β) β ⟨fun it out => it.it.IsPlausibleIndirectOutput out⟩ where
   forIn' it init f := IterM.instForIn'.forIn' it.it init f
 
-instance {m : Type w → Type w'} {n : Type w → Type w''}
+instance IterM.Partial.instForInOfIteratorLoop {m : Type w → Type w'} {n : Type w → Type w''}
     {α : Type w} {β : Type w} [Iterator α m β] [IteratorLoop α m n] [MonadLiftT m n] [Monad n] :
     ForIn n (IterM.Partial (α := α) m β) β :=
   haveI : ForIn' n (IterM.Partial (α := α) m β) β _ := IterM.Partial.instForIn'
@@ -246,12 +246,13 @@ instance {m : Type w → Type w'} {n : Type w → Type w''}
   haveI : ForIn' n (IterM.Total (α := α) m β) β _ := IterM.Total.instForIn'
   instForInOfForIn'
 
-instance {m : Type w → Type w'} {n : Type w → Type w''} {α : Type w} {β : Type w} [Iterator α m β]
-    [IteratorLoop α m n] [Monad n] [MonadLiftT m n] : ForM n (IterM (α := α) m β) β where
+instance IterM.instForMOfIteratorLoop {m : Type w → Type w'} {n : Type w → Type w''}
+    {α : Type w} {β : Type w} [Iterator α m β] [IteratorLoop α m n] [Monad n] [MonadLiftT m n] :
+    ForM n (IterM (α := α) m β) β where
   forM it f := forIn it PUnit.unit (fun out _ => do f out; return .yield .unit)
 
-instance {m : Type w → Type w'} {n : Type w → Type w''} {α : Type w} {β : Type w} [Monad n]
-    [Iterator α m β] [IteratorLoop α m n] [MonadLiftT m n] :
+instance IterM.Partial.instForMOfItreratorLoop {m : Type w → Type w'} {n : Type w → Type w''}
+    {α : Type w} {β : Type w} [Monad n] [Iterator α m β] [IteratorLoop α m n] [MonadLiftT m n] :
     ForM n (IterM.Partial (α := α) m β) β where
   forM it f := forIn it PUnit.unit (fun out _ => do f out; return .yield .unit)
 
@@ -943,4 +944,4 @@ def IterM.Partial.size {α : Type w} {m : Type w → Type w'} {β : Type w} [Ite
 
 end Count
 
-end Std.Iterators
+end Std

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

@@ -10,7 +10,7 @@ public import Init.Data.Iterators.Basic
 
 public section
 
-namespace Std.Iterators
+namespace Std
 
 /--
 A wrapper around an iterator that provides partial consumers. See `IterM.allowNontermination`.
@@ -29,4 +29,4 @@ def IterM.allowNontermination {α : Type w} {m : Type w → Type w'} {β : Type
     (it : IterM (α := α) m β) : IterM.Partial (α := α) m β :=
   ⟨it⟩
 
-end Std.Iterators
+end Std

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

@@ -12,7 +12,7 @@ set_option doc.verso true
 
 public section
 
-namespace Std.Iterators
+namespace Std
 
 structure IterM.Total {α : Type w} (m : Type w → Type w') (β : Type w) where
   it : IterM (α := α) m β
@@ -33,4 +33,4 @@ A wrapper around an iterator that provides strictly terminating consumers. See
 -/
 add_decl_doc IterM.Total
 
-end Std.Iterators
+end Std

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

@@ -10,7 +10,7 @@ public import Init.Data.Iterators.Basic
 
 public section
 
-namespace Std.Iterators
+namespace Std
 
 /--
 A wrapper around an iterator that provides partial consumers. See `Iter.allowNontermination`.
@@ -29,4 +29,4 @@ def Iter.allowNontermination {α : Type w} {β : Type w}
     (it : Iter (α := α) β) : Iter.Partial (α := α) β :=
   ⟨it⟩
 
-end Std.Iterators
+end Std

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

@@ -11,7 +11,8 @@ public import Init.Data.Iterators.Consumers.Access
 
 public section
 
-namespace Std.Iterators
+namespace Std
+open Std.Iterators
 
 instance {α β} [Iterator α Id β] [Productive α Id] [IteratorAccess α Id] :
     Stream (Iter (α := α) β) β where
@@ -24,4 +25,4 @@ instance {α β} [Iterator α Id β] [Productive α Id] [IteratorAccess α Id] :
       revert h
       exact IterM.not_isPlausibleNthOutputStep_yield
 
-end Std.Iterators
+end Std

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

@@ -12,7 +12,7 @@ set_option doc.verso true
 
 public section
 
-namespace Std.Iterators
+namespace Std
 
 structure Iter.Total {α : Type w} (β : Type w) where
   it : Iter (α := α) β
@@ -33,4 +33,4 @@ A wrapper around an iterator that provides strictly terminating consumers. See
 -/
 add_decl_doc Iter.Total
 
-end Std.Iterators
+end Std

src/Init/Data/Iterators/Lemmas/Basic.lean

@@ -10,7 +10,8 @@ public import Init.Data.Iterators.Basic
 
 public section
 
-namespace Std.Iterators
+namespace Std
+open Std.Iterators
 
 /--
 Induction principle for finite iterators: One can define a function `f` that maps every
@@ -46,4 +47,4 @@ def Iter.inductSkips {α β} [Iterator α Id β] [Productive α Id]
   step it (fun {it'} _ => inductSkips motive step it')
 termination_by it.finitelyManySkips
 
-end Std.Iterators
+end Std

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

@@ -16,7 +16,8 @@ public import Init.Data.Array.Attach
 
 public section
 
-namespace Std.Iterators
+namespace Std
+open Std.Iterators
 
 theorem Iter.unattach_eq_toIter_unattach_toIterM [Iterator α Id β] {it : Iter (α := α) β} {hP} :
     it.attachWith P hP =
@@ -93,4 +94,4 @@ theorem Iter.count_attachWith [Iterator α Id β]
   rw [← Iter.length_toList_eq_count, toList_attachWith]
   simp
 
-end Std.Iterators
+end Std

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

@@ -12,7 +12,8 @@ public import Init.Data.Iterators.Combinators.FilterMap
 
 public section
 
-namespace Std.Iterators
+namespace Std
+open Std.Iterators
 
 variable {α β γ : Type w} [Iterator α Id β] {it : Iter (α := α) β}
     {m : Type w → Type w'} {n : Type w → Type w''}
@@ -791,4 +792,4 @@ theorem Iter.all_map {α β β' : Type w}
   · simp [ihs ‹_›]
   · simp
 
-end Std.Iterators
+end Std

src/Init/Data/Iterators/Lemmas/Combinators/FlatMap.lean

@@ -11,8 +11,10 @@ public import Init.Data.Iterators.Combinators.FlatMap
 import all Init.Data.Iterators.Combinators.FlatMap
 public import Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
 
-namespace Std.Iterators
-open Std.Internal
+namespace Std
+open Std.Internal Std.Iterators
+
+namespace Iterators.Types
 
 public theorem Flatten.IsPlausibleStep.outerYield_flatMapM_pure {α : Type w} {β : Type w} {α₂ : Type w}
     {γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α Id β] [Iterator α₂ m γ]
@@ -99,6 +101,8 @@ public theorem Flatten.IsPlausibleStep.innerDone_flatMap_pure {α : Type w} {β
     (it₁.flatMapAfter f (some it₂)).IsPlausibleStep (.skip (it₁.flatMapAfter f none)) :=
   innerDone_flatMap h
 
+end Iterators.Types
+
 public theorem Iter.step_flatMapAfterM {α : Type w} {β : Type w} {α₂ : Type w}
     {γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α Id β] [Iterator α₂ m γ]
     {f : β → m (IterM (α := α₂) m γ)} {it₁ : Iter (α := α) β} {it₂ : Option (IterM (α := α₂) m γ)} :
@@ -263,4 +267,4 @@ public theorem Iter.toArray_flatMap {α α₂ β γ : Type w} [Iterator α Id β
     (it₁.flatMap f).toArray = (it₁.map fun b => (f b).toArray).toArray.flatten := by
   simp [flatMap, toArray_flatMapAfter]
 
-end Std.Iterators
+end Std

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

@@ -13,13 +13,14 @@ public import Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
 
 public section
 
-namespace Std.Iterators
+namespace Std
+open Std.Iterators Std.Iterators.Types
 
 variable {α : Type w} {m : Type w → Type w'} {β : Type w} {P : β → Prop}
 
 theorem IterM.step_attachWith [Iterator α m β] [Monad m] {it : IterM (α := α) m β} {hP} :
     (it.attachWith P hP).step =
-      (fun s => .deflate ⟨Types.Attach.Monadic.modifyStep (it.attachWith P hP) s.inflate, s.inflate, rfl⟩) <$> it.step :=
+      (fun s => .deflate ⟨Attach.Monadic.modifyStep (it.attachWith P hP) s.inflate, s.inflate, rfl⟩) <$> it.step :=
   rfl
 
 @[simp]
@@ -70,4 +71,4 @@ theorem IterM.count_attachWith [Iterator α m β] [Monad m] [Monad n]
     ← map_unattach_toList_attachWith (it := it) (P := P) (hP := hP)]
   simp only [Functor.map_map, List.length_unattach]
 
-end Std.Iterators
+end Std

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

@@ -12,8 +12,8 @@ import all Init.Data.Iterators.Consumers.Monadic.Collect
 
 public section
 
-namespace Std.Iterators
-open Std.Internal
+namespace Std
+open Std.Internal Std.Iterators Std.Iterators.Types
 
 section Step
 
@@ -234,7 +234,8 @@ end Step
 section Lawful
 
 @[no_expose]
-instance {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type x}
+instance Iterators.Types.Map.instLawfulIteratorCollect {α β γ : Type w} {m : Type w → Type w'}
+    {n : Type w → Type w''} {o : Type w → Type x}
     [Monad m] [Monad n] [Monad o] [LawfulMonad n] [LawfulMonad o] [Iterator α m β] [Finite α m]
     [IteratorCollect α m o] [LawfulIteratorCollect α m o]
     {lift : ⦃δ : Type w⦄ -> m δ → n δ} {f : β → PostconditionT n γ} [LawfulMonadLiftFunction lift] :
@@ -483,12 +484,12 @@ theorem IterM.toList_map {α β β' : Type w} {m : Type w → Type w'} [Monad m]
   let t' := type_of% (it.filterMap (some ∘ f))
   congr
   · simp [Map]
-  · simp [instIteratorMap, inferInstanceAs]
+  · simp [Map.instIterator, inferInstanceAs]
     congr
     simp
   · congr
     simp only [Map, PostconditionT.map_pure, Function.comp_apply]
-  · simp only [instIteratorMap, inferInstanceAs, Function.comp_apply]
+  · simp only [Map.instIterator, inferInstanceAs, Function.comp_apply]
     congr
     simp
   · simp only [map, mapWithPostcondition, InternalCombinators.map, Function.comp_apply, filterMap,
@@ -1262,4 +1263,4 @@ theorem IterM.all_map {α β β' : Type w} {m : Type w → Type w'}
 
 end AnyAll
 
-end Std.Iterators
+end Std

src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FlatMap.lean

@@ -11,8 +11,8 @@ import Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
 public import Init.Data.Iterators.Combinators.Monadic.FlatMap
 import all Init.Data.Iterators.Combinators.Monadic.FlatMap
 
-namespace Std.Iterators
-open Std.Internal
+namespace Std
+open Std.Internal Std.Iterators
 
 theorem IterM.step_flattenAfter {α α₂ β : Type w} {m : Type w → Type w'} [Monad m]
     [Iterator α m (IterM (α := α₂) m β)] [Iterator α₂ m β]
@@ -32,7 +32,9 @@ theorem IterM.step_flattenAfter {α α₂ β : Type w} {m : Type w → Type w'}
   cases it₂
   all_goals
   · apply bind_congr; intro step
-    cases step.inflate using PlausibleIterStep.casesOn <;> simp [IterM.flattenAfter, toIterM]
+    cases step.inflate using PlausibleIterStep.casesOn <;> simp [IterM.flattenAfter, IterM.mk]
+
+namespace Iterators.Types
 
 public theorem Flatten.IsPlausibleStep.outerYield_flatMapM {α : Type w} {β : Type w} {α₂ : Type w}
     {γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ]
@@ -118,6 +120,8 @@ public theorem Flatten.IsPlausibleStep.innerDone_flatMap {α : Type w} {β : Typ
     (it₁.flatMapAfter f (some it₂)).IsPlausibleStep (.skip (it₁.flatMapAfter f none)) :=
   .innerDone h
 
+end Iterators.Types
+
 public theorem IterM.step_flatMapAfterM {α : Type w} {β : Type w} {α₂ : Type w}
     {γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ]
     {f : β → m (IterM (α := α₂) m γ)} {it₁ : IterM (α := α) m β} {it₂ : Option (IterM (α := α₂) m γ)} :
@@ -341,4 +345,4 @@ public theorem IterM.toArray_flatMap {α α₂ β γ : Type w} {m : Type w → T
     (it₁.flatMap f).toArray = Array.flatten <$> (it₁.mapM fun b => (f b).toArray).toArray := by
   simp [flatMap, toArray_flatMapAfter]
 
-end Std.Iterators
+end Std

src/Init/Data/Iterators/Lemmas/Combinators/Monadic/Take.lean

@@ -11,7 +11,10 @@ public import Init.Data.Iterators.Lemmas.Consumers.Monadic
 
 @[expose] public section
 
-namespace Std.Iterators
+namespace Std
+open Std.Iterators Std.Iterators.Types
+
+namespace Iterators.Types
 
 theorem Take.isPlausibleStep_take_yield [Monad m] [Iterator α m β] {n : Nat}
     {it : IterM (α := α) m β} (h : it.IsPlausibleStep (.yield it' out)) :
@@ -23,6 +26,8 @@ theorem Take.isPlausibleStep_take_skip [Monad m] [Iterator α m β] {n : Nat}
     (it.take (n + 1)).IsPlausibleStep (.skip (it'.take (n + 1))) :=
   (.skip h (by simp [IterM.take]))
 
+end Iterators.Types
+
 theorem IterM.step_take {α m β} [Monad m] [Iterator α m β] {n : Nat}
     {it : IterM (α := α) m β} :
     (it.take n).step = (match n with
@@ -74,4 +79,4 @@ theorem IterM.toList_toTake {α m β} [Monad m] [LawfulMonad m] [Iterator α m
   · simp [ihs ‹_›]
   · simp
 
-end Std.Iterators
+end Std

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

@@ -12,7 +12,8 @@ public import Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
 
 public section
 
-namespace Std.Iterators
+namespace Std
+open Std.Iterators
 
 variable {α : Type u} {m : Type u → Type u'} {n : Type max u v → Type v'}
     {β : Type u}
@@ -80,4 +81,4 @@ theorem IterM.count_uLift [Iterator α m β] [Monad m] [Monad n] {it : IterM (α
   · simp [ihs ‹_›]
   · simp
 
-end Std.Iterators
+end Std

src/Init/Data/Iterators/Lemmas/Combinators/Take.lean

@@ -12,7 +12,8 @@ public import Init.Data.Iterators.Lemmas.Consumers
 
 @[expose] public section
 
-namespace Std.Iterators
+namespace Std
+open Std.Iterators Std.Iterators.Types
 
 theorem Iter.take_eq_toIter_take_toIterM {α β} [Iterator α Id β] {n : Nat}
     {it : Iter (α := α) β} :
@@ -118,4 +119,4 @@ theorem Iter.toList_toTake {α β} [Iterator α Id β] [Finite α Id]
     it.toTake.toList = it.toList := by
   simp [toTake_eq_toIter_toTake_toIterM, toList_eq_toList_toIterM]
 
-end Std.Iterators
+end Std

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

@@ -14,7 +14,8 @@ public import Init.Data.Iterators.Lemmas.Consumers.Loop
 
 public section
 
-namespace Std.Iterators
+namespace Std
+open Std.Iterators
 
 variable {α : Type u} {β : Type u}
 
@@ -66,4 +67,4 @@ theorem Iter.count_uLift [Iterator α Id β] {it : Iter (α := α) β}
   rw [IterM.count_uLift]
   simp [monadLift]
 
-end Std.Iterators
+end Std

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

@@ -16,7 +16,8 @@ import all Init.Data.Iterators.Consumers.Monadic.Total
 
 public section
 
-namespace Std.Iterators
+namespace Std
+open Std.Iterators
 
 theorem Iter.toArray_eq_toArray_toIterM {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id]
     [LawfulIteratorCollect α Id Id] {it : Iter (α := α) β} :
@@ -218,4 +219,4 @@ theorem Iter.isPlausibleIndirectOutput_of_mem_toArray
   rw [← Array.mem_toList_iff] at h
   simpa [toList_toArray] using h
 
-end Std.Iterators
+end Std

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

@@ -15,7 +15,8 @@ import Init.Data.Array.Monadic
 
 public section
 
-namespace Std.Iterators
+namespace Std
+open Std.Iterators
 
 theorem Iter.forIn'_eq {α β : Type w} [Iterator α Id β] [Finite α Id]
     {m : Type x → Type x'} [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [hl : LawfulIteratorLoop α Id m]
@@ -938,4 +939,4 @@ theorem Iter.findM?_pure {α β : Type w} {m : Type w → Type w'} [Monad m]
   · simp [ihs ‹_›]
   · simp
 
-end Std.Iterators
+end Std

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

@@ -15,8 +15,8 @@ import all Init.WFExtrinsicFix
 
 public section
 
-namespace Std.Iterators
-open Std.Internal
+namespace Std
+open Std.Iterators Std.Internal
 
 variable {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
   {lift : ⦃δ : Type w⦄ → m δ → n δ} {f : β → n γ} {it : IterM (α := α) m β}
@@ -263,4 +263,4 @@ theorem LawfulIteratorCollect.toList_eq {α β : Type w} {m : Type w → Type w'
     it.toList = (letI : IteratorCollect α m m := .defaultImplementation; it.toList) := by
   simp [IterM.toList, toArray_eq, -IterM.toList_toArray]
 
-end Std.Iterators
+end Std

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

@@ -12,7 +12,8 @@ import all Init.Data.Iterators.Consumers.Monadic.Loop
 
 public section
 
-namespace Std.Iterators
+namespace Std
+open 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] [LawfulMonad n]
@@ -780,4 +781,4 @@ theorem IterM.findM?_pure {α β : Type w} {m : Type w → Type w'} [Monad m]
   · simp [ihs ‹_›]
   · simp
 
-end Std.Iterators
+end Std

src/Init/Data/Iterators/Lemmas/Monadic/Basic.lean

@@ -10,7 +10,8 @@ public import Init.Data.Iterators.Basic
 
 public section
 
-namespace Std.Iterators
+namespace Std
+open Std.Iterators
 
 /--
 Induction principle for finite monadic iterators: One can define a function `f` that maps every
@@ -46,4 +47,4 @@ def IterM.inductSkips {α m β} [Iterator α m β] [Productive α m]
   step it (fun {it'} _ => inductSkips motive step it')
 termination_by it.finitelyManySkips
 
-end Std.Iterators
+end Std

src/Init/Data/Iterators/Lemmas/Producers/List.lean

@@ -19,34 +19,32 @@ This module provides lemmas about the interactions of `List.iter` with `Iter.ste
 collectors.
 -/
 
-namespace Std.Iterators
+open Std Std.Iterators
 
 variable {β : Type w}
 
 @[simp]
-theorem _root_.List.step_iter_nil :
+theorem List.step_iter_nil :
     (([] : List β).iter).step = ⟨.done, rfl⟩ := by
-  simp [Iter.step, IterM.step, Iterator.step, List.iter, List.iterM, toIterM]
+  simp [Iter.step, IterM.step, Iterator.step, List.iter, List.iterM, IterM.mk]
 
 @[simp]
-theorem _root_.List.step_iter_cons {x : β} {xs : List β} :
+theorem List.step_iter_cons {x : β} {xs : List β} :
     ((x :: xs).iter).step = ⟨.yield xs.iter x, rfl⟩ := by
-  simp [List.iter, List.iterM, toIterM, IterM.toIter, Iter.step, Iter.toIterM, IterM.step,
+  simp [List.iter, List.iterM, IterM.mk, IterM.toIter, Iter.step, Iter.toIterM, IterM.step,
     Iterator.step]
 
 @[simp]
-theorem _root_.List.toArray_iter {l : List β} :
+theorem List.toArray_iter {l : List β} :
     l.iter.toArray = l.toArray := by
   simp [List.iter, List.toArray_iterM, Iter.toArray_eq_toArray_toIterM]
 
 @[simp]
-theorem _root_.List.toList_iter {l : List β} :
+theorem List.toList_iter {l : List β} :
     l.iter.toList = l := by
   simp [List.iter, List.toList_iterM]
 
 @[simp]
-theorem _root_.List.toListRev_iter {l : List β} :
+theorem List.toListRev_iter {l : List β} :
     l.iter.toListRev = l.reverse := by
   simp [List.iter, Iter.toListRev_eq_toListRev_toIterM, List.toListRev_iterM]
-
-end Std.Iterators

src/Init/Data/Iterators/Lemmas/Producers/Monadic/List.lean

@@ -18,28 +18,27 @@ This module provides lemmas about the interactions of `List.iterM` with `IterM.s
 collectors.
 -/
 
-namespace Std.Iterators
-open Std.Internal
+open Std Std.Internal Std.Iterators Std.Iterators.Types
 
 variable {m : Type w → Type w'} {n : Type w → Type w''} [Monad m] {β : Type w}
 
 @[simp]
-theorem _root_.List.step_iterM_nil :
+theorem List.step_iterM_nil :
     (([] : List β).iterM m).step = pure (.deflate ⟨.done, rfl⟩) := by
   simp only [IterM.step, Iterator.step]; rfl
 
 @[simp]
-theorem _root_.List.step_iterM_cons {x : β} {xs : List β} :
+theorem List.step_iterM_cons {x : β} {xs : List β} :
     ((x :: xs).iterM m).step = pure (.deflate ⟨.yield (xs.iterM m) x, rfl⟩) := by
   simp only [List.iterM, IterM.step, Iterator.step]; rfl
 
-theorem _root_.List.step_iterM {l : List β} :
+theorem List.step_iterM {l : List β} :
     (l.iterM m).step = match l with
       | [] => pure (.deflate ⟨.done, rfl⟩)
       | x :: xs => pure (.deflate ⟨.yield (xs.iterM m) x, rfl⟩) := by
   cases l <;> simp [List.step_iterM_cons, List.step_iterM_nil]
 
-theorem ListIterator.toArrayMapped_iterM [Monad n] [LawfulMonad n]
+theorem Std.Iterators.Types.ListIterator.toArrayMapped_iterM [Monad n] [LawfulMonad n]
     {β : Type w} {γ : Type w} {lift : ⦃δ : Type w⦄ → m δ → n δ}
     [LawfulMonadLiftFunction lift] {f : β → n γ} {l : List β} :
     IteratorCollect.toArrayMapped lift f (l.iterM m) (m := m) = List.toArray <$> l.mapM f := by
@@ -53,19 +52,17 @@ theorem ListIterator.toArrayMapped_iterM [Monad n] [LawfulMonad n]
     simp [List.step_iterM_cons, List.mapM_cons, pure_bind, ih, LawfulMonadLiftFunction.lift_pure]
 
 @[simp]
-theorem _root_.List.toArray_iterM [LawfulMonad m] {l : List β} :
+theorem List.toArray_iterM [LawfulMonad m] {l : List β} :
     (l.iterM m).toArray = pure l.toArray := by
   simp only [IterM.toArray, ListIterator.toArrayMapped_iterM]
   rw [List.mapM_pure, map_pure, List.map_id']
 
 @[simp]
-theorem _root_.List.toList_iterM [LawfulMonad m] {l : List β} :
+theorem List.toList_iterM [LawfulMonad m] {l : List β} :
     (l.iterM m).toList = pure l := by
   rw [← IterM.toList_toArray, List.toArray_iterM, map_pure, List.toList_toArray]
 
 @[simp]
-theorem _root_.List.toListRev_iterM [LawfulMonad m] {l : List β} :
+theorem List.toListRev_iterM [LawfulMonad m] {l : List β} :
     (l.iterM m).toListRev = pure l.reverse := by
   simp [IterM.toListRev_eq, List.toList_iterM]
-
-end Std.Iterators

src/Init/Data/Iterators/Producers/List.lean

@@ -10,14 +10,14 @@ public import Init.Data.Iterators.Producers.Monadic.List
 
 @[expose] public section
 
+open Std Std.Iterators Std.Iterators.Types
+
 /-!
 # List iterator
 
 This module provides an iterator for lists that is accessible via `List.iter`.
 -/
 
-namespace Std.Iterators
-
 /--
 Returns a finite iterator for the given list.
 The iterator yields the elements of the list in order and then terminates.
@@ -30,8 +30,6 @@ The monadic version of this iterator is `List.iterM`.
 * `Productive` instance: always
 -/
 @[always_inline, inline]
-def _root_.List.iter {α : Type w} (l : List α) :
+def List.iter {α : Type w} (l : List α) :
     Iter (α := ListIterator α) α :=
   ((l.iterM Id).toIter : Iter α)
-
-end Std.Iterators

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

@@ -17,9 +17,9 @@ public import Init.Data.Iterators.Internal.Termination
 This module provides an iterator for lists that is accessible via `List.iterM`.
 -/
 
-namespace Std.Iterators
+namespace Std
 
-variable {α : Type w} {m : Type w → Type w'}
+namespace Iterators.Types
 
 /--
 The underlying state of a list iterator. Its contents are internal and should
@@ -29,6 +29,12 @@ not be used by downstream users of the library.
 structure ListIterator (α : Type w) where
   list : List α
 
+end Iterators.Types
+
+open Std.Iterators Std.Iterators.Types
+
+variable {α : Type w} {m : Type w → Type w'}
+
 /--
 Returns a finite iterator for the given list.
 The iterator yields the elements of the list in order and then terminates.
@@ -43,19 +49,21 @@ The non-monadic version of this iterator is `List.iter`.
 @[always_inline, inline]
 def _root_.List.iterM {α : Type w} (l : List α) (m : Type w → Type w') [Pure m] :
     IterM (α := ListIterator α) m α :=
-  toIterM { list := l } m α
+  .mk { list := l } m α
+
+namespace Iterators.Types
 
 @[always_inline, inline]
-instance {α : Type w} [Pure m] : Iterator (ListIterator α) m α where
+instance ListIterator.instIterator {α : Type w} [Pure m] : Iterator (ListIterator α) m α where
   IsPlausibleStep it
     | .yield it' out => it.internalState.list = out :: it'.internalState.list
     | .skip _ => False
     | .done => it.internalState.list = []
   step it := pure (match it with
         | ⟨⟨[]⟩⟩ => .deflate ⟨.done, rfl⟩
-        | ⟨⟨x :: xs⟩⟩ => .deflate ⟨.yield (toIterM ⟨xs⟩ m α) x, rfl⟩)
+        | ⟨⟨x :: xs⟩⟩ => .deflate ⟨.yield (.mk ⟨xs⟩ m α) x, rfl⟩)
 
-private def ListIterator.finitenessRelation [Pure m] :
+private def ListIterator.instFinitenessRelation [Pure m] :
     FinitenessRelation (ListIterator α) m where
   rel := InvImage WellFoundedRelation.rel (ListIterator.list ∘ IterM.internalState)
   wf := InvImage.wf _ WellFoundedRelation.wf
@@ -64,17 +72,17 @@ private def ListIterator.finitenessRelation [Pure m] :
     obtain ⟨step, h, h'⟩ := h
     cases step <;> simp_all [IterStep.successor, IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
 
-instance [Pure m] : Finite (ListIterator α) m :=
-  by exact Finite.of_finitenessRelation ListIterator.finitenessRelation
+instance ListIterator.instFinite [Pure m] : Finite (ListIterator α) m :=
+  by exact Finite.of_finitenessRelation ListIterator.instFinitenessRelation
 
 @[always_inline, inline]
-instance {α : Type w} [Monad m] {n : Type w → Type w''} [Monad n] :
+instance ListIterator.instIteratorCollect{α : Type w} [Monad m] {n : Type w → Type w''} [Monad n] :
     IteratorCollect (ListIterator α) m n :=
   .defaultImplementation
 
 @[always_inline, inline]
-instance {α : Type w} [Monad m] {n : Type x → Type x'} [Monad n] :
+instance ListIterator.instIteratorLoop {α : Type w} [Monad m] {n : Type x → Type x'} [Monad n] :
     IteratorLoop (ListIterator α) m n :=
   .defaultImplementation
 
-end Std.Iterators
+end Std.Iterators.Types

src/Init/Data/Iterators/ToIterator.lean

@@ -15,9 +15,7 @@ This module provides the typeclass `ToIterator`, which is implemented by types t
 converted into iterators.
 -/
 
-open Std.Iterators
-
-namespace Std.Iterators
+namespace Std
 
 /-- This typeclass provides an iterator for elements of type `γ`. -/
 class ToIterator (γ : Type u) (m : Type w → Type w') (α β : outParam (Type w)) where
@@ -60,4 +58,4 @@ theorem ToIterator.iter_eq {γ : Type u} {x : γ} {α β : Type v} {it} :
     ToIterator.iter x = (it x).toIter :=
   rfl
 
-end Std.Iterators
+end Std

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

@@ -99,7 +99,7 @@ theorem Iterator.Monadic.isPlausibleStep_iff [UpwardEnumerable α] [LE α] [Deci
 theorem Iterator.Monadic.step_eq_step [UpwardEnumerable α] [LE α] [DecidableLE α]
     {it : IterM (α := Rxc.Iterator α) Id α} :
     it.step = pure (.deflate ⟨Iterator.Monadic.step it, isPlausibleStep_iff.mpr rfl⟩) := by
-  simp [IterM.step, Iterators.Iterator.step]
+  simp [IterM.step, Std.Iterator.step]
 
 theorem Iterator.isPlausibleStep_iff [UpwardEnumerable α] [LE α] [DecidableLE α]
     {it : Iter (α := Rxc.Iterator α) α} {step} :
@@ -679,7 +679,7 @@ theorem Iterator.Monadic.isPlausibleStep_iff [UpwardEnumerable α] [LT α] [Deci
 theorem Iterator.Monadic.step_eq_step [UpwardEnumerable α] [LT α] [DecidableLT α]
     {it : IterM (α := Rxo.Iterator α) Id α} :
     it.step = pure (.deflate ⟨Iterator.Monadic.step it, isPlausibleStep_iff.mpr rfl⟩) := by
-  simp [IterM.step, Iterators.Iterator.step]
+  simp [IterM.step, Std.Iterator.step]
 
 theorem Iterator.isPlausibleStep_iff [UpwardEnumerable α] [LT α] [DecidableLT α]
     {it : Iter (α := Rxo.Iterator α) α} {step} :
@@ -1245,7 +1245,7 @@ theorem Iterator.Monadic.isPlausibleStep_iff [UpwardEnumerable α]
 theorem Iterator.Monadic.step_eq_step [UpwardEnumerable α]
     {it : IterM (α := Rxi.Iterator α) Id α} :
     it.step = pure (.deflate ⟨Iterator.Monadic.step it, isPlausibleStep_iff.mpr rfl⟩) := by
-  simp [IterM.step, Iterators.Iterator.step]
+  simp [IterM.step, Std.Iterator.step]
 
 theorem Iterator.isPlausibleStep_iff [UpwardEnumerable α]
     {it : Iter (α := Rxi.Iterator α) α} {step} :

src/Init/Data/Slice/List/Lemmas.lean

@@ -15,12 +15,10 @@ import all Init.Data.Range.Polymorphic.Lemmas
 public import Init.Data.Slice.Lemmas
 public import Init.Data.Iterators.Lemmas
 
-open Std.Iterators Std.PRange
+open Std Std.PRange Std.Slice
 
 namespace ListSlice
 
-open Std.Slice
-
 theorem internalIter_eq {α : Type u} {s : ListSlice α} :
     Internal.iter s = match s.internalRepresentation.stop with
         | some stop => s.internalRepresentation.list.iter.take stop

src/Init/Data/String/Lemmas/Search.lean

@@ -12,11 +12,11 @@ import all Init.Data.String.Search
 public section
 
 namespace String
-open String.Slice Pattern
+open Std String.Slice Pattern
 
 variable {ρ : Type} {σ : Slice → Type}
-variable [∀ s, Std.Iterators.Iterator (σ s) Id (SearchStep s)]
-variable [∀ s, Std.Iterators.IteratorLoop (σ s) Id Id]
+variable [∀ s, Std.Iterator (σ s) Id (SearchStep s)]
+variable [∀ s, Std.IteratorLoop (σ s) Id Id]
 
 @[simp]
 theorem Slice.Pos.le_find {s : Slice} (pos : s.Pos) (pattern : ρ) [ToForwardSearcher pattern σ] :

src/Init/Data/String/Pattern/Basic.lean

@@ -125,7 +125,7 @@ end Internal
 namespace ForwardPattern
 
 variable {ρ : Type} {σ : Slice → Type}
-variable [∀ s, Std.Iterators.Iterator (σ s) Id (SearchStep s)]
+variable [∀ s, Std.Iterator (σ s) Id (SearchStep s)]
 variable (pat : ρ) [ToForwardSearcher pat σ]
 
 @[specialize pat]
@@ -184,7 +184,7 @@ class BackwardPattern {ρ : Type} (pat : ρ) where
 namespace ToBackwardSearcher
 
 variable {ρ : Type} {σ : Slice → Type}
-variable [∀ s, Std.Iterators.Iterator (σ s) Id (SearchStep s)]
+variable [∀ s, Std.Iterator (σ s) Id (SearchStep s)]
 variable (pat : ρ) [ToBackwardSearcher pat σ]
 
 @[specialize pat]

src/Init/Data/String/Pattern/Char.lean

@@ -31,7 +31,7 @@ namespace ForwardCharSearcher
 def iter (c : Char) (s : Slice) : Std.Iter (α := ForwardCharSearcher c s) (SearchStep s) :=
   { internalState := { currPos := s.startPos }}
 
-instance (s : Slice) : Std.Iterators.Iterator (ForwardCharSearcher c s) Id (SearchStep s) where
+instance (s : Slice) : Std.Iterator (ForwardCharSearcher c s) Id (SearchStep s) where
   IsPlausibleStep it
     | .yield it' out =>
       ∃ h1 : it.internalState.currPos ≠ s.endPos,
@@ -74,7 +74,7 @@ def finitenessRelation : Std.Iterators.FinitenessRelation (ForwardCharSearcher s
 instance : Std.Iterators.Finite (ForwardCharSearcher s c) Id :=
   .of_finitenessRelation finitenessRelation
 
-instance : Std.Iterators.IteratorLoop (ForwardCharSearcher s c) Id Id :=
+instance : Std.IteratorLoop (ForwardCharSearcher s c) Id Id :=
   .defaultImplementation
 
 instance {c : Char} : ToForwardSearcher c (ForwardCharSearcher c) where
@@ -95,7 +95,7 @@ namespace BackwardCharSearcher
 def iter (c : Char) (s : Slice) : Std.Iter (α := BackwardCharSearcher s) (SearchStep s) :=
   { internalState := { currPos := s.endPos, needle := c }}
 
-instance (s : Slice) : Std.Iterators.Iterator (BackwardCharSearcher s) Id (SearchStep s) where
+instance (s : Slice) : Std.Iterator (BackwardCharSearcher s) Id (SearchStep s) where
   IsPlausibleStep it
     | .yield it' out =>
       it.internalState.needle = it'.internalState.needle ∧
@@ -139,7 +139,7 @@ def finitenessRelation : Std.Iterators.FinitenessRelation (BackwardCharSearcher
 instance : Std.Iterators.Finite (BackwardCharSearcher s) Id :=
   .of_finitenessRelation finitenessRelation
 
-instance : Std.Iterators.IteratorLoop (BackwardCharSearcher s) Id Id :=
+instance : Std.IteratorLoop (BackwardCharSearcher s) Id Id :=
   .defaultImplementation
 
 instance {c : Char} : ToBackwardSearcher c BackwardCharSearcher where

src/Init/Data/String/Pattern/Pred.lean

@@ -32,7 +32,7 @@ namespace ForwardCharPredSearcher
 def iter (p : Char → Bool) (s : Slice) : Std.Iter (α := ForwardCharPredSearcher p s) (SearchStep s) :=
   { internalState := { currPos := s.startPos }}
 
-instance (s : Slice) : Std.Iterators.Iterator (ForwardCharPredSearcher p s) Id (SearchStep s) where
+instance (s : Slice) : Std.Iterator (ForwardCharPredSearcher p s) Id (SearchStep s) where
   IsPlausibleStep it
     | .yield it' out =>
       ∃ h1 : it.internalState.currPos ≠ s.endPos,
@@ -76,7 +76,7 @@ def finitenessRelation : Std.Iterators.FinitenessRelation (ForwardCharPredSearch
 instance : Std.Iterators.Finite (ForwardCharPredSearcher p s) Id :=
   .of_finitenessRelation finitenessRelation
 
-instance : Std.Iterators.IteratorLoop (ForwardCharPredSearcher p s) Id Id :=
+instance : Std.IteratorLoop (ForwardCharPredSearcher p s) Id Id :=
   .defaultImplementation
 
 @[default_instance]
@@ -105,7 +105,7 @@ namespace BackwardCharPredSearcher
 def iter (c : Char → Bool) (s : Slice) : Std.Iter (α := BackwardCharPredSearcher s) (SearchStep s) :=
   { internalState := { currPos := s.endPos, needle := c }}
 
-instance (s : Slice) : Std.Iterators.Iterator (BackwardCharPredSearcher s) Id (SearchStep s) where
+instance (s : Slice) : Std.Iterator (BackwardCharPredSearcher s) Id (SearchStep s) where
   IsPlausibleStep it
     | .yield it' out =>
       it.internalState.needle = it'.internalState.needle ∧
@@ -152,7 +152,7 @@ def finitenessRelation : Std.Iterators.FinitenessRelation (BackwardCharPredSearc
 instance : Std.Iterators.Finite (BackwardCharPredSearcher s) Id :=
   .of_finitenessRelation finitenessRelation
 
-instance : Std.Iterators.IteratorLoop (BackwardCharPredSearcher s) Id Id :=
+instance : Std.IteratorLoop (BackwardCharPredSearcher s) Id Id :=
   .defaultImplementation
 
 @[default_instance]

src/Init/Data/String/Pattern/String.lean

@@ -91,7 +91,7 @@ def iter (pat : Slice) (s : Slice) : Std.Iter (α := ForwardSliceSearcher s) (Se
     { internalState := .proper pat (buildTable pat) rfl s.startPos.offset pat.startPos.offset
         (by simp [Pos.Raw.lt_iff]; omega) }
 
-instance (s : Slice) : Std.Iterators.Iterator (ForwardSliceSearcher s) Id (SearchStep s) where
+instance (s : Slice) : Std.Iterator (ForwardSliceSearcher s) Id (SearchStep s) where
   IsPlausibleStep it
     | .yield it' out | .skip it' =>
      match it.internalState with
@@ -232,7 +232,7 @@ private def finitenessRelation :
     all_goals try
       cases h
       revert h'
-      simp only [Std.Iterators.IterM.IsPlausibleStep, Std.Iterators.Iterator.IsPlausibleStep]
+      simp only [Std.IterM.IsPlausibleStep, Std.Iterator.IsPlausibleStep]
       match it.internalState with
       | .emptyBefore pos =>
         rintro (⟨h, h'⟩|h') <;> simp [h', ForwardSliceSearcher.toOption, Option.lt, Prod.lex_def]
@@ -253,10 +253,10 @@ private def finitenessRelation :
 instance : Std.Iterators.Finite (ForwardSliceSearcher s) Id :=
   .of_finitenessRelation finitenessRelation
 
-instance : Std.Iterators.IteratorCollect (ForwardSliceSearcher s) Id Id :=
+instance : Std.IteratorCollect (ForwardSliceSearcher s) Id Id :=
   .defaultImplementation
 
-instance : Std.Iterators.IteratorLoop (ForwardSliceSearcher s) Id Id :=
+instance : Std.IteratorLoop (ForwardSliceSearcher s) Id Id :=
   .defaultImplementation
 
 instance {pat : Slice} : ToForwardSearcher pat ForwardSliceSearcher where

src/Init/Data/String/Search.lean

@@ -25,9 +25,9 @@ section
 open String.Slice Pattern
 
 variable {ρ : Type} {σ : Slice → Type}
-variable [∀ s, Std.Iterators.Iterator (σ s) Id (SearchStep s)]
+variable [∀ s, Std.Iterator (σ s) Id (SearchStep s)]
 variable [∀ s, Std.Iterators.Finite (σ s) Id]
-variable [∀ s, Std.Iterators.IteratorLoop (σ s) Id Id]
+variable [∀ s, Std.IteratorLoop (σ s) Id Id]
 
 
 /--

src/Init/Data/String/Slice.lean

@@ -100,9 +100,9 @@ instance : DecidableLE Slice :=
 section ForwardPatternUsers
 
 variable {ρ : Type} {σ : Slice → Type}
-variable [∀ s, Std.Iterators.Iterator (σ s) Id (SearchStep s)]
+variable [∀ s, Std.Iterator (σ s) Id (SearchStep s)]
 variable [∀ s, Std.Iterators.Finite (σ s) Id]
-variable [∀ s, Std.Iterators.IteratorLoop (σ s) Id Id]
+variable [∀ s, Std.IteratorLoop (σ s) Id Id]
 
 /--
 Checks whether the slice ({name}`s`) begins with the pattern ({name}`pat`).
@@ -131,7 +131,7 @@ variable {pat : ρ} [ToForwardSearcher pat σ]
 
 inductive PlausibleStep
 
-instance : Std.Iterators.Iterator (SplitIterator pat s) Id Slice where
+instance : Std.Iterator (SplitIterator pat s) Id Slice where
   IsPlausibleStep
     | ⟨.operating _ s⟩, .yield ⟨.operating _ s'⟩ _ => s'.IsPlausibleSuccessorOf s
     | ⟨.operating _ s⟩, .yield ⟨.atEnd ..⟩ _ => True
@@ -165,8 +165,8 @@ private def toOption : SplitIterator pat s → Option (Std.Iter (α := σ s) (Se
 
 private def finitenessRelation [Std.Iterators.Finite (σ s) Id] :
     Std.Iterators.FinitenessRelation (SplitIterator pat s) Id where
-  rel := InvImage (Option.lt Std.Iterators.Iter.IsPlausibleSuccessorOf)
-    (SplitIterator.toOption ∘ Std.Iterators.IterM.internalState)
+  rel := InvImage (Option.lt Std.Iter.IsPlausibleSuccessorOf)
+    (SplitIterator.toOption ∘ Std.IterM.internalState)
   wf := InvImage.wf _ (Option.wellFounded_lt Std.Iterators.Finite.wf_of_id)
   subrelation {it it'} h := by
     simp_wf
@@ -174,7 +174,7 @@ private def finitenessRelation [Std.Iterators.Finite (σ s) Id] :
     match step with
     | .yield it'' out | .skip it'' =>
       obtain rfl : it' = it'' := by simpa using h.symm
-      simp only [Std.Iterators.IterM.IsPlausibleStep, Std.Iterators.Iterator.IsPlausibleStep] at h'
+      simp only [Std.IterM.IsPlausibleStep, Std.Iterator.IsPlausibleStep] at h'
       revert h'
       match it, it' with
       | ⟨.operating _ searcher⟩, ⟨.operating _ searcher'⟩ => simp [SplitIterator.toOption, Option.lt]
@@ -185,10 +185,10 @@ private def finitenessRelation [Std.Iterators.Finite (σ s) Id] :
 instance [Std.Iterators.Finite (σ s) Id] : Std.Iterators.Finite (SplitIterator pat s) Id :=
   .of_finitenessRelation finitenessRelation
 
-instance [Monad n] : Std.Iterators.IteratorCollect (SplitIterator pat s) Id n :=
+instance [Monad n] : Std.IteratorCollect (SplitIterator pat s) Id n :=
   .defaultImplementation
 
-instance [Monad n] : Std.Iterators.IteratorLoop (SplitIterator pat s) Id n :=
+instance [Monad n] : Std.IteratorLoop (SplitIterator pat s) Id n :=
   .defaultImplementation
 
 end SplitIterator
@@ -221,7 +221,7 @@ namespace SplitInclusiveIterator
 
 variable {pat : ρ} [ToForwardSearcher pat σ]
 
-instance : Std.Iterators.Iterator (SplitInclusiveIterator pat s) Id Slice where
+instance : Std.Iterator (SplitInclusiveIterator pat s) Id Slice where
   IsPlausibleStep
     | ⟨.operating _ s⟩, .yield ⟨.operating _ s'⟩ _ => s'.IsPlausibleSuccessorOf s
     | ⟨.operating _ s⟩, .yield ⟨.atEnd ..⟩ _ => True
@@ -259,8 +259,8 @@ private def toOption : SplitInclusiveIterator pat s → Option (Std.Iter (α :=
 
 private def finitenessRelation [Std.Iterators.Finite (σ s) Id] :
     Std.Iterators.FinitenessRelation (SplitInclusiveIterator pat s) Id where
-  rel := InvImage (Option.lt Std.Iterators.Iter.IsPlausibleSuccessorOf)
-    (SplitInclusiveIterator.toOption ∘ Std.Iterators.IterM.internalState)
+  rel := InvImage (Option.lt Std.Iter.IsPlausibleSuccessorOf)
+    (SplitInclusiveIterator.toOption ∘ Std.IterM.internalState)
   wf := InvImage.wf _ (Option.wellFounded_lt Std.Iterators.Finite.wf_of_id)
   subrelation {it it'} h := by
     simp_wf
@@ -268,7 +268,7 @@ private def finitenessRelation [Std.Iterators.Finite (σ s) Id] :
     match step with
     | .yield it'' out | .skip it'' =>
       obtain rfl : it' = it'' := by simpa using h.symm
-      simp only [Std.Iterators.IterM.IsPlausibleStep, Std.Iterators.Iterator.IsPlausibleStep] at h'
+      simp only [Std.IterM.IsPlausibleStep, Std.Iterator.IsPlausibleStep] at h'
       revert h'
       match it, it' with
       | ⟨.operating _ searcher⟩, ⟨.operating _ searcher'⟩ => simp [SplitInclusiveIterator.toOption, Option.lt]
@@ -281,11 +281,11 @@ instance [Std.Iterators.Finite (σ s) Id] :
   .of_finitenessRelation finitenessRelation
 
 instance [Monad n] {s} :
-    Std.Iterators.IteratorCollect (SplitInclusiveIterator pat s) Id n :=
+    Std.IteratorCollect (SplitInclusiveIterator pat s) Id n :=
   .defaultImplementation
 
 instance [Monad n] {s} :
-    Std.Iterators.IteratorLoop (SplitInclusiveIterator pat s) Id n :=
+    Std.IteratorLoop (SplitInclusiveIterator pat s) Id n :=
   .defaultImplementation
 
 end SplitInclusiveIterator
@@ -537,9 +537,9 @@ end ForwardPatternUsers
 section BackwardPatternUsers
 
 variable {σ : Slice → Type}
-variable [∀ s, Std.Iterators.Iterator (σ s) Id (SearchStep s)]
+variable [∀ s, Std.Iterator (σ s) Id (SearchStep s)]
 variable [∀ s, Std.Iterators.Finite (σ s) Id]
-variable [∀ s, Std.Iterators.IteratorLoop (σ s) Id Id]
+variable [∀ s, Std.IteratorLoop (σ s) Id Id]
 
 /--
 Checks whether the slice ({name}`s`) ends with the pattern ({name}`pat`).
@@ -566,7 +566,7 @@ namespace RevSplitIterator
 
 variable [ToBackwardSearcher ρ σ]
 
-instance [Pure m] : Std.Iterators.Iterator (RevSplitIterator ρ s) m Slice where
+instance [Pure m] : Std.Iterator (RevSplitIterator ρ s) m Slice where
   IsPlausibleStep
     | ⟨.operating _ s⟩, .yield ⟨.operating _ s'⟩ _ => s'.IsPlausibleSuccessorOf s
     | ⟨.operating _ s⟩, .yield ⟨.atEnd ..⟩ _ => True
@@ -603,8 +603,8 @@ private def toOption : RevSplitIterator ρ s → Option (Std.Iter (α := σ s) (
 
 private def finitenessRelation [Std.Iterators.Finite (σ s) Id] :
     Std.Iterators.FinitenessRelation (RevSplitIterator ρ s) Id where
-  rel := InvImage (Option.lt Std.Iterators.Iter.IsPlausibleSuccessorOf)
-    (RevSplitIterator.toOption ∘ Std.Iterators.IterM.internalState)
+  rel := InvImage (Option.lt Std.Iter.IsPlausibleSuccessorOf)
+    (RevSplitIterator.toOption ∘ Std.IterM.internalState)
   wf := InvImage.wf _ (Option.wellFounded_lt Std.Iterators.Finite.wf_of_id)
   subrelation {it it'} h := by
     simp_wf
@@ -612,7 +612,7 @@ private def finitenessRelation [Std.Iterators.Finite (σ s) Id] :
     match step with
     | .yield it'' out | .skip it'' =>
       obtain rfl : it' = it'' := by simpa using h.symm
-      simp only [Std.Iterators.IterM.IsPlausibleStep, Std.Iterators.Iterator.IsPlausibleStep] at h'
+      simp only [Std.IterM.IsPlausibleStep, Std.Iterator.IsPlausibleStep] at h'
       revert h'
       match it, it' with
       | ⟨.operating _ searcher⟩, ⟨.operating _ searcher'⟩ => simp [RevSplitIterator.toOption, Option.lt]
@@ -623,10 +623,10 @@ private def finitenessRelation [Std.Iterators.Finite (σ s) Id] :
 instance [Std.Iterators.Finite (σ s) Id] : Std.Iterators.Finite (RevSplitIterator ρ s) Id :=
   .of_finitenessRelation finitenessRelation
 
-instance [Monad m] [Monad n] : Std.Iterators.IteratorCollect (RevSplitIterator ρ s) m n :=
+instance [Monad m] [Monad n] : Std.IteratorCollect (RevSplitIterator ρ s) m n :=
   .defaultImplementation
 
-instance [Monad m] [Monad n] : Std.Iterators.IteratorLoop (RevSplitIterator ρ s) m n :=
+instance [Monad m] [Monad n] : Std.IteratorLoop (RevSplitIterator ρ s) m n :=
   .defaultImplementation
 
 end RevSplitIterator
@@ -861,7 +861,7 @@ set_option doc.verso true
 namespace PosIterator
 
 instance [Pure m] :
-    Std.Iterators.Iterator (PosIterator s) m { p : s.Pos // p ≠ s.endPos } where
+    Std.Iterator (PosIterator s) m { p : s.Pos // p ≠ s.endPos } where
   IsPlausibleStep it
     | .yield it' out =>
       ∃ h : it.internalState.currPos ≠ s.endPos,
@@ -897,10 +897,10 @@ private def finitenessRelation [Pure m] :
 instance [Pure m] : Std.Iterators.Finite (PosIterator s) m :=
   .of_finitenessRelation finitenessRelation
 
-instance [Monad m] [Monad n] : Std.Iterators.IteratorCollect (PosIterator s) m n :=
+instance [Monad m] [Monad n] : Std.IteratorCollect (PosIterator s) m n :=
   .defaultImplementation
 
-instance [Monad m] [Monad n] : Std.Iterators.IteratorLoop (PosIterator s) m n :=
+instance [Monad m] [Monad n] : Std.IteratorLoop (PosIterator s) m n :=
   .defaultImplementation
 
 docs_to_verso positions
@@ -916,7 +916,7 @@ Examples:
 -/
 @[expose, inline]
 def chars (s : Slice) :=
-  Std.Iterators.Iter.map (fun ⟨pos, h⟩ => pos.get h) (positions s)
+  Std.Iter.map (fun ⟨pos, h⟩ => pos.get h) (positions s)
 
 @[deprecated "There is no constant-time length function on slices. Use `s.positions.count` instead, or `isEmpty` if you only need to know whether the slice is empty." (since := "2025-11-20")]
 def length (s : Slice) : Nat :=
@@ -945,7 +945,7 @@ set_option doc.verso true
 namespace RevPosIterator
 
 instance [Pure m] :
-    Std.Iterators.Iterator (RevPosIterator s) m { p : s.Pos // p ≠ s.endPos } where
+    Std.Iterator (RevPosIterator s) m { p : s.Pos // p ≠ s.endPos } where
   IsPlausibleStep it
     | .yield it' out =>
       ∃ h : it.internalState.currPos ≠ s.startPos,
@@ -981,10 +981,10 @@ private def finitenessRelation [Pure m] :
 instance [Pure m] : Std.Iterators.Finite (RevPosIterator s) m :=
   .of_finitenessRelation finitenessRelation
 
-instance [Monad m] [Monad n] : Std.Iterators.IteratorCollect (RevPosIterator s) m n :=
+instance [Monad m] [Monad n] : Std.IteratorCollect (RevPosIterator s) m n :=
   .defaultImplementation
 
-instance [Monad m] [Monad n] : Std.Iterators.IteratorLoop (RevPosIterator s) m n :=
+instance [Monad m] [Monad n] : Std.IteratorLoop (RevPosIterator s) m n :=
   .defaultImplementation
 
 docs_to_verso revPositions
@@ -1001,7 +1001,7 @@ Example:
 -/
 @[expose, inline]
 def revChars (s : Slice) :=
-  Std.Iterators.Iter.map (fun ⟨pos, h⟩ => pos.get h) (revPositions s)
+  Std.Iter.map (fun ⟨pos, h⟩ => pos.get h) (revPositions s)
 
 structure ByteIterator where
   s : Slice
@@ -1023,7 +1023,7 @@ set_option doc.verso true
 
 namespace ByteIterator
 
-instance [Pure m] : Std.Iterators.Iterator ByteIterator m UInt8 where
+instance [Pure m] : Std.Iterator ByteIterator m UInt8 where
   IsPlausibleStep it
     | .yield it' out =>
       ∃ h1 : it.internalState.offset < it.internalState.s.rawEndPos,
@@ -1061,10 +1061,10 @@ private def finitenessRelation [Pure m] :
 instance [Pure m] : Std.Iterators.Finite ByteIterator m :=
   .of_finitenessRelation finitenessRelation
 
-instance [Monad m] [Monad n] : Std.Iterators.IteratorCollect ByteIterator m n :=
+instance [Monad m] [Monad n] : Std.IteratorCollect ByteIterator m n :=
   .defaultImplementation
 
-instance [Monad m] [Monad n] : Std.Iterators.IteratorLoop ByteIterator m n :=
+instance [Monad m] [Monad n] : Std.IteratorLoop ByteIterator m n :=
   .defaultImplementation
 
 docs_to_verso bytes
@@ -1097,7 +1097,7 @@ instance : Inhabited RevByteIterator where
 
 namespace RevByteIterator
 
-instance [Pure m] : Std.Iterators.Iterator RevByteIterator m UInt8 where
+instance [Pure m] : Std.Iterator RevByteIterator m UInt8 where
   IsPlausibleStep it
     | .yield it' out =>
       ∃ h1 : it.internalState.offset.dec < it.internalState.s.rawEndPos,
@@ -1142,10 +1142,10 @@ private def finitenessRelation [Pure m] :
 instance [Pure m] : Std.Iterators.Finite RevByteIterator m :=
   .of_finitenessRelation finitenessRelation
 
-instance [Monad m] [Monad n] : Std.Iterators.IteratorCollect RevByteIterator m n :=
+instance [Monad m] [Monad n] : Std.IteratorCollect RevByteIterator m n :=
   .defaultImplementation
 
-instance [Monad m] [Monad n] : Std.Iterators.IteratorLoop RevByteIterator m n :=
+instance [Monad m] [Monad n] : Std.IteratorLoop RevByteIterator m n :=
   .defaultImplementation
 
 docs_to_verso revBytes
@@ -1184,7 +1184,7 @@ Examples:
 -/
 @[inline]
 def foldl {α : Type u} (f : α → Char → α) (init : α) (s : Slice) : α :=
-  Std.Iterators.Iter.fold f init (chars s)
+  Std.Iter.fold f init (chars s)
 
 /--
 Folds a function over a slice from the end, accumulating a value starting with {name}`init`. The
@@ -1197,7 +1197,7 @@ Examples:
 -/
 @[inline]
 def foldr {α : Type u} (f : Char → α → α) (init : α) (s : Slice) : α :=
-  Std.Iterators.Iter.fold (flip f) init (revChars s)
+  Std.Iter.fold (flip f) init (revChars s)
 
 /--
 Checks whether the slice can be interpreted as the decimal representation of a natural number.
@@ -1455,13 +1455,13 @@ end String.Slice
 
 /-- Converts a {lean}`Std.Iter String.Slice` to a {lean}`List String`. -/
 @[inline]
-def Std.Iterators.Iter.toStringList {α : Type} [Std.Iterators.Iterator α Id String.Slice]
-    [Std.Iterators.Finite α Id] [Std.Iterators.IteratorCollect α Id Id]
+def Std.Iter.toStringList {α : Type} [Std.Iterator α Id String.Slice]
+    [Std.Iterators.Finite α Id] [Std.IteratorCollect α Id Id]
     (i : Std.Iter (α := α) String.Slice) : List String :=
   i.map String.Slice.copy |>.toList
 
 /-- Converts a {lean}`Std.Iter String.Slice` to an {lean}`Array String`. -/
-def Std.Iterators.Iter.toStringArray {α : Type} [Std.Iterators.Iterator α Id String.Slice]
-    [Std.Iterators.Finite α Id] [Std.Iterators.IteratorCollect α Id Id]
+def Std.Iter.toStringArray {α : Type} [Std.Iterator α Id String.Slice]
+    [Std.Iterators.Finite α Id] [Std.IteratorCollect α Id Id]
     (i : Std.Iter (α := α) String.Slice) : Array String :=
   i.map String.Slice.copy |>.toArray

src/Init/Grind/Attr.lean

@@ -143,7 +143,7 @@ the `grind_pattern` command, which lets you specify how `grind` should
 match and use particular theorems.
 
 Example:
-- `grind [usr myThm]` means `grind` is using `myThm`, but with the
+- `grind [usr myThm]` means `grind` is using `myThm`, but with
   the custom pattern you defined with `grind_pattern`.
 -/
 syntax grindUsr    := &"usr"

src/Init/Grind/Ordered/Linarith.lean

@@ -554,4 +554,13 @@ theorem eq_eq_subst {α} [IntModule α] (ctx : Context α) (x : Var) (p₁ p₂
     : eq_eq_subst_cert x p₁ p₂ p₃ → p₁.denote' ctx = 0 → p₂.denote' ctx = 0 → p₃.denote' ctx = 0 := by
   simp [eq_eq_subst_cert]; intro _ h₁ h₂; subst p₃; simp [h₁, h₂]
 
+def imp_eq_cert (p : Poly) (x y : Var) : Bool :=
+  p == .add 1 x (.add (-1) y .nil)
+
+theorem imp_eq {α} [IntModule α] (ctx : Context α) (p : Poly) (x y : Var)
+    : imp_eq_cert p x y → p.denote' ctx = 0 → x.denote ctx = y.denote ctx := by
+  simp [imp_eq_cert]; intro; subst p; simp [Poly.denote]
+  rw [neg_zsmul, ← sub_eq_add_neg, one_zsmul, sub_eq_zero_iff]
+  simp
+
 end Lean.Grind.Linarith

src/Init/Prelude.lean

@@ -2075,6 +2075,13 @@ protected def Nat.sub : (@& Nat) → (@& Nat) → Nat
 
 attribute [gen_constructor_elims] Nat
 
+-- Grind setup for Nat.ctorIdx, the built-in propagator for `.ctorIdx` does not kick in
+-- due to the special representation of Nat constructors.
+protected theorem Nat.ctorIdx_zero : Eq (Nat.ctorIdx 0) 0 := rfl
+protected theorem Nat.ctorIdx_succ : Eq (Nat.ctorIdx (succ n)) 1 := rfl
+grind_pattern Nat.ctorIdx_zero => Nat.ctorIdx 0
+grind_pattern Nat.ctorIdx_succ => Nat.ctorIdx (.succ n)
+
 instance instSubNat : Sub Nat where
   sub := Nat.sub
 

src/Lean/Elab/Parallel.lean

@@ -63,7 +63,7 @@ information. For consumers that require `Finite` (like `.toList`), use `.allowNo
 
 public section
 
-namespace Std.Iterators
+namespace Std.Iterators.Types
 
 /--
 Internal state for an iterator over tasks.
@@ -85,14 +85,14 @@ private instance {α : Type} : Iterator (TaskIterator α) BaseIO α where
         have hlen : 0 < (task :: rest).length := by simp
         let (result, remaining) ← IO.waitAny' (task :: rest) hlen
         pure <| .deflate ⟨
-          .yield (Std.Iterators.toIterM { tasks := remaining } BaseIO α) result,
+          .yield (.mk { tasks := remaining } BaseIO α) result,
           trivial⟩
 
-end Std.Iterators
+end Std.Iterators.Types
 
 namespace IO
 
-open Std.Iterators
+open Std Std.Iterators.Types
 
 /--
 Creates an iterator over a list of tasks that yields results in completion order.
@@ -117,7 +117,7 @@ for result in iter do
 ```
 -/
 private def iterTasks {α : Type} (tasks : List (Task α)) : IterM (α := TaskIterator α) BaseIO α :=
-  Std.Iterators.toIterM { tasks } BaseIO α
+  .mk { tasks } BaseIO α
 
 end IO
 

src/Lean/Elab/SyntheticMVars.lean

@@ -523,7 +523,9 @@ mutual
             if !e.isFVar then
               e ← mvarId'.withContext do
                 withExporting (isExporting := wasExporting) do
-                  abstractProof e
+                  -- Like `abstractProof`, but use the expected and not given type here as
+                  -- the latter might not make sense outside the current module (#11672).
+                  mkAuxTheorem (cache := !e.hasSorry) (← mvarId.getType) e (zetaDelta := true)
             mvarId.assign e)
       fun ex => do
         if report then

src/Lean/Meta/Constructions.lean

@@ -12,3 +12,4 @@ public import Lean.Meta.Constructions.RecOn
 public import Lean.Meta.Constructions.BRecOn
 public import Lean.Meta.Constructions.CasesOnSameCtor
 public import Lean.Meta.Constructions.SparseCasesOn
+public import Lean.Meta.Constructions.SparseCasesOnEq

src/Lean/Meta/Constructions/SparseCasesOn.lean

@@ -29,6 +29,19 @@ deriving BEq, Hashable
 private builtin_initialize sparseCasesOnCacheExt : EnvExtension (PHashMap SparseCasesOnKey Name) ←
   registerEnvExtension (pure {}) (asyncMode := .local)  -- mere cache, keep it local
 
+/-- Information necessary to recognize and split on sparse casesOn (in particular in MatchEqs) -/
+public structure SparseCasesOnInfo where
+  indName : Name
+  majorPos : Nat
+  arity : Nat
+  insterestingCtors : Array Name
+deriving Inhabited
+
+private builtin_initialize sparseCasesOnInfoExt : MapDeclarationExtension SparseCasesOnInfo ←
+  mkMapDeclarationExtension (exportEntriesFn := fun env s _ =>
+    -- Do not export for non-exposed defs
+    s.filter (fun n _ => env.find? n |>.any (·.hasValue)) |>.toArray)
+
 /--
 This module creates sparse variants of `casesOn` that have arms only for some of the constructors,
 offering a catch-all.
@@ -94,7 +107,7 @@ public def mkSparseCasesOn (indName : Name) (ctors : Array Name) : MetaM Name :=
     let e := casesOnInfo.value!
     let e := mkAppN e params
     let motive' ← id do
-      mkLambdaFVars ism (← mkArrow catchAllType (mkAppN motive ism))
+      mkLambdaFVars ism (mkForall (← mkFreshUserName `else) BinderInfo.default catchAllType (mkAppN motive ism))
     let e := mkApp e motive'
     let e := mkAppN e indices
     let e := mkApp e major
@@ -123,8 +136,19 @@ public def mkSparseCasesOn (indName : Name) (ctors : Array Name) : MetaM Name :=
   addDecl (.defnDecl decl)
   modifyEnv fun env => sparseCasesOnCacheExt.modifyState env fun s => s.insert key declName
   setReducibleAttribute declName
-  modifyEnv fun env => markAuxRecursor env declName -- TODO: is this right?
   modifyEnv fun env => markSparseCasesOn env declName
+  modifyEnv fun env => sparseCasesOnInfoExt.insert env declName {
+    indName
+    majorPos := indInfo.numParams + 1 + indInfo.numIndices,
+    arity := indInfo.numParams + 1 + indInfo.numIndices + 1 + ctors.size + 1
+    insterestingCtors := ctors
+  }
+  enableRealizationsForConst declName
   pure declName
 
-end Lean.Meta
+public def getSparseCasesOnInfoCore (env : Environment) (sparseCasesOnName : Name) : (Option SparseCasesOnInfo) := do
+  sparseCasesOnInfoExt.find? env sparseCasesOnName
+
+public def getSparseCasesOnInfo (sparseCasesOnName : Name) : CoreM (Option SparseCasesOnInfo) := do
+  let env ← getEnv
+  return sparseCasesOnInfoExt.find? env sparseCasesOnName

src/Lean/Meta/Constructions/SparseCasesOnEq.lean

@@ -0,0 +1,103 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joachim Breitner
+-/
+
+module
+
+prelude
+public import Lean.Meta.Basic
+import Lean.AddDecl
+import Lean.Meta.Constructions.SparseCasesOn
+import Lean.Meta.AppBuilder
+import Lean.Meta.HasNotBit
+import Lean.Meta.Tactic.Util
+import Lean.Meta.Tactic.Cases
+import Lean.Meta.Tactic.Refl
+
+namespace Lean.Meta
+
+/--
+Given a sparseCasesOn, creates an equational theorem for the else-case.
+-/
+public def getSparseCasesOnEq (sparseCasesOnName : Name) : MetaM Name := do
+  let thmName := sparseCasesOnName.str "else_eq"
+  realizeConst sparseCasesOnName thmName (realize thmName)
+  return thmName
+where
+  realize thmName := do
+    let some casesOnInfo ← getSparseCasesOnInfo sparseCasesOnName
+      | throwError "mkSparseCasesOnEq: {sparseCasesOnName} is not a sparse casesOn combinator"
+    let info ← getConstVal sparseCasesOnName
+    let us := info.levelParams.map mkLevelParam
+    forallTelescope info.type fun xs _ => do
+      let otherAlt := xs.back!
+      forallTelescope (← inferType otherAlt) fun hyps _ => do
+        assert! hyps.size = 1
+        let hyp := hyps[0]!
+        let lhs := mkAppN (mkConst sparseCasesOnName us) xs
+        let rhs := mkAppN otherAlt hyps
+        let eq ← mkEq lhs rhs
+        let val ← mkFreshExprSyntheticOpaqueMVar eq
+        let mvarId := val.mvarId!
+        -- We separate `hasNotBit mask x.ctorIdx` into `hasNotBit mask i` and `i = x.ctorIdx`
+        -- to prevent the kernel from running into #11181
+        -- (Even with #11181 fixes this may be necessary to avoid the kernel from reducing
+        -- `hasNotBit` without native nat computation)
+        let_expr Nat.hasNotBit mask ctorIdxApp := (← inferType hyp) | throwError "mkSparseCasesOnEq: unexpected hyp type {← inferType hyp}"
+        -- Simulate `generalize h : x.ctorIdx = i`
+        let mvarId ← mvarId.assertExt `idx (type := mkConst ``Nat) (val := ctorIdxApp) `hidx
+        let (ctorIdxApp, mvarId) ← mvarId.intro1P
+        let (ctorIdxAppEq, mvarId) ← mvarId.intro1P
+        mvarId.withContext do
+        let hyp'Type := mkApp2 (mkConst ``Nat.hasNotBit) mask (mkFVar ctorIdxApp)
+        let hyp'Val ← do
+          let val ← mkFreshExprSyntheticOpaqueMVar hyp'Type
+          let (subst, hypMVarId) ← substEq val.mvarId! ctorIdxAppEq
+          hypMVarId.assign (hyp.applyFVarSubst subst)
+          pure val
+        let (hyp', mvarId) ← mvarId.note `h hyp'Val hyp'Type
+        -- The original hyp is still mentioned, so we cannot
+        --   let mvarId ← mvarId.clear hyp.fvarId!
+        -- but that is ok.
+        let subgoals ← mvarId.cases xs[casesOnInfo.majorPos]!.fvarId!
+        subgoals.forM fun s => s.mvarId.withContext do
+          assert! s.ctorName.isSome
+          if s.ctorName.get! ∈ casesOnInfo.insterestingCtors then
+            let hyp := s.subst.get hyp'
+            let ctorIdxAppEq := s.subst.get ctorIdxAppEq
+            let (subst, mvarId) ← substEq s.mvarId ctorIdxAppEq.fvarId!
+            let hyp := hyp.applyFVarSubst subst
+            mvarId.withContext do
+              let some prf ← refutableHasNotBit? (← inferType hyp)
+                | throwError m!"mkSparseCasesOnEq: not refutable {← inferType hyp}"
+              mvarId.assign (← mkAbsurd (← mvarId.getType) prf hyp)
+          else
+            s.mvarId.refl
+        let val ← instantiateMVars val
+        let type ← mkForallFVars (xs ++ hyps) eq
+        let val ← mkLambdaFVars (xs ++ hyps) val
+
+        addDecl (.thmDecl {
+          name := thmName
+          levelParams := info.levelParams
+          type := type
+          value := val
+        })
+
+private def isName (env : Environment) (n : Name) : Bool :=
+  if let .str p "else_eq" := n then
+    (getSparseCasesOnInfoCore env p).isSome
+  else
+    false
+
+builtin_initialize registerReservedNamePredicate isName
+
+builtin_initialize registerReservedNameAction fun name => do
+  if isName (← getEnv) name then
+    let name' ← MetaM.run' <| getSparseCasesOnEq name.getPrefix
+    assert! name = name'
+    return true
+  else
+    return false

src/Lean/Meta/Match/MatchEqs.lean

@@ -14,8 +14,8 @@ import Lean.Meta.Tactic.SplitIf
 import Lean.Meta.Tactic.CasesOnStuckLHS
 import Lean.Meta.Match.SimpH
 import Lean.Meta.Match.AltTelescopes
-import Lean.Meta.Match.SolveOverlap
 import Lean.Meta.Match.NamedPatterns
+import Lean.Meta.SplitSparseCasesOn
 
 public section
 
@@ -95,6 +95,10 @@ where
       <|>
       (casesOnStuckLHS mvarId)
       <|>
+      (reduceSparseCasesOn mvarId)
+      <|>
+      (splitSparseCasesOn mvarId)
+      <|>
       (do let mvarId' ← simpIfTarget mvarId (useDecide := true) (useNewSemantics := true)
           if mvarId' == mvarId then throwError "simpIf failed"
           return #[mvarId'])

src/Lean/Meta/SplitSparseCasesOn.lean

@@ -0,0 +1,80 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joachim Breitner
+-/
+
+module
+prelude
+public import Lean.Meta.Basic
+import Lean.Meta.Tactic.Delta
+import Lean.Meta.Tactic.Rewrite
+import Lean.Meta.Constructions.SparseCasesOn
+import Lean.Meta.Constructions.SparseCasesOnEq
+import Lean.Meta.HasNotBit
+import Lean.Meta.Tactic.Cases
+
+namespace Lean.Meta
+
+private def rewriteGoalUsingEq (goal : MVarId) (eq : Expr) (symm : Bool := false) : MetaM MVarId := do
+  let rewriteResult ← goal.rewrite (←goal.getType) eq symm
+  goal.replaceTargetEq rewriteResult.eNew rewriteResult.eqProof
+
+/--
+Reduces a sparse casesOn applied to a concrete constructor.
+-/
+public def reduceSparseCasesOn (mvarId : MVarId) : MetaM (Array MVarId) := do
+  let some (_, lhs) ← matchEqHEqLHS? (← mvarId.getType) | throwError "Target not an equality"
+  lhs.withApp fun f xs => do
+  let .const matchDeclName _  := f | throwError "Not a const application"
+  let some sparseCasesOnInfo ← getSparseCasesOnInfo matchDeclName | throwError "Not a sparse casesOn application"
+  withTraceNode `Meta.Match.matchEqs (msg := (return m!"{exceptEmoji ·} splitSparseCasesOn")) do
+  if xs.size < sparseCasesOnInfo.arity then
+    throwError "Not enough arguments for sparse casesOn application"
+  let majorIdx := sparseCasesOnInfo.majorPos
+  let major := xs[majorIdx]!
+  let some ctorInfo  ← isConstructorApp'? major
+    | throwError "Major premise is not a constructor application:{indentExpr major}"
+  if sparseCasesOnInfo.insterestingCtors.contains ctorInfo.name then
+    let mvarId' ← mvarId.modifyTargetEqLHS fun lhs =>
+      unfoldDefinition lhs
+    return #[mvarId']
+  else
+    let sparseCasesOnEqName ← getSparseCasesOnEq matchDeclName
+    let eqProof := mkConst sparseCasesOnEqName lhs.getAppFn.constLevels!
+    let eqProof := mkAppN eqProof lhs.getAppArgs[:sparseCasesOnInfo.arity]
+    let eqProof := mkApp eqProof (← mkHasNotBitProof (mkRawNatLit ctorInfo.cidx) (←  sparseCasesOnInfo.insterestingCtors.mapM (fun n => return (← getConstInfoCtor n).cidx)))
+    let mvarId' ← rewriteGoalUsingEq mvarId eqProof
+    return #[mvarId']
+
+public def splitSparseCasesOn (mvarId : MVarId) : MetaM (Array MVarId) := do
+  let some (_, lhs) ← matchEqHEqLHS? (← mvarId.getType) | throwError "Target not an equality"
+  lhs.withApp fun f xs => do
+  let .const matchDeclName _  := f | throwError "Not a const application"
+  let some sparseCasesOnInfo ← getSparseCasesOnInfo matchDeclName | throwError "Not a sparse casesOn application"
+  withTraceNode `Meta.Match.matchEqs (msg := (return m!"{exceptEmoji ·} splitSparseCasesOn")) do
+  try
+    trace[Meta.Match.matchEqs] "splitSparseCasesOn running on\n{mvarId}"
+    if xs.size < sparseCasesOnInfo.arity then
+      throwError "Not enough arguments for sparse casesOn application"
+    let majorIdx := sparseCasesOnInfo.majorPos
+    unless xs[majorIdx]!.isFVar do
+      throwError "Major premise is not a free variable:{indentExpr xs[majorIdx]!}"
+    let fvarId := xs[majorIdx]!.fvarId!
+    let subgoals ← mvarId.cases fvarId (interestingCtors? := sparseCasesOnInfo.insterestingCtors)
+    subgoals.mapM fun s => s.mvarId.withContext do
+      if s.ctorName.isNone then
+        unless s.fields.size = 1 do
+          throwError "Unexpected number of fields for catch-all branch: {s.fields}"
+        let sparseCasesOnEqName ← getSparseCasesOnEq matchDeclName
+        let some (_, lhs) ← matchEqHEqLHS? (← s.mvarId.getType) | throwError "Target not an equality"
+        let eqProof := mkConst sparseCasesOnEqName lhs.getAppFn.constLevels!
+        let eqProof := mkAppN eqProof lhs.getAppArgs[:sparseCasesOnInfo.arity]
+        let eqProof := mkApp eqProof s.fields[0]!
+        rewriteGoalUsingEq s.mvarId eqProof
+      else
+        s.mvarId.modifyTargetEqLHS fun lhs =>
+          unfoldDefinition lhs
+  catch e =>
+    trace[Meta.Match.matchEqs] "splitSparseCasesOn failed{indentD e.toMessageData}"
+    throw e

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

@@ -50,8 +50,10 @@ def _root_.Int.Linear.Poly.normCommRing? (p : Poly) : GoalM (Option (CommRing.Ri
     let some p' ← re.toPolyM? | return none
     let e' ← p'.denoteExpr
     let e' ← preprocessLight e'
-    -- Remark: we are reusing the `IntModule` virtual parent.
-    -- TODO: Investigate whether we should have a custom virtual parent for cutsat
+    /-
+    **Note**: We are reusing the `IntModule` virtual parent.
+    **TODO**: Investigate whether we should have a custom virtual parent for cutsat
+    -/
     internalize e' gen (some getIntModuleVirtualParent)
     let p'' ← toPoly e'
     if p == p'' then return none

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

@@ -42,7 +42,7 @@ private partial def registerNonlinearOccsAt (e : Expr) (x : Var) : GoalM Unit :=
   | HPow.hPow _ _ _ _ a b =>
     if (← getIntValue? a).isNone then
       registerNonlinearOcc a x
-    if (← getIntValue? b).isNone then
+    if (← getIntValue? b).isNone && (← getNatValue? b).isNone then
       -- Recall that `b : Nat`, we must create `NatCast.natCast b` and watch it.
       let (b', _) ← mkNatVar b
       internalize b' (← getGeneration b)

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

@@ -486,6 +486,16 @@ def setInconsistent (h : UnsatProof) : LinearM Unit := do
     let h ← h.toExprProof
     closeGoal h
 
+def propagateImpEq (c : EqCnstr) : LinearM Unit := do
+  let .add 1 x (.add (-1) y .nil) := c.p | unreachable!
+  let a ← getVar x
+  let b ← getVar y
+  let h ← withProofContext do
+    let h ← mkIntModThmPrefix ``Grind.Linarith.imp_eq
+    return mkApp5 h (← mkPolyDecl c.p) (← mkVarDecl x) (← mkVarDecl y) eagerReflBoolTrue (← c.toExprProof)
+  let h := mkExpectedPropHint h (← mkEq a b)
+  pushEq a b h
+
 /-!
 A linarith proof may depend on decision variables.
 We collect them and perform non chronological backtracking.

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

@@ -198,6 +198,21 @@ private def updateOccs (a : Nat) (x : Var) (c : EqCnstr) : LinearM Unit := do
   for y in ys do
     updateOccsAt a x c y
 
+private def isImpliedEq (c : EqCnstr) : LinearM Bool := do
+  match c.p with
+  | .add (-1) x (.add 1 y .nil)
+  | .add 1 x (.add (-1) y .nil) =>
+    if (← isEqv (← getVar x) (← getVar y)) then return false
+    return true
+  | _ => return false
+
+private def ensureLeadCoeffPos (c : EqCnstr) : LinearM EqCnstr := do
+  let .add k _ _ := c.p | return c
+  if k < 0 then
+    return { p := c.p.mul (-1), h := .neg c }
+  else
+    return c
+
 private def EqCnstr.assert (c : EqCnstr) : LinearM Unit := do
   trace[grind.linarith.assert] "{← c.denoteExpr}"
   let c ← c.applySubsts
@@ -207,6 +222,17 @@ private def EqCnstr.assert (c : EqCnstr) : LinearM Unit := do
   let (a, x, c) ← c.norm
   trace[grind.debug.linarith.subst] ">> {← getVar x}, {← c.denoteExpr}"
   trace[grind.linarith.assert.store] "{← c.denoteExpr}"
+  /-
+  **Note**:
+  We currently only catch equalities of the form `x + -1*y = 0`
+  This is sufficient for catching trivial cases, but to catch all implied equalities
+  we need to keep a mapping from `(Poly, Int)` to `Var`. The mapping contains an entry `(p, k) ↦ x`
+  if `x` is an eliminated variable and there is a constraint that implies `k*x = p`.
+  We need this mapping to catch `k*x = p` and `k*y = p`
+  -/
+  unless (← getStruct).caseSplits do
+    if (← isImpliedEq c) then
+      propagateImpEq (← ensureLeadCoeffPos c)
   modifyStruct fun s => { s with
     elimEqs := s.elimEqs.set x (some c)
     elimStack := x :: s.elimStack

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

@@ -33,6 +33,12 @@ def isNegInst (struct : Struct) (inst : Expr) : Bool :=
 def reportInstIssue (e : Expr) : GoalM Unit := do
   reportIssue! "`grind linarith` term with unexpected instance{indentExpr e}"
 
+private def assertNatCastNonneg (a : Expr) : LinearM Unit := do
+  let s ← getStruct
+  let h := mkApp8 (mkConst ``Grind.OrderedRing.natCast_nonneg [s.u]) s.type s.ringInst?.get!
+    s.leInst?.get! s.ltInst?.get! s.lawfulOrderLTInst?.get! s.isPreorderInst?.get! s.orderedRingInst?.get! a
+  addNewRawFact h (← inferType h) (← getGeneration a) (.ematch (.decl ``Grind.OrderedRing.natCast_nonneg))
+
 /--
 Converts a Lean `IntModule` expression `e` into a `LinExpr`
 
@@ -54,11 +60,11 @@ partial def reify? (e : Expr) (skipVar : Bool) (generation : Nat := 0) : LinearM
     if isZeroInst (← getStruct) i then return some .zero else asTopVar e
   | OfNat.ofNat _ _ _ =>
     if (← isOfNatZero e) then return some .zero else asTopVar e
-  | _ =>
-    if skipVar then
-      return none
-    else
-      return some (← toVar e)
+  | NatCast.natCast _ _ a =>
+    if (← getStruct).orderedRingInst?.isSome then
+      assertNatCastNonneg a
+    toTopVar e
+  | _ => toTopVar e
 where
   toVar (e : Expr) : LinearM LinExpr := do
     if (← alreadyInternalized e) then
@@ -69,6 +75,11 @@ where
   asVar (e : Expr) : LinearM LinExpr := do
     reportInstIssue e
     toVar e
+  toTopVar (e : Expr) : LinearM (Option LinExpr) := do
+    if skipVar then
+      return none
+    else
+      return some (← toVar e)
   asTopVar (e : Expr) : LinearM (Option LinExpr) := do
     reportInstIssue e
     if skipVar then
@@ -100,6 +111,10 @@ where
       if isZeroInst (← getStruct) i then return .zero else asVar e
     | OfNat.ofNat _ _ _ =>
       if (← isOfNatZero e) then return .zero else toVar e
+    | NatCast.natCast _ _ a =>
+      if (← getStruct).orderedRingInst?.isSome then
+        assertNatCastNonneg a
+      toVar e
     | _ => toVar e
 
 end  Lean.Meta.Grind.Arith.Linear

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

@@ -21,7 +21,10 @@ def propagateCtorIdxUp (e : Expr) : GoalM Unit := e.withApp fun f xs => do
   unless xs.size == indInfo.numParams + indInfo.numIndices + 1 do return
   let a := xs.back!
   let aNode ← getRootENode a
-  unless aNode.ctor do return
+  -- NB: This does not work for `Nat.ctorIdx`, as grind normalizes `Nat.succ` to `_ + k`.
+  -- But we have `attribute [grind] Nat.ctorIdx` to handle that case.
+  unless aNode.ctor do
+    return
   let some conInfo ← isConstructorApp? aNode.self | return
   if aNode.heqProofs then
     unless (← hasSameType a aNode.self) do
@@ -46,6 +49,8 @@ def propagateCtorIdxUp (e : Expr) : GoalM Unit := e.withApp fun f xs => do
   -- Homogeneous case
   let e' ← shareCommon (mkNatLit conInfo.cidx)
   internalize e' 0
-  pushEq e e' (← mkCongrArg e.appFn! (← mkEqProof a aNode.self))
+  -- We used `mkExpectedPropHint` so that the inferred type of the proof matches the goal,
+  -- to satisfy `debug.grind` checks
+  pushEq e e' (mkExpectedPropHint (← mkCongrArg e.appFn! (← mkEqProof a aNode.self)) (← mkEq e e'))
 
 end Lean.Meta.Grind

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

@@ -662,10 +662,23 @@ def getPatternArgKinds (f : Expr) (numArgs : Nat) : MetaM (Array PatternArgKind)
           if pinfos[idx].hasFwdDeps then return .typeFormer else return .relevant
         else
           return .typeFormer
-      else if (← x.fvarId!.getDecl).binderInfo matches .instImplicit then
-        return .instImplicit
       else
-        return .relevant
+        let xDecl ← x.fvarId!.getDecl
+        if xDecl.binderInfo matches .instImplicit then
+          return .instImplicit
+        /-
+        **Note**: Even if the binder is not marked as instance implicit, we may still
+        synthesize it using type class resolution. The motivation is declarations such as
+        ```
+        ZeroMemClass.zero_mem {S : Type} {M : outParam Type} {inst1 : Zero M} {inst2 : SetLike S M}
+            [self : @ZeroMemClass S M inst1 inst2] (s : S) : 0 ∈ s
+        ```
+        Recall that a similar approach is used in `simp`.
+        -/
+        else if (← isClass? xDecl.type).isSome then
+          return .instImplicit
+        else
+          return .relevant
 
 private def getPatternFn? (pattern : Expr) (inSupport : Bool) (root : Bool) (argKind : PatternArgKind) : M (Option Expr) := do
   if !pattern.isApp && !pattern.isConst then
@@ -860,27 +873,34 @@ private def checkCoverage (thmProof : Expr) (numParams : Nat) (bvarsFound : Std.
       for x in xs do
         let fvarId := x.fvarId!
         unless processed.contains fvarId do
-          let xType ← inferType x
+          let xDecl ← fvarId.getDecl
+          let xType := xDecl.type
           if fvarsFound.contains fvarId then
             -- Collect free vars in `x`s type and mark as processed
             fvarsFound := update fvarsFound xType
             processed := processed.insert fvarId
             modified := true
-          else if (← fvarId.getDecl).binderInfo matches .instImplicit then
-            -- If `x` is instance implicit, check whether
-            -- we have found all free variables needed to synthesize instance
-            if (← canBeSynthesized thmVars fvarsFound xType) then
-              fvarsFound := fvarsFound.insert fvarId
-              fvarsFound := update fvarsFound xType
-              processed := processed.insert fvarId
-              modified := true
-          else if (← isProp xType) then
-            -- If `x` is a proposition, and all theorem variables in `x`s type have already been found
-            -- add it to `fvarsFound` and mark it as processed.
-            if checkTypeFVars thmVars fvarsFound xType then
-              fvarsFound := fvarsFound.insert fvarId
-              processed := processed.insert fvarId
-              modified := true
+          else
+            /- **Note**: See comment at `getPatternArgKinds` -/
+            let instImplicit ← if xDecl.binderInfo matches .instImplicit then
+              pure true
+            else
+              pure <| (← isClass? xType).isSome
+            if instImplicit then
+              -- If `x` is instance implicit, check whether
+              -- we have found all free variables needed to synthesize instance
+              if (← canBeSynthesized thmVars fvarsFound xType) then
+                fvarsFound := fvarsFound.insert fvarId
+                fvarsFound := update fvarsFound xType
+                processed := processed.insert fvarId
+                modified := true
+            else if (← isProp xType) then
+              -- If `x` is a proposition, and all theorem variables in `x`s type have already been found
+              -- add it to `fvarsFound` and mark it as processed.
+              if checkTypeFVars thmVars fvarsFound xType then
+                fvarsFound := fvarsFound.insert fvarId
+                processed := processed.insert fvarId
+                modified := true
       if fvarsFound.size == numParams then
         return .ok
       if !modified then

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

@@ -1041,7 +1041,7 @@ def addNewRawFact (proof : Expr) (prop : Expr) (generation : Nat) (splitSource :
     unless (← withGTransparency <| isDefEq (← inferType proof) prop) do
       throwError "`grind` internal error, trying to assert{indentExpr prop}\n\
         with proof{indentExpr proof}\nwhich has type{indentExpr (← inferType proof)}\n\
-        which is not definitionally equal with `reducible` transparency setting}"
+        which is not definitionally equal with `reducible` transparency setting"
   modify fun s => { s with newRawFacts := s.newRawFacts.enqueue { proof, prop, generation, splitSource } }
 
 /-- Returns the number of theorem instances generated so far. -/
@@ -1198,7 +1198,7 @@ def pushEqCore (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit := do
       unless (← withGTransparency <| isDefEq (← inferType proof) expectedType) do
         throwError "`grind` internal error, trying to assert equality{indentExpr expectedType}\n\
             with proof{indentExpr proof}\nwhich has type{indentExpr (← inferType proof)}\n\
-            which is not definitionally equal with `reducible` transparency setting}"
+            which is not definitionally equal with `reducible` transparency setting"
       trace[grind.debug] "pushEqCore: {expectedType}"
   modify fun s => { s with newFacts := s.newFacts.push <| .eq lhs rhs proof isHEq }
 

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

@@ -33,7 +33,7 @@ public instance : Iterator (α := AssocListIterator α β) Id ((a : α) × β a)
     | .done => it.internalState.l = .nil
   step it := pure (match it with
         | ⟨⟨.nil⟩⟩ => .deflate ⟨.done, rfl⟩
-        | ⟨⟨.cons k v l⟩⟩ => .deflate ⟨.yield (toIterM ⟨l⟩ Id _) ⟨k, v⟩, rfl⟩)
+        | ⟨⟨.cons k v l⟩⟩ => .deflate ⟨.yield (.mk ⟨l⟩ Id _) ⟨k, v⟩, rfl⟩)
 
 def AssocListIterator.finitenessRelation :
     FinitenessRelation (AssocListIterator α β) Id where

src/Std/Data/DHashMap/IteratorLemmas.lean

@@ -27,7 +27,7 @@ public theorem step_iter_nil {α : Type u} {β : α → Type v} :
 @[simp]
 public theorem step_iter_cons {α : Type u} {β : α → Type v} {k v} {l : AssocList α β} :
     ((AssocList.cons k v l).iter).step = ⟨.yield l.iter ⟨k, v⟩, rfl⟩ := by
-  simp [Iter.step, IterM.step, Iterator.step, Iter.toIterM, iter, toIterM, IterM.toIter]
+  simp [Iter.step, IterM.step, Iterator.step, Iter.toIterM, iter, IterM.mk, IterM.toIter]
 
 @[simp]
 public theorem toList_iter {α : Type u} {β : α → Type v} {l : AssocList α β} :

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

@@ -10,7 +10,8 @@ public import Std.Data.Iterators.Combinators.Monadic.Drop
 
 @[expose] public section
 
-namespace Std.Iterators
+namespace Std
+open Std.Iterators.Types
 
 /--
 Given an iterator `it` and a natural number `n`, `it.drop n` is an iterator that forwards all of
@@ -41,4 +42,4 @@ def Iter.drop {α : Type w} {β : Type w} (n : Nat) (it : Iter (α := α) β) :
     Iter (α := Drop α Id β) β :=
   it.toIterM.drop n |>.toIter
 
-end Std.Iterators
+end Std

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

@@ -10,7 +10,7 @@ public import Std.Data.Iterators.Combinators.Monadic.DropWhile
 
 @[expose] public section
 
-namespace Std.Iterators
+namespace Std
 
 /--
 Constructs intermediate states of an iterator created with the combinator `Iter.dropWhile`.
@@ -60,4 +60,4 @@ that, the combinator incurs an additional O(1) cost for each value emitted by `i
 def Iter.dropWhile {α : Type w} {β : Type w} (P : β → Bool) (it : Iter (α := α) β) :=
   (it.toIterM.dropWhile P |>.toIter : Iter β)
 
-end Std.Iterators
+end Std

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

@@ -15,7 +15,7 @@ public import Init.Data.Iterators.Internal.Termination
 This file provides the iterator combinator `IterM.drop`.
 -/
 
-namespace Std.Iterators
+namespace Std
 
 variable {α : Type w} {m : Type w → Type w'} {β : Type w}
 
@@ -23,7 +23,7 @@ variable {α : Type w} {m : Type w → Type w'} {β : Type w}
 The internal state of the `IterM.drop` combinator.
 -/
 @[unbox]
-structure Drop (α : Type w) (m : Type w → Type w') (β : Type w) where
+structure Iterators.Types.Drop (α : Type w) (m : Type w → Type w') (β : Type w) where
   /-- Internal implementation detail of the iterator library -/
   remaining : Nat
   /-- Internal implementation detail of the iterator library -/
@@ -55,7 +55,9 @@ does not drop any elements anymore.
 -/
 @[always_inline, inline]
 def IterM.drop (n : Nat) (it : IterM (α := α) m β) :=
-  toIterM (Drop.mk n it) m β
+  IterM.mk (Iterators.Types.Drop.mk n it) m β
+
+namespace Iterators.Types
 
 inductive Drop.PlausibleStep [Iterator α m β] (it : IterM (α := Drop α m β) m β) :
     (step : IterStep (IterM (α := Drop α m β) m β) β) → Prop where
@@ -160,4 +162,4 @@ instance Drop.instIteratorLoop {n : Type x → Type x'} [Monad m] [Monad n] [Ite
     IteratorLoop (Drop α m β) m n :=
   .defaultImplementation
 
-end Std.Iterators
+end Std.Iterators.Types

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

@@ -31,7 +31,8 @@ Several variants of this combinator are provided:
   iterator, and particularly for specialized termination proofs. If possible, avoid this.
 -/
 
-namespace Std.Iterators
+namespace Std
+open Std.Iterators
 
 variable {α : Type w} {m : Type w → Type w'} {β : Type w}
 
@@ -39,7 +40,7 @@ variable {α : Type w} {m : Type w → Type w'} {β : Type w}
 Internal state of the `dropWhile` combinator. Do not depend on its internals.
 -/
 @[unbox]
-structure DropWhile (α : Type w) (m : Type w → Type w') (β : Type w)
+structure Iterators.Types.DropWhile (α : Type w) (m : Type w → Type w') (β : Type w)
     (P : β → PostconditionT m (ULift Bool)) where
   /-- Internal implementation detail of the iterator library. -/
   dropping : Bool
@@ -59,7 +60,7 @@ verification purposes.
 @[always_inline, inline]
 def IterM.Intermediate.dropWhileWithPostcondition (P : β → PostconditionT m (ULift Bool))
     (dropping : Bool) (it : IterM (α := α) m β) :=
-  (toIterM (DropWhile.mk (P := P) dropping it) m β : IterM m β)
+  (IterM.mk (Iterators.Types.DropWhile.mk (P := P) dropping it) m β : IterM m β)
 
 /--
 Constructs intermediate states of an iterator created with the combinator `IterM.dropWhileM`.
@@ -200,6 +201,8 @@ that, the combinator incurs an addictional O(1) cost for each value emitted by `
 def IterM.dropWhile [Monad m] (P : β → Bool) (it : IterM (α := α) m β) :=
   (Intermediate.dropWhile P true it: IterM m β)
 
+namespace Iterators.Types
+
 /--
 `it.PlausibleStep step` is the proposition that `step` is a possible next step from the
 `dropWhile` iterator `it`. This is mostly internally relevant, except if one needs to manually
@@ -279,4 +282,4 @@ instance DropWhile.instIteratorLoop [Monad m] [Monad n] [Iterator α m β] :
     IteratorLoop (DropWhile α m β P) m n :=
   .defaultImplementation
 
-end Std.Iterators
+end Std.Iterators.Types

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

@@ -17,93 +17,15 @@ public import Init.Data.Iterators.Consumers.Monadic.Loop
 This module implements a combinator that only yields every `n`-th element of another iterator.
 -/
 
-namespace Std.Iterators
+namespace Std
+open Std.Iterators
 
 @[unbox]
-structure Types.StepSizeIterator (α : Type w) (m : Type w → Type w') (β : Type w) where
+structure Iterators.Types.StepSizeIterator (α : Type w) (m : Type w → Type w') (β : Type w) where
   nextIdx : Nat
   n : Nat
   inner : IterM (α := α) m β
 
-instance [Iterator α m β] [IteratorAccess α m] [Monad m] :
-    Iterator (Types.StepSizeIterator α m β) m β where
-  IsPlausibleStep it step :=
-    it.internalState.inner.IsPlausibleNthOutputStep it.internalState.nextIdx
-        (step.mapIterator (Types.StepSizeIterator.inner ∘ IterM.internalState)) ∧
-      ∀ it' out, step = .yield it' out →
-        it'.internalState.n = it.internalState.n ∧ it'.internalState.nextIdx = it.internalState.n
-  step it := (fun s => .deflate ⟨s.1.mapIterator (⟨⟨it.internalState.n, it.internalState.n, ·⟩⟩), by
-      simp only [IterStep.mapIterator_mapIterator]
-      refine cast ?_ s.property
-      rw (occs := [1]) [← IterStep.mapIterator_id (step := s.val)]
-      congr, by
-      intro it' out
-      cases s.val
-      · simp only [IterStep.mapIterator_yield, IterStep.yield.injEq, and_imp]
-        rintro h _
-        simp [← h]
-      · simp
-      · simp
-      done⟩) <$> it.internalState.inner.nextAtIdx? it.internalState.nextIdx
-
-def Types.StepSizeIterator.instFinitenessRelation [Iterator α m β] [IteratorAccess α m] [Monad m]
-    [Finite α m] : FinitenessRelation (Types.StepSizeIterator α m β) m where
-  rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.inner.finitelyManySteps)
-  wf := by
-    apply InvImage.wf
-    apply WellFoundedRelation.wf
-  subrelation {it it'} h := by
-    obtain ⟨step, hs, h⟩ := h
-    simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep] at h
-    simp only [InvImage]
-    obtain ⟨⟨n, it⟩⟩ := it
-    simp only at ⊢ h
-    generalize h' : step.mapIterator (Types.StepSizeIterator.inner ∘ IterM.internalState) = s at h
-    replace h := h.1
-    induction h
-    case zero_yield =>
-      cases step <;> (try exfalso; simp at h'; done)
-      cases hs; cases h'
-      apply IterM.TerminationMeasures.Finite.rel_of_yield ‹_›
-    case done =>
-      cases step <;> simp_all [IterStep.successor]
-    case yield ih =>
-      apply Relation.TransGen.trans
-      · exact ih h'
-      · exact IterM.TerminationMeasures.Finite.rel_of_yield ‹_›
-    case skip ih  =>
-      apply Relation.TransGen.trans
-      · exact ih h'
-      · exact IterM.TerminationMeasures.Finite.rel_of_skip ‹_›
-
-instance Types.StepSizeIterator.instFinite [Iterator α m β] [IteratorAccess α m] [Monad m]
-    [Finite α m] : Finite (Types.StepSizeIterator α m β) m :=
-  .of_finitenessRelation instFinitenessRelation
-
-def Types.StepSizeIterator.instProductivenessRelation [Iterator α m β] [IteratorAccess α m] [Monad m]
-    [Productive α m] : ProductivenessRelation (Types.StepSizeIterator α m β) m where
-  rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.inner.finitelyManySkips)
-  wf := by
-    apply InvImage.wf
-    apply WellFoundedRelation.wf
-  subrelation {it it'} h := by
-    simp only [IterM.IsPlausibleSkipSuccessorOf, IterM.IsPlausibleStep, Iterator.IsPlausibleStep] at h
-    simp only [InvImage]
-    obtain ⟨⟨n, it⟩⟩ := it
-    simp only [IterStep.mapIterator_skip, Function.comp_apply] at ⊢ h
-    generalize h' : IterStep.skip _ = s at h
-    exfalso
-    replace h := h.1
-    induction h
-    case zero_yield => cases h'
-    case done => cases h'
-    case yield hp ih => exact ih h'
-    case skip ih  => exact ih h'
-
-instance Types.StepSizeIterator.instProductive [Iterator α m β] [IteratorAccess α m] [Monad m]
-    [Productive α m] : Productive (Types.StepSizeIterator α m β) m :=
-  .of_productivenessRelation instProductivenessRelation
-
 /--
 Produces an iterator that emits one value of `it`, then drops `n - 1` elements, then emits another
 value, and so on. In other words, it emits every `n`-th value of `it`, starting with the first one.
@@ -134,14 +56,95 @@ def IterM.stepSize [Iterator α m β] [IteratorAccess α m] [Monad m]
     IterM (α := Types.StepSizeIterator α m β) m β :=
   ⟨⟨0, n - 1, it⟩⟩
 
-instance Types.StepSizeIterator.instIteratorCollect {m n} [Iterator α m β]
+namespace Iterators.Types
+
+instance StepSizeIterator.instIterator [Iterator α m β] [IteratorAccess α m] [Monad m] :
+    Iterator (Types.StepSizeIterator α m β) m β where
+  IsPlausibleStep it step :=
+    it.internalState.inner.IsPlausibleNthOutputStep it.internalState.nextIdx
+        (step.mapIterator (Types.StepSizeIterator.inner ∘ IterM.internalState)) ∧
+      ∀ it' out, step = .yield it' out →
+        it'.internalState.n = it.internalState.n ∧ it'.internalState.nextIdx = it.internalState.n
+  step it := (fun s => .deflate ⟨s.1.mapIterator (⟨⟨it.internalState.n, it.internalState.n, ·⟩⟩), by
+      simp only [IterStep.mapIterator_mapIterator]
+      refine cast ?_ s.property
+      rw (occs := [1]) [← IterStep.mapIterator_id (step := s.val)]
+      congr, by
+      intro it' out
+      cases s.val
+      · simp only [IterStep.mapIterator_yield, IterStep.yield.injEq, and_imp]
+        rintro h _
+        simp [← h]
+      · simp
+      · simp
+      done⟩) <$> it.internalState.inner.nextAtIdx? it.internalState.nextIdx
+
+def StepSizeIterator.instFinitenessRelation [Iterator α m β] [IteratorAccess α m] [Monad m]
+    [Finite α m] : FinitenessRelation (Types.StepSizeIterator α m β) m where
+  rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.inner.finitelyManySteps)
+  wf := by
+    apply InvImage.wf
+    apply WellFoundedRelation.wf
+  subrelation {it it'} h := by
+    obtain ⟨step, hs, h⟩ := h
+    simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep] at h
+    simp only [InvImage]
+    obtain ⟨⟨n, it⟩⟩ := it
+    simp only at ⊢ h
+    generalize h' : step.mapIterator (Types.StepSizeIterator.inner ∘ IterM.internalState) = s at h
+    replace h := h.1
+    induction h
+    case zero_yield =>
+      cases step <;> (try exfalso; simp at h'; done)
+      cases hs; cases h'
+      apply IterM.TerminationMeasures.Finite.rel_of_yield ‹_›
+    case done =>
+      cases step <;> simp_all [IterStep.successor]
+    case yield ih =>
+      apply Relation.TransGen.trans
+      · exact ih h'
+      · exact IterM.TerminationMeasures.Finite.rel_of_yield ‹_›
+    case skip ih  =>
+      apply Relation.TransGen.trans
+      · exact ih h'
+      · exact IterM.TerminationMeasures.Finite.rel_of_skip ‹_›
+
+instance StepSizeIterator.instFinite [Iterator α m β] [IteratorAccess α m] [Monad m]
+    [Finite α m] : Finite (Types.StepSizeIterator α m β) m :=
+  .of_finitenessRelation instFinitenessRelation
+
+def StepSizeIterator.instProductivenessRelation [Iterator α m β] [IteratorAccess α m] [Monad m]
+    [Productive α m] : ProductivenessRelation (Types.StepSizeIterator α m β) m where
+  rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.inner.finitelyManySkips)
+  wf := by
+    apply InvImage.wf
+    apply WellFoundedRelation.wf
+  subrelation {it it'} h := by
+    simp only [IterM.IsPlausibleSkipSuccessorOf, IterM.IsPlausibleStep, Iterator.IsPlausibleStep] at h
+    simp only [InvImage]
+    obtain ⟨⟨n, it⟩⟩ := it
+    simp only [IterStep.mapIterator_skip, Function.comp_apply] at ⊢ h
+    generalize h' : IterStep.skip _ = s at h
+    exfalso
+    replace h := h.1
+    induction h
+    case zero_yield => cases h'
+    case done => cases h'
+    case yield hp ih => exact ih h'
+    case skip ih  => exact ih h'
+
+instance StepSizeIterator.instProductive [Iterator α m β] [IteratorAccess α m] [Monad m]
+    [Productive α m] : Productive (Types.StepSizeIterator α m β) m :=
+  .of_productivenessRelation instProductivenessRelation
+
+instance StepSizeIterator.instIteratorCollect {m n} [Iterator α m β]
     [IteratorAccess α m] [Monad m] [Monad n] :
     IteratorCollect (Types.StepSizeIterator α m β) m n :=
   .defaultImplementation
 
-instance Types.StepSizeIterator.instIteratorLoop {m n} [Iterator α m β]
+instance StepSizeIterator.instIteratorLoop {m n} [Iterator α m β]
     [IteratorAccess α m] [Monad m] [Monad n] :
     IteratorLoop (Types.StepSizeIterator α m β) m n :=
   .defaultImplementation
 
-end Std.Iterators
+end Std.Iterators.Types

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

@@ -31,7 +31,8 @@ Several variants of this combinator are provided:
   iterator, and particularly for specialized termination proofs. If possible, avoid this.
 -/
 
-namespace Std.Iterators
+namespace Std
+open Std.Iterators
 
 variable {α : Type w} {m : Type w → Type w'} {β : Type w}
 
@@ -39,7 +40,7 @@ variable {α : Type w} {m : Type w → Type w'} {β : Type w}
 Internal state of the `takeWhile` combinator. Do not depend on its internals.
 -/
 @[unbox]
-structure TakeWhile (α : Type w) (m : Type w → Type w') (β : Type w)
+structure Iterators.Types.TakeWhile (α : Type w) (m : Type w → Type w') (β : Type w)
     (P : β → PostconditionT m (ULift Bool)) where
   /-- Internal implementation detail of the iterator library. -/
   inner : IterM (α := α) m β
@@ -85,7 +86,7 @@ it terminates.
 -/
 @[always_inline, inline]
 def IterM.takeWhileWithPostcondition (P : β → PostconditionT m (ULift Bool)) (it : IterM (α := α) m β) :=
-  (toIterM (TakeWhile.mk (P := P) it) m β : IterM m β)
+  (IterM.mk (Types.TakeWhile.mk (P := P) it) m β : IterM m β)
 
 /--
 Given an iterator `it` and a monadic predicate `P`, `it.takeWhileM P` is an iterator that outputs
@@ -159,6 +160,8 @@ it terminates.
 def IterM.takeWhile [Monad m] (P : β → Bool) (it : IterM (α := α) m β) :=
   (it.takeWhileM (pure ∘ ULift.up ∘ P) : IterM m β)
 
+namespace Iterators.Types
+
 /--
 `it.PlausibleStep step` is the proposition that `step` is a possible next step from the
 `takeWhile` iterator `it`. This is mostly internally relevant, except if one needs to manually
@@ -235,4 +238,4 @@ instance TakeWhile.instIteratorLoop [Monad m] [Monad n] [Iterator α m β]
     IteratorLoop (TakeWhile α m β P) m n :=
   .defaultImplementation
 
-end Std.Iterators
+end Std.Iterators.Types

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

@@ -20,8 +20,8 @@ This file provides an iterator combinator `IterM.zip` that combines two iterator
 of pairs.
 -/
 
-namespace Std.Iterators
-open Std.Internal
+namespace Std
+open Std.Internal Std.Iterators
 
 variable {m : Type w → Type w'}
   {α₁ : Type w} {β₁ : Type w} [Iterator α₁ m β₁]
@@ -31,11 +31,50 @@ variable {m : Type w → Type w'}
 Internal state of the `zip` combinator. Do not depend on its internals.
 -/
 @[unbox]
-structure Zip (α₁ : Type w) (m : Type w → Type w') {β₁ : Type w} [Iterator α₁ m β₁] (α₂ : Type w) (β₂ : Type w) where
+structure Iterators.Types.Zip (α₁ : Type w) (m : Type w → Type w') {β₁ : Type w} [Iterator α₁ m β₁]
+    (α₂ : Type w) (β₂ : Type w) where
   left : IterM (α := α₁) m β₁
   memoizedLeft : (Option { out : β₁ // ∃ it : IterM (α := α₁) m β₁, it.IsPlausibleOutput out })
   right : IterM (α := α₂) m β₂
 
+/--
+Given two iterators `left` and `right`, `left.zip right` is an iterator that yields pairs of
+outputs of `left` and `right`. When one of them terminates,
+the `zip` iterator will also terminate.
+
+**Marble diagram:**
+
+```text
+left               --a        ---b        --c
+right                 --x         --y        --⊥
+left.zip right     -----(a, x)------(b, y)-----⊥
+```
+
+**Termination properties:**
+
+* `Finite` instance: only if either `left` or `right` is finite and the other is productive
+* `Productive` instance: only if `left` and `right` are productive
+
+There are situations where `left.zip right` is finite (or productive) but none of the instances
+above applies. For example, if the computation happens in an `Except` monad and `left` immediately
+fails when calling `step`, then `left.zip right` will also do so. In such a case, the `Finite`
+(or `Productive`) instance needs to be proved manually.
+
+**Performance:**
+
+This combinator incurs an additional O(1) cost with each step taken by `left` or `right`.
+
+Right now, the compiler does not unbox the internal state, leading to worse performance than
+possible.
+-/
+@[always_inline, inline]
+def IterM.zip
+    (left : IterM (α := α₁) m β₁) (right : IterM (α := α₂) m β₂) :
+    IterM (α := Types.Zip α₁ m α₂ β₂) m (β₁ × β₂) :=
+  .mk ⟨left, none, right⟩ m _
+
+namespace Iterators.Types
+
 /--
 `it.PlausibleStep step` is the proposition that `step` is a possible next step from the
 `zip` iterator `it`. This is mostly internally relevant, except if one needs to manually
@@ -84,42 +123,6 @@ instance Zip.instIterator [Monad m] :
       | .done hp =>
           pure <| .deflate <| .done (.doneRight hm hp)
 
-/--
-Given two iterators `left` and `right`, `left.zip right` is an iterator that yields pairs of
-outputs of `left` and `right`. When one of them terminates,
-the `zip` iterator will also terminate.
-
-**Marble diagram:**
-
-```text
-left               --a        ---b        --c
-right                 --x         --y        --⊥
-left.zip right     -----(a, x)------(b, y)-----⊥
-```
-
-**Termination properties:**
-
-* `Finite` instance: only if either `left` or `right` is finite and the other is productive
-* `Productive` instance: only if `left` and `right` are productive
-
-There are situations where `left.zip right` is finite (or productive) but none of the instances
-above applies. For example, if the computation happens in an `Except` monad and `left` immediately
-fails when calling `step`, then `left.zip right` will also do so. In such a case, the `Finite`
-(or `Productive`) instance needs to be proved manually.
-
-**Performance:**
-
-This combinator incurs an additional O(1) cost with each step taken by `left` or `right`.
-
-Right now, the compiler does not unbox the internal state, leading to worse performance than
-possible.
--/
-@[always_inline, inline]
-def IterM.zip
-    (left : IterM (α := α₁) m β₁) (right : IterM (α := α₂) m β₂) :
-    IterM (α := Zip α₁ m α₂ β₂) m (β₁ × β₂) :=
-  toIterM ⟨left, none, right⟩ m _
-
 variable (m) in
 def Zip.Rel₁ [Finite α₁ m] [Productive α₂ m] :
     IterM (α := Zip α₁ m α₂ β₂) m (β₁ × β₂) → IterM (α := Zip α₁ m α₂ β₂) m (β₁ × β₂) → Prop :=
@@ -319,4 +322,4 @@ instance Zip.instIteratorLoop [Monad m] [Monad n] :
     IteratorLoop (Zip α₁ m α₂ β₂) m n :=
   .defaultImplementation
 
-end Std.Iterators
+end Std.Iterators.Types

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

@@ -14,7 +14,8 @@ public import Std.Data.Iterators.Combinators.Monadic.StepSize
 This module provides a combinator that only yields every `n`-th element of another iterator.
 -/
 
-namespace Std.Iterators
+namespace Std
+open Std.Iterators
 
 @[always_inline, inline, inherit_doc IterM.stepSize]
 def Iter.stepSize [Iterator α Id β] [IteratorAccess α Id]
@@ -22,4 +23,4 @@ def Iter.stepSize [Iterator α Id β] [IteratorAccess α Id]
     Iter (α := Types.StepSizeIterator α Id β) β :=
   (it.toIterM.stepSize n).toIter
 
-end Std.Iterators
+end Std

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

@@ -10,7 +10,7 @@ public import Std.Data.Iterators.Combinators.Monadic.TakeWhile
 
 @[expose] public section
 
-namespace Std.Iterators
+namespace Std
 
 /--
 Given an iterator `it` and a predicate `P`, `it.takeWhile P` is an iterator that outputs
@@ -46,4 +46,4 @@ it terminates.
 def Iter.takeWhile {α : Type w} {β : Type w} (P : β → Bool) (it : Iter (α := α) β) :=
   (it.toIterM.takeWhile P |>.toIter : Iter β)
 
-end Std.Iterators
+end Std

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

@@ -10,7 +10,7 @@ public import Std.Data.Iterators.Combinators.Monadic.Zip
 
 @[expose] public section
 
-namespace Std.Iterators
+namespace Std
 
 /--
 Given two iterators `left` and `right`, `left.zip right` is an iterator that yields pairs of
@@ -48,4 +48,4 @@ def Iter.zip {α₁ : Type w} {β₁: Type w} {α₂ : Type w} {β₂ : Type w}
     (left : Iter (α := α₁) β₁) (right : Iter (α := α₂) β₂) :=
   ((left.toIterM.zip right.toIterM).toIter : Iter (β₁ × β₂))
 
-end Std.Iterators
+end Std

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

@@ -12,7 +12,8 @@ public import Init.Data.Iterators.Lemmas.Combinators.Take
 
 @[expose] public section
 
-namespace Std.Iterators
+namespace Std
+open Std.Iterators
 
 theorem Iter.drop_eq {α β} [Iterator α Id β] {n : Nat}
     {it : Iter (α := α) β} :
@@ -59,17 +60,6 @@ theorem Iter.toListRev_drop {α β} [Iterator α Id β] {n : Nat}
     (it.drop n).toListRev = (it.toList.reverse.take (it.toList.length - n)) := by
   rw [toListRev_eq, toList_drop, List.reverse_drop]
 
-theorem List.drop_eq_extract {l : List α} {k : Nat} :
-    l.drop k = l.extract k := by
-  induction l generalizing k
-  case nil => simp
-  case cons _ _ ih =>
-    match k with
-    | 0 => simp
-    | _ + 1 =>
-      simp only [List.drop_succ_cons, List.length_cons, ih]
-      simp only [List.extract_eq_drop_take, Nat.reduceSubDiff, List.drop_succ_cons]
-
 @[simp]
 theorem Iter.toArray_drop {α β} [Iterator α Id β] {n : Nat}
     [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
@@ -77,4 +67,4 @@ theorem Iter.toArray_drop {α β} [Iterator α Id β] {n : Nat}
     (it.drop n).toArray = it.toArray.extract n := by
   rw [← toArray_toList, ← toArray_toList, ← List.toArray_drop, toList_drop]
 
-end Std.Iterators
+end Std

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

@@ -12,7 +12,8 @@ public import Init.Data.Iterators.Lemmas.Consumers
 
 @[expose] public section
 
-namespace Std.Iterators
+namespace Std
+open Std.Iterators
 
 theorem Iter.dropWhile_eq_intermediateDropWhile {α β} [Iterator α Id β] {P}
     {it : Iter (α := α) β} :
@@ -125,4 +126,4 @@ theorem Iter.toListRev_dropWhile_of_finite {α β} [Iterator α Id β] {P}
     (it.dropWhile P).toListRev = (it.toList.dropWhile P).reverse := by
   rw [toListRev_eq, toList_dropWhile_of_finite]
 
-end Std.Iterators
+end Std

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

@@ -11,7 +11,7 @@ public import Init.Data.Iterators.Lemmas.Consumers.Monadic
 
 @[expose] public section
 
-namespace Std.Iterators
+namespace Std
 
 theorem IterM.step_drop {α m β} [Monad m] [Iterator α m β] {n : Nat}
     {it : IterM (α := α) m β} :
@@ -31,4 +31,4 @@ theorem IterM.step_drop {α m β} [Monad m] [Iterator α m β] {n : Nat}
   · rfl
   · rfl
 
-end Std.Iterators
+end Std

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

@@ -11,7 +11,8 @@ public import Init.Data.Iterators.Lemmas.Consumers.Monadic
 
 @[expose] public section
 
-namespace Std.Iterators
+namespace Std
+open Std.Iterators
 
 theorem IterM.Intermediate.dropWhileM_eq_dropWhileWithPostcondition {α m β} [Monad m]
     [Iterator α m β] {it : IterM (α := α) m β} {P dropping} :
@@ -173,4 +174,4 @@ theorem IterM.step_dropWhile {α m β} [Monad m] [LawfulMonad m] [Iterator α m
       return .deflate <| .done (.done h)) := by
   simp [dropWhile_eq_intermediateDropWhile, step_intermediateDropWhile]
 
-end Std.Iterators
+end Std

src/Std/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean

@@ -11,10 +11,10 @@ public import Std.Data.Iterators.Lemmas.Equivalence.StepCongr
 
 @[expose] public section
 
-namespace Std.Iterators
-open Std.Internal
+namespace Std
+open Std.Internal Std.Iterators
 
-theorem stepAsHetT_filterMapWithPostcondition [Monad m] [LawfulMonad m] [Monad n]
+theorem IterM.stepAsHetT_filterMapWithPostcondition [Monad m] [LawfulMonad m] [Monad n]
     [LawfulMonad n] [Iterator α m β] [MonadLiftT m n] [LawfulMonadLiftT m n]
     {f : β → PostconditionT n (Option γ)} {it : IterM (α := α) m β} :
     (IterM.stepAsHetT (it.filterMapWithPostcondition f)) =
@@ -200,4 +200,4 @@ theorem IterM.Equiv.map {α₁ α₂ β γ : Type w}
     IterM.Equiv (ita.map f) (itb.map f) :=
   IterM.Equiv.filterMapWithPostcondition h
 
-end Std.Iterators
+end Std

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

@@ -11,7 +11,8 @@ public import Std.Data.Iterators.Lemmas.Consumers.Monadic
 
 @[expose] public section
 
-namespace Std.Iterators
+namespace Std
+open Std.Iterators
 
 theorem IterM.step_takeWhileWithPostcondition {α m β} [Monad m] [Iterator α m β]
     {it : IterM (α := α) m β} {P} :
@@ -66,4 +67,4 @@ theorem IterM.step_takeWhile {α m β} [Monad m] [LawfulMonad m] [Iterator α m
   · simp
   · simp
 
-end Std.Iterators
+end Std

src/Std/Data/Iterators/Lemmas/Combinators/Monadic/Zip.lean

@@ -11,7 +11,8 @@ public import Init.Data.Iterators.Lemmas.Consumers.Monadic
 
 @[expose] public section
 
-namespace Std.Iterators
+namespace Std
+open Std.Iterators Std.Iterators.Types
 
 variable {α₁ α₂ β₁ β₂ : Type w} {m : Type w → Type w'}
 
@@ -87,4 +88,4 @@ theorem IterM.step_zip [Monad m] [Iterator α₁ m β₁] [Iterator α₂ m β
         pure <| .deflate <| .done (.doneLeft rfl hp)) := by
   simp [zip_eq_intermediateZip, step_intermediateZip]
 
-end Std.Iterators
+end Std

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

@@ -12,7 +12,8 @@ public import Std.Data.Iterators.Lemmas.Consumers
 
 @[expose] public section
 
-namespace Std.Iterators
+namespace Std
+open Std.Iterators
 
 theorem Iter.takeWhile_eq {α β} [Iterator α Id β] {P}
     {it : Iter (α := α) β} :
@@ -135,4 +136,4 @@ theorem Iter.toArray_takeWhile_of_finite {α β} [Iterator α Id β] {P}
     (it.takeWhile P).toArray = it.toArray.takeWhile P := by
   rw [← toArray_toList, ← toArray_toList, List.takeWhile_toArray, toList_takeWhile_of_finite]
 
-end Std.Iterators
+end Std

src/Std/Data/Iterators/Lemmas/Combinators/Zip.lean

@@ -12,7 +12,8 @@ public import Init.Data.Iterators.Lemmas.Combinators.Take
 
 @[expose] public section
 
-namespace Std.Iterators
+namespace Std
+open Std.Iterators Std.Iterators.Types
 
 variable {α₁ α₂ β₁ β₂ : Type w} {m : Type w → Type w'}
 
@@ -394,4 +395,4 @@ theorem Iter.toArray_take_zip {α₁ α₂ β₁ β₂} [Iterator α₁ Id β₁
     ((it₁.zip it₂).take n).toArray = ((it₁.take n).toList.zip (it₂.take n).toList).toArray := by
   simp [← toArray_toList]
 
-end Iterators
+end Std

src/Std/Data/Iterators/Lemmas/Consumers/Collect.lean

@@ -11,7 +11,8 @@ public import Std.Data.Iterators.Lemmas.Consumers.Monadic.Collect
 
 @[expose] public section
 
-namespace Std.Iterators
+namespace Std
+open Std.Iterators
 
 theorem Iter.Equiv.toListRev_eq
     [Iterator α₁ Id β] [Iterator α₂ Id β] [Finite α₁ Id] [Finite α₂ Id]
@@ -35,4 +36,4 @@ theorem Iter.Equiv.toArray_eq
     ita.toArray = itb.toArray := by
   simp only [← Iter.toArray_toList, toList_eq h]
 
-end Std.Iterators
+end Std

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

@@ -12,7 +12,8 @@ public import Std.Data.Iterators.Lemmas.Consumers.Monadic.Loop
 
 @[expose] public section
 
-namespace Std.Iterators
+namespace Std
+open Std.Iterators
 
 theorem Iter.Equiv.forIn_eq {α₁ α₂ β γ : Type w} {m : Type w → Type w'}
     [Iterator α₁ Id β] [Iterator α₂ Id β] [Finite α₁ Id] [Finite α₂ Id]
@@ -44,4 +45,4 @@ theorem Iter.Equiv.fold_eq {α₁ α₂ β γ : Type w} {m : Type w → Type w'}
     ita.fold (init := init) f = itb.fold (init := init) f := by
   simp [Iter.fold_eq_foldM, h.foldM_eq]
 
-end Std.Iterators
+end Std

src/Std/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean

@@ -11,7 +11,8 @@ public import Std.Data.Iterators.Lemmas.Equivalence.StepCongr
 
 @[expose] public section
 
-namespace Std.Iterators
+namespace Std
+open Std.Iterators
 
 theorem IterM.Equiv.toListRev_eq [Monad m] [LawfulMonad m]
     [Iterator α₁ m β] [Iterator α₂ m β] [Finite α₁ m] [Finite α₂ m]
@@ -51,4 +52,4 @@ theorem IterM.Equiv.toArray_eq [Monad m] [LawfulMonad m]
     ita.toArray = itb.toArray := by
   simp only [← IterM.toArray_toList, toList_eq h]
 
-end Std.Iterators
+end Std

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

@@ -11,7 +11,8 @@ public import Std.Data.Iterators.Lemmas.Consumers.Monadic.Collect
 
 @[expose] public section
 
-namespace Std.Iterators
+namespace Std
+open Std.Iterators
 
 theorem IterM.Equiv.forIn_eq {α₁ α₂ β γ : Type w} {m : Type w → Type w'}
     {n : Type w → Type w''} [Iterator α₁ m β] [Iterator α₂ m β]
@@ -74,4 +75,4 @@ theorem IterM.Equiv.drain_eq {α₁ α₂ β : Type w} {m : Type w → Type w'}
     ita.drain = itb.drain := by
   simp [IterM.drain_eq_fold, h.fold_eq]
 
-end Std.Iterators
+end Std

src/Std/Data/Iterators/Lemmas/Equivalence/Basic.lean

@@ -12,7 +12,8 @@ public import Std.Data.Iterators.Lemmas.Equivalence.HetT
 
 @[expose] public section
 
-namespace Std.Iterators
+namespace Std
+open Std.Iterators
 
 section Definition
 
@@ -276,4 +277,4 @@ theorem IterM.Equiv.of_morphism {α₁ α₂} {m : Type w → Type w'} [Monad m]
   case hf =>
     exact ⟨ita, rfl, rfl⟩
 
-end Std.Iterators
+end Std

src/Std/Data/Iterators/Lemmas/Equivalence/StepCongr.lean

@@ -15,7 +15,8 @@ This module proves that the step functions of equivalent iterators behave the sa
 circumstances.
 -/
 
-namespace Std.Iterators
+namespace Std
+open Std.Iterators
 
 /--
 This function is used in lemmas about iterator equivalence (`Iter.Equiv` and `IterM.Equiv`).
@@ -232,4 +233,4 @@ theorem IterM.Equiv.liftInner_stepAsHetT_bind_congr [Monad m] [LawfulMonad m]
   apply liftInner_stepAsHetT_pbind_congr h
   exact hfg
 
-end Std.Iterators
+end Std