diff --git a/src/Init/Data/Iterators/Basic.lean b/src/Init/Data/Iterators/Basic.lean
index c5a69df4bf95..943f04186f86 100644
--- a/src/Init/Data/Iterators/Basic.lean
+++ b/src/Init/Data/Iterators/Basic.lean
@@ -10,6 +10,7 @@ public import Init.Classical
 public import Init.Ext
 
 set_option doc.verso true
+set_option linter.missingDocs true
 
 public section
 
@@ -349,14 +350,24 @@ abbrev PlausibleIterStep.casesOn {IsPlausibleStep : IterStep α β → Prop}
 end IterStep
 
 /--
-The typeclass providing the step function of an iterator in `Iter (α := α) β` or
-`IterM (α := α) m β`.
+The step function of an iterator in `Iter (α := α) β` or `IterM (α := α) m β`.
 
 In order to allow intrinsic termination proofs when iterating with the `step` function, the
 step object is bundled with a proof that it is a "plausible" step for the given current iterator.
 -/
 class Iterator (α : Type w) (m : Type w → Type w') (β : outParam (Type w)) where
+  /--
+  A relation that governs the allowed steps from a given iterator.
+
+  The "plausible" steps are those which make sense for a given state; plausibility can ensure
+  properties such as the successor iterator being drawn from the same collection, that an iterator
+  resulting from a skip will return the same next value, or that the next item yielded is next one
+  in the original collection.
+  -/
   IsPlausibleStep : IterM (α := α) m β → IterStep (IterM (α := α) m β) β → Prop
+  /--
+  Carries out a step of iteration.
+  -/
   step : (it : IterM (α := α) m β) → m (Shrink <| PlausibleIterStep <| IsPlausibleStep it)
 
 section Monadic
@@ -369,7 +380,7 @@ 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]
+@[deprecated IterM.mk (since := "2025-12-01"), inline, expose, inherit_doc IterM.mk]
 def Iterators.toIterM := @IterM.mk
 
 @[simp]
@@ -377,6 +388,7 @@ theorem IterM.mk_internalState {α m β} (it : IterM (α := α) m β) :
     .mk it.internalState m β = it :=
   rfl
 
+set_option linter.missingDocs false in
 @[deprecated IterM.mk_internalState (since := "2025-12-01")]
 def Iterators.toIterM_internalState := @IterM.mk_internalState
 
