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
    @[deprecated Std.Rcc.length_iter (since := "2025-11-13")]
    def Std.Rcc.count_iter_eq_size {α : 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
        @[deprecated Std.Rco.length_iter (since := "2025-11-13")]
        def Std.Rco.count_iter_eq_size {α : 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
            @[deprecated Std.Rci.length_iter (since := "2025-11-13")]
            def Std.Rci.count_iter_eq_size {α : 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
                @[deprecated Std.Roc.length_iter (since := "2025-11-13")]
                def Std.Roc.count_iter_eq_size {α : 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
                    @[deprecated Std.Roo.length_iter (since := "2025-11-13")]
                    def Std.Roo.count_iter_eq_size {α : 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
                        @[deprecated Std.Roi.length_iter (since := "2025-11-13")]
                        def Std.Roi.count_iter_eq_size {α : 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
                            @[deprecated Std.Ric.length_iter (since := "2025-11-13")]
                            def Std.Ric.count_iter_eq_size {α : 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
                                @[deprecated Std.Rio.length_iter (since := "2025-11-13")]
                                def Std.Rio.count_iter_eq_size {α : 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
                                    source
                                    @[deprecated Std.Rii.length_iter (since := "2025-11-13")]
                                    def Std.Rii.count_iter_eq_size {α : Type u_1} [PRange.Least? α] [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [Rxi.HasSize α] [Rxi.LawfulHasSize α] {r : Rii α} :
                                    r.iter.length = r.size
                                    Instances For