address remarks

Author: datokrat

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

@@ -260,7 +260,7 @@ Steps through the whole iterator, counting the number of outputs emitted.
 
 **Performance**:
 
-linear in the number of steps taken by the iterator
+This function's runtime is linear in the number of steps taken by the iterator.
 -/
 @[always_inline, inline, expose]
 def Iter.count {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id]
@@ -272,7 +272,7 @@ Steps through the whole iterator, counting the number of outputs emitted.
 
 **Performance**:
 
-linear in the number of steps taken by the iterator
+This function's runtime is linear in the number of steps taken by the iterator.
 -/
 @[always_inline, inline, expose, deprecated Iter.count (since := "2025-10-29")]
 def Iter.size {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id]
@@ -284,7 +284,7 @@ Steps through the whole iterator, counting the number of outputs emitted.
 
 **Performance**:
 
-linear in the number of steps taken by the iterator
+This function's runtime is linear in the number of steps taken by the iterator.
 -/
 @[always_inline, inline, expose]
 def Iter.Partial.count {α : Type w} {β : Type w} [Iterator α Id β] [IteratorLoopPartial α Id Id]
@@ -296,7 +296,7 @@ Steps through the whole iterator, counting the number of outputs emitted.
 
 **Performance**:
 
-linear in the number of steps taken by the iterator
+This function's runtime is linear in the number of steps taken by the iterator.
 -/
 @[always_inline, inline, expose, deprecated Iter.Partial.count (since := "2025-10-29")]
 def Iter.Partial.size {α : Type w} {β : Type w} [Iterator α Id β] [IteratorLoopPartial α Id Id]

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

