diff --git a/src/Init/Data/Iterators/Consumers/Loop.lean b/src/Init/Data/Iterators/Consumers/Loop.lean
index 34353d0dd3..29e9f2a715 100644
--- a/src/Init/Data/Iterators/Consumers/Loop.lean
+++ b/src/Init/Data/Iterators/Consumers/Loop.lean
@@ -675,9 +675,15 @@ Steps through the whole iterator, counting the number of outputs emitted.
 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 β] [IteratorLoop α Id Id]
+def Iter.length {α : Type w} {β : Type w} [Iterator α Id β] [IteratorLoop α Id Id]
     (it : Iter (α := α) β) : Nat :=
-  it.toIterM.count.run.down
+  it.toIterM.length.run.down
+
+@[inline, inherit_doc Iter.length, deprecated Iter.length (since := "2026-01-28"), expose]
+def Iter.count := @Iter.length
+
+@[inline, inherit_doc Iter.length, deprecated Iter.length (since := "2025-10-29"), expose]
+def Iter.size := @Iter.length
 
 /--
 Steps through the whole iterator, counting the number of outputs emitted.
@@ -686,22 +692,10 @@ Steps through the whole iterator, counting the number of outputs emitted.
 
 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 β] [IteratorLoop α Id Id]
-    (it : Iter (α := α) β) : Nat :=
-   it.count
-
-/--
-Steps through the whole iterator, counting the number of outputs emitted.
-
-**Performance**:
-
-This function's runtime is linear in the number of steps taken by the iterator.
--/
-@[always_inline, inline, expose, deprecated Iter.count (since := "2025-12-04")]
+@[always_inline, inline, expose, deprecated Iter.length (since := "2025-12-04")]
 def Iter.Partial.count {α : Type w} {β : Type w} [Iterator α Id β] [IteratorLoop α Id Id]
     (it : Iter.Partial (α := α) β) : Nat :=
-  it.it.toIterM.count.run.down
+  it.it.toIterM.length.run.down
 
 /--
 Steps through the whole iterator, counting the number of outputs emitted.
@@ -710,9 +704,9 @@ Steps through the whole iterator, counting the number of outputs emitted.
 
 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")]
+@[always_inline, inline, expose, deprecated Iter.length (since := "2025-10-29")]
 def Iter.Partial.size {α : Type w} {β : Type w} [Iterator α Id β] [IteratorLoop α Id Id]
     (it : Iter.Partial (α := α) β) : Nat :=
-  it.it.count
+  it.it.length
 
 end Std
diff --git a/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean b/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean
index 3bbb537f2f..372ca8171b 100644
--- a/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean
+++ b/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean
@@ -960,21 +960,15 @@ Steps through the whole iterator, counting the number of outputs emitted.
 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 β]
+def IterM.length {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
     [IteratorLoop α m m] [Monad m] (it : IterM (α := α) m β) : m (ULift Nat) :=
   it.fold (init := .up 0) fun acc _ => .up (acc.down + 1)
 
-/--
-Steps through the whole iterator, counting the number of outputs emitted.
+@[inline, inherit_doc IterM.length, deprecated IterM.length (since := "2026-01-28"), expose]
+def IterM.count := @IterM.length
 
-**Performance**:
-
-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 β]
-    [IteratorLoop α m m] [Monad m] (it : IterM (α := α) m β) : m (ULift Nat) :=
-  it.count
+@[inline, inherit_doc IterM.length, deprecated IterM.length (since := "2025-10-29"), expose]
+def IterM.size := @IterM.length
 
 /--
 Steps through the whole iterator, counting the number of outputs emitted.
@@ -983,7 +977,7 @@ Steps through the whole iterator, counting the number of outputs emitted.
 
 This function's runtime is linear in the number of steps taken by the iterator.
 -/
-@[always_inline, inline, deprecated IterM.count (since := "2025-12-04")]
+@[always_inline, inline, deprecated IterM.length (since := "2025-12-04")]
 def IterM.Partial.count {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
     [IteratorLoop α m m] [Monad m] (it : IterM.Partial (α := α) m β) : m (ULift Nat) :=
   it.it.fold (init := .up 0) fun acc _ => .up (acc.down + 1)
@@ -995,10 +989,10 @@ Steps through the whole iterator, counting the number of outputs emitted.
 
 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")]
+@[always_inline, inline, deprecated IterM.length (since := "2025-10-29")]
 def IterM.Partial.size {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
     [IteratorLoop α m m] [Monad m] (it : IterM.Partial (α := α) m β) : m (ULift Nat) :=
-  it.it.count
+  it.it.length
 
 end Count
 
diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Attach.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Attach.lean
index d4cd6f310c..c5f70936ca 100644
--- a/src/Init/Data/Iterators/Lemmas/Combinators/Attach.lean
+++ b/src/Init/Data/Iterators/Lemmas/Combinators/Attach.lean
@@ -79,12 +79,15 @@ theorem Iter.toArray_attachWith [Iterator α Id β]
   simp [Iter.toList_toArray]
 
 @[simp]
-theorem Iter.count_attachWith [Iterator α Id β]
+theorem Iter.length_attachWith [Iterator α Id β]
     {it : Iter (α := α) β} {hP}
     [Finite α Id] [IteratorLoop α Id Id]
     [LawfulIteratorLoop α Id Id] :
-    (it.attachWith P hP).count = it.count := by
-  rw [← Iter.length_toList_eq_count, toList_attachWith]
+    (it.attachWith P hP).length = it.length := by
+  rw [← Iter.length_toList_eq_length, toList_attachWith]
   simp
 
+@[deprecated Iter.length_attachWith (since := "2026-01-28")]
+def Iter.count_attachWith := @Iter.length_attachWith
+
 end Std
diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean b/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean
index 9de230600e..19cac45e86 100644
--- a/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean
+++ b/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean
@@ -722,11 +722,14 @@ end Fold
 section Count
 
 @[simp]
-theorem Iter.count_map {α β β' : Type w} [Iterator α Id β]
+theorem Iter.length_map {α β β' : Type w} [Iterator α Id β]
     [IteratorLoop α Id Id] [Finite α Id] [LawfulIteratorLoop α Id Id]
     {it : Iter (α := α) β} {f : β → β'} :
-    (it.map f).count = it.count := by
-  simp [map_eq_toIter_map_toIterM, count_eq_count_toIterM]
+    (it.map f).length = it.length := by
+  simp [map_eq_toIter_map_toIterM, length_eq_length_toIterM]
+
+@[deprecated Iter.length_map (since := "2026-01-28")]
+def Iter.count_map := @Iter.length_map
 
 end Count
 
diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/Attach.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/Attach.lean
index 94c65513da..5d356d40cb 100644
--- a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/Attach.lean
+++ b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/Attach.lean
@@ -60,12 +60,15 @@ theorem IterM.map_unattach_toArray_attachWith [Iterator α m β] [Monad m] [Mona
   simp [-map_unattach_toList_attachWith, -IterM.toArray_toList]
 
 @[simp]
-theorem IterM.count_attachWith [Iterator α m β] [Monad m] [Monad n]
+theorem IterM.length_attachWith [Iterator α m β] [Monad m] [Monad n]
     {it : IterM (α := α) m β} {hP}
     [Finite α m] [IteratorLoop α m m] [LawfulMonad m] [LawfulIteratorLoop α m m] :
-    (it.attachWith P hP).count = it.count := by
-  rw [← up_length_toList_eq_count, ← up_length_toList_eq_count,
+    (it.attachWith P hP).length = it.length := by
+  rw [← up_length_toList_eq_length, ← up_length_toList_eq_length,
     ← map_unattach_toList_attachWith (it := it) (P := P) (hP := hP)]
   simp only [Functor.map_map, List.length_unattach]
 
+@[deprecated IterM.length_attachWith (since := "2026-01-28")]
+def IterM.count_attachWith := @IterM.length_attachWith
+
 end Std
diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
index f1ea02df95..f5d32b4ed4 100644
--- a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
+++ b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
@@ -1620,18 +1620,21 @@ end Fold
 section Count
 
 @[simp]
-theorem IterM.count_map {α β β' : Type w} {m : Type w → Type w'} [Iterator α m β] [Monad m]
+theorem IterM.length_map {α β β' : Type w} {m : Type w → Type w'} [Iterator α m β] [Monad m]
     [IteratorLoop α m m] [Finite α m] [LawfulMonad m] [LawfulIteratorLoop α m m]
     {it : IterM (α := α) m β} {f : β → β'} :
-    (it.map f).count = it.count := by
+    (it.map f).length = it.length := by
   induction it using IterM.inductSteps with | step it ihy ihs
-  rw [count_eq_match_step, count_eq_match_step, step_map, bind_assoc]
+  rw [length_eq_match_step, length_eq_match_step, step_map, bind_assoc]
   apply bind_congr; intro step
   cases step.inflate using PlausibleIterStep.casesOn
   · simp [ihy ‹_›]
   · simp [ihs ‹_›]
   · simp
 
+@[deprecated IterM.length_map (since := "2026-01-28")]
+def IterM.count_map := @IterM.length_map
+
 end Count
 
 section AnyAll
diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.lean
index ba5ad245ad..16c7095646 100644
--- a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.lean
+++ b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.lean
@@ -66,14 +66,14 @@ theorem IterM.toArray_uLift [Iterator α m β] [Monad m] [Monad n] {it : IterM (
   simp
 
 @[simp]
-theorem IterM.count_uLift [Iterator α m β] [Monad m] [Monad n] {it : IterM (α := α) m β}
+theorem IterM.length_uLift [Iterator α m β] [Monad m] [Monad n] {it : IterM (α := α) m β}
     [MonadLiftT m (ULiftT n)] [Finite α m] [IteratorLoop α m m]
     [LawfulMonad m] [LawfulMonad n] [LawfulIteratorLoop α m m]
     [LawfulMonadLiftT m (ULiftT n)] :
-    (it.uLift n).count =
-      (.up ·.down.down) <$> (monadLift (n := ULiftT n) it.count).run := by
+    (it.uLift n).length =
+      (.up ·.down.down) <$> (monadLift (n := ULiftT n) it.length).run := by
   induction it using IterM.inductSteps with | step it ihy ihs
-  rw [count_eq_match_step, count_eq_match_step, monadLift_bind, map_eq_pure_bind, step_uLift]
+  rw [length_eq_match_step, length_eq_match_step, monadLift_bind, map_eq_pure_bind, step_uLift]
   simp only [bind_assoc, ULiftT.run_bind]
   apply bind_congr; intro step
   cases step.down.inflate using PlausibleIterStep.casesOn
@@ -81,4 +81,7 @@ theorem IterM.count_uLift [Iterator α m β] [Monad m] [Monad n] {it : IterM (α
   · simp [ihs ‹_›]
   · simp
 
+@[deprecated IterM.length_uLift (since := "2026-01-28")]
+def IterM.count_uLift := @IterM.length_uLift
+
 end Std
diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/ULift.lean b/src/Init/Data/Iterators/Lemmas/Combinators/ULift.lean
index 1cffee449e..af1983e64c 100644
--- a/src/Init/Data/Iterators/Lemmas/Combinators/ULift.lean
+++ b/src/Init/Data/Iterators/Lemmas/Combinators/ULift.lean
@@ -57,11 +57,14 @@ theorem Iter.toArray_uLift [Iterator α Id β] {it : Iter (α := α) β}
   simp [-toArray_toList]
 
 @[simp]
-theorem Iter.count_uLift [Iterator α Id β] {it : Iter (α := α) β}
+theorem Iter.length_uLift [Iterator α Id β] {it : Iter (α := α) β}
     [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] :
-    it.uLift.count = it.count := by
-  simp only [monadLift, uLift_eq_toIter_uLift_toIterM, count_eq_count_toIterM, toIterM_toIter]
-  rw [IterM.count_uLift]
+    it.uLift.length = it.length := by
+  simp only [monadLift, uLift_eq_toIter_uLift_toIterM, length_eq_length_toIterM, toIterM_toIter]
+  rw [IterM.length_uLift]
   simp [monadLift]
 
+@[deprecated Iter.length_uLift (since := "2026-01-28")]
+def Iter.count_uLift := @Iter.length_uLift
+
 end Std
diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean
index 74e0e47384..d357010a7a 100644
--- a/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean
+++ b/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean
@@ -460,69 +460,90 @@ theorem Iter.foldl_toArray {α β : Type w} {γ : Type x} [Iterator α Id β] [F
     it.toArray.foldl (init := init) f = it.fold (init := init) f := by
   rw [fold_eq_foldM, Array.foldl_eq_foldlM, ← Iter.foldlM_toArray]
 
-theorem Iter.count_eq_count_toIterM {α β : Type w} [Iterator α Id β]
+theorem Iter.length_eq_length_toIterM {α β : Type w} [Iterator α Id β]
     [Finite α Id] [IteratorLoop α Id Id.{w}] {it : Iter (α := α) β} :
-    it.count = it.toIterM.count.run.down :=
+    it.length = it.toIterM.length.run.down :=
   (rfl)
 
-theorem Iter.count_eq_fold {α β : Type w} [Iterator α Id β]
+@[deprecated Iter.length_eq_length_toIterM (since := "2026-01-28")]
+def Iter.count_eq_count_toIterM := @Iter.length_eq_length_toIterM
+
+theorem Iter.length_eq_fold {α β : Type w} [Iterator α Id β]
     [Finite α Id] [IteratorLoop α Id Id.{w}] [LawfulIteratorLoop α Id Id.{w}]
     [IteratorLoop α Id Id.{0}] [LawfulIteratorLoop α Id Id.{0}]
     {it : Iter (α := α) β} :
-    it.count = it.fold (γ := Nat) (init := 0) (fun acc _ => acc + 1) := by
-  rw [count_eq_count_toIterM, IterM.count_eq_fold, ← fold_eq_fold_toIterM]
+    it.length = it.fold (γ := Nat) (init := 0) (fun acc _ => acc + 1) := by
+  rw [length_eq_length_toIterM, IterM.length_eq_fold, ← fold_eq_fold_toIterM]
   rw [← fold_hom (f := ULift.down)]
   simp
 
-theorem Iter.count_eq_forIn {α β : Type w} [Iterator α Id β]
+@[deprecated Iter.length_eq_fold (since := "2026-01-28")]
+def Iter.count_eq_fold := @Iter.length_eq_fold
+
+theorem Iter.length_eq_forIn {α β : Type w} [Iterator α Id β]
     [Finite α Id] [IteratorLoop α Id Id.{w}] [LawfulIteratorLoop α Id Id.{w}]
     [IteratorLoop α Id Id.{0}] [LawfulIteratorLoop α Id Id.{0}]
     {it : Iter (α := α) β} :
-    it.count = (ForIn.forIn (m := Id) it 0 (fun _ acc => return .yield (acc + 1))).run := by
-  rw [count_eq_fold, forIn_pure_yield_eq_fold, Id.run_pure]
+    it.length = (ForIn.forIn (m := Id) it 0 (fun _ acc => return .yield (acc + 1))).run := by
+  rw [length_eq_fold, forIn_pure_yield_eq_fold, Id.run_pure]
 
-theorem Iter.count_eq_match_step {α β : Type w} [Iterator α Id β]
+@[deprecated Iter.length_eq_forIn (since := "2026-01-28")]
+def Iter.count_eq_forIn := @Iter.length_eq_forIn
+
+theorem Iter.length_eq_match_step {α β : Type w} [Iterator α Id β]
     [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
     {it : Iter (α := α) β} :
-    it.count = (match it.step.val with
-      | .yield it' _ => it'.count + 1
-      | .skip it' => it'.count
+    it.length = (match it.step.val with
+      | .yield it' _ => it'.length + 1
+      | .skip it' => it'.length
       | .done => 0) := by
-  simp only [count_eq_count_toIterM]
-  rw [IterM.count_eq_match_step]
+  simp only [length_eq_length_toIterM]
+  rw [IterM.length_eq_match_step]
   simp only [bind_pure_comp, id_map', Id.run_bind, Iter.step]
   cases it.toIterM.step.run.inflate using PlausibleIterStep.casesOn <;> simp
 
-@[simp]
-theorem Iter.size_toArray_eq_count {α β : Type w} [Iterator α Id β] [Finite α Id]
-    [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
-    {it : Iter (α := α) β} :
-    it.toArray.size = it.count := by
-  simp only [toArray_eq_toArray_toIterM, count_eq_count_toIterM, Id.run_map,
-    ← IterM.up_size_toArray_eq_count]
-
-@[deprecated Iter.size_toArray_eq_count (since := "2025-10-29")]
-def Iter.size_toArray_eq_size := @size_toArray_eq_count
+@[deprecated Iter.length_eq_match_step (since := "2026-01-28")]
+def Iter.count_eq_match_step := @Iter.length_eq_match_step
 
 @[simp]
-theorem Iter.length_toList_eq_count {α β : Type w} [Iterator α Id β] [Finite α Id]
+theorem Iter.size_toArray_eq_length {α β : Type w} [Iterator α Id β] [Finite α Id]
     [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
     {it : Iter (α := α) β} :
-    it.toList.length = it.count := by
-  rw [← toList_toArray, Array.length_toList, size_toArray_eq_count]
+    it.toArray.size = it.length := by
+  simp only [toArray_eq_toArray_toIterM, length_eq_length_toIterM, Id.run_map,
+    ← IterM.up_size_toArray_eq_length]
 
-@[deprecated Iter.length_toList_eq_count (since := "2025-10-29")]
-def Iter.length_toList_eq_size := @length_toList_eq_count
+@[deprecated Iter.size_toArray_eq_length (since := "2025-10-29")]
+def Iter.size_toArray_eq_size := @size_toArray_eq_length
+
+@[deprecated Iter.size_toArray_eq_length (since := "2026-01-28")]
+def Iter.size_toArray_eq_count := @size_toArray_eq_length
 
 @[simp]
-theorem Iter.length_toListRev_eq_count {α β : Type w} [Iterator α Id β] [Finite α Id]
+theorem Iter.length_toList_eq_length {α β : Type w} [Iterator α Id β] [Finite α Id]
     [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
     {it : Iter (α := α) β} :
-    it.toListRev.length = it.count := by
-  rw [toListRev_eq, List.length_reverse, length_toList_eq_count]
+    it.toList.length = it.length := by
+  rw [← toList_toArray, Array.length_toList, size_toArray_eq_length]
 
-@[deprecated Iter.length_toListRev_eq_count (since := "2025-10-29")]
-def Iter.length_toListRev_eq_size := @length_toListRev_eq_count
+@[deprecated Iter.length_toList_eq_length (since := "2025-10-29")]
+def Iter.length_toList_eq_size := @length_toList_eq_length
+
+@[deprecated Iter.length_toList_eq_length (since := "2026-01-28")]
+def Iter.length_toList_eq_count := @length_toList_eq_length
+
+@[simp]
+theorem Iter.length_toListRev_eq_length {α β : Type w} [Iterator α Id β] [Finite α Id]
+    [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
+    {it : Iter (α := α) β} :
+    it.toListRev.length = it.length := by
+  rw [toListRev_eq, List.length_reverse, length_toList_eq_length]
+
+@[deprecated Iter.length_toListRev_eq_length (since := "2025-10-29")]
+def Iter.length_toListRev_eq_size := @length_toListRev_eq_length
+
+@[deprecated Iter.length_toListRev_eq_length (since := "2026-01-28")]
+def Iter.length_toListRev_eq_count := @length_toListRev_eq_length
 
 theorem Iter.anyM_eq_forIn {α β : Type w} {m : Type → Type w'} [Iterator α Id β]
     [Finite α Id] [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean
index 1599b1e560..c4d95f9c31 100644
--- a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean
+++ b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean
@@ -476,27 +476,33 @@ theorem IterM.drain_eq_map_toArray {α β : Type w} {m : Type w → Type w'} [It
     it.drain = (fun _ => .unit) <$> it.toList := by
   simp [IterM.drain_eq_map_toList]
 
-theorem IterM.count_eq_fold {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
+theorem IterM.length_eq_fold {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
     [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m]
     {it : IterM (α := α) m β} :
-    it.count = it.fold (init := .up 0) (fun acc _ => .up <| acc.down + 1) :=
+    it.length = it.fold (init := .up 0) (fun acc _ => .up <| acc.down + 1) :=
   (rfl)
 
-theorem IterM.count_eq_forIn {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
+@[deprecated IterM.length_eq_fold (since := "2026-01-28")]
+def IterM.count_eq_fold := @IterM.length_eq_fold
+
+theorem IterM.length_eq_forIn {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
     [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m]
     {it : IterM (α := α) m β} :
-    it.count = ForIn.forIn it (.up 0) (fun _ acc => return .yield (.up (acc.down + 1))) :=
+    it.length = ForIn.forIn it (.up 0) (fun _ acc => return .yield (.up (acc.down + 1))) :=
   (rfl)
 
-theorem IterM.count_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
+@[deprecated IterM.length_eq_forIn (since := "2026-01-28")]
+def IterM.count_eq_forIn := @IterM.length_eq_forIn
+
+theorem IterM.length_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
     [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
     {it : IterM (α := α) m β} :
-    it.count = (do
+    it.length = (do
       match (← it.step).inflate.val with
-      | .yield it' _ => return .up ((← it'.count).down + 1)
-      | .skip it' => return .up (← it'.count).down
+      | .yield it' _ => return .up ((← it'.length).down + 1)
+      | .skip it' => return .up (← it'.length).down
       | .done => return .up 0) := by
-  simp only [count_eq_fold]
+  simp only [length_eq_fold]
   have (acc : Nat) (it' : IterM (α := α) m β) :
       it'.fold (init := ULift.up acc) (fun acc _ => .up (acc.down + 1)) =
         (ULift.up <| ·.down + acc) <$>
@@ -512,33 +518,45 @@ theorem IterM.count_eq_match_step {α β : Type w} {m : Type w → Type w'} [Ite
   · simp
   · simp
 
+@[deprecated IterM.length_eq_match_step (since := "2026-01-28")]
+def IterM.count_eq_match_step := @IterM.length_eq_match_step
+
 @[simp]
-theorem IterM.up_size_toArray_eq_count {α β : Type w} [Iterator α m β] [Finite α m]
+theorem IterM.up_size_toArray_eq_length {α β : Type w} [Iterator α m β] [Finite α m]
     [Monad m] [LawfulMonad m]
     [IteratorLoop α m m] [LawfulIteratorLoop α m m]
     {it : IterM (α := α) m β} :
-    (.up <| ·.size) <$> it.toArray = it.count := by
-  rw [toArray_eq_fold, count_eq_fold, ← fold_hom]
+    (.up <| ·.size) <$> it.toArray = it.length := by
+  rw [toArray_eq_fold, length_eq_fold, ← fold_hom]
   · simp only [List.size_toArray, List.length_nil]; rfl
   · simp
 
+@[deprecated IterM.up_size_toArray_eq_length (since := "2026-01-28")]
+def IterM.up_size_toArray_eq_count := @IterM.up_size_toArray_eq_length
+
 @[simp]
-theorem IterM.up_length_toList_eq_count {α β : Type w} [Iterator α m β] [Finite α m]
+theorem IterM.up_length_toList_eq_length {α β : Type w} [Iterator α m β] [Finite α m]
     [Monad m] [LawfulMonad m]
     [IteratorLoop α m m] [LawfulIteratorLoop α m m]
     {it : IterM (α := α) m β} :
-    (.up <| ·.length) <$> it.toList = it.count := by
-  rw [toList_eq_fold, count_eq_fold, ← fold_hom]
+    (.up <| ·.length) <$> it.toList = it.length := by
+  rw [toList_eq_fold, length_eq_fold, ← fold_hom]
   · simp only [List.length_nil]; rfl
   · simp
 
+@[deprecated IterM.up_length_toList_eq_length (since := "2026-01-28")]
+def IterM.up_length_toList_eq_count := @IterM.up_length_toList_eq_length
+
 @[simp]
-theorem IterM.up_length_toListRev_eq_count {α β : Type w} [Iterator α m β] [Finite α m]
+theorem IterM.up_length_toListRev_eq_length {α β : Type w} [Iterator α m β] [Finite α m]
     [Monad m] [LawfulMonad m]
     [IteratorLoop α m m] [LawfulIteratorLoop α m m]
     {it : IterM (α := α) m β} :
-    (.up <| ·.length) <$> it.toListRev = it.count := by
-  simp only [toListRev_eq, Functor.map_map, List.length_reverse, up_length_toList_eq_count]
+    (.up <| ·.length) <$> it.toListRev = it.length := by
+  simp only [toListRev_eq, Functor.map_map, List.length_reverse, up_length_toList_eq_length]
+
+@[deprecated IterM.up_length_toListRev_eq_length (since := "2026-01-28")]
+def IterM.up_length_toListRev_eq_count := @IterM.up_length_toListRev_eq_length
 
 theorem IterM.anyM_eq_forIn {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
     [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
diff --git a/src/Init/Data/Slice/Array/Lemmas.lean b/src/Init/Data/Slice/Array/Lemmas.lean
index dd8e1bfbf4..8549aed766 100644
--- a/src/Init/Data/Slice/Array/Lemmas.lean
+++ b/src/Init/Data/Slice/Array/Lemmas.lean
@@ -85,9 +85,12 @@ theorem toList_eq {α : Type u} {it : Iter (α := SubarrayIterator α) α} :
   · rw [dif_neg]; rotate_left; exact h
     simp_all [it.internalState.xs.stop_le_array_size]
 
-theorem count_eq {α : Type u} {it : Iter (α := SubarrayIterator α) α} :
-    it.count = it.internalState.xs.stop - it.internalState.xs.start := by
-  simp [← Iter.length_toList_eq_count, toList_eq, it.internalState.xs.stop_le_array_size]
+theorem length_eq {α : Type u} {it : Iter (α := SubarrayIterator α) α} :
+    it.length = it.internalState.xs.stop - it.internalState.xs.start := by
+  simp [← Iter.length_toList_eq_length, toList_eq, it.internalState.xs.stop_le_array_size]
+
+@[deprecated length_eq (since := "2026-01-28")]
+def count_eq := @length_eq
 
 end SubarrayIterator
 
@@ -105,7 +108,7 @@ theorem toList_internalIter {α : Type u} {s : Subarray α} :
 public instance : LawfulSliceSize (Internal.SubarrayData α) where
   lawful s := by
     simp [SliceSize.size, ToIterator.iter_eq, Iter.toIter_toIterM,
-      ← Iter.length_toList_eq_count, SubarrayIterator.toList_eq,
+      ← Iter.length_toList_eq_length, SubarrayIterator.toList_eq,
       s.internalRepresentation.stop_le_array_size, start, stop, array]
 
 public theorem toArray_eq_sliceToArray {α : Type u} {s : Subarray α} :
diff --git a/src/Init/Data/Slice/Lemmas.lean b/src/Init/Data/Slice/Lemmas.lean
index b0707cd9fd..d5e436e523 100644
--- a/src/Init/Data/Slice/Lemmas.lean
+++ b/src/Init/Data/Slice/Lemmas.lean
@@ -60,12 +60,15 @@ public theorem forIn_toArray {γ : Type u} {β : Type v}
     ForIn.forIn s.toArray init f = ForIn.forIn s init f := by
   rw [← forIn_internalIter, ← Iter.forIn_toArray, Slice.toArray]
 
-theorem Internal.size_eq_count_iter [ToIterator (Slice γ) Id α β]
+theorem Internal.size_eq_length_iter [ToIterator (Slice γ) Id α β]
     [Iterator α Id β] [Finite α Id]
     [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
     {s : Slice γ} [SliceSize γ] [LawfulSliceSize γ] :
-    s.size = (Internal.iter s).count := by
-  simp only [Slice.size, iter, LawfulSliceSize.lawful, ← Iter.length_toList_eq_count]
+    s.size = (Internal.iter s).length := by
+  simp only [Slice.size, iter, LawfulSliceSize.lawful, ← Iter.length_toList_eq_length]
+
+@[deprecated Internal.size_eq_length_iter (since := "2026-01-28")]
+def Internal.size_eq_count_iter := @Internal.size_eq_length_iter
 
 theorem Internal.toArray_eq_toArray_iter {s : Slice γ} [ToIterator (Slice γ) Id α β]
     [Iterator α Id β]
@@ -91,7 +94,7 @@ theorem size_toArray_eq_size [ToIterator (Slice γ) Id α β]
     {s : Slice γ} :
     s.toArray.size = s.size := by
   letI : IteratorLoop α Id Id := .defaultImplementation
-  rw [Internal.size_eq_count_iter, Internal.toArray_eq_toArray_iter, Iter.size_toArray_eq_count]
+  rw [Internal.size_eq_length_iter, Internal.toArray_eq_toArray_iter, Iter.size_toArray_eq_length]
 
 @[simp]
 theorem length_toList_eq_size [ToIterator (Slice γ) Id α β]
@@ -100,7 +103,7 @@ theorem length_toList_eq_size [ToIterator (Slice γ) Id α β]
     [Finite α Id] :
     s.toList.length = s.size := by
   letI : IteratorLoop α Id Id := .defaultImplementation
-  rw [Internal.size_eq_count_iter, Internal.toList_eq_toList_iter, Iter.length_toList_eq_count]
+  rw [Internal.size_eq_length_iter, Internal.toList_eq_toList_iter, Iter.length_toList_eq_length]
 
 @[simp]
 theorem length_toListRev_eq_size [ToIterator (Slice γ) Id α β]
@@ -109,7 +112,7 @@ theorem length_toListRev_eq_size [ToIterator (Slice γ) Id α β]
     [Finite α Id]
     [LawfulIteratorLoop α Id Id] :
     s.toListRev.length = s.size := by
-  rw [Internal.size_eq_count_iter, Internal.toListRev_eq_toListRev_iter,
-    Iter.length_toListRev_eq_count]
+  rw [Internal.size_eq_length_iter, Internal.toListRev_eq_toListRev_iter,
+    Iter.length_toListRev_eq_length]
 
 end Std.Slice
diff --git a/src/Init/Data/Slice/List/Iterator.lean b/src/Init/Data/Slice/List/Iterator.lean
index 087155ef6f..6e81ce4680 100644
--- a/src/Init/Data/Slice/List/Iterator.lean
+++ b/src/Init/Data/Slice/List/Iterator.lean
@@ -34,7 +34,7 @@ attribute [instance] ListSlice.instToIterator
 universe v w
 
 instance : SliceSize (Internal.ListSliceData α) where
-  size s := (Internal.iter s).count
+  size s := (Internal.iter s).length
 
 @[no_expose]
 instance {α : Type u} {m : Type v → Type w} [Monad m] :
diff --git a/src/Init/Data/Slice/List/Lemmas.lean b/src/Init/Data/Slice/List/Lemmas.lean
index 6678085516..bfb4f0d7b7 100644
--- a/src/Init/Data/Slice/List/Lemmas.lean
+++ b/src/Init/Data/Slice/List/Lemmas.lean
@@ -60,7 +60,7 @@ public theorem toList_toArray {xs : ListSlice α} :
 @[simp, grind =]
 public theorem length_toList {xs : ListSlice α} :
     xs.toList.length = xs.size := by
-  simp [ListSlice.toList_eq, Std.Slice.size, Std.Slice.SliceSize.size, ← Iter.length_toList_eq_count,
+  simp [ListSlice.toList_eq, Std.Slice.size, Std.Slice.SliceSize.size, ← Iter.length_toList_eq_length,
     toList_internalIter]; rfl
 
 @[grind =]
diff --git a/src/Init/Data/Slice/Operations.lean b/src/Init/Data/Slice/Operations.lean
index bdc11145aa..67b8f79d74 100644
--- a/src/Init/Data/Slice/Operations.lean
+++ b/src/Init/Data/Slice/Operations.lean
@@ -45,7 +45,7 @@ class LawfulSliceSize (γ : Type u) [SliceSize γ] [ToIterator (Slice γ) Id α
   /-- The iterator of a slice `s` of type `Slice γ` emits exactly `SliceSize.size s` elements. -/
   lawful :
       letI : IteratorLoop α Id Id := .defaultImplementation
-      ∀ s : Slice γ, SliceSize.size s = (ToIterator.iter (γ := Slice γ) s).count
+      ∀ s : Slice γ, SliceSize.size s = (ToIterator.iter (γ := Slice γ) s).length
 
 /--
 Returns the number of elements with distinct indices in the given slice.
diff --git a/src/Init/Data/String/Slice.lean b/src/Init/Data/String/Slice.lean
index e04bbd6956..a54f2ffb5e 100644
--- a/src/Init/Data/String/Slice.lean
+++ b/src/Init/Data/String/Slice.lean
@@ -905,9 +905,9 @@ Examples:
 def chars (s : Slice) :=
   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")]
+@[deprecated "There is no constant-time length function on slices. Use `s.positions.length` instead, or `isEmpty` if you only need to know whether the slice is empty." (since := "2025-11-20")]
 def length (s : Slice) : Nat :=
-  s.positions.count
+  s.positions.length
 
 structure RevPosIterator (s : Slice) where
   currPos : s.Pos
diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Range.lean b/src/Std/Data/Iterators/Lemmas/Producers/Range.lean
index d5b7482c22..06488b691d 100644
--- a/src/Std/Data/Iterators/Lemmas/Producers/Range.lean
+++ b/src/Std/Data/Iterators/Lemmas/Producers/Range.lean
@@ -39,19 +39,17 @@ theorem Rcc.toArray_iter_eq_toArray [LE α] [DecidableLE α] [UpwardEnumerable 
  rfl
 
 @[simp]
-theorem Rcc.count_iter [LE α] [DecidableLE α] [UpwardEnumerable α]
+theorem Rcc.length_iter [LE α] [DecidableLE α] [UpwardEnumerable α]
     [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
     [Rxc.HasSize α] [Rxc.LawfulHasSize α] {r : Rcc α} :
-    r.iter.count = r.size := by
-  rw [← size_toArray, ← toArray_iter, Iter.size_toArray_eq_count]
+    r.iter.length = r.size := by
+  rw [← size_toArray, ← toArray_iter, Iter.size_toArray_eq_length]
 
-@[deprecated Rcc.count_iter (since := "2025-11-13")]
-theorem Rcc.count_iter_eq_size [LE α] [DecidableLE α] [UpwardEnumerable α]
-    [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
-    [Rxc.HasSize α] [Rxc.LawfulHasSize α]
-    {r : Rcc α} :
-    r.iter.count = r.size :=
-  count_iter
+@[deprecated Rcc.length_iter (since := "2026-01-28")]
+def Rcc.count_iter := @Rcc.length_iter
+
+@[deprecated Rcc.length_iter (since := "2025-11-13")]
+def Rcc.count_iter_eq_size := @Rcc.length_iter
 
 @[simp]
 theorem Rco.toList_iter [LT α] [DecidableLT α] [UpwardEnumerable α]
@@ -78,20 +76,18 @@ theorem Rco.toArray_iter_eq_toArray [LT α] [DecidableLT α] [UpwardEnumerable 
  rfl
 
 @[simp]
-theorem Rco.count_iter [LT α] [DecidableLT α] [UpwardEnumerable α]
+theorem Rco.length_iter [LT α] [DecidableLT α] [UpwardEnumerable α]
     [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
     [Rxo.HasSize α] [Rxo.LawfulHasSize α]
     {r : Rco α} :
-    r.iter.count = r.size := by
-  rw [← size_toArray, ← toArray_iter, Iter.size_toArray_eq_count]
+    r.iter.length = r.size := by
+  rw [← size_toArray, ← toArray_iter, Iter.size_toArray_eq_length]
 
-@[deprecated Rco.count_iter (since := "2025-11-13")]
-theorem Rco.count_iter_eq_size [LT α] [DecidableLT α] [UpwardEnumerable α]
-    [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
-    [Rxo.HasSize α] [Rxo.LawfulHasSize α]
-    {r : Rco α} :
-    r.iter.count = r.size := by
-  rw [← size_toArray, ← toArray_iter, Iter.size_toArray_eq_count]
+@[deprecated Rco.length_iter (since := "2026-01-28")]
+def Rco.count_iter := @Rco.length_iter
+
+@[deprecated Rco.length_iter (since := "2025-11-13")]
+def Rco.count_iter_eq_size := @Rco.length_iter
 
 @[simp]
 theorem Rci.toList_iter [UpwardEnumerable α]
@@ -118,20 +114,18 @@ theorem Rci.toArray_iter_eq_toArray [UpwardEnumerable α]
  rfl
 
 @[simp]
-theorem Rci.count_iter [UpwardEnumerable α]
+theorem Rci.length_iter [UpwardEnumerable α]
     [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
     [Rxi.HasSize α] [Rxi.LawfulHasSize α]
     {r : Rci α} :
-    r.iter.count = r.size := by
-  rw [← size_toArray, ← toArray_iter_eq_toArray, Iter.size_toArray_eq_count]
+    r.iter.length = r.size := by
+  rw [← size_toArray, ← toArray_iter_eq_toArray, Iter.size_toArray_eq_length]
 
-@[deprecated Rci.count_iter (since := "2025-11-13")]
-theorem Rci.count_iter_eq_size [UpwardEnumerable α]
-    [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
-    [Rxi.HasSize α] [Rxi.LawfulHasSize α]
-    {r : Rci α} :
-    r.iter.count = r.size := by
-  rw [← size_toArray, ← toArray_iter_eq_toArray, Iter.size_toArray_eq_count]
+@[deprecated Rci.length_iter (since := "2026-01-28")]
+def Rci.count_iter := @Rci.length_iter
+
+@[deprecated Rci.length_iter (since := "2025-11-13")]
+def Rci.count_iter_eq_size := @Rci.length_iter
 
 @[simp]
 theorem Roc.toList_iter [LE α] [DecidableLE α] [UpwardEnumerable α]
@@ -158,20 +152,18 @@ theorem Roc.toArray_iter_eq_toArray [LE α] [DecidableLE α] [UpwardEnumerable 
  rfl
 
 @[simp]
-theorem Roc.count_iter [LE α] [DecidableLE α] [UpwardEnumerable α]
+theorem Roc.length_iter [LE α] [DecidableLE α] [UpwardEnumerable α]
     [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
     [Rxc.HasSize α] [Rxc.LawfulHasSize α]
     {r : Roc α} :
-    r.iter.count = r.size := by
-  rw [← size_toArray, ← toArray_iter_eq_toArray, Iter.size_toArray_eq_count]
+    r.iter.length = r.size := by
+  rw [← size_toArray, ← toArray_iter_eq_toArray, Iter.size_toArray_eq_length]
 
-@[deprecated Roc.count_iter (since := "2025-11-13")]
-theorem Roc.count_iter_eq_size [LE α] [DecidableLE α] [UpwardEnumerable α]
-    [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
-    [Rxc.HasSize α] [Rxc.LawfulHasSize α]
-    {r : Roc α} :
-    r.iter.count = r.size := by
-  rw [← size_toArray, ← toArray_iter_eq_toArray, Iter.size_toArray_eq_count]
+@[deprecated Roc.length_iter (since := "2026-01-28")]
+def Roc.count_iter := @Roc.length_iter
+
+@[deprecated Roc.length_iter (since := "2025-11-13")]
+def Roc.count_iter_eq_size := @Roc.length_iter
 
 @[simp]
 theorem Roo.toList_iter [LT α] [DecidableLT α] [UpwardEnumerable α]
@@ -198,20 +190,18 @@ theorem Roo.toArray_iter_eq_toArray [LT α] [DecidableLT α] [UpwardEnumerable 
  rfl
 
 @[simp]
-theorem Roo.count_iter [LT α] [DecidableLT α] [UpwardEnumerable α]
+theorem Roo.length_iter [LT α] [DecidableLT α] [UpwardEnumerable α]
     [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
     [Rxo.HasSize α] [Rxo.LawfulHasSize α]
     {r : Roo α} :
-    r.iter.count = r.size := by
-  rw [← size_toArray, ← toArray_iter_eq_toArray, Iter.size_toArray_eq_count]
+    r.iter.length = r.size := by
+  rw [← size_toArray, ← toArray_iter_eq_toArray, Iter.size_toArray_eq_length]
 
-@[deprecated Roo.count_iter (since := "2025-11-13")]
-theorem Roo.count_iter_eq_size [LT α] [DecidableLT α] [UpwardEnumerable α]
-    [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
-    [Rxo.HasSize α] [Rxo.LawfulHasSize α]
-    {r : Roo α} :
-    r.iter.count = r.size := by
-  rw [← size_toArray, ← toArray_iter_eq_toArray, Iter.size_toArray_eq_count]
+@[deprecated Roo.length_iter (since := "2026-01-28")]
+def Roo.count_iter := @Roo.length_iter
+
+@[deprecated Roo.length_iter (since := "2025-11-13")]
+def Roo.count_iter_eq_size := @Roo.length_iter
 
 @[simp]
 theorem Roi.toList_iter [UpwardEnumerable α]
@@ -238,20 +228,18 @@ theorem Roi.toArray_iter_eq_toArray [UpwardEnumerable α]
  rfl
 
 @[simp]
-theorem Roi.count_iter [UpwardEnumerable α]
+theorem Roi.length_iter [UpwardEnumerable α]
     [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
     [Rxi.HasSize α] [Rxi.LawfulHasSize α]
     {r : Roi α} :
-    r.iter.count = r.size := by
-  rw [← size_toArray, ← toArray_iter, Iter.size_toArray_eq_count]
+    r.iter.length = r.size := by
+  rw [← size_toArray, ← toArray_iter, Iter.size_toArray_eq_length]
 
-@[deprecated Roi.count_iter (since := "2025-11-13")]
-theorem Roi.count_iter_eq_size [UpwardEnumerable α]
-    [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
-    [Rxi.HasSize α] [Rxi.LawfulHasSize α]
-    {r : Roi α} :
-    r.iter.count = r.size := by
-  rw [← size_toArray, ← toArray_iter, Iter.size_toArray_eq_count]
+@[deprecated Roi.length_iter (since := "2026-01-28")]
+def Roi.count_iter := @Roi.length_iter
+
+@[deprecated Roi.length_iter (since := "2025-11-13")]
+def Roi.count_iter_eq_size := @Roi.length_iter
 
 @[simp]
 theorem Ric.toList_iter [Least? α] [LE α] [DecidableLE α] [UpwardEnumerable α]
@@ -278,20 +266,18 @@ theorem Ric.toArray_iter_eq_toArray [Least? α] [LE α] [DecidableLE α] [Upward
  rfl
 
 @[simp]
-theorem Ric.count_iter [Least? α] [LE α] [DecidableLE α] [UpwardEnumerable α]
+theorem Ric.length_iter [Least? α] [LE α] [DecidableLE α] [UpwardEnumerable α]
     [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
     [Rxc.HasSize α] [Rxc.LawfulHasSize α]
     {r : Ric α} :
-    r.iter.count = r.size := by
-  rw [← size_toArray, ← toArray_iter, Iter.size_toArray_eq_count]
+    r.iter.length = r.size := by
+  rw [← size_toArray, ← toArray_iter, Iter.size_toArray_eq_length]
 
-@[deprecated Ric.count_iter (since := "2025-11-13")]
-theorem Ric.count_iter_eq_size [Least? α] [LE α] [DecidableLE α] [UpwardEnumerable α]
-    [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
-    [Rxc.HasSize α] [Rxc.LawfulHasSize α]
-    {r : Ric α} :
-    r.iter.count = r.size := by
-  rw [← size_toArray, ← toArray_iter, Iter.size_toArray_eq_count]
+@[deprecated Ric.length_iter (since := "2026-01-28")]
+def Ric.count_iter := @Ric.length_iter
+
+@[deprecated Ric.length_iter (since := "2025-11-13")]
+def Ric.count_iter_eq_size := @Ric.length_iter
 
 @[simp]
 theorem Rio.toList_iter [Least? α] [LT α] [DecidableLT α] [UpwardEnumerable α]
@@ -318,20 +304,18 @@ theorem Rio.toArray_iter_eq_toArray [Least? α] [LT α] [DecidableLT α] [Upward
  rfl
 
 @[simp]
-theorem Rio.count_iter [Least? α] [LT α] [DecidableLT α] [UpwardEnumerable α]
+theorem Rio.length_iter [Least? α] [LT α] [DecidableLT α] [UpwardEnumerable α]
     [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
     [Rxo.HasSize α] [Rxo.LawfulHasSize α]
     {r : Rio α} :
-    r.iter.count = r.size := by
-  rw [← size_toArray, ← toArray_iter, Iter.size_toArray_eq_count]
+    r.iter.length = r.size := by
+  rw [← size_toArray, ← toArray_iter, Iter.size_toArray_eq_length]
 
-@[deprecated Rio.count_iter (since := "2025-11-13")]
-theorem Rio.count_iter_eq_size [Least? α] [LT α] [DecidableLT α] [UpwardEnumerable α]
-    [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
-    [Rxo.HasSize α] [Rxo.LawfulHasSize α]
-    {r : Rio α} :
-    r.iter.count = r.size := by
-  rw [← size_toArray, ← toArray_iter, Iter.size_toArray_eq_count]
+@[deprecated Rio.length_iter (since := "2026-01-28")]
+def Rio.count_iter := @Rio.length_iter
+
+@[deprecated Rio.length_iter (since := "2025-11-13")]
+def Rio.count_iter_eq_size := @Rio.length_iter
 
 @[simp]
 theorem Rii.toList_iter [Least? α] [UpwardEnumerable α]
@@ -358,19 +342,17 @@ theorem Rii.toArray_iter_eq_toArray [Least? α] [UpwardEnumerable α]
  rfl
 
 @[simp]
-theorem Rii.count_iter [Least? α] [UpwardEnumerable α]
+theorem Rii.length_iter [Least? α] [UpwardEnumerable α]
     [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
     [Rxi.HasSize α] [Rxi.LawfulHasSize α]
     {r : Rii α} :
-    r.iter.count = r.size := by
-  rw [← size_toArray, ← toArray_iter, Iter.size_toArray_eq_count]
+    r.iter.length = r.size := by
+  rw [← size_toArray, ← toArray_iter, Iter.size_toArray_eq_length]
 
-@[deprecated Rii.count_iter (since := "2025-11-13")]
-theorem Rii.count_iter_eq_size [Least? α] [UpwardEnumerable α]
-    [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
-    [Rxi.HasSize α] [Rxi.LawfulHasSize α]
-    {r : Rii α} :
-    r.iter.count = r.size := by
-  rw [← size_toArray, ← toArray_iter, Iter.size_toArray_eq_count]
+@[deprecated Rii.length_iter (since := "2026-01-28")]
+def Rii.count_iter := @Rii.length_iter
+
+@[deprecated Rii.length_iter (since := "2025-11-13")]
+def Rii.count_iter_eq_size := @Rii.length_iter
 
 end Std
diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Slice.lean b/src/Std/Data/Iterators/Lemmas/Producers/Slice.lean
index dafdfae36e..295ea9c7d3 100644
--- a/src/Std/Data/Iterators/Lemmas/Producers/Slice.lean
+++ b/src/Std/Data/Iterators/Lemmas/Producers/Slice.lean
@@ -27,21 +27,27 @@ 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_count_iter [ToIterator (Slice γ) Id α β]
+theorem size_eq_length_iter [ToIterator (Slice γ) Id α β]
     [Iterator α Id β] {s : Slice γ}
     [Finite α Id]
     [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
     [SliceSize γ] [LawfulSliceSize γ] :
-    s.size = s.iter.count := by
-  simp [Internal.iter_eq_iter, Internal.size_eq_count_iter]
+    s.size = s.iter.length := by
+  simp [Internal.iter_eq_iter, Internal.size_eq_length_iter]
 
-theorem count_iter_eq_size [ToIterator (Slice γ) Id α β]
+@[deprecated size_eq_length_iter (since := "2026-01-28")]
+def size_eq_count_iter := @size_eq_length_iter
+
+theorem length_iter_eq_size [ToIterator (Slice γ) Id α β]
     [Iterator α Id β] {s : Slice γ}
     [Finite α Id]
     [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
     [SliceSize γ] [LawfulSliceSize γ] :
-    s.iter.count = s.size :=
-  size_eq_count_iter.symm
+    s.iter.length = s.size :=
+  size_eq_length_iter.symm
+
+@[deprecated length_iter_eq_size (since := "2026-01-28")]
+def count_iter_eq_size := @length_iter_eq_size
 
 @[simp]
 theorem toArray_iter {s : Slice γ} [ToIterator (Slice γ) Id α β]
diff --git a/src/lake/Lake/Toml/Data/DateTime.lean b/src/lake/Lake/Toml/Data/DateTime.lean
index 1f3999a4e8..646fac98dd 100644
--- a/src/lake/Lake/Toml/Data/DateTime.lean
+++ b/src/lake/Lake/Toml/Data/DateTime.lean
@@ -69,7 +69,7 @@ public def ofString? (t : String) : Option Time := do
     match s.split '.' |>.toList with
     | [s,f] =>
       let time ← ofValid? (← h.toNat?) (← m.toNat?) (← s.toNat?)
-      return {time with fracExponent := f.positions.count-1, fracMantissa := ← f.toNat?}
+      return {time with fracExponent := f.positions.length-1, fracMantissa := ← f.toNat?}
     | [s] =>
       ofValid? (← h.toNat?) (← m.toNat?) (← s.toNat?)
     | _ => none