@@ -459,8 +471,10 @@ number of steps.
 -/
 inductive IterM.IsPlausibleIndirectOutput {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
     : IterM (α := α) m β → β → Prop where
+  /-- The output value could plausibly be emitted in the next step. -/
   | direct {it : IterM (α := α) m β} {out : β} : it.IsPlausibleOutput out →
       it.IsPlausibleIndirectOutput out
+  /-- The output value could plausibly be emitted in a step after the next step. -/
   | indirect {it it' : IterM (α := α) m β} {out : β} : it'.IsPlausibleSuccessorOf it →
       it'.IsPlausibleIndirectOutput out → it.IsPlausibleIndirectOutput out
 
@@ -470,7 +484,9 @@ finitely many steps. This relation is reflexive.
 -/
 inductive IterM.IsPlausibleIndirectSuccessorOf {α β : Type w} {m : Type w → Type w'}
     [Iterator α m β] : IterM (α := α) m β → IterM (α := α) m β → Prop where
+  /-- Every iterator is a plausible indirect successor of itself. -/
   | refl (it : IterM (α := α) m β) : it.IsPlausibleIndirectSuccessorOf it
+  /-- The iterator is a plausible successor of one of the current iterator's successors. -/
   | cons_right {it'' it' it : IterM (α := α) m β} (h' : it''.IsPlausibleIndirectSuccessorOf it')
       (h : it'.IsPlausibleSuccessorOf it) : it''.IsPlausibleIndirectSuccessorOf it
 
@@ -595,8 +611,10 @@ number of steps.
 -/
 inductive Iter.IsPlausibleIndirectOutput {α β : Type w} [Iterator α Id β] :
     Iter (α := α) β → β → Prop where
+  /-- The output value could plausibly be emitted in the next step. -/
   | direct {it : Iter (α := α) β} {out : β} : it.IsPlausibleOutput out →
       it.IsPlausibleIndirectOutput out
+  /-- The output value could plausibly be emitted in a step after the next step. -/
   | indirect {it it' : Iter (α := α) β} {out : β} : it'.IsPlausibleSuccessorOf it →
       it'.IsPlausibleIndirectOutput out → it.IsPlausibleIndirectOutput out
 
@@ -627,7 +645,9 @@ finitely many steps. This relation is reflexive.
 -/
 inductive Iter.IsPlausibleIndirectSuccessorOf {α : Type w} {β : Type w} [Iterator α Id β] :
     Iter (α := α) β → Iter (α := α) β → Prop where
+  /-- Every iterator is a plausible indirect successor of itself. -/
   | refl (it : Iter (α := α) β) : IsPlausibleIndirectSuccessorOf it it
+  /-- The iterator is a plausible indirect successor of one of the current iterator's successors. -/
   | cons_right {it'' it' it : Iter (α := α) β} (h' : it''.IsPlausibleIndirectSuccessorOf it')
       (h : it'.IsPlausibleSuccessorOf it) : it''.IsPlausibleIndirectSuccessorOf it
 
@@ -701,6 +721,11 @@ recursion over finite iterators. See also `IterM.finitelyManySteps` and `Iter.fi
 -/
 structure IterM.TerminationMeasures.Finite
     (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] where
+  /--
+  The wrapped iterator.
+
+  In the wrapper, its finiteness is used as a termination measure.
+  -/
   it : IterM (α := α) m β
 
 /--
@@ -827,6 +852,11 @@ recursion over productive iterators. See also `IterM.finitelyManySkips` and `Ite
 -/
 structure IterM.TerminationMeasures.Productive
     (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] where
+  /--
+  The wrapped iterator.
+
+  In the wrapper, its productivity is used as a termination measure.
+  -/
   it : IterM (α := α) m β
 
 /--
@@ -930,6 +960,9 @@ library.
 -/
 class LawfulDeterministicIterator (α : Type w) (m : Type w → Type w') [Iterator α m β]
     where
+  /--
+  Every iterator with state `α` in monad `m` has exactly one plausible step.
+  -/
   isPlausibleStep_eq_eq : ∀ it : IterM (α := α) m β, ∃ step, it.IsPlausibleStep = (· = step)
 
 namespace Iterators
@@ -940,14 +973,13 @@ This structure provides a more convenient way to define `Finite α m` instances
 -/
 structure FinitenessRelation (α : Type w) (m : Type w → Type w') {β : Type w}
     [Iterator α m β] where
-  /-
-  A well-founded relation such that if `it'` is a successor iterator of `it`, then
-  `Rel it' it`.
+  /--
+  A well-founded relation such that if `it'` is a successor iterator of `it`, then `Rel it' it`.
   -/
   Rel (it' it : IterM (α := α) m β) : Prop
-  /- A proof that `Rel` is well-founded. -/
+  /-- `Rel` is well-founded. -/
   wf : WellFounded Rel
-  /- A proof that if `it'` is a successor iterator of `it`, then `Rel it' it`. -/
+  /-- If `it'` is a successor iterator of `it`, then `Rel it' it`. -/
   subrelation : ∀ {it it'}, it'.IsPlausibleSuccessorOf it → Rel it' it
 
 theorem Finite.of_finitenessRelation
@@ -967,14 +999,13 @@ This structure provides a more convenient way to define `Productive α m` instan
 -/
 structure ProductivenessRelation (α : Type w) (m : Type w → Type w') {β : Type w}
     [Iterator α m β] where
-  /-
-  A well-founded relation such that if `it'` is obtained from `it` by skipping, then
-  `Rel it' it`.
+  /--
+  A well-founded relation such that if `it'` is obtained from `it` by skipping, then `Rel it' it`.
   -/
   Rel : (IterM (α := α) m β) → (IterM (α := α) m β) → Prop
-  /- A proof that `Rel` is well-founded. -/
+  /-- `Rel` is well-founded. -/
   wf : WellFounded Rel
-  /- A proof that if `it'` is obtained from `it` by skipping, then `Rel it' it`. -/
+  /-- If `it'` is obtained from `it` by skipping, then `Rel it' it`. -/
   subrelation : ∀ {it it'}, it'.IsPlausibleSkipSuccessorOf it → Rel it' it
 
 theorem Productive.of_productivenessRelation
diff --git a/src/Init/Data/Iterators/Consumers/Access.lean b/src/Init/Data/Iterators/Consumers/Access.lean
index 19e8560190c5..8e3e0b9f70fa 100644
--- a/src/Init/Data/Iterators/Consumers/Access.lean
+++ b/src/Init/Data/Iterators/Consumers/Access.lean
@@ -9,6 +9,8 @@ prelude
 public import Init.Data.Iterators.Consumers.Loop
 public import Init.Data.Iterators.Consumers.Monadic.Access
 
+set_option linter.missingDocs true
+
 @[expose] public section
 
 namespace Std
diff --git a/src/Init/Data/Iterators/Consumers/Monadic/Access.lean b/src/Init/Data/Iterators/Consumers/Monadic/Access.lean
index 52b26747adcc..da556b180dab 100644
--- a/src/Init/Data/Iterators/Consumers/Monadic/Access.lean
+++ b/src/Init/Data/Iterators/Consumers/Monadic/Access.lean
@@ -8,6 +8,8 @@ module
 prelude
 public import Init.Data.Iterators.Basic
 
+set_option linter.missingDocs true
+
 public section
 
 namespace Std
@@ -57,8 +59,8 @@ theorem IterM.not_isPlausibleNthOutputStep_yield {α β : Type w} {m : Type w 
 
 /--
 `IteratorAccess α m` provides efficient implementations for random access or iterators that support
-it. `it.nextAtIdx? n` either returns the step in which the `n`-th value of `it` is emitted
-(necessarily of the form `.yield _ _`) or `.done` if `it` terminates before emitting the `n`-th
+it. `it.nextAtIdx? n` either returns the step in which the `n`th value of `it` is emitted
+(necessarily of the form `.yield _ _`) or `.done` if `it` terminates before emitting the `n`th
 value.
 
 For monadic iterators, the monadic effects of this operation may differ from manually iterating
@@ -68,6 +70,11 @@ is guaranteed to plausible in the sense of `IterM.IsPlausibleNthOutputStep`.
 This class is experimental and users of the iterator API should not explicitly depend on it.
 -/
 class IteratorAccess (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] where
+  /--
+  `nextAtIdx? it n` either returns the step in which the `n`th value of `it` is emitted
+  (necessarily of the form `.yield _ _`) or `.done` if `it` terminates before emitting the `n`th
+  value.
+  -/
   nextAtIdx? (it : IterM (α := α) m β) (n : Nat) :
     m (PlausibleIterStep (it.IsPlausibleNthOutputStep n))
 
diff --git a/src/Init/Data/Iterators/Consumers/Monadic/Collect.lean b/src/Init/Data/Iterators/Consumers/Monadic/Collect.lean
index 53400e889331..e5b35a75ad3b 100644
--- a/src/Init/Data/Iterators/Consumers/Monadic/Collect.lean
+++ b/src/Init/Data/Iterators/Consumers/Monadic/Collect.lean
@@ -11,6 +11,8 @@ public import Init.Data.Iterators.Consumers.Monadic.Total
 public import Init.Data.Iterators.Internal.LawfulMonadLiftFunction
 public import Init.WFExtrinsicFix
 
+set_option linter.missingDocs true
+
 @[expose] public section
 
 /-!
diff --git a/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean b/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean
index 2c37dca73949..6c89c180cffb 100644
--- a/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean
+++ b/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean
@@ -11,6 +11,8 @@ public import Init.Data.Iterators.Internal.LawfulMonadLiftFunction
 public import Init.WFExtrinsicFix
 public import Init.Data.Iterators.Consumers.Monadic.Total
 
+set_option linter.missingDocs true
+
 public section
 
 /-!
@@ -70,6 +72,9 @@ provided by the standard library.
 @[ext]
 class IteratorLoop (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β]
     (n : Type x → Type x') where
+  /--
+  Iteration over the iterator `it` in the manner expected by `for` loops.
+  -/
   forIn : ∀ (_liftBind : (γ : Type w) → (δ : Type x) → (γ → n δ) → m γ → n δ) (γ : Type x),
       (plausible_forInStep : β → γ → ForInStep γ → Prop) →
       (it : IterM (α := α) m β) → γ →
@@ -82,7 +87,9 @@ end Typeclasses
 structure IteratorLoop.WithWF (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β]
     {γ : Type x} (PlausibleForInStep : β → γ → ForInStep γ → Prop)
     (hwf : IteratorLoop.WellFounded α m PlausibleForInStep) where
+  /-- Internal implementation detail of the iterator library. -/
   it : IterM (α := α) m β
+  /-- Internal implementation detail of the iterator library. -/
   acc : γ
 
 instance IteratorLoop.WithWF.instWellFoundedRelation
@@ -163,6 +170,7 @@ Asserts that a given `IteratorLoop` instance is equal to `IteratorLoop.defaultIm
 -/
 class LawfulIteratorLoop (α : Type w) (m : Type w → Type w') (n : Type x → Type x')
     [Monad m] [Monad n] [Iterator α m β] [i : IteratorLoop α m n] where
+  /-- The implementation of `IteratorLoop.forIn` in `i` is equal to the default implementation. -/
   lawful lift [LawfulMonadLiftBindFunction lift] γ it init
       (Pl : β → γ → ForInStep γ → Prop) (wf : IteratorLoop.WellFounded α m Pl)
       (f : (b : β) → it.IsPlausibleIndirectOutput b → (c : γ) → n (Subtype (Pl b c))) :
@@ -219,6 +227,7 @@ instance IterM.instForInOfIteratorLoop {m : Type w → Type w'} {n : Type w →
   haveI : ForIn' n (IterM (α := α) m β) β _ := IterM.instForIn'
   instForInOfForIn'
 
+/-- Internal implementation detail of the iterator library. -/
 @[always_inline, inline]
 def IterM.Partial.instForIn' {m : Type w → Type w'} {n : Type w → Type w''}
     {α : Type w} {β : Type w} [Iterator α m β] [IteratorLoop α m n] [MonadLiftT m n] [Monad n] :
@@ -226,6 +235,7 @@ def IterM.Partial.instForIn' {m : Type w → Type w'} {n : Type w → Type w''}
   forIn' it init f :=
     haveI := @IterM.instForIn'; forIn' it.it init f
 
+/-- Internal implementation detail of the iterator library. -/
 @[always_inline, inline]
 def IterM.Total.instForIn' {m : Type w → Type w'} {n : Type w → Type w''}
     {α : Type w} {β : Type w} [Iterator α m β] [IteratorLoop α m n] [MonadLiftT m n] [Monad n]
diff --git a/src/Init/Data/Iterators/Consumers/Monadic/Partial.lean b/src/Init/Data/Iterators/Consumers/Monadic/Partial.lean
index 50fb71983275..41545adc42d0 100644
--- a/src/Init/Data/Iterators/Consumers/Monadic/Partial.lean
+++ b/src/Init/Data/Iterators/Consumers/Monadic/Partial.lean
@@ -8,6 +8,8 @@ module
 prelude
 public import Init.Data.Iterators.Basic
 
+set_option linter.missingDocs true
+
 public section
 
 namespace Std
@@ -16,6 +18,9 @@ namespace Std
 A wrapper around an iterator that provides partial consumers. See `IterM.allowNontermination`.
 -/
 structure IterM.Partial {α : Type w} (m : Type w → Type w') (β : Type w) where
+  /--
+  The wrapped iterator, which was wrapped by `IterM.allowNontermination`.
+  -/
   it : IterM (α := α) m β
 
 /--
diff --git a/src/Init/Data/Iterators/Consumers/Monadic/Total.lean b/src/Init/Data/Iterators/Consumers/Monadic/Total.lean
index 87e7eaacece9..bf43a94998a9 100644
--- a/src/Init/Data/Iterators/Consumers/Monadic/Total.lean
+++ b/src/Init/Data/Iterators/Consumers/Monadic/Total.lean
@@ -9,12 +9,19 @@ prelude
 public import Init.Data.Iterators.Basic
 
 set_option doc.verso true
+set_option linter.missingDocs true
 
 public section
 
 namespace Std
 
+/--
+A wrapper around an iterator that provides total consumers. See `IterM.ensureTermination`.
+-/
 structure IterM.Total {α : Type w} (m : Type w → Type w') (β : Type w) where
+  /--
+  The wrapped iterator, which was wrapped by `IterM.ensureTermination`.
+  -/
   it : IterM (α := α) m β
 
 /--
diff --git a/src/Init/Data/Iterators/Consumers/Partial.lean b/src/Init/Data/Iterators/Consumers/Partial.lean
index 94fbed0f15ba..2eee2bf5ec60 100644
--- a/src/Init/Data/Iterators/Consumers/Partial.lean
+++ b/src/Init/Data/Iterators/Consumers/Partial.lean
@@ -8,6 +8,8 @@ module
 prelude
 public import Init.Data.Iterators.Basic
 
+set_option linter.missingDocs true
+
 public section
 
 namespace Std
@@ -16,6 +18,9 @@ namespace Std
 A wrapper around an iterator that provides partial consumers. See `Iter.allowNontermination`.
 -/
 structure Iter.Partial {α : Type w} (β : Type w) where
+  /--
+  The wrapped iterator, which was wrapped by `Iter.allowNontermination`.
+  -/
   it : Iter (α := α) β
 
 /--
diff --git a/src/Init/Data/Iterators/Consumers/Stream.lean b/src/Init/Data/Iterators/Consumers/Stream.lean
index 94332a520def..b62968042a3d 100644
--- a/src/Init/Data/Iterators/Consumers/Stream.lean
+++ b/src/Init/Data/Iterators/Consumers/Stream.lean
@@ -9,6 +9,8 @@ prelude
 public import Init.Data.Stream
 public import Init.Data.Iterators.Consumers.Access
 
+set_option linter.missingDocs true
+
 public section
 
 namespace Std
diff --git a/src/Init/Data/Iterators/Consumers/Total.lean b/src/Init/Data/Iterators/Consumers/Total.lean
index 5fd2d9611523..b3fd8e79c702 100644
--- a/src/Init/Data/Iterators/Consumers/Total.lean
+++ b/src/Init/Data/Iterators/Consumers/Total.lean
@@ -9,12 +9,19 @@ prelude
 public import Init.Data.Iterators.Basic
 
 set_option doc.verso true
+set_option linter.missingDocs true
 
 public section
 
 namespace Std
 
+/--
+A wrapper around an iterator that provides total consumers. See `Iter.ensureTermination`.
+-/
 structure Iter.Total {α : Type w} (β : Type w) where
+  /--
+  The wrapped iterator, which was wrapped by `Iter.ensureTermination`.
+  -/
   it : Iter (α := α) β
 
 /--
diff --git a/src/Init/Data/Range/Polymorphic/UpwardEnumerable.lean b/src/Init/Data/Range/Polymorphic/UpwardEnumerable.lean
index 92d774be4f8d..04d101a8b210 100644
--- a/src/Init/Data/Range/Polymorphic/UpwardEnumerable.lean
+++ b/src/Init/Data/Range/Polymorphic/UpwardEnumerable.lean
@@ -246,8 +246,12 @@ class InfinitelyUpwardEnumerable (α : Type u) [UpwardEnumerable α] where
 This propositional typeclass ensures that `UpwardEnumerable.succ?` is injective.
 -/
 class LinearlyUpwardEnumerable (α : Type u) [UpwardEnumerable α] where
+  /-- The implementation of `UpwardEnumerable.succ?` for `α` is injective. -/
   eq_of_succ?_eq : ∀ a b : α, UpwardEnumerable.succ? a = UpwardEnumerable.succ? b → a = b
 
+/--
+If a type is infinitely upwardly enumerable, then every element has a successor.
+-/
 theorem UpwardEnumerable.isSome_succ? {α : Type u} [UpwardEnumerable α]
     [InfinitelyUpwardEnumerable α] {a : α} : (succ? a).isSome :=
   InfinitelyUpwardEnumerable.isSome_succ? a