@@ -614,43 +614,25 @@ def IterM.Partial.find? {α β : Type w} {m : Type w → Type w'} [Monad m] [Ite
 
 section Count
 
-/--
-This is the implementation of the default instance `IteratorSize.defaultImplementation`.
--/
-@[always_inline, inline]
-def IterM.DefaultConsumers.count {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w}
-    [Iterator α m β] [Finite α m] [IteratorLoop α m m] (it : IterM (α := α) m β) :
-    m (ULift Nat) :=
-  it.fold (init := .up 0) fun acc _ => .up (acc.down + 1)
-
-/--
-This is the implementation of the default instance `IteratorSizePartial.defaultImplementation`.
--/
-@[always_inline, inline]
-def IterM.DefaultConsumers.countPartial {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w}
-    [Iterator α m β] [IteratorLoopPartial α m m] (it : IterM (α := α) m β) :
-    m (ULift Nat) :=
-  it.allowNontermination.fold (init := .up 0) fun acc _ => .up (acc.down + 1)
-
 /--
 Steps through the whole iterator, counting the number of outputs emitted.
 
 **Performance**:
 
-linear in the number of steps taken by the iterator
+This function's runtime is linear in the number of steps taken by the iterator.
 -/
 @[always_inline, inline]
 def IterM.count {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] [Finite α m]
     [IteratorLoop α m m]
     [Monad m] (it : IterM (α := α) m β) : m (ULift Nat) :=
-  IterM.DefaultConsumers.count it
+  it.fold (init := .up 0) fun acc _ => .up (acc.down + 1)
 
 /--
 Steps through the whole iterator, counting the number of outputs emitted.
 
 **Performance**:
 
-linear in the number of steps taken by the iterator
+This function's runtime is linear in the number of steps taken by the iterator.
 -/
 @[always_inline, inline, deprecated IterM.count (since := "2025-10-29")]
 def IterM.size {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] [Finite α m]
@@ -663,19 +645,19 @@ Steps through the whole iterator, counting the number of outputs emitted.
 
 **Performance**:
 
-linear in the number of steps taken by the iterator
+This function's runtime is linear in the number of steps taken by the iterator.
 -/
 @[always_inline, inline]
 def IterM.Partial.count {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
     [IteratorLoopPartial α m m] [Monad m] (it : IterM.Partial (α := α) m β) : m (ULift Nat) :=
-  IterM.DefaultConsumers.countPartial it.it
+  it.fold (init := .up 0) fun acc _ => .up (acc.down + 1)
 
 /--
 Steps through the whole iterator, counting the number of outputs emitted.
 
 **Performance**:
 
-linear in the number of steps taken by the iterator
+This function's runtime is linear in the number of steps taken by the iterator.
 -/
 @[always_inline, inline, deprecated IterM.Partial.count (since := "2025-10-29")]
 def IterM.Partial.size {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]

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

@@ -27,7 +27,7 @@ theorem Rcc.toArray_iter_eq_toArray [LE α] [DecidableLE α] [UpwardEnumerable 
  rfl
 
 @[simp]
-theorem Rcc.count_iter_eq_count [LE α] [DecidableLE α] [UpwardEnumerable α]
+theorem Rcc.count_iter_eq_size [LE α] [DecidableLE α] [UpwardEnumerable α]
     [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
     [Rxc.HasSize α] [Rxc.LawfulHasSize α]
     {r : Rcc α} :
@@ -47,7 +47,7 @@ theorem Rco.toArray_iter_eq_toArray [LT α] [DecidableLT α] [UpwardEnumerable 
  rfl
 
 @[simp]
-theorem Rco.count_iter_eq_count [LT α] [DecidableLT α] [UpwardEnumerable α]
+theorem Rco.count_iter_eq_size [LT α] [DecidableLT α] [UpwardEnumerable α]
     [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
     [Rxo.HasSize α] [Rxo.LawfulHasSize α]
     {r : Rco α} :
@@ -67,7 +67,7 @@ theorem Rci.toArray_iter_eq_toArray [UpwardEnumerable α]
  rfl
 
 @[simp]
-theorem Rci.count_iter_eq_count [UpwardEnumerable α]
+theorem Rci.count_iter_eq_size [UpwardEnumerable α]
     [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
     [Rxi.HasSize α] [Rxi.LawfulHasSize α]
     {r : Rci α} :
@@ -87,7 +87,7 @@ theorem Roc.toArray_iter_eq_toArray [LE α] [DecidableLE α] [UpwardEnumerable 
  rfl
 
 @[simp]
-theorem Roc.count_iter_eq_count [LE α] [DecidableLE α] [UpwardEnumerable α]
+theorem Roc.count_iter_eq_size [LE α] [DecidableLE α] [UpwardEnumerable α]
     [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
     [Rxc.HasSize α] [Rxc.LawfulHasSize α]
     {r : Roc α} :
@@ -107,7 +107,7 @@ theorem Roo.toArray_iter_eq_toArray [LT α] [DecidableLT α] [UpwardEnumerable 
  rfl
 
 @[simp]
-theorem Roo.count_iter_eq_count [LT α] [DecidableLT α] [UpwardEnumerable α]
+theorem Roo.count_iter_eq_size [LT α] [DecidableLT α] [UpwardEnumerable α]
     [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
     [Rxo.HasSize α] [Rxo.LawfulHasSize α]
     {r : Roo α} :
@@ -127,7 +127,7 @@ theorem Roi.toArray_iter_eq_toArray [UpwardEnumerable α]
  rfl
 
 @[simp]
-theorem Roi.count_iter_eq_count [UpwardEnumerable α]
+theorem Roi.count_iter_eq_size [UpwardEnumerable α]
     [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
     [Rxi.HasSize α] [Rxi.LawfulHasSize α]
     {r : Roi α} :
@@ -147,7 +147,7 @@ theorem Ric.toArray_iter_eq_toArray [Least? α] [LE α] [DecidableLE α] [Upward
  rfl
 
 @[simp]
-theorem Ric.count_iter_eq_count [Least? α] [LE α] [DecidableLE α] [UpwardEnumerable α]
+theorem Ric.count_iter_eq_size [Least? α] [LE α] [DecidableLE α] [UpwardEnumerable α]
     [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
     [Rxc.HasSize α] [Rxc.LawfulHasSize α]
     {r : Ric α} :
@@ -167,7 +167,7 @@ theorem Rio.toArray_iter_eq_toArray [Least? α] [LT α] [DecidableLT α] [Upward
  rfl
 
 @[simp]
-theorem Rio.count_iter_eq_count [Least? α] [LT α] [DecidableLT α] [UpwardEnumerable α]
+theorem Rio.count_iter_eq_size [Least? α] [LT α] [DecidableLT α] [UpwardEnumerable α]
     [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
     [Rxo.HasSize α] [Rxo.LawfulHasSize α]
     {r : Rio α} :
@@ -187,7 +187,7 @@ theorem Rii.toArray_iter_eq_toArray [Least? α] [UpwardEnumerable α]
  rfl
 
 @[simp]
-theorem Rii.count_iter_eq_count [Least? α] [UpwardEnumerable α]
+theorem Rii.count_iter_eq_size [Least? α] [UpwardEnumerable α]
     [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
     [Rxi.HasSize α] [Rxi.LawfulHasSize α]
     {r : Rii α} :

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

@@ -27,14 +27,22 @@ theorem iter_eq_toIteratorIter {γ : Type u} {s : Slice γ}
     s.iter = ToIterator.iter s := by
   simp [Internal.iter_eq_iter, Internal.iter_eq_toIteratorIter]
 
-theorem size_eq_size_iter [∀ s : Slice γ, ToIterator s Id β]
+theorem size_eq_count_iter [∀ s : Slice γ, ToIterator s Id β]
     [∀ s : Slice γ, Iterator (ToIterator.State s Id) Id β] {s : Slice γ}
     [Finite (ToIterator.State s Id) Id]
     [IteratorLoop (ToIterator.State s Id) Id Id] [LawfulIteratorLoop (ToIterator.State s Id) Id Id]
     [SliceSize γ] [LawfulSliceSize γ] :
     s.size = s.iter.count := by
   simp [Internal.iter_eq_iter, Internal.size_eq_count_iter]
 
+theorem count_iter_eq_size [∀ s : Slice γ, ToIterator s Id β]
+    [∀ s : Slice γ, Iterator (ToIterator.State s Id) Id β] {s : Slice γ}
+    [Finite (ToIterator.State s Id) Id]
+    [IteratorLoop (ToIterator.State s Id) Id Id] [LawfulIteratorLoop (ToIterator.State s Id) Id Id]
+    [SliceSize γ] [LawfulSliceSize γ] :
+    s.iter.count = s.size :=
+  size_eq_count_iter.symm
+
 theorem toArray_eq_toArray_iter {s : Slice γ} [ToIterator s Id β]
     [Iterator (ToIterator.State s Id) Id β] [IteratorCollect (ToIterator.State s Id) Id Id]
     [Finite (ToIterator.State s Id) Id] :