@[simp]

theorem Std.Rcc.toList_iter {α : Type u_1} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Rcc α} : r.iter.toList = r.toList

@[deprecated Std.Rcc.toList_iter (since := "2025-11-13")]

theorem Std.Rcc.toList_iter_eq_toList {α : Type u_1} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Rcc α} : r.iter.toList = r.toList

@[simp]

theorem Std.Rcc.toArray_iter {α : Type u_1} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Rcc α} : r.iter.toArray = r.toArray

@[deprecated Std.Rcc.toArray_iter (since := "2025-11-13")]

theorem Std.Rcc.toArray_iter_eq_toArray {α : Type u_1} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Rcc α} : r.iter.toArray = r.toArray

@[simp]

theorem Std.Rcc.length_iter {α : Type u_1} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [Rxc.HasSize α] [Rxc.LawfulHasSize α] {r : Rcc α} : r.iter.length = r.size

@[deprecated Std.Rcc.length_iter (since := "2026-01-28")]

def Std.Rcc.count_iter {α : Type u_1} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [Rxc.HasSize α] [Rxc.LawfulHasSize α] {r : Rcc α} : r.iter.length = r.size

Equations

• @Std.Rcc.count_iter = @Std.Rcc.length_iter

@[simp]

theorem Std.Rco.toList_iter {α : Type u_1} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Rco α} : r.iter.toList = r.toList

@[deprecated Std.Rco.toList_iter (since := "2025-11-13")]

theorem Std.Rco.toList_iter_eq_toList {α : Type u_1} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Rco α} : r.iter.toList = r.toList

@[simp]

theorem Std.Rco.toArray_iter {α : Type u_1} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Rco α} : r.iter.toArray = r.toArray

@[deprecated Std.Rco.toArray_iter (since := "2025-11-13")]

theorem Std.Rco.toArray_iter_eq_toArray {α : Type u_1} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Rco α} : r.iter.toArray = r.toArray

@[simp]

theorem Std.Rco.length_iter {α : Type u_1} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [Rxo.HasSize α] [Rxo.LawfulHasSize α] {r : Rco α} : r.iter.length = r.size

@[deprecated Std.Rco.length_iter (since := "2026-01-28")]

def Std.Rco.count_iter {α : Type u_1} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [Rxo.HasSize α] [Rxo.LawfulHasSize α] {r : Rco α} : r.iter.length = r.size

Equations

• @Std.Rco.count_iter = @Std.Rco.length_iter

@[simp]

theorem Std.Rci.toList_iter {α : Type u_1} [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Rci α} : r.iter.toList = r.toList

@[deprecated Std.Rci.toList_iter (since := "2025-11-13")]

theorem Std.Rci.toList_iter_eq_toList {α : Type u_1} [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Rci α} : r.iter.toList = r.toList

@[simp]

theorem Std.Rci.toArray_iter {α : Type u_1} [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Rci α} : r.iter.toArray = r.toArray

@[simp]

theorem Std.Rci.toArray_iter_eq_toArray {α : Type u_1} [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Rci α} : r.iter.toArray = r.toArray

@[simp]

theorem Std.Rci.length_iter {α : Type u_1} [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [Rxi.HasSize α] [Rxi.LawfulHasSize α] {r : Rci α} : r.iter.length = r.size

@[deprecated Std.Rci.length_iter (since := "2026-01-28")]

def Std.Rci.count_iter {α : Type u_1} [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [Rxi.HasSize α] [Rxi.LawfulHasSize α] {r : Rci α} : r.iter.length = r.size

Equations

• @Std.Rci.count_iter = @Std.Rci.length_iter

@[simp]

theorem Std.Roc.toList_iter {α : Type u_1} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Roc α} : r.iter.toList = r.toList

@[deprecated Std.Roc.toList_iter (since := "2025-11-13")]

theorem Std.Roc.toList_iter_eq_toList {α : Type u_1} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Roc α} : r.iter.toList = r.toList

@[simp]

theorem Std.Roc.toArray_iter {α : Type u_1} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Roc α} : r.iter.toArray = r.toArray

@[simp]

theorem Std.Roc.toArray_iter_eq_toArray {α : Type u_1} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Roc α} : r.iter.toArray = r.toArray

@[simp]

theorem Std.Roc.length_iter {α : Type u_1} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [Rxc.HasSize α] [Rxc.LawfulHasSize α] {r : Roc α} : r.iter.length = r.size

@[deprecated Std.Roc.length_iter (since := "2026-01-28")]

def Std.Roc.count_iter {α : Type u_1} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [Rxc.HasSize α] [Rxc.LawfulHasSize α] {r : Roc α} : r.iter.length = r.size

Equations

• @Std.Roc.count_iter = @Std.Roc.length_iter

@[simp]

theorem Std.Roo.toList_iter {α : Type u_1} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Roo α} : r.iter.toList = r.toList

@[deprecated Std.Roo.toList_iter (since := "2025-11-13")]

theorem Std.Roo.toList_iter_eq_toList {α : Type u_1} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Roo α} : r.iter.toList = r.toList

@[simp]

theorem Std.Roo.toArray_iter {α : Type u_1} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Roo α} : r.iter.toArray = r.toArray

@[simp]

theorem Std.Roo.toArray_iter_eq_toArray {α : Type u_1} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Roo α} : r.iter.toArray = r.toArray

@[simp]

theorem Std.Roo.length_iter {α : Type u_1} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [Rxo.HasSize α] [Rxo.LawfulHasSize α] {r : Roo α} : r.iter.length = r.size

@[deprecated Std.Roo.length_iter (since := "2026-01-28")]

def Std.Roo.count_iter {α : Type u_1} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [Rxo.HasSize α] [Rxo.LawfulHasSize α] {r : Roo α} : r.iter.length = r.size

Equations

• @Std.Roo.count_iter = @Std.Roo.length_iter

@[simp]

theorem Std.Roi.toList_iter {α : Type u_1} [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Roi α} : r.iter.toList = r.toList

@[deprecated Std.Roi.toList_iter (since := "2025-11-13")]

theorem Std.Roi.toList_iter_eq_toList {α : Type u_1} [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Roi α} : r.iter.toList = r.toList

@[simp]

theorem Std.Roi.toArray_iter {α : Type u_1} [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Roi α} : r.iter.toArray = r.toArray

@[deprecated Std.Roi.toArray_iter (since := "2025-11-13")]

theorem Std.Roi.toArray_iter_eq_toArray {α : Type u_1} [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Roi α} : r.iter.toArray = r.toArray

@[simp]

theorem Std.Roi.length_iter {α : Type u_1} [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [Rxi.HasSize α] [Rxi.LawfulHasSize α] {r : Roi α} : r.iter.length = r.size

@[deprecated Std.Roi.length_iter (since := "2026-01-28")]

def Std.Roi.count_iter {α : Type u_1} [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [Rxi.HasSize α] [Rxi.LawfulHasSize α] {r : Roi α} : r.iter.length = r.size

Equations

• @Std.Roi.count_iter = @Std.Roi.length_iter

@[simp]

theorem Std.Ric.toList_iter {α : Type u_1} [PRange.Least? α] [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Ric α} : r.iter.toList = r.toList

@[deprecated Std.Ric.toList_iter (since := "2025-11-13")]

theorem Std.Ric.toList_iter_eq_toList {α : Type u_1} [PRange.Least? α] [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Ric α} : r.iter.toList = r.toList

@[simp]

theorem Std.Ric.toArray_iter {α : Type u_1} [PRange.Least? α] [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Ric α} : r.iter.toArray = r.toArray

@[deprecated Std.Ric.toArray_iter (since := "2025-11-13")]

theorem Std.Ric.toArray_iter_eq_toArray {α : Type u_1} [PRange.Least? α] [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Ric α} : r.iter.toArray = r.toArray

@[simp]

theorem Std.Ric.length_iter {α : Type u_1} [PRange.Least? α] [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [Rxc.HasSize α] [Rxc.LawfulHasSize α] {r : Ric α} : r.iter.length = r.size

@[deprecated Std.Ric.length_iter (since := "2026-01-28")]

def Std.Ric.count_iter {α : Type u_1} [PRange.Least? α] [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [Rxc.HasSize α] [Rxc.LawfulHasSize α] {r : Ric α} : r.iter.length = r.size

Equations

• @Std.Ric.count_iter = @Std.Ric.length_iter

@[simp]

theorem Std.Rio.toList_iter {α : Type u_1} [PRange.Least? α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Rio α} : r.iter.toList = r.toList

@[deprecated Std.Rio.toList_iter (since := "2025-11-13")]

theorem Std.Rio.toList_iter_eq_toList {α : Type u_1} [PRange.Least? α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Rio α} : r.iter.toList = r.toList

@[simp]

theorem Std.Rio.toArray_iter {α : Type u_1} [PRange.Least? α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Rio α} : r.iter.toArray = r.toArray

@[deprecated Std.Rio.toArray_iter (since := "2025-11-13")]

theorem Std.Rio.toArray_iter_eq_toArray {α : Type u_1} [PRange.Least? α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Rio α} : r.iter.toArray = r.toArray

@[simp]

theorem Std.Rio.length_iter {α : Type u_1} [PRange.Least? α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [Rxo.HasSize α] [Rxo.LawfulHasSize α] {r : Rio α} : r.iter.length = r.size

@[deprecated Std.Rio.length_iter (since := "2026-01-28")]

def Std.Rio.count_iter {α : Type u_1} [PRange.Least? α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [Rxo.HasSize α] [Rxo.LawfulHasSize α] {r : Rio α} : r.iter.length = r.size

Equations

• @Std.Rio.count_iter = @Std.Rio.length_iter

@[simp]

theorem Std.Rii.toList_iter {α : Type u_1} [PRange.Least? α] [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Rii α} : r.iter.toList = r.toList

@[deprecated Std.Rii.toList_iter (since := "2025-11-13")]

theorem Std.Rii.toList_iter_eq_toList {α : Type u_1} [PRange.Least? α] [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Rii α} : r.iter.toList = r.toList

@[simp]

theorem Std.Rii.toArray_iter {α : Type u_1} [PRange.Least? α] [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Rii α} : r.iter.toArray = r.toArray

@[deprecated Std.Rii.toArray_iter (since := "2025-11-13")]

theorem Std.Rii.toArray_iter_eq_toArray {α : Type u_1} [PRange.Least? α] [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Rii α} : r.iter.toArray = r.toArray

@[simp]

theorem Std.Rii.length_iter {α : Type u_1} [PRange.Least? α] [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [Rxi.HasSize α] [Rxi.LawfulHasSize α] {r : Rii α} : r.iter.length = r.size

@[deprecated Std.Rii.length_iter (since := "2026-01-28")]

def Std.Rii.count_iter {α : Type u_1} [PRange.Least? α] [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [Rxi.HasSize α] [Rxi.LawfulHasSize α] {r : Rii α} : r.iter.length = r.size

Equations

• @Std.Rii.count_iter = @Std.Rii.length_iter