From 1a4c3ca35df6e4a4bfc99fe1189151dd537aad6c Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Tue, 18 Nov 2025 10:28:55 +0100
Subject: [PATCH] refactor: small iterator improvements (#11175)

This PR removes duplicated instance parameters in the standard library
and flips lemmas of the form `toList_eq_toListIter` into a form that is
suitable for `simp`.
---
 src/Init/Data/Range/Polymorphic/Lemmas.lean   | 183 ++++++++---------
 src/Std/Data/DTreeMap/Internal/Zipper.lean    |  54 ++---
 .../Iterators/Lemmas/Producers/Range.lean     | 193 +++++++++++++++++-
 .../Iterators/Lemmas/Producers/Slice.lean     |  29 ++-
 4 files changed, 324 insertions(+), 135 deletions(-)

diff --git a/src/Init/Data/Range/Polymorphic/Lemmas.lean b/src/Init/Data/Range/Polymorphic/Lemmas.lean
index acc408cb37..24bb3280c3 100644
--- a/src/Init/Data/Range/Polymorphic/Lemmas.lean
+++ b/src/Init/Data/Range/Polymorphic/Lemmas.lean
@@ -490,7 +490,7 @@ public theorem Rxi.Iterator.toArray_eq_match
 
 public theorem Rxc.Iterator.pairwise_toList_upwardEnumerableLt [LE α] [DecidableLE α]
     [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
-    [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
+    [Rxc.IsAlwaysFinite α]
     (it : Iter (α := Rxc.Iterator α) α) :
     it.toList.Pairwise (fun a b => UpwardEnumerable.LT a b) := by
   induction it using Iter.inductSteps with | step it ihy ihs
@@ -513,7 +513,7 @@ public theorem Rxc.Iterator.pairwise_toList_upwardEnumerableLt [LE α] [Decidabl
 
 public theorem Rxo.Iterator.pairwise_toList_upwardEnumerableLt [LT α] [DecidableLT α]
     [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
-    [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
+    [Rxo.IsAlwaysFinite α]
     (it : Iter (α := Rxo.Iterator α) α) :
     it.toList.Pairwise (fun a b => UpwardEnumerable.LT a b) := by
   induction it using Iter.inductSteps with | step it ihy ihs
@@ -536,7 +536,7 @@ public theorem Rxo.Iterator.pairwise_toList_upwardEnumerableLt [LT α] [Decidabl
 
 public theorem Rxi.Iterator.pairwise_toList_upwardEnumerableLt
     [UpwardEnumerable α] [LawfulUpwardEnumerable α]
-    [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
+    [Rxi.IsAlwaysFinite α]
     (it : Iter (α := Rxi.Iterator α) α) :
     it.toList.Pairwise (fun a b => UpwardEnumerable.LT a b) := by
   induction it using Iter.inductSteps with | step it ihy ihs
@@ -589,8 +589,7 @@ public theorem toList_eq_if_roc [LE α] [DecidableLE α] [UpwardEnumerable α]
 def toList_eq_match := @toList_eq_if_roc
 
 public theorem toArray_eq_if_roc [LE α] [DecidableLE α] [UpwardEnumerable α]
-    [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α]
-    [LawfulUpwardEnumerable α] :
+    [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] :
     r.toArray = if r.lower ≤ r.upper then
         #[r.lower] ++ (r.lower<...=r.upper).toArray
       else
@@ -613,53 +612,51 @@ public theorem toList_toArray [LE α] [DecidableLE α] [UpwardEnumerable α]
   simp [Internal.toList_eq_toList_iter, Internal.toArray_eq_toArray_iter]
 
 public theorem toList_eq_nil_iff [LE α] [DecidableLE α] [UpwardEnumerable α]
-    [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α]
-    [LawfulUpwardEnumerable α] :
+    [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] :
     r.toList = [] ↔ ¬ (r.lower ≤ r.upper) := by
   rw [Internal.toList_eq_toList_iter, Rxc.Iterator.toList_eq_match, Internal.iter]
   simp only
   split <;> rename_i heq <;> simp [heq]
 
 public theorem toArray_eq_empty_iff [LE α] [DecidableLE α] [UpwardEnumerable α]
-    [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α]
-    [LawfulUpwardEnumerable α] :
+    [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] :
     r.toArray = #[] ↔ ¬ (r.lower ≤ r.upper) := by
   simp [← toArray_toList, toList_eq_nil_iff]
 
 public theorem mem_toList_iff_mem [LE α] [DecidableLE α] [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α]
-    [LawfulUpwardEnumerable α] {a : α} : a ∈ r.toList ↔ a ∈ r := by
+    {a : α} : a ∈ r.toList ↔ a ∈ r := by
   rw [Internal.toList_eq_toList_iter, Iter.mem_toList_iff_isPlausibleIndirectOutput,
     Internal.isPlausibleIndirectOutput_iter_iff]
 
 public theorem mem_toArray_iff_mem [LE α] [DecidableLE α] [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α]
-    [LawfulUpwardEnumerable α] {a : α} : a ∈ r.toArray ↔ a ∈ r := by
+    {a : α} : a ∈ r.toArray ↔ a ∈ r := by
   simp [← toArray_toList, mem_toList_iff_mem]
 
 public theorem pairwise_toList_upwardEnumerableLt [LE α] [DecidableLE α]
     [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
-    [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
+    [Rxc.IsAlwaysFinite α] :
     r.toList.Pairwise (fun a b => UpwardEnumerable.LT a b) := by
   rw [Internal.toList_eq_toList_iter]
   apply Rxc.Iterator.pairwise_toList_upwardEnumerableLt
 
 public theorem pairwise_toList_ne [LE α] [DecidableLE α]
     [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
-    [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
+    [Rxc.IsAlwaysFinite α] :
     r.toList.Pairwise (fun a b => a ≠ b) :=
   List.Pairwise.imp (fun hlt => UpwardEnumerable.ne_of_lt hlt) pairwise_toList_upwardEnumerableLt
 
 public theorem pairwise_toList_lt [LE α] [DecidableLE α] [LT α]
     [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
-    [LawfulUpwardEnumerableLT α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
+    [LawfulUpwardEnumerableLT α] [Rxc.IsAlwaysFinite α] :
     r.toList.Pairwise (fun a b => a < b) :=
   List.Pairwise.imp
     (fun hlt => (LawfulUpwardEnumerableLT.lt_iff ..).mpr hlt) pairwise_toList_upwardEnumerableLt
 
 public theorem pairwise_toList_le [LE α] [DecidableLE α] [LT α]
     [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
-    [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
+    [Rxc.IsAlwaysFinite α] :
     r.toList.Pairwise (fun a b => a ≤ b) :=
   pairwise_toList_upwardEnumerableLt
     |> List.Pairwise.imp UpwardEnumerable.le_of_lt
@@ -852,54 +849,52 @@ public theorem toList_toArray [LT α] [DecidableLT α] [UpwardEnumerable α]
   simp [Internal.toList_eq_toList_iter, Internal.toArray_eq_toArray_iter]
 
 public theorem toList_eq_nil_iff [LT α] [DecidableLT α] [UpwardEnumerable α]
-    [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α]
-    [LawfulUpwardEnumerable α] :
+    [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] :
     r.toList = [] ↔ ¬ (r.lower < r.upper) := by
   rw [Internal.toList_eq_toList_iter, Rxo.Iterator.toList_eq_match, Internal.iter]
   simp only
   split <;> rename_i heq <;> simp [heq]
 
 public theorem toArray_eq_empty_iff [LT α] [DecidableLT α] [UpwardEnumerable α]
-    [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α]
-    [LawfulUpwardEnumerable α] :
+    [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] :
     r.toArray = #[] ↔ ¬ (r.lower < r.upper) := by
   simp [← toArray_toList, toList_eq_nil_iff]
 
 public theorem mem_toList_iff_mem [LE α] [LT α] [DecidableLT α] [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [LawfulUpwardEnumerableLE α]
-    [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {a : α} : a ∈ r.toList ↔ a ∈ r := by
+    [Rxo.IsAlwaysFinite α] {a : α} : a ∈ r.toList ↔ a ∈ r := by
   rw [Internal.toList_eq_toList_iter, Iter.mem_toList_iff_isPlausibleIndirectOutput,
     Internal.isPlausibleIndirectOutput_iter_iff]
 
 public theorem mem_toArray_iff_mem [LE α] [LT α] [DecidableLT α] [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [LawfulUpwardEnumerableLE α]
-    [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {a : α} : a ∈ r.toArray ↔ a ∈ r := by
+    [Rxo.IsAlwaysFinite α] {a : α} : a ∈ r.toArray ↔ a ∈ r := by
   rw [Internal.toArray_eq_toArray_iter, Iter.mem_toArray_iff_isPlausibleIndirectOutput,
     Internal.isPlausibleIndirectOutput_iter_iff]
 
 public theorem pairwise_toList_upwardEnumerableLt [LE α] [LT α] [DecidableLT α]
     [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
-    [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
+    [Rxo.IsAlwaysFinite α] :
     r.toList.Pairwise (fun a b => UpwardEnumerable.LT a b) := by
   rw [Internal.toList_eq_toList_iter]
   apply Rxo.Iterator.pairwise_toList_upwardEnumerableLt
 
 public theorem pairwise_toList_ne [LE α] [LT α] [DecidableLT α]
     [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
-    [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
+    [Rxo.IsAlwaysFinite α] :
     r.toList.Pairwise (fun a b => a ≠ b) :=
   List.Pairwise.imp (fun hlt => UpwardEnumerable.ne_of_lt hlt) pairwise_toList_upwardEnumerableLt
 
 public theorem pairwise_toList_lt [LE α] [LT α] [DecidableLT α]
     [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
-    [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
+    [Rxo.IsAlwaysFinite α] :
     r.toList.Pairwise (fun a b => a < b) :=
   List.Pairwise.imp
     (fun hlt => (LawfulUpwardEnumerableLT.lt_iff ..).mpr hlt) pairwise_toList_upwardEnumerableLt
 
 public theorem pairwise_toList_le [LE α] [LT α] [DecidableLT α]
     [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
-    [LawfulUpwardEnumerableLE α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
+    [LawfulUpwardEnumerableLE α] [Rxo.IsAlwaysFinite α] :
     r.toList.Pairwise (fun a b => a ≤ b) :=
   pairwise_toList_upwardEnumerableLt
     |> List.Pairwise.imp UpwardEnumerable.le_of_lt
@@ -1039,7 +1034,7 @@ namespace Rci
 variable {r : Rci α}
 
 public theorem toList_eq_toList_roi [UpwardEnumerable α]
-    [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
+    [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] :
     r.toList = r.lower :: (r.lower<...*).toList := by
   rw [Internal.toList_eq_toList_iter, Rxi.Iterator.toList_eq_match]; rfl
 
@@ -1047,7 +1042,7 @@ public theorem toList_eq_toList_roi [UpwardEnumerable α]
 def toList_eq_toList_Roi := @toList_eq_toList_roi
 
 public theorem toArray_eq_toArray_roi [UpwardEnumerable α]
-    [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
+    [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] :
     r.toArray = #[r.lower] ++ (r.lower<...*).toArray := by
   rw [Internal.toArray_eq_toArray_iter, Rxi.Iterator.toArray_eq_match]; rfl
 
@@ -1067,51 +1062,49 @@ public theorem toList_toArray [UpwardEnumerable α] [LawfulUpwardEnumerable α]
   simp [Internal.toList_eq_toList_iter, Internal.toArray_eq_toArray_iter]
 
 public theorem toList_ne_nil [UpwardEnumerable α]
-    [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α]
-    [LawfulUpwardEnumerable α] :
+    [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] :
     r.toList ≠ [] := by
   rw [Internal.toList_eq_toList_iter, Rxi.Iterator.toList_eq_match, Internal.iter]
   simp
 
 public theorem toArray_ne_nil [UpwardEnumerable α]
-    [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α]
-    [LawfulUpwardEnumerable α] :
+    [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] :
     r.toArray ≠ #[] := by
   simp [← toArray_toList, toList_ne_nil]
 
 public theorem mem_toList_iff_mem [LE α] [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
-    [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {a : α} : a ∈ r.toList ↔ a ∈ r := by
+    [Rxi.IsAlwaysFinite α] {a : α} : a ∈ r.toList ↔ a ∈ r := by
   rw [Internal.toList_eq_toList_iter, Iter.mem_toList_iff_isPlausibleIndirectOutput,
     Internal.isPlausibleIndirectOutput_iter_iff]
 
 public theorem mem_toArray_iff_mem [LE α] [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
-    [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {a : α} : a ∈ r.toArray ↔ a ∈ r := by
+    [Rxi.IsAlwaysFinite α] {a : α} : a ∈ r.toArray ↔ a ∈ r := by
   rw [Internal.toArray_eq_toArray_iter, Iter.mem_toArray_iff_isPlausibleIndirectOutput,
     Internal.isPlausibleIndirectOutput_iter_iff]
 
 public theorem pairwise_toList_upwardEnumerableLt [LE α]
-    [UpwardEnumerable α] [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
+    [UpwardEnumerable α] [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] :
     r.toList.Pairwise (fun a b => UpwardEnumerable.LT a b) := by
   rw [Internal.toList_eq_toList_iter]
   apply Rxi.Iterator.pairwise_toList_upwardEnumerableLt
 
 public theorem pairwise_toList_ne [LE α]
-    [UpwardEnumerable α] [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
+    [UpwardEnumerable α] [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] :
     r.toList.Pairwise (fun a b => a ≠ b) :=
   List.Pairwise.imp (fun hlt => UpwardEnumerable.ne_of_lt hlt) pairwise_toList_upwardEnumerableLt
 
 public theorem pairwise_toList_lt [LE α] [LT α]
     [UpwardEnumerable α] [LawfulUpwardEnumerable α]
-    [LawfulUpwardEnumerableLT α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
+    [LawfulUpwardEnumerableLT α] [Rxi.IsAlwaysFinite α] :
     r.toList.Pairwise (fun a b => a < b) :=
   List.Pairwise.imp
     (fun hlt => (LawfulUpwardEnumerableLT.lt_iff ..).mpr hlt) pairwise_toList_upwardEnumerableLt
 
 public theorem pairwise_toList_le [LE α]
     [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
-    [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
+    [Rxi.IsAlwaysFinite α] :
     r.toList.Pairwise (fun a b => a ≤ b) :=
   pairwise_toList_upwardEnumerableLt
     |> List.Pairwise.imp UpwardEnumerable.le_of_lt
@@ -1293,7 +1286,7 @@ public theorem toList_toArray [LE α] [DecidableLE α] [UpwardEnumerable α] [La
 
 public theorem toList_eq_nil_iff [LE α] [DecidableLE α] [LT α] [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLT α]
-    [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
+    [Rxc.IsAlwaysFinite α] :
     r.toList = [] ↔ ¬ (r.lower < r.upper) := by
   rw [Internal.toList_eq_toList_iter, Rxc.Iterator.toList_eq_match, Internal.iter]
   simp only
@@ -1304,45 +1297,45 @@ public theorem toList_eq_nil_iff [LE α] [DecidableLE α] [LT α] [UpwardEnumera
 
 public theorem toArray_eq_empty_iff [LE α] [DecidableLE α] [LT α] [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLT α]
-    [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
+    [Rxc.IsAlwaysFinite α] :
     r.toArray = #[] ↔ ¬ (r.lower < r.upper) := by
   simp [← toArray_toList, toList_eq_nil_iff]
 
 public theorem mem_toList_iff_mem [LE α] [DecidableLE α] [LT α] [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLT α]
-    [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {a : α} : a ∈ r.toList ↔ a ∈ r := by
+    [Rxc.IsAlwaysFinite α] {a : α} : a ∈ r.toList ↔ a ∈ r := by
   rw [Internal.toList_eq_toList_iter, Iter.mem_toList_iff_isPlausibleIndirectOutput,
     Internal.isPlausibleIndirectOutput_iter_iff]
 
 public theorem mem_toArray_iff_mem [LE α] [DecidableLE α] [LT α] [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLT α]
-    [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {a : α} : a ∈ r.toArray ↔ a ∈ r := by
+    [Rxc.IsAlwaysFinite α] {a : α} : a ∈ r.toArray ↔ a ∈ r := by
   rw [Internal.toArray_eq_toArray_iter, Iter.mem_toArray_iff_isPlausibleIndirectOutput,
     Internal.isPlausibleIndirectOutput_iter_iff]
 
 public theorem pairwise_toList_upwardEnumerableLt [LE α] [DecidableLE α]
     [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
-    [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
+    [Rxc.IsAlwaysFinite α] :
     r.toList.Pairwise (fun a b => UpwardEnumerable.LT a b) := by
   rw [Internal.toList_eq_toList_iter]
   apply Rxc.Iterator.pairwise_toList_upwardEnumerableLt
 
 public theorem pairwise_toList_ne [LE α] [DecidableLE α]
     [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
-    [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
+    [Rxc.IsAlwaysFinite α] :
     r.toList.Pairwise (fun a b => a ≠ b) :=
   List.Pairwise.imp (fun hlt => UpwardEnumerable.ne_of_lt hlt) pairwise_toList_upwardEnumerableLt
 
 public theorem pairwise_toList_lt [LE α] [DecidableLE α] [LT α]
     [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
-    [LawfulUpwardEnumerableLT α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
+    [LawfulUpwardEnumerableLT α] [Rxc.IsAlwaysFinite α] :
     r.toList.Pairwise (fun a b => a < b) :=
   List.Pairwise.imp
     (fun hlt => (LawfulUpwardEnumerableLT.lt_iff ..).mpr hlt) pairwise_toList_upwardEnumerableLt
 
 public theorem pairwise_toList_le [LE α] [DecidableLE α] [LT α]
     [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
-    [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
+    [Rxc.IsAlwaysFinite α] :
     r.toList.Pairwise (fun a b => a ≤ b) :=
   pairwise_toList_upwardEnumerableLt
     |> List.Pairwise.imp UpwardEnumerable.le_of_lt
@@ -1466,8 +1459,7 @@ namespace Roo
 variable {r : Roo α}
 
 public theorem toList_eq_match [LT α] [DecidableLT α] [UpwardEnumerable α]
-    [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α]
-    [LawfulUpwardEnumerable α] :
+    [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] :
     r.toList = match UpwardEnumerable.succ? r.lower with
       | none => []
       | some next =>
@@ -1478,8 +1470,7 @@ public theorem toList_eq_match [LT α] [DecidableLT α] [UpwardEnumerable α]
   rw [Internal.toList_eq_toList_iter, Rxo.Iterator.toList_eq_match]; rfl
 
 public theorem toArray_eq_match [LE α] [LT α] [DecidableLT α] [UpwardEnumerable α]
-    [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α]
-    [LawfulUpwardEnumerable α] :
+    [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] :
     r.toArray = match UpwardEnumerable.succ? r.lower with
       | none => #[]
       | some next =>
@@ -1524,54 +1515,52 @@ public theorem toList_toArray [LT α] [DecidableLT α] [UpwardEnumerable α] [La
   simp [Internal.toList_eq_toList_iter, Internal.toArray_eq_toArray_iter]
 
 public theorem toList_eq_nil_iff [LE α] [LT α] [DecidableLT α] [UpwardEnumerable α]
-    [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α]
-    [LawfulUpwardEnumerable α] :
+    [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] :
     r.toList = [] ↔ ∀ a, UpwardEnumerable.succ? r.lower = some a → ¬ (a < r.upper) := by
   rw [Internal.toList_eq_toList_iter, Rxo.Iterator.toList_eq_match, Internal.iter]
   simp only
   split <;> rename_i heq <;> simp [heq]
 
 public theorem toArray_eq_empty_iff [LE α] [LT α] [DecidableLT α] [UpwardEnumerable α]
-    [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α]
-    [LawfulUpwardEnumerable α] :
+    [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] :
     r.toArray = #[] ↔ ∀ a, UpwardEnumerable.succ? r.lower = some a → ¬ (a < r.upper) := by
   simp [← toArray_toList, toList_eq_nil_iff]
 
 public theorem mem_toList_iff_mem [LT α] [DecidableLT α] [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
-    [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {a : α} : a ∈ r.toList ↔ a ∈ r := by
+    [Rxo.IsAlwaysFinite α] {a : α} : a ∈ r.toList ↔ a ∈ r := by
   rw [Internal.toList_eq_toList_iter, Iter.mem_toList_iff_isPlausibleIndirectOutput,
     Internal.isPlausibleIndirectOutput_iter_iff]
 
 public theorem mem_toArray_iff_mem [LT α] [DecidableLT α] [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
-    [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {a : α} : a ∈ r.toArray ↔ a ∈ r := by
+    [Rxo.IsAlwaysFinite α] {a : α} : a ∈ r.toArray ↔ a ∈ r := by
   rw [Internal.toArray_eq_toArray_iter, Iter.mem_toArray_iff_isPlausibleIndirectOutput,
     Internal.isPlausibleIndirectOutput_iter_iff]
 
 public theorem pairwise_toList_upwardEnumerableLt [LT α] [DecidableLT α]
     [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
-    [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
+    [Rxo.IsAlwaysFinite α] :
     r.toList.Pairwise (fun a b => UpwardEnumerable.LT a b) := by
   rw [Internal.toList_eq_toList_iter]
   apply Rxo.Iterator.pairwise_toList_upwardEnumerableLt
 
 public theorem pairwise_toList_ne [LT α] [DecidableLT α]
     [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
-    [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
+    [Rxo.IsAlwaysFinite α] :
     r.toList.Pairwise (fun a b => a ≠ b) :=
   List.Pairwise.imp (fun hlt => UpwardEnumerable.ne_of_lt hlt) pairwise_toList_upwardEnumerableLt
 
 public theorem pairwise_toList_lt [LT α] [DecidableLT α]
     [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
-    [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
+    [Rxo.IsAlwaysFinite α] :
     r.toList.Pairwise (fun a b => a < b) :=
   List.Pairwise.imp
     (fun hlt => (LawfulUpwardEnumerableLT.lt_iff ..).mpr hlt) pairwise_toList_upwardEnumerableLt
 
 public theorem pairwise_toList_le [LE α] [LT α] [DecidableLT α]
     [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
-    [LawfulUpwardEnumerableLE α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
+    [LawfulUpwardEnumerableLE α] [Rxo.IsAlwaysFinite α] :
     r.toList.Pairwise (fun a b => a ≤ b) :=
   pairwise_toList_upwardEnumerableLt
     |> List.Pairwise.imp UpwardEnumerable.le_of_lt
@@ -1762,25 +1751,25 @@ public theorem toList_eq_match_rci [UpwardEnumerable α]
   split <;> simp
 
 public theorem toList_eq_nil_iff [UpwardEnumerable α] [LawfulUpwardEnumerable α]
-    [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
+    [Rxi.IsAlwaysFinite α] :
     r.toList = [] ↔ (UpwardEnumerable.succ? r.lower).isNone := by
   rw [Internal.toList_eq_toList_iter, Rxi.Iterator.toList_eq_match, Internal.iter]
   simp only
   split <;> rename_i heq <;> simp [heq]
 
 public theorem toArray_eq_empty_iff [UpwardEnumerable α] [LawfulUpwardEnumerable α]
-    [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
+    [Rxi.IsAlwaysFinite α] :
     r.toArray = #[] ↔ (UpwardEnumerable.succ? r.lower).isNone := by
   simp [← toArray_toList, toList_eq_nil_iff]
 
 public theorem mem_toList_iff_mem [LT α] [UpwardEnumerable α]
-    [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
-    [LawfulUpwardEnumerableLT α] {a : α} : a ∈ r.toList ↔ a ∈ r := by
+    [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerableLT α]
+    {a : α} : a ∈ r.toList ↔ a ∈ r := by
   rw [Internal.toList_eq_toList_iter, Iter.mem_toList_iff_isPlausibleIndirectOutput,
     Internal.isPlausibleIndirectOutput_iter_iff]
 
 public theorem mem_toArray_iff_mem [LT α] [UpwardEnumerable α]
-    [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
+    [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α]
     [LawfulUpwardEnumerableLT α] {a : α} : a ∈ r.toArray ↔ a ∈ r := by
   rw [Internal.toArray_eq_toArray_iter, Iter.mem_toArray_iff_isPlausibleIndirectOutput,
     Internal.isPlausibleIndirectOutput_iter_iff]
@@ -1977,7 +1966,7 @@ def toArray_eq_toArray_Rcc := @toArray_eq_toArray_rcc
 
 public theorem toList_eq_if_roc [LE α] [DecidableLE α] [Least? α] [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLeast? α]
-    [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
+    [Rxc.IsAlwaysFinite α] :
     r.toList = let init : α := UpwardEnumerable.least (hn := ⟨r.upper⟩)
       if init ≤ r.upper then
         init :: (init<...=r.upper).toList
@@ -1990,7 +1979,7 @@ def toList_eq_if := @toList_eq_if_roc
 
 public theorem toArray_eq_if_roc [LE α] [DecidableLE α] [Least? α] [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLeast? α]
-    [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
+    [Rxc.IsAlwaysFinite α] :
     r.toArray = let init : α := UpwardEnumerable.least (hn := ⟨r.upper⟩)
       if init ≤ r.upper then
         #[init] ++ (init<...=r.upper).toArray
@@ -2003,14 +1992,14 @@ def toArray_eq_if := @toArray_eq_if_roc
 
 public theorem toList_ne_nil [LE α] [DecidableLE α] [Least? α] [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
-    [LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
+    [LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] :
     r.toList ≠ [] := by
   simp [toList_eq_toList_rcc, Rcc.toList_eq_nil_iff, UpwardEnumerable.le_iff,
     UpwardEnumerable.least_le]
 
 public theorem toArray_ne_empty [LE α] [DecidableLE α] [Least? α] [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
-    [LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
+    [LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] :
     r.toArray ≠ #[] := by
   simp [toArray_eq_toArray_rcc, Rcc.toArray_eq_empty_iff, UpwardEnumerable.le_iff,
     UpwardEnumerable.least_le]
@@ -2026,29 +2015,29 @@ def mem_iff_mem_Rcc := @mem_iff_mem_rcc
 
 public theorem mem_toList_iff_mem [LE α] [DecidableLE α] [Least? α] [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLeast? α]
-    [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {a : α} : a ∈ r.toList ↔ a ∈ r := by
+    [Rxc.IsAlwaysFinite α] {a : α} : a ∈ r.toList ↔ a ∈ r := by
   simp [toList_eq_toList_rcc, mem_iff_mem_rcc, Rcc.mem_toList_iff_mem]
 
 public theorem mem_toArray_iff_mem [LE α] [DecidableLE α] [Least? α] [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLeast? α]
-    [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {a : α} : a ∈ r.toArray ↔ a ∈ r := by
+    [Rxc.IsAlwaysFinite α] {a : α} : a ∈ r.toArray ↔ a ∈ r := by
   simp [toArray_eq_toArray_rcc, mem_iff_mem_rcc, Rcc.mem_toArray_iff_mem]
 
 public theorem pairwise_toList_upwardEnumerableLt [LE α] [DecidableLE α] [Least? α]
     [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
-    [LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
+    [LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] :
     r.toList.Pairwise (fun a b => UpwardEnumerable.LT a b) := by
   simp [toList_eq_toList_rcc, Rcc.pairwise_toList_upwardEnumerableLt]
 
 public theorem pairwise_toList_ne [LE α] [DecidableLE α] [Least? α]
     [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
-    [LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
+    [LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] :
     r.toList.Pairwise (fun a b => a ≠ b) :=
   List.Pairwise.imp (fun hlt => UpwardEnumerable.ne_of_lt hlt) pairwise_toList_upwardEnumerableLt
 
 public theorem pairwise_toList_lt [LE α] [DecidableLE α] [LT α] [Least? α]
     [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
-    [LawfulUpwardEnumerableLT α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
+    [LawfulUpwardEnumerableLT α] [Rxc.IsAlwaysFinite α]
     [LawfulUpwardEnumerableLeast? α] :
     r.toList.Pairwise (fun a b => a < b) :=
   List.Pairwise.imp
@@ -2056,7 +2045,7 @@ public theorem pairwise_toList_lt [LE α] [DecidableLE α] [LT α] [Least? α]
 
 public theorem pairwise_toList_le [LE α] [DecidableLE α] [LT α] [Least? α]
     [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
-    [LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
+    [LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] :
     r.toList.Pairwise (fun a b => a ≤ b) :=
   pairwise_toList_upwardEnumerableLt
     |> List.Pairwise.imp UpwardEnumerable.le_of_lt
@@ -2282,7 +2271,7 @@ def toArray_eq_toArray_Rco := @toArray_eq_toArray_rco
 
 public theorem toList_eq_if_roo [LT α] [DecidableLT α] [Least? α] [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [LawfulUpwardEnumerableLeast? α]
-    [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
+    [Rxo.IsAlwaysFinite α] :
     r.toList = let init : α := UpwardEnumerable.least (hn := ⟨r.upper⟩)
       if init < r.upper then
         init :: (init<...r.upper).toList
@@ -2296,7 +2285,7 @@ def toList_eq_if := @toList_eq_if_roo
 
 public theorem toArray_eq_if_roo [LT α] [DecidableLT α] [Least? α] [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [LawfulUpwardEnumerableLeast? α]
-    [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
+    [Rxo.IsAlwaysFinite α] :
     r.toArray = let init : α := UpwardEnumerable.least (hn := ⟨r.upper⟩)
       if init < r.upper then
         #[init] ++ (init<...r.upper).toArray
@@ -2310,13 +2299,13 @@ def toArray_eq_if := @toArray_eq_if_roo
 
 public theorem toList_eq_nil_iff [LT α] [DecidableLT α] [Least? α] [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
-    [LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
+    [LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] :
     r.toList = [] ↔ ¬ UpwardEnumerable.least (hn := ⟨r.upper⟩) < r.upper := by
   simp [toList_eq_if_roo]
 
 public theorem toArray_eq_nil_iff [LT α] [DecidableLT α] [Least? α] [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
-    [LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
+    [LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] :
     r.toArray = #[] ↔ ¬ UpwardEnumerable.least (hn := ⟨r.upper⟩) < r.upper := by
   simp [toArray_eq_if_roo]
 
@@ -2331,7 +2320,7 @@ def mem_iff_mem_Rco := @mem_iff_mem_rco
 
 public theorem mem_toList_iff_mem [LT α] [DecidableLT α] [Least? α] [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [LawfulUpwardEnumerableLeast? α]
-    [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {a : α} : a ∈ r.toList ↔ a ∈ r := by
+    [Rxo.IsAlwaysFinite α] {a : α} : a ∈ r.toList ↔ a ∈ r := by
   simp only [toList_eq_if_roo, List.mem_ite_nil_right, List.mem_cons, Roo.mem_toList_iff_mem]
   simp only [Membership.mem]
   constructor
@@ -2348,12 +2337,12 @@ public theorem mem_toList_iff_mem [LT α] [DecidableLT α] [Least? α] [UpwardEn
 
 public theorem mem_toArray_iff_mem [LT α] [DecidableLT α] [Least? α] [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [LawfulUpwardEnumerableLeast? α]
-    [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {a : α} : a ∈ r.toArray ↔ a ∈ r := by
+    [Rxo.IsAlwaysFinite α] {a : α} : a ∈ r.toArray ↔ a ∈ r := by
   simp [← toArray_toList, mem_toList_iff_mem]
 
 public theorem pairwise_toList_upwardEnumerableLt [LT α] [DecidableLT α] [Least? α]
     [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
-    [LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
+    [LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] :
     r.toList.Pairwise (fun a b => UpwardEnumerable.LT a b) := by
   simp only [toList_eq_if_roo]
   split
@@ -2365,13 +2354,13 @@ public theorem pairwise_toList_upwardEnumerableLt [LT α] [DecidableLT α] [Leas
 
 public theorem pairwise_toList_ne [LT α] [DecidableLT α] [Least? α]
     [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
-    [LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
+    [LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] :
     r.toList.Pairwise (fun a b => a ≠ b) :=
   List.Pairwise.imp (fun hlt => UpwardEnumerable.ne_of_lt hlt) pairwise_toList_upwardEnumerableLt
 
 public theorem pairwise_toList_lt [LT α] [DecidableLT α] [Least? α]
     [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
-    [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
+    [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α]
     [LawfulUpwardEnumerableLeast? α] :
     r.toList.Pairwise (fun a b => a < b) :=
   List.Pairwise.imp
@@ -2379,8 +2368,7 @@ public theorem pairwise_toList_lt [LT α] [DecidableLT α] [Least? α]
 
 public theorem pairwise_toList_le [LE α] [LT α] [DecidableLT α] [Least? α]
     [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
-    [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α]
-    [LawfulUpwardEnumerable α] :
+    [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] :
     r.toList.Pairwise (fun a b => a ≤ b) :=
   pairwise_toList_upwardEnumerableLt
     |> List.Pairwise.imp UpwardEnumerable.le_of_lt
@@ -2585,7 +2573,7 @@ public theorem toArray_eq_match_rci [Least? α] [UpwardEnumerable α]
 def toArray_eq_match_toArray_Rci := @toArray_eq_match_rci
 
 public theorem toList_eq_match_roi [Least? α] [UpwardEnumerable α]
-    [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
+    [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] :
     r.toList = match Least?.least? (α := α) with
       | none => []
       | some init => init :: (init<...*).toList := by
@@ -2597,7 +2585,7 @@ def toList_eq_match_toList_Roi := @toList_eq_match_roi
 
 public theorem toArray_eq_match_roi [Least? α] [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLeast? α]
-    [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
+    [Rxi.IsAlwaysFinite α] :
     r.toArray = match Least?.least? (α := α) with
       | none => #[]
       | some init => #[init] ++ (init<...*).toArray := by
@@ -2609,7 +2597,7 @@ def toArray_eq_match_Roi := @toArray_eq_match_roi
 
 public theorem toList_eq_nil_iff [LT α] [DecidableLT α] [Least? α] [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
-    [LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
+    [LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] :
     r.toList = [] ↔ ¬ Nonempty α := by
   simp only [toList_eq_match_roi]
   split
@@ -2619,7 +2607,7 @@ public theorem toList_eq_nil_iff [LT α] [DecidableLT α] [Least? α] [UpwardEnu
 
 public theorem toArray_eq_empty_iff [LT α] [DecidableLT α] [Least? α] [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
-    [LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
+    [LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] :
     r.toArray = #[] ↔ ¬ Nonempty α := by
   simp [← toArray_toList, toList_eq_nil_iff]
 
@@ -2634,7 +2622,7 @@ def mem_iff_mem_Rci := @mem_iff_mem_rci
 
 public theorem mem_toList [Least? α] [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLeast? α]
-    [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {a : α} : a ∈ r.toList := by
+    [Rxi.IsAlwaysFinite α] {a : α} : a ∈ r.toList := by
   letI : LE α := ⟨UpwardEnumerable.LE⟩
   haveI : LawfulUpwardEnumerableLE α := ⟨fun _ _ => Iff.rfl⟩
   simp only [toList_eq_match_rci, UpwardEnumerable.least?_eq_some (hn := ⟨a⟩),
@@ -2643,12 +2631,12 @@ public theorem mem_toList [Least? α] [UpwardEnumerable α]
 
 public theorem mem_toArray [Least? α] [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLeast? α]
-    [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {a : α} : a ∈ r.toArray := by
+    [Rxi.IsAlwaysFinite α] {a : α} : a ∈ r.toArray := by
   simp [← toArray_toList, mem_toList]
 
 public theorem pairwise_toList_upwardEnumerableLt [Least? α]
     [UpwardEnumerable α] [LawfulUpwardEnumerable α]
-    [LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
+    [LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] :
     r.toList.Pairwise (fun a b => UpwardEnumerable.LT a b) := by
   letI : LE α := ⟨UpwardEnumerable.LE⟩
   haveI : LawfulUpwardEnumerableLE α := ⟨fun _ _ => Iff.rfl⟩
@@ -2659,19 +2647,19 @@ public theorem pairwise_toList_upwardEnumerableLt [Least? α]
 
 public theorem pairwise_toList_ne [Least? α]
     [UpwardEnumerable α] [LawfulUpwardEnumerable α]
-    [LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
+    [LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] :
     r.toList.Pairwise (fun a b => a ≠ b) :=
   List.Pairwise.imp (fun hlt => UpwardEnumerable.ne_of_lt hlt) pairwise_toList_upwardEnumerableLt
 
 public theorem pairwise_toList_lt [LT α] [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerable α]
-    [LawfulUpwardEnumerableLT α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
+    [LawfulUpwardEnumerableLT α] [Rxi.IsAlwaysFinite α]
     [LawfulUpwardEnumerableLeast? α] : r.toList.Pairwise (fun a b => a < b) :=
   List.Pairwise.imp
     (fun hlt => (LawfulUpwardEnumerableLT.lt_iff ..).mpr hlt) pairwise_toList_upwardEnumerableLt
 
 public theorem pairwise_toList_le [LE α] [Least? α]
     [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
-    [LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
+    [LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] :
     r.toList.Pairwise (fun a b => a ≤ b) :=
   pairwise_toList_upwardEnumerableLt
     |> List.Pairwise.imp UpwardEnumerable.le_of_lt
@@ -2766,7 +2754,6 @@ private theorem Internal.iter_roc_eq_iter_rcc_of_isSome_succ?
 
 public theorem toList_roc_eq_toList_rcc_of_isSome_succ? [LE α] [DecidableLE α] [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α]
-    [LawfulUpwardEnumerable α]
     {lo hi : α} (h : (UpwardEnumerable.succ? lo).isSome) :
     (lo<...=hi).toList =
       ((UpwardEnumerable.succ? lo |>.get h)...=hi).toList := by
@@ -2786,7 +2773,7 @@ private theorem Internal.iter_roo_eq_iter_rco_of_isSome_succ?
 public theorem toList_roo_eq_toList_rco_of_isSome_succ?
     [LT α] [DecidableLT α] [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
-    [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
+    [Rxo.IsAlwaysFinite α]
     {lo hi : α} (h : (UpwardEnumerable.succ? lo).isSome) :
     (lo<...hi).toList =
       ((UpwardEnumerable.succ? lo |>.get h)...hi).toList := by
@@ -2806,7 +2793,7 @@ private theorem Internal.iter_roi_eq_iter_rci_of_isSome_succ?
 public theorem toList_roi_eq_toList_rci_of_isSome_succ?
     [UpwardEnumerable α]
     [LawfulUpwardEnumerable α]
-    [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
+    [Rxi.IsAlwaysFinite α]
     {lo : α} (h : (UpwardEnumerable.succ? lo).isSome) :
     (lo<...*).toList = ((UpwardEnumerable.succ? lo |>.get h)...*).toList := by
   simp [Rci.Internal.toList_eq_toList_iter, Roi.Internal.toList_eq_toList_iter,
diff --git a/src/Std/Data/DTreeMap/Internal/Zipper.lean b/src/Std/Data/DTreeMap/Internal/Zipper.lean
index 2d02be2977..a4e182c104 100644
--- a/src/Std/Data/DTreeMap/Internal/Zipper.lean
+++ b/src/Std/Data/DTreeMap/Internal/Zipper.lean
@@ -689,7 +689,7 @@ public instance [Ord α] {s : RicSlice α β} : ToIterator s Id ((a : α) × β
 
 public theorem toList_ric {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (t : Impl α β)
     (ordered : t.Ordered) (bound : α) : t[*...=bound].toList = t.toList.filter (fun e => (compare e.fst bound).isLE) := by
-  simp only [Ric.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
+  simp only [Ric.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
     Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
     Iter.toIter_toIterM]
   rw [RxcIterator.toList_rxcIter, RxcIterator.takeWhile_eq_filter]
@@ -717,7 +717,7 @@ public instance [Ord α] {s : Unit.RicSlice α} : ToIterator s Id α := by
 
 public theorem toList_ric {α : Type u} [Ord α] [TransOrd α] (t : Impl α (fun _ => Unit))
     (ordered : t.Ordered) (bound : α) : (t : Impl α (fun _ => Unit))[*...=bound].toList = (Internal.Impl.keys t).filter (fun e => (compare e bound).isLE) := by
-  simp only [Ric.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
+  simp only [Ric.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
     Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
     Iter.toIter_toIterM]
   rw [Iter.toList_map]
@@ -749,7 +749,7 @@ public instance [Ord α] {s : RicSlice α β} : ToIterator s Id (α × β) := by
 
 public theorem toList_ric {α : Type u} {β : Type v} [Ord α] [TransOrd α] (t : Impl α (fun _ => β))
     (ordered : t.Ordered) (bound : α) : t[*...=bound].toList = (Internal.Impl.Const.toList t).filter (fun e => (compare e.fst bound).isLE) := by
-  simp only [Ric.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
+  simp only [Ric.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
     Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
     Iter.toIter_toIterM]
   rw [Iter.toList_map]
@@ -780,7 +780,7 @@ public instance [Ord α] {s : RioSlice α β} : ToIterator s Id ((a : α) × β
 
 public theorem toList_rio {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (t : Impl α β)
     (ordered : t.Ordered) (bound : α) : t[*...bound].toList = t.toList.filter (fun e => (compare e.fst bound).isLT) := by
-  simp only [Rio.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
+  simp only [Rio.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
     Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
     Iter.toIter_toIterM]
   rw [RxoIterator.toList_rxoIter, RxoIterator.takeWhile_eq_filter]
@@ -808,7 +808,7 @@ public instance [Ord α] {s : Unit.RioSlice α} : ToIterator s Id α := by
 
 public theorem toList_rio {α : Type u} [Ord α] [TransOrd α] (t : Impl α (fun _ => Unit))
     (ordered : t.Ordered) (bound : α) : (t : Impl α (fun _ => Unit))[*...<bound].toList = (Internal.Impl.keys t).filter (fun e => (compare e bound).isLT) := by
-  simp only [Rio.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
+  simp only [Rio.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
     Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
     Iter.toIter_toIterM]
   rw [Iter.toList_map]
@@ -840,7 +840,7 @@ public instance [Ord α] {s : RioSlice α β} : ToIterator s Id (α × β) := by
 
 public theorem toList_rio {α : Type u} {β : Type v} [Ord α] [TransOrd α] (t : Impl α (fun _ => β))
     (ordered : t.Ordered) (bound : α) : t[*...<bound].toList = (Internal.Impl.Const.toList t).filter (fun e => (compare e.fst bound).isLT) := by
-  simp only [Rio.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
+  simp only [Rio.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
     Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
     Iter.toIter_toIterM]
   rw [Iter.toList_map]
@@ -904,7 +904,7 @@ public instance [Ord α] {s : RccSlice α β} : ToIterator s Id ((a : α) × β
 
 public theorem toList_rcc {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (t : Impl α β)
     (ordered : t.Ordered) (lowerBound upperBound : α) : t[lowerBound...=upperBound].toList = t.toList.filter (fun e => (compare e.fst lowerBound).isGE ∧ (compare e.fst upperBound).isLE) := by
-  simp only [Rcc.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
+  simp only [Rcc.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
     Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
     Iter.toIter_toIterM]
   rw [toList_rccIter]
@@ -929,7 +929,7 @@ public instance [Ord α] {s : Unit.RccSlice α} : ToIterator s Id α := by
 
 public theorem toList_rcc {α : Type u} [Ord α] [TransOrd α] (t : Impl α (fun _ => Unit))
     (ordered : t.Ordered) (lowerBound upperBound: α) : (t : Impl α (fun _ => Unit))[lowerBound...=upperBound].toList = (Internal.Impl.keys t).filter (fun e => (compare e lowerBound).isGE ∧ (compare e upperBound).isLE) := by
-  simp only [Rcc.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
+  simp only [Rcc.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
     Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
     Iter.toIter_toIterM]
   rw [Iter.toList_map]
@@ -963,7 +963,7 @@ public instance [Ord α] {s : RccSlice α β} : ToIterator s Id (α × β) := by
 
 public theorem toList_rcc {α : Type u} {β : Type v} [Ord α] [TransOrd α] (t : Impl α (fun _ => β))
     (ordered : t.Ordered) (lowerBound upperBound : α) : t[lowerBound...=upperBound].toList = (Internal.Impl.Const.toList t).filter (fun e => (compare e.fst lowerBound).isGE ∧ (compare e.fst upperBound).isLE) := by
-  simp only [Rcc.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
+  simp only [Rcc.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
     Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
     Iter.toIter_toIterM]
   rw [Iter.toList_map]
@@ -1031,7 +1031,7 @@ public instance [Ord α] {s : RcoSlice α β} : ToIterator s Id ((a : α) × β
 
 public theorem toList_rco {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (t : Impl α β)
     (ordered : t.Ordered) (lowerBound upperBound : α) : t[lowerBound...<upperBound].toList = t.toList.filter (fun e => (compare e.fst lowerBound).isGE ∧ (compare e.fst upperBound).isLT) := by
-  simp only [Rco.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
+  simp only [Rco.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
     Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
     Iter.toIter_toIterM]
   rw [toList_rcoIter]
@@ -1056,7 +1056,7 @@ public instance [Ord α] {s : Unit.RcoSlice α} : ToIterator s Id α := by
 
 public theorem toList_rco {α : Type u} [Ord α] [TransOrd α] (t : Impl α (fun _ => Unit))
     (ordered : t.Ordered) (lowerBound upperBound: α) : (t : Impl α (fun _ => Unit))[lowerBound...<upperBound].toList = (Internal.Impl.keys t).filter (fun e => (compare e lowerBound).isGE ∧ (compare e upperBound).isLT) := by
-  simp only [Rco.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
+  simp only [Rco.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
     Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
     Iter.toIter_toIterM]
   rw [Iter.toList_map]
@@ -1090,7 +1090,7 @@ public instance [Ord α] {s : RcoSlice α β} : ToIterator s Id (α × β) := by
 
 public theorem toList_rco {α : Type u} {β : Type v} [Ord α] [TransOrd α] (t : Impl α (fun _ => β))
     (ordered : t.Ordered) (lowerBound upperBound : α) : t[lowerBound...<upperBound].toList = (Internal.Impl.Const.toList t).filter (fun e => (compare e.fst lowerBound).isGE ∧ (compare e.fst upperBound).isLT) := by
-  simp only [Rco.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
+  simp only [Rco.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
     Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
     Iter.toIter_toIterM]
   rw [Iter.toList_map]
@@ -1157,7 +1157,7 @@ public instance [Ord α] {s : RooSlice α β} : ToIterator s Id ((a : α) × β
 
 public theorem toList_roo {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (t : Impl α β)
     (ordered : t.Ordered) (lowerBound upperBound : α) : t[lowerBound<...<upperBound].toList = t.toList.filter (fun e => (compare e.fst lowerBound).isGT ∧ (compare e.fst upperBound).isLT) := by
-  simp only [Roo.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
+  simp only [Roo.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
     Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
     Iter.toIter_toIterM]
   rw [toList_rooIter]
@@ -1182,7 +1182,7 @@ public instance [Ord α] {s : Unit.RooSlice α} : ToIterator s Id α := by
 
 public theorem toList_roo {α : Type u} [Ord α] [TransOrd α] (t : Impl α (fun _ => Unit))
     (ordered : t.Ordered) (lowerBound upperBound: α) : (t : Impl α (fun _ => Unit))[lowerBound<...<upperBound].toList = (Internal.Impl.keys t).filter (fun e => (compare e lowerBound).isGT ∧ (compare e upperBound).isLT) := by
-  simp only [Roo.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
+  simp only [Roo.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
     Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
     Iter.toIter_toIterM]
   rw [Iter.toList_map]
@@ -1216,7 +1216,7 @@ public instance [Ord α] {s : RooSlice α β} : ToIterator s Id (α × β) := by
 
 public theorem toList_roo {α : Type u} {β : Type v} [Ord α] [TransOrd α] (t : Impl α (fun _ => β))
     (ordered : t.Ordered) (lowerBound upperBound : α) : t[lowerBound<...<upperBound].toList = (Internal.Impl.Const.toList t).filter (fun e => (compare e.fst lowerBound).isGT ∧ (compare e.fst upperBound).isLT) := by
-  simp only [Roo.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
+  simp only [Roo.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
     Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
     Iter.toIter_toIterM]
   rw [Iter.toList_map]
@@ -1284,7 +1284,7 @@ public instance [Ord α] {s : RocSlice α β} : ToIterator s Id ((a : α) × β
 
 public theorem toList_roc {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (t : Impl α β)
     (ordered : t.Ordered) (lowerBound upperBound : α) : t[lowerBound<...=upperBound].toList = t.toList.filter (fun e => (compare e.fst lowerBound).isGT ∧ (compare e.fst upperBound).isLE) := by
-  simp only [Roc.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
+  simp only [Roc.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
     Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
     Iter.toIter_toIterM]
   rw [toList_rocIter]
@@ -1309,7 +1309,7 @@ public instance [Ord α] {s : Unit.RocSlice α} : ToIterator s Id α := by
 
 public theorem toList_roc {α : Type u} [Ord α] [TransOrd α] (t : Impl α (fun _ => Unit))
     (ordered : t.Ordered) (lowerBound upperBound: α) : (t : Impl α (fun _ => Unit))[lowerBound<...=upperBound].toList = (Internal.Impl.keys t).filter (fun e => (compare e lowerBound).isGT ∧ (compare e upperBound).isLE) := by
-  simp only [Roc.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
+  simp only [Roc.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
     Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
     Iter.toIter_toIterM]
   rw [Iter.toList_map]
@@ -1343,7 +1343,7 @@ public instance [Ord α] {s : RocSlice α β} : ToIterator s Id (α × β) := by
 
 public theorem toList_roc {α : Type u} {β : Type v} [Ord α] [TransOrd α] (t : Impl α (fun _ => β))
     (ordered : t.Ordered) (lowerBound upperBound : α) : t[lowerBound<...=upperBound].toList = (Internal.Impl.Const.toList t).filter (fun e => (compare e.fst lowerBound).isGT ∧ (compare e.fst upperBound).isLE) := by
-  simp only [Roc.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
+  simp only [Roc.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
     Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
     Iter.toIter_toIterM]
   rw [Iter.toList_map]
@@ -1396,7 +1396,7 @@ public instance [Ord α] {s : RciSlice α β} : ToIterator s Id ((a : α) × β
 
 public theorem toList_rci {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (t : Impl α β)
     (ordered : t.Ordered) (lowerBound : α) : t[lowerBound...*].toList = t.toList.filter (fun e => (compare e.fst lowerBound).isGE) := by
-  simp only [Rci.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
+  simp only [Rci.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
     Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
     Iter.toIter_toIterM]
   rw [toList_rciIter]
@@ -1421,7 +1421,7 @@ public instance [Ord α] {s : Unit.RciSlice α} : ToIterator s Id α := by
 
 public theorem toList_rci {α : Type u} [Ord α] [TransOrd α] (t : Impl α (fun _ => Unit))
     (ordered : t.Ordered) (lowerBound : α) : (t : Impl α (fun _ => Unit))[lowerBound...*].toList = (Internal.Impl.keys t).filter (fun e => (compare e lowerBound).isGE) := by
-  simp only [Rci.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
+  simp only [Rci.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
     Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
     Iter.toIter_toIterM]
   rw [Iter.toList_map]
@@ -1458,7 +1458,7 @@ public instance [Ord α] {s : RciSlice α β} : ToIterator s Id (α × β) := by
 
 public theorem toList_rci {α : Type u} {β : Type v} [Ord α] [TransOrd α] (t : Impl α (fun _ => β))
     (ordered : t.Ordered) (lowerBound : α) : t[lowerBound...*].toList = (Internal.Impl.Const.toList t).filter (fun e => (compare e.fst lowerBound).isGE) := by
-  simp only [Rci.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
+  simp only [Rci.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
     Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
     Iter.toIter_toIterM]
   rw [Iter.toList_map]
@@ -1512,7 +1512,7 @@ public instance [Ord α] {s : RoiSlice α β} : ToIterator s Id ((a : α) × β
 
 public theorem toList_roi {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (t : Impl α β)
     (ordered : t.Ordered) (lowerBound : α) : t[lowerBound<...*].toList = t.toList.filter (fun e => (compare e.fst lowerBound).isGT) := by
-  simp only [Roi.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
+  simp only [Roi.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
     Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
     Iter.toIter_toIterM]
   rw [toList_roiIter]
@@ -1537,7 +1537,7 @@ public instance [Ord α] {s : Unit.RoiSlice α} : ToIterator s Id α := by
 
 public theorem toList_roi {α : Type u} [Ord α] [TransOrd α] (t : Impl α (fun _ => Unit))
     (ordered : t.Ordered) (lowerBound : α) : (t : Impl α (fun _ => Unit))[lowerBound<...*].toList = (Internal.Impl.keys t).filter (fun e => (compare e lowerBound).isGT) := by
-  simp only [Roi.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
+  simp only [Roi.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
     Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
     Iter.toIter_toIterM]
   rw [Iter.toList_map]
@@ -1574,7 +1574,7 @@ public instance [Ord α] {s : RoiSlice α β} : ToIterator s Id (α × β) := by
 
 public theorem toList_roi {α : Type u} {β : Type v} [Ord α] [TransOrd α] (t : Impl α (fun _ => β))
     (ordered : t.Ordered) (lowerBound : α) : t[lowerBound<...*].toList = (Internal.Impl.Const.toList t).filter (fun e => (compare e.fst lowerBound).isGT) := by
-  simp only [Roi.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
+  simp only [Roi.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
     Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
     Iter.toIter_toIterM]
   rw [Iter.toList_map]
@@ -1621,7 +1621,7 @@ public instance {s : RiiSlice α β} : ToIterator s Id ((a : α) × β a) :=
   ToIterator.of (Zipper α β) (riiIterator s.1.treeMap)
 
 public theorem toList_rii {α : Type u} {β : α → Type v} (t : Impl α β) : t[*...*].toList = t.toList := by
-  simp only [Rii.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
+  simp only [Rii.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
     Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
     Iter.toIter_toIterM]
   rw [toList_riiIter]
@@ -1645,7 +1645,7 @@ public instance {s : Unit.RiiSlice α} : ToIterator s Id α := by
 
 public theorem toList_rii {α : Type u} (t : Impl α (fun _ => Unit)) :
     (t : Impl α fun _ => Unit)[*...*].toList = Internal.Impl.keys t := by
-  simp only [Rii.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
+  simp only [Rii.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
     Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
     Iter.toIter_toIterM]
   rw [Iter.toList_map]
@@ -1675,7 +1675,7 @@ public instance {s : Const.RiiSlice α β} : ToIterator s Id (α × β) := by
 
 public theorem toList_rii {α : Type u} {β : Type v} (t : Impl α (fun _ => β)) :
     (t : Impl α fun _ => β)[*...*].toList = Internal.Impl.Const.toList t := by
-  simp only [Rii.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
+  simp only [Rii.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
     Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
     Iter.toIter_toIterM]
   rw [Iter.toList_map]
diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Range.lean b/src/Std/Data/Iterators/Lemmas/Producers/Range.lean
index 68eb660a54..d5b7482c22 100644
--- a/src/Std/Data/Iterators/Lemmas/Producers/Range.lean
+++ b/src/Std/Data/Iterators/Lemmas/Producers/Range.lean
@@ -15,51 +15,102 @@ namespace Std
 open Std.PRange Std.Iterators
 
 @[simp]
+theorem Rcc.toList_iter [LE α] [DecidableLE α] [UpwardEnumerable α]
+    [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rcc α} :
+    r.iter.toList = r.toList := by
+ rfl
+
+@[deprecated Rcc.toList_iter (since := "2025-11-13")]
 theorem Rcc.toList_iter_eq_toList [LE α] [DecidableLE α] [UpwardEnumerable α]
     [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rcc α} :
     r.iter.toList = r.toList := by
  rfl
 
 @[simp]
+theorem Rcc.toArray_iter [LE α] [DecidableLE α] [UpwardEnumerable α]
+    [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rcc α} :
+    r.iter.toArray = r.toArray := by
+ rfl
+
+@[deprecated Rcc.toArray_iter (since := "2025-11-13")]
 theorem Rcc.toArray_iter_eq_toArray [LE α] [DecidableLE α] [UpwardEnumerable α]
     [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rcc α} :
     r.iter.toArray = r.toArray := by
  rfl
 
 @[simp]
+theorem Rcc.count_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]
+
+@[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 := by
-  rw [← size_toArray, ← toArray_iter_eq_toArray, Iter.size_toArray_eq_count]
+    r.iter.count = r.size :=
+  count_iter
 
 @[simp]
+theorem Rco.toList_iter [LT α] [DecidableLT α] [UpwardEnumerable α]
+    [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rco α} :
+    r.iter.toList = r.toList := by
+ rfl
+
+@[deprecated Rco.toList_iter (since := "2025-11-13")]
 theorem Rco.toList_iter_eq_toList [LT α] [DecidableLT α] [UpwardEnumerable α]
     [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rco α} :
     r.iter.toList = r.toList := by
  rfl
 
 @[simp]
+theorem Rco.toArray_iter [LT α] [DecidableLT α] [UpwardEnumerable α]
+    [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rco α} :
+    r.iter.toArray = r.toArray := by
+ rfl
+
+@[deprecated Rco.toArray_iter (since := "2025-11-13")]
 theorem Rco.toArray_iter_eq_toArray [LT α] [DecidableLT α] [UpwardEnumerable α]
     [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rco α} :
     r.iter.toArray = r.toArray := by
  rfl
 
 @[simp]
+theorem Rco.count_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]
+
+@[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_eq_toArray, Iter.size_toArray_eq_count]
+  rw [← size_toArray, ← toArray_iter, Iter.size_toArray_eq_count]
 
 @[simp]
+theorem Rci.toList_iter [UpwardEnumerable α]
+    [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rci α} :
+    r.iter.toList = r.toList := by
+ rfl
+
+@[deprecated Rci.toList_iter (since := "2025-11-13")]
 theorem Rci.toList_iter_eq_toList [UpwardEnumerable α]
     [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rci α} :
     r.iter.toList = r.toList := by
  rfl
 
+@[simp]
+theorem Rci.toArray_iter [UpwardEnumerable α]
+    [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rci α} :
+    r.iter.toArray = r.toArray := by
+ rfl
+
 @[simp]
 theorem Rci.toArray_iter_eq_toArray [UpwardEnumerable α]
     [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rci α} :
@@ -67,6 +118,14 @@ theorem Rci.toArray_iter_eq_toArray [UpwardEnumerable α]
  rfl
 
 @[simp]
+theorem Rci.count_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]
+
+@[deprecated Rci.count_iter (since := "2025-11-13")]
 theorem Rci.count_iter_eq_size [UpwardEnumerable α]
     [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
     [Rxi.HasSize α] [Rxi.LawfulHasSize α]
@@ -75,11 +134,23 @@ theorem Rci.count_iter_eq_size [UpwardEnumerable α]
   rw [← size_toArray, ← toArray_iter_eq_toArray, Iter.size_toArray_eq_count]
 
 @[simp]
+theorem Roc.toList_iter [LE α] [DecidableLE α] [UpwardEnumerable α]
+    [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Roc α} :
+    r.iter.toList = r.toList := by
+ rfl
+
+@[deprecated Roc.toList_iter (since := "2025-11-13")]
 theorem Roc.toList_iter_eq_toList [LE α] [DecidableLE α] [UpwardEnumerable α]
     [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Roc α} :
     r.iter.toList = r.toList := by
  rfl
 
+@[simp]
+theorem Roc.toArray_iter [LE α] [DecidableLE α] [UpwardEnumerable α]
+    [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Roc α} :
+    r.iter.toArray = r.toArray := by
+ rfl
+
 @[simp]
 theorem Roc.toArray_iter_eq_toArray [LE α] [DecidableLE α] [UpwardEnumerable α]
     [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Roc α} :
@@ -87,6 +158,14 @@ theorem Roc.toArray_iter_eq_toArray [LE α] [DecidableLE α] [UpwardEnumerable 
  rfl
 
 @[simp]
+theorem Roc.count_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]
+
+@[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 α]
@@ -95,11 +174,23 @@ theorem Roc.count_iter_eq_size [LE α] [DecidableLE α] [UpwardEnumerable α]
   rw [← size_toArray, ← toArray_iter_eq_toArray, Iter.size_toArray_eq_count]
 
 @[simp]
+theorem Roo.toList_iter [LT α] [DecidableLT α] [UpwardEnumerable α]
+    [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Roo α} :
+    r.iter.toList = r.toList := by
+ rfl
+
+@[deprecated Roo.toList_iter (since := "2025-11-13")]
 theorem Roo.toList_iter_eq_toList [LT α] [DecidableLT α] [UpwardEnumerable α]
     [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Roo α} :
     r.iter.toList = r.toList := by
  rfl
 
+@[simp]
+theorem Roo.toArray_iter [LT α] [DecidableLT α] [UpwardEnumerable α]
+    [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Roo α} :
+    r.iter.toArray = r.toArray := by
+ rfl
+
 @[simp]
 theorem Roo.toArray_iter_eq_toArray [LT α] [DecidableLT α] [UpwardEnumerable α]
     [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Roo α} :
@@ -107,6 +198,14 @@ theorem Roo.toArray_iter_eq_toArray [LT α] [DecidableLT α] [UpwardEnumerable 
  rfl
 
 @[simp]
+theorem Roo.count_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]
+
+@[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 α]
@@ -115,83 +214,163 @@ theorem Roo.count_iter_eq_size [LT α] [DecidableLT α] [UpwardEnumerable α]
   rw [← size_toArray, ← toArray_iter_eq_toArray, Iter.size_toArray_eq_count]
 
 @[simp]
+theorem Roi.toList_iter [UpwardEnumerable α]
+    [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Roi α} :
+    r.iter.toList = r.toList := by
+ rfl
+
+@[deprecated Roi.toList_iter (since := "2025-11-13")]
 theorem Roi.toList_iter_eq_toList [UpwardEnumerable α]
     [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Roi α} :
     r.iter.toList = r.toList := by
  rfl
 
 @[simp]
+theorem Roi.toArray_iter [UpwardEnumerable α]
+    [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Roi α} :
+    r.iter.toArray = r.toArray := by
+ rfl
+
+@[deprecated Roi.toArray_iter (since := "2025-11-13")]
 theorem Roi.toArray_iter_eq_toArray [UpwardEnumerable α]
     [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Roi α} :
     r.iter.toArray = r.toArray := by
  rfl
 
 @[simp]
+theorem Roi.count_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]
+
+@[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_eq_toArray, Iter.size_toArray_eq_count]
+  rw [← size_toArray, ← toArray_iter, Iter.size_toArray_eq_count]
 
 @[simp]
+theorem Ric.toList_iter [Least? α] [LE α] [DecidableLE α] [UpwardEnumerable α]
+    [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Ric α} :
+    r.iter.toList = r.toList := by
+ rfl
+
+@[deprecated Ric.toList_iter (since := "2025-11-13")]
 theorem Ric.toList_iter_eq_toList [Least? α] [LE α] [DecidableLE α] [UpwardEnumerable α]
     [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Ric α} :
     r.iter.toList = r.toList := by
  rfl
 
 @[simp]
+theorem Ric.toArray_iter [Least? α] [LE α] [DecidableLE α] [UpwardEnumerable α]
+    [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Ric α} :
+    r.iter.toArray = r.toArray := by
+ rfl
+
+@[deprecated Ric.toArray_iter (since := "2025-11-13")]
 theorem Ric.toArray_iter_eq_toArray [Least? α] [LE α] [DecidableLE α] [UpwardEnumerable α]
     [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Ric α} :
     r.iter.toArray = r.toArray := by
  rfl
 
 @[simp]
+theorem Ric.count_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]
+
+@[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_eq_toArray, Iter.size_toArray_eq_count]
+  rw [← size_toArray, ← toArray_iter, Iter.size_toArray_eq_count]
 
 @[simp]
+theorem Rio.toList_iter [Least? α] [LT α] [DecidableLT α] [UpwardEnumerable α]
+    [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rio α} :
+    r.iter.toList = r.toList := by
+ rfl
+
+@[deprecated Rio.toList_iter (since := "2025-11-13")]
 theorem Rio.toList_iter_eq_toList [Least? α] [LT α] [DecidableLT α] [UpwardEnumerable α]
     [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rio α} :
     r.iter.toList = r.toList := by
  rfl
 
 @[simp]
+theorem Rio.toArray_iter [Least? α] [LT α] [DecidableLT α] [UpwardEnumerable α]
+    [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rio α} :
+    r.iter.toArray = r.toArray := by
+ rfl
+
+@[deprecated Rio.toArray_iter (since := "2025-11-13")]
 theorem Rio.toArray_iter_eq_toArray [Least? α] [LT α] [DecidableLT α] [UpwardEnumerable α]
     [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rio α} :
     r.iter.toArray = r.toArray := by
  rfl
 
 @[simp]
+theorem Rio.count_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]
+
+@[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_eq_toArray, Iter.size_toArray_eq_count]
+  rw [← size_toArray, ← toArray_iter, Iter.size_toArray_eq_count]
 
 @[simp]
+theorem Rii.toList_iter [Least? α] [UpwardEnumerable α]
+    [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rii α} :
+    r.iter.toList = r.toList := by
+ rfl
+
+@[deprecated Rii.toList_iter (since := "2025-11-13")]
 theorem Rii.toList_iter_eq_toList [Least? α] [UpwardEnumerable α]
     [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rii α} :
     r.iter.toList = r.toList := by
  rfl
 
 @[simp]
+theorem Rii.toArray_iter [Least? α] [UpwardEnumerable α]
+    [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rii α} :
+    r.iter.toArray = r.toArray := by
+ rfl
+
+@[deprecated Rii.toArray_iter (since := "2025-11-13")]
 theorem Rii.toArray_iter_eq_toArray [Least? α] [UpwardEnumerable α]
     [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rii α} :
     r.iter.toArray = r.toArray := by
  rfl
 
 @[simp]
+theorem Rii.count_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]
+
+@[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_eq_toArray, Iter.size_toArray_eq_count]
+  rw [← size_toArray, ← toArray_iter, Iter.size_toArray_eq_count]
 
 end Std
diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Slice.lean b/src/Std/Data/Iterators/Lemmas/Producers/Slice.lean
index eb3927c60e..e9d1988c39 100644
--- a/src/Std/Data/Iterators/Lemmas/Producers/Slice.lean
+++ b/src/Std/Data/Iterators/Lemmas/Producers/Slice.lean
@@ -43,21 +43,44 @@ theorem count_iter_eq_size [∀ s : Slice γ, ToIterator s Id β]
     s.iter.count = s.size :=
   size_eq_count_iter.symm
 
+@[simp]
+theorem 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] :
+    s.iter.toArray = s.toArray := by
+  simp [Internal.iter_eq_iter, Internal.toArray_eq_toArray_iter]
+
+@[deprecated toArray_iter (since := "2025-11-13")]
 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] :
     s.toArray = s.iter.toArray := by
-  simp [Internal.iter_eq_iter, Internal.toArray_eq_toArray_iter]
+  simp
 
+@[simp]
+theorem toList_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] :
+    s.iter.toList = s.toList := by
+  simp [Internal.iter_eq_iter, Internal.toList_eq_toList_iter]
+
+@[deprecated toList_iter (since := "2025-11-13")]
 theorem toList_eq_toList_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] :
     s.toList = s.iter.toList := by
-  simp [Internal.iter_eq_iter, Internal.toList_eq_toList_iter]
+  simp
 
+@[simp]
+theorem toListRev_iter {s : Slice γ} [ToIterator s Id β]
+    [Iterator (ToIterator.State s Id) Id β] [Finite (ToIterator.State s Id) Id] :
+    s.iter.toListRev = s.toListRev := by
+  simp [Internal.iter_eq_iter, Internal.toListRev_eq_toListRev_iter]
+
+@[deprecated toListRev_iter (since := "2025-11-13")]
 theorem toListRev_eq_toListRev_iter {s : Slice γ} [ToIterator s Id β]
     [Iterator (ToIterator.State s Id) Id β] [Finite (ToIterator.State s Id) Id] :
     s.toListRev = s.iter.toListRev := by
-  simp [Internal.iter_eq_iter, Internal.toListRev_eq_toListRev_iter]
+  simp
 
 end Std.Slice