Documentation

Std.Data.Iterators.Lemmas.Producers.Range

source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
Instances For
    source
    @[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
    source
    @[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
    source
    @[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
    source
    @[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
    source
    @[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
    source
    @[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
    Instances For
      source
      @[simp]
      theorem Std.Rci.toList_iter {α : Type u_1} [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Rci α} :
      r.iter.toList = r.toList
      source
      @[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
      source
      @[simp]
      theorem Std.Rci.toArray_iter {α : Type u_1} [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Rci α} :
      r.iter.toArray = r.toArray
      source
      @[simp]
      theorem Std.Rci.toArray_iter_eq_toArray {α : Type u_1} [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Rci α} :
      r.iter.toArray = r.toArray
      source
      @[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
      source
      @[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
      Instances For
        source
        @[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
        source
        @[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
        source
        @[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
        source
        @[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
        source
        @[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
        source
        @[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
        Instances For
          source
          @[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
          source
          @[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
          source
          @[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
          source
          @[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
          source
          @[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
          source
          @[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
          Instances For
            source
            @[simp]
            theorem Std.Roi.toList_iter {α : Type u_1} [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Roi α} :
            r.iter.toList = r.toList
            source
            @[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
            source
            @[simp]
            theorem Std.Roi.toArray_iter {α : Type u_1} [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Roi α} :
            r.iter.toArray = r.toArray
            source
            @[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
            source
            @[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
            source
            @[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
            Instances For
              source
              @[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
              source
              @[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
              source
              @[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
              source
              @[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
              source
              @[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
              source
              @[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
              Instances For
                source
                @[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
                source
                @[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
                source
                @[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
                source
                @[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
                source
                @[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
                source
                @[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
                Instances For
                  source
                  @[simp]
                  theorem Std.Rii.toList_iter {α : Type u_1} [PRange.Least? α] [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Rii α} :
                  r.iter.toList = r.toList
                  source
                  @[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
                  source
                  @[simp]
                  theorem Std.Rii.toArray_iter {α : Type u_1} [PRange.Least? α] [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {r : Rii α} :
                  r.iter.toArray = r.toArray
                  source
                  @[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
                  source
                  @[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
                  source
                  @[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
                  Instances For