Lemmas about ranges

This file provides lemmas about Std.PRange.

theorem Std.PRange.UpwardEnumerable.exists_of_succ_le {α : Type u} [UpwardEnumerable α] [LawfulUpwardEnumerable α] [InfinitelyUpwardEnumerable α] {a b : α} (h : UpwardEnumerable.LE (succ a) b) : ∃ (b' : α), b = succ b' ∧ UpwardEnumerable.LE a b'

theorem Std.PRange.UpwardEnumerable.exists_of_succ_lt {α : Type u} [UpwardEnumerable α] [LawfulUpwardEnumerable α] [InfinitelyUpwardEnumerable α] {a b : α} (h : UpwardEnumerable.LT (succ a) b) : ∃ (b' : α), b = succ b' ∧ UpwardEnumerable.LT a b'

theorem Std.Rcc.forIn'_congr {α : Type u} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] {γ : Type u} {init init' : γ} {r r' : Rcc α} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} {f' : (a : α) → a ∈ r' → γ → m (ForInStep γ)} (hr : r = r') (hi : init = init') (h : ∀ (a : α) (m_1 : a ∈ r') (b : γ), f a ⋯ b = f' a m_1 b) : forIn' r init f = forIn' r' init' f'

theorem Std.Rco.forIn'_congr {α : Type u} [LE α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] {γ : Type u} {init init' : γ} {r r' : Rco α} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} {f' : (a : α) → a ∈ r' → γ → m (ForInStep γ)} (hr : r = r') (hi : init = init') (h : ∀ (a : α) (m_1 : a ∈ r') (b : γ), f a ⋯ b = f' a m_1 b) : forIn' r init f = forIn' r' init' f'

theorem Std.Rci.forIn'_congr {α : Type u} [LE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] {γ : Type u} {init init' : γ} {r r' : Rci α} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} {f' : (a : α) → a ∈ r' → γ → m (ForInStep γ)} (hr : r = r') (hi : init = init') (h : ∀ (a : α) (m_1 : a ∈ r') (b : γ), f a ⋯ b = f' a m_1 b) : forIn' r init f = forIn' r' init' f'

theorem Std.Roc.forIn'_congr {α : Type u} [LE α] [LT α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLT α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] {γ : Type u} {init init' : γ} {r r' : Roc α} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} {f' : (a : α) → a ∈ r' → γ → m (ForInStep γ)} (hr : r = r') (hi : init = init') (h : ∀ (a : α) (m_1 : a ∈ r') (b : γ), f a ⋯ b = f' a m_1 b) : forIn' r init f = forIn' r' init' f'

theorem Std.Roo.forIn'_congr {α : Type u} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] {γ : Type u} {init init' : γ} {r r' : Roo α} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} {f' : (a : α) → a ∈ r' → γ → m (ForInStep γ)} (hr : r = r') (hi : init = init') (h : ∀ (a : α) (m_1 : a ∈ r') (b : γ), f a ⋯ b = f' a m_1 b) : forIn' r init f = forIn' r' init' f'

theorem Std.Roi.forIn'_congr {α : Type u} [LT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] {γ : Type u} {init init' : γ} {r r' : Roi α} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} {f' : (a : α) → a ∈ r' → γ → m (ForInStep γ)} (hr : r = r') (hi : init = init') (h : ∀ (a : α) (m_1 : a ∈ r') (b : γ), f a ⋯ b = f' a m_1 b) : forIn' r init f = forIn' r' init' f'

theorem Std.Ric.forIn'_congr {α : Type u} [LE α] [DecidableLE α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] {γ : Type u} {init init' : γ} {r r' : Ric α} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} {f' : (a : α) → a ∈ r' → γ → m (ForInStep γ)} (hr : r = r') (hi : init = init') (h : ∀ (a : α) (m_1 : a ∈ r') (b : γ), f a ⋯ b = f' a m_1 b) : forIn' r init f = forIn' r' init' f'

theorem Std.Rio.forIn'_congr {α : Type u} [LT α] [DecidableLT α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] {γ : Type u} {init init' : γ} {r r' : Rio α} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} {f' : (a : α) → a ∈ r' → γ → m (ForInStep γ)} (hr : r = r') (hi : init = init') (h : ∀ (a : α) (m_1 : a ∈ r') (b : γ), f a ⋯ b = f' a m_1 b) : forIn' r init f = forIn' r' init' f'

theorem Std.Rii.forIn'_congr {α : Type u} [PRange.UpwardEnumerable α] [PRange.Least? α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLeast? α] {m : Type u → Type w} [Monad m] {γ : Type u} {init init' : γ} {r r' : Rii α} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} {f' : (a : α) → a ∈ r' → γ → m (ForInStep γ)} (hr : r = r') (hi : init = init') (h : ∀ (a : α) (m_1 : a ∈ r') (b : γ), f a ⋯ b = f' a m_1 b) : forIn' r init f = forIn' r' init' f'

theorem Std.Rxc.Iterator.toList_eq_match {α : Type u} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] {it : Iter α} : it.toList = match it.internalState.next with | none => [] | some a => if a ≤ it.internalState.upperBound then a :: { internalState := { next := PRange.succ? a, upperBound := it.internalState.upperBound } }.toList else []

theorem Std.Rxc.Iterator.toArray_eq_match {α : Type u} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] {it : Iter α} : it.toArray = match it.internalState.next with | none => #[] | some a => if a ≤ it.internalState.upperBound then #[a] ++ { internalState := { next := PRange.succ? a, upperBound := it.internalState.upperBound } }.toArray else #[]

theorem Std.Rxo.Iterator.toList_eq_match {α : Type u} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] {it : Iter α} : it.toList = match it.internalState.next with | none => [] | some a => if a < it.internalState.upperBound then a :: { internalState := { next := PRange.succ? a, upperBound := it.internalState.upperBound } }.toList else []

theorem Std.Rxo.Iterator.toArray_eq_match {α : Type u} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] {it : Iter α} : it.toArray = match it.internalState.next with | none => #[] | some a => if a < it.internalState.upperBound then #[a] ++ { internalState := { next := PRange.succ? a, upperBound := it.internalState.upperBound } }.toArray else #[]

theorem Std.Rxc.Iterator.toList_eq_toList_rxoIterator {α : Type u} [LE α] [DecidableLE α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [IsAlwaysFinite α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLT α] [PRange.InfinitelyUpwardEnumerable α] [PRange.LinearlyUpwardEnumerable α] {it : Iter α} : it.toList = { internalState := { next := it.internalState.next, upperBound := PRange.succ it.internalState.upperBound } }.toList

theorem Std.Rxi.Iterator.toList_eq_match {α : Type u} [PRange.UpwardEnumerable α] [IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {it : Iter α} : it.toList = match it.internalState.next with | none => [] | some a => a :: { internalState := { next := PRange.succ? a } }.toList

theorem Std.Rxi.Iterator.toArray_eq_match {α : Type u} [PRange.UpwardEnumerable α] [IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {it : Iter α} : it.toArray = match it.internalState.next with | none => #[] | some a => #[a] ++ { internalState := { next := PRange.succ? a } }.toArray

theorem Std.Rxc.Iterator.pairwise_toList_upwardEnumerableLt {α : Type u} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [IsAlwaysFinite α] (it : Iter α) : List.Pairwise (fun (a b : α) => PRange.UpwardEnumerable.LT a b) it.toList

theorem Std.Rxc.Iterator.nodup_toList {α : Type u} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] {it : Iter α} : it.toList.Nodup

theorem Std.Rxo.Iterator.pairwise_toList_upwardEnumerableLt {α : Type u} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [IsAlwaysFinite α] (it : Iter α) : List.Pairwise (fun (a b : α) => PRange.UpwardEnumerable.LT a b) it.toList

theorem Std.Rxo.Iterator.nodup_toList {α : Type u} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] {it : Iter α} : it.toList.Nodup

theorem Std.Rxi.Iterator.pairwise_toList_upwardEnumerableLt {α : Type u} [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [IsAlwaysFinite α] (it : Iter α) : List.Pairwise (fun (a b : α) => PRange.UpwardEnumerable.LT a b) it.toList

theorem Std.Rxi.Iterator.nodup_toList {α : Type u} [PRange.UpwardEnumerable α] [IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {it : Iter α} : it.toList.Nodup

theorem Std.Rcc.toList_eq_ite_roc {α : Type u} {r : Rcc α} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] : r.toList = if r.lower ≤ r.upper then r.lower :: (r.lower<...=r.upper).toList else []

@[deprecated Std.Rcc.toList_eq_ite_roc (since := "2026-07-21")]

theorem Std.Rcc.toList_eq_if_roc {α : Type u} {r : Rcc α} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] : r.toList = if r.lower ≤ r.upper then r.lower :: (r.lower<...=r.upper).toList else []

theorem Std.Rcc.toList_eq_toList_rco {α : Type u} {r : Rcc α} [LE α] [DecidableLE α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLT α] [Rxc.IsAlwaysFinite α] [Rxo.IsAlwaysFinite α] [PRange.InfinitelyUpwardEnumerable α] [PRange.LinearlyUpwardEnumerable α] : r.toList = (r.lower...PRange.succ r.upper).toList

theorem Std.Rcc.toArray_eq_ite_roc {α : Type u} {r : Rcc α} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] : r.toArray = if r.lower ≤ r.upper then #[r.lower] ++ (r.lower<...=r.upper).toArray else #[]

@[deprecated Std.Rcc.toArray_eq_ite_roc (since := "2026-07-21")]

theorem Std.Rcc.toArray_eq_if_roc {α : Type u} {r : Rcc α} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] : r.toArray = if r.lower ≤ r.upper then #[r.lower] ++ (r.lower<...=r.upper).toArray else #[]

@[simp]

theorem Std.Rcc.toArray_toList {α : Type u} {r : Rcc α} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxc.IsAlwaysFinite α] : r.toList.toArray = r.toArray

@[simp]

theorem Std.Rcc.toList_toArray {α : Type u} {r : Rcc α} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxc.IsAlwaysFinite α] : r.toArray.toList = r.toList

theorem Std.Rcc.toList_eq_nil_iff {α : Type u} {r : Rcc α} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] : r.toList = [] ↔ ¬r.lower ≤ r.upper

theorem Std.Rcc.toArray_eq_empty_iff {α : Type u} {r : Rcc α} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] : r.toArray = #[] ↔ ¬r.lower ≤ r.upper

theorem Std.Rcc.mem_toList_iff_mem {α : Type u} {r : Rcc α} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] {a : α} : a ∈ r.toList ↔ a ∈ r

theorem Std.Rcc.mem_toArray_iff_mem {α : Type u} {r : Rcc α} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] {a : α} : a ∈ r.toArray ↔ a ∈ r

theorem Std.Rcc.pairwise_toList_upwardEnumerableLt {α : Type u} {r : Rcc α} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] : List.Pairwise (fun (a b : α) => PRange.UpwardEnumerable.LT a b) r.toList

theorem Std.Rcc.nodup_toList {α : Type u} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] {a b : α} : (a...=b).toList.Nodup

theorem Std.Rcc.pairwise_toList_ne {α : Type u} {r : Rcc α} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] : List.Pairwise (fun (a b : α) => a ≠ b) r.toList

theorem Std.Rcc.pairwise_toList_lt {α : Type u} {r : Rcc α} [LE α] [DecidableLE α] [LT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLT α] [Rxc.IsAlwaysFinite α] : List.Pairwise (fun (a b : α) => a < b) r.toList

theorem Std.Rcc.pairwise_toList_le {α : Type u} {r : Rcc α} [LE α] [DecidableLE α] [LT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] : List.Pairwise (fun (a b : α) => a ≤ b) r.toList

theorem Std.Rcc.mem_succ_succ_iff {α : Type u} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LinearlyUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.InfinitelyUpwardEnumerable α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {lo hi a : α} : a ∈ PRange.succ lo...=PRange.succ hi ↔ ∃ (a' : α), a = PRange.succ a' ∧ a' ∈ lo...=hi

theorem Std.Rcc.succ_mem_succ_succ_iff {α : Type u} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LinearlyUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.InfinitelyUpwardEnumerable α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {lo hi a : α} : PRange.succ a ∈ PRange.succ lo...=PRange.succ hi ↔ a ∈ lo...=hi

theorem Std.Rcc.toList_succ_succ_eq_map {α : Type u} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LinearlyUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.InfinitelyUpwardEnumerable α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {lo hi : α} : (PRange.succ lo...=PRange.succ hi).toList = List.map PRange.succ (lo...=hi).toList

theorem Std.Rcc.toArray_succ_succ_eq_map {α : Type u} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LinearlyUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.InfinitelyUpwardEnumerable α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {lo hi : α} : (PRange.succ lo...=PRange.succ hi).toArray = Array.map PRange.succ (lo...=hi).toArray

@[deprecated Std.Rcc.toList_succ_succ_eq_map (since := "2025-08-22")]

theorem Std.Rcc.ClosedOpen.toList_succ_succ_eq_map {α : Type u} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LinearlyUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.InfinitelyUpwardEnumerable α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {lo hi : α} : (PRange.succ lo...=PRange.succ hi).toList = List.map PRange.succ (lo...=hi).toList

theorem Std.Rcc.forIn'_eq_forIn'_toList {α : Type u} {r : Rcc α} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} : forIn' r init f = forIn' r.toList init fun (a : α) (ha : a ∈ r.toList) (acc : γ) => f a ⋯ acc

theorem Std.Rcc.forIn'_eq_forIn'_toArray {α : Type u} {r : Rcc α} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} : forIn' r init f = forIn' r.toArray init fun (a : α) (ha : a ∈ r.toArray) (acc : γ) => f a ⋯ acc

theorem Std.Rcc.forIn'_toList_eq_forIn' {α : Type u} {r : Rcc α} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r.toList → γ → m (ForInStep γ)} : forIn' r.toList init f = forIn' r init fun (a : α) (ha : a ∈ r) (acc : γ) => f a ⋯ acc

theorem Std.Rcc.forIn'_toArray_eq_forIn' {α : Type u} {r : Rcc α} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r.toArray → γ → m (ForInStep γ)} : forIn' r.toArray init f = forIn' r init fun (a : α) (ha : a ∈ r) (acc : γ) => f a ⋯ acc

theorem Std.Rcc.mem_of_mem_roc {α : Type u} {r : Rcc α} [LE α] [LT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLT α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {a b : α} (hrb : r.lower ≤ b) (hmem : a ∈ b<...=r.upper) : a ∈ r

theorem Std.Rcc.forIn'_eq_ite {α : Type u} {r : Rcc α} [LE α] [DecidableLE α] [LT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] [LawfulMonad m] {γ : Type u} {init : γ} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} : forIn' r init f = if hu : r.lower ≤ r.upper then have hle := ⋯; do let __do_lift ← f r.lower ⋯ init match __do_lift with | ForInStep.yield c => forIn' (r.lower<...=r.upper) c fun (a : α) (ha : a ∈ r.lower<...=r.upper) (acc : γ) => f a ⋯ acc | ForInStep.done c => pure c else pure init

@[deprecated Std.Rcc.forIn'_eq_ite (since := "2026-07-21")]

theorem Std.Rcc.forIn'_eq_if {α : Type u} {r : Rcc α} [LE α] [DecidableLE α] [LT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] [LawfulMonad m] {γ : Type u} {init : γ} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} : forIn' r init f = if hu : r.lower ≤ r.upper then have hle := ⋯; do let __do_lift ← f r.lower ⋯ init match __do_lift with | ForInStep.yield c => forIn' (r.lower<...=r.upper) c fun (a : α) (ha : a ∈ r.lower<...=r.upper) (acc : γ) => f a ⋯ acc | ForInStep.done c => pure c else pure init

theorem Std.Rcc.isEmpty_iff_forall_not_mem {α : Type u} {r : Rcc α} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [Rxc.HasSize α] [Rxc.LawfulHasSize α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] : r.isEmpty = true ↔ ∀ (a : α), ¬a ∈ r

theorem Std.Rco.toList_eq_ite_roo {α : Type u} {r : Rco α} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] [PRange.LawfulUpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerableLT α] : r.toList = if r.lower < r.upper then r.lower :: (r.lower<...r.upper).toList else []

@[deprecated Std.Rco.toList_eq_ite_roo (since := "2026-07-21")]

theorem Std.Rco.toList_eq_if_roo {α : Type u} {r : Rco α} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] [PRange.LawfulUpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerableLT α] : r.toList = if r.lower < r.upper then r.lower :: (r.lower<...r.upper).toList else []

theorem Std.Rco.toArray_eq_ite_roo {α : Type u} {r : Rco α} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] [PRange.LawfulUpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerableLT α] : r.toArray = if r.lower < r.upper then #[r.lower] ++ (r.lower<...r.upper).toArray else #[]

@[deprecated Std.Rco.toArray_eq_ite_roo (since := "2026-07-21")]

theorem Std.Rco.toArray_eq_if_roo {α : Type u} {r : Rco α} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] [PRange.LawfulUpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerableLT α] : r.toArray = if r.lower < r.upper then #[r.lower] ++ (r.lower<...r.upper).toArray else #[]

theorem Std.Rco.toList_eq_ite_rco {α : Type u} {r : Rco α} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] [PRange.LawfulUpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerableLT α] : r.toList = if r.lower < r.upper then match PRange.succ? r.lower with | none => [r.lower] | some next => r.lower :: (next...r.upper).toList else []

@[deprecated Std.Rco.toList_eq_ite_rco (since := "2026-07-21")]

theorem Std.Rco.toList_eq_if_rco {α : Type u} {r : Rco α} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] [PRange.LawfulUpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerableLT α] : r.toList = if r.lower < r.upper then match PRange.succ? r.lower with | none => [r.lower] | some next => r.lower :: (next...r.upper).toList else []

theorem Std.Rco.toArray_eq_ite_rco {α : Type u} {r : Rco α} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] [PRange.LawfulUpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerableLT α] : r.toArray = if r.lower < r.upper then match PRange.succ? r.lower with | none => #[r.lower] | some next => #[r.lower] ++ (next...r.upper).toArray else #[]

@[deprecated Std.Rco.toArray_eq_ite_rco (since := "2026-07-21")]

theorem Std.Rco.toArray_eq_if_rco {α : Type u} {r : Rco α} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] [PRange.LawfulUpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerableLT α] : r.toArray = if r.lower < r.upper then match PRange.succ? r.lower with | none => #[r.lower] | some next => #[r.lower] ++ (next...r.upper).toArray else #[]

@[simp]

theorem Std.Rco.toArray_toList {α : Type u} {r : Rco α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxo.IsAlwaysFinite α] : r.toList.toArray = r.toArray

@[simp]

theorem Std.Rco.toList_toArray {α : Type u} {r : Rco α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxo.IsAlwaysFinite α] : r.toArray.toList = r.toList

theorem Std.Rco.toList_eq_nil_iff {α : Type u} {r : Rco α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] : r.toList = [] ↔ ¬r.lower < r.upper

theorem Std.Rco.toArray_eq_empty_iff {α : Type u} {r : Rco α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] : r.toArray = #[] ↔ ¬r.lower < r.upper

theorem Std.Rco.mem_toList_iff_mem {α : Type u} {r : Rco α} [LE α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLE α] [Rxo.IsAlwaysFinite α] {a : α} : a ∈ r.toList ↔ a ∈ r

theorem Std.Rco.mem_toArray_iff_mem {α : Type u} {r : Rco α} [LE α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLE α] [Rxo.IsAlwaysFinite α] {a : α} : a ∈ r.toArray ↔ a ∈ r

theorem Std.Rco.pairwise_toList_upwardEnumerableLt {α : Type u} {r : Rco α} [LE α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] : List.Pairwise (fun (a b : α) => PRange.UpwardEnumerable.LT a b) r.toList

theorem Std.Rco.nodup_toList {α : Type u} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] {a b : α} : (a...b).toList.Nodup

theorem Std.Rco.pairwise_toList_ne {α : Type u} {r : Rco α} [LE α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] : List.Pairwise (fun (a b : α) => a ≠ b) r.toList

theorem Std.Rco.pairwise_toList_lt {α : Type u} {r : Rco α} [LE α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] : List.Pairwise (fun (a b : α) => a < b) r.toList

theorem Std.Rco.pairwise_toList_le {α : Type u} {r : Rco α} [LE α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLE α] [Rxo.IsAlwaysFinite α] : List.Pairwise (fun (a b : α) => a ≤ b) r.toList

theorem Std.Rco.mem_succ_succ_iff {α : Type u} [LE α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LinearlyUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLE α] [PRange.InfinitelyUpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {lo hi a : α} : a ∈ PRange.succ lo...PRange.succ hi ↔ ∃ (a' : α), a = PRange.succ a' ∧ a' ∈ lo...hi

theorem Std.Rco.succ_mem_succ_succ_iff {α : Type u} [LE α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LinearlyUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLT α] [PRange.InfinitelyUpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {lo hi a : α} : PRange.succ a ∈ PRange.succ lo...PRange.succ hi ↔ a ∈ lo...hi

theorem Std.Rco.toList_succ_succ_eq_map {α : Type u} [LE α] [DecidableLE α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LinearlyUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLT α] [PRange.InfinitelyUpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {lo hi : α} : (PRange.succ lo...PRange.succ hi).toList = List.map PRange.succ (lo...hi).toList

theorem Std.Rco.toArray_succ_succ_eq_map {α : Type u} [LE α] [DecidableLE α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LinearlyUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLT α] [PRange.InfinitelyUpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {lo hi : α} : (PRange.succ lo...PRange.succ hi).toArray = Array.map PRange.succ (lo...hi).toArray

theorem Std.Rco.forIn'_eq_forIn'_toList {α : Type u} {r : Rco α} [LE α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} : forIn' r init f = forIn' r.toList init fun (a : α) (ha : a ∈ r.toList) (acc : γ) => f a ⋯ acc

theorem Std.Rco.forIn'_eq_forIn'_toArray {α : Type u} {r : Rco α} [LE α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} : forIn' r init f = forIn' r.toArray init fun (a : α) (ha : a ∈ r.toArray) (acc : γ) => f a ⋯ acc

theorem Std.Rco.forIn'_toList_eq_forIn' {α : Type u} {r : Rco α} [LE α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r.toList → γ → m (ForInStep γ)} : forIn' r.toList init f = forIn' r init fun (a : α) (ha : a ∈ r) (acc : γ) => f a ⋯ acc

theorem Std.Rco.forIn'_toArray_eq_forIn' {α : Type u} {r : Rco α} [LE α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r.toArray → γ → m (ForInStep γ)} : forIn' r.toArray init f = forIn' r init fun (a : α) (ha : a ∈ r) (acc : γ) => f a ⋯ acc

theorem Std.Rco.mem_of_mem_roo {α : Type u} {r : Rco α} [LE α] [LT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {a b : α} (hrb : r.lower ≤ b) (hmem : a ∈ b<...r.upper) : a ∈ r

theorem Std.Rco.forIn'_eq_ite {α : Type u} {r : Rco α} [LE α] [DecidableLE α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLE α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] [LawfulMonad m] {γ : Type u} {init : γ} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} : forIn' r init f = if hu : r.lower < r.upper then have hle := ⋯; do let __do_lift ← f r.lower ⋯ init match __do_lift with | ForInStep.yield c => forIn' (r.lower<...r.upper) c fun (a : α) (ha : a ∈ r.lower<...r.upper) (acc : γ) => f a ⋯ acc | ForInStep.done c => pure c else pure init

@[deprecated Std.Rco.forIn'_eq_ite (since := "2026-07-21")]

theorem Std.Rco.forIn'_eq_if {α : Type u} {r : Rco α} [LE α] [DecidableLE α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLE α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] [LawfulMonad m] {γ : Type u} {init : γ} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} : forIn' r init f = if hu : r.lower < r.upper then have hle := ⋯; do let __do_lift ← f r.lower ⋯ init match __do_lift with | ForInStep.yield c => forIn' (r.lower<...r.upper) c fun (a : α) (ha : a ∈ r.lower<...r.upper) (acc : γ) => f a ⋯ acc | ForInStep.done c => pure c else pure init

theorem Std.Rco.isEmpty_iff_forall_not_mem {α : Type u} {r : Rco α} [LE α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [Rxo.HasSize α] [Rxo.LawfulHasSize α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] : r.isEmpty = true ↔ ∀ (a : α), ¬a ∈ r

theorem Std.Rci.toList_eq_toList_roi {α : Type u} {r : Rci α} [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] : r.toList = r.lower :: r.lower<...*.toList

theorem Std.Rci.toArray_eq_toArray_roi {α : Type u} {r : Rci α} [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] : r.toArray = #[r.lower] ++ r.lower<...*.toArray

@[simp]

theorem Std.Rci.toArray_toList {α : Type u} {r : Rci α} [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] : r.toList.toArray = r.toArray

@[simp]

theorem Std.Rci.toList_toArray {α : Type u} {r : Rci α} [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] : r.toArray.toList = r.toList

theorem Std.Rci.toList_ne_nil {α : Type u} {r : Rci α} [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] : r.toList ≠ []

theorem Std.Rci.toArray_ne_nil {α : Type u} {r : Rci α} [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] : r.toArray ≠ #[]

theorem Std.Rci.mem_toList_iff_mem {α : Type u} {r : Rci α} [LE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxi.IsAlwaysFinite α] {a : α} : a ∈ r.toList ↔ a ∈ r

theorem Std.Rci.mem_toArray_iff_mem {α : Type u} {r : Rci α} [LE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxi.IsAlwaysFinite α] {a : α} : a ∈ r.toArray ↔ a ∈ r

theorem Std.Rci.pairwise_toList_upwardEnumerableLt {α : Type u} {r : Rci α} [LE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] : List.Pairwise (fun (a b : α) => PRange.UpwardEnumerable.LT a b) r.toList

theorem Std.Rci.nodup_toList {α : Type u} [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {a : α} : a...*.toList.Nodup

theorem Std.Rci.pairwise_toList_ne {α : Type u} {r : Rci α} [LE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] : List.Pairwise (fun (a b : α) => a ≠ b) r.toList

theorem Std.Rci.pairwise_toList_lt {α : Type u} {r : Rci α} [LE α] [LT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxi.IsAlwaysFinite α] : List.Pairwise (fun (a b : α) => a < b) r.toList

theorem Std.Rci.pairwise_toList_le {α : Type u} {r : Rci α} [LE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxi.IsAlwaysFinite α] : List.Pairwise (fun (a b : α) => a ≤ b) r.toList

theorem Std.Rci.mem_succ_iff {α : Type u} [LE α] [PRange.UpwardEnumerable α] [PRange.LinearlyUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.InfinitelyUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {lo a : α} : a ∈ PRange.succ lo...* ↔ ∃ (a' : α), a = PRange.succ a' ∧ a' ∈ lo...*

theorem Std.Rci.succ_mem_succ_succ_iff {α : Type u} [LE α] [PRange.UpwardEnumerable α] [PRange.LinearlyUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.InfinitelyUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {lo a : α} : PRange.succ a ∈ PRange.succ lo...* ↔ a ∈ lo...*

theorem Std.Rci.toList_succ_succ_eq_map {α : Type u} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LinearlyUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.InfinitelyUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {lo : α} : PRange.succ lo...*.toList = List.map PRange.succ lo...*.toList

theorem Std.Rci.toArray_succ_succ_eq_map {α : Type u} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LinearlyUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.InfinitelyUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {lo : α} : PRange.succ lo...*.toArray = Array.map PRange.succ lo...*.toArray

theorem Std.Rci.forIn'_eq_forIn'_toList {α : Type u} {r : Rci α} [LE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} : forIn' r init f = forIn' r.toList init fun (a : α) (ha : a ∈ r.toList) (acc : γ) => f a ⋯ acc

theorem Std.Rci.forIn'_eq_forIn'_toArray {α : Type u} {r : Rci α} [LE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} : forIn' r init f = forIn' r.toArray init fun (a : α) (ha : a ∈ r.toArray) (acc : γ) => f a ⋯ acc

theorem Std.Rci.forIn'_toList_eq_forIn' {α : Type u} {r : Rci α} [LE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r.toList → γ → m (ForInStep γ)} : forIn' r.toList init f = forIn' r init fun (a : α) (ha : a ∈ r) (acc : γ) => f a ⋯ acc

theorem Std.Rci.forIn'_toArray_eq_forIn' {α : Type u} {r : Rci α} [LE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r.toArray → γ → m (ForInStep γ)} : forIn' r.toArray init f = forIn' r init fun (a : α) (ha : a ∈ r) (acc : γ) => f a ⋯ acc

theorem Std.Rci.mem_of_mem_roi {α : Type u} {r : Rci α} [LE α] [LT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLT α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {a b : α} (hrb : r.lower ≤ b) (hmem : a ∈ b<...*) : a ∈ r

theorem Std.Rci.forIn'_eq_match {α : Type u} {r : Rci α} [LE α] [DecidableLE α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLE α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] [LawfulMonad m] {γ : Type u} {init : γ} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} : forIn' r init f = have hle := ⋯; do let __do_lift ← f r.lower hle init match __do_lift with | ForInStep.yield c => forIn' (r.lower<...*) c fun (a : α) (ha : a ∈ r.lower<...*) (acc : γ) => f a ⋯ acc | ForInStep.done c => pure c

theorem Std.Rci.isEmpty_iff_forall_not_mem {α : Type u} {r : Rci α} [LE α] [PRange.UpwardEnumerable α] [Rxi.HasSize α] [Rxi.LawfulHasSize α] [PRange.LawfulUpwardEnumerableLE α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] : r.isEmpty = true ↔ ∀ (a : α), ¬a ∈ r

theorem Std.Roc.toList_eq_match {α : Type u} {r : Roc α} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] : r.toList = match PRange.succ? r.lower with | none => [] | some next => if next ≤ r.upper then next :: (next<...=r.upper).toList else []

theorem Std.Roc.toArray_eq_match {α : Type u} {r : Roc α} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] : r.toArray = match PRange.succ? r.lower with | none => #[] | some next => if next ≤ r.upper then #[next] ++ (next<...=r.upper).toArray else #[]

theorem Std.Roc.toList_eq_match_rcc {α : Type u} {r : Roc α} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] : r.toList = match PRange.succ? r.lower with | none => [] | some next => (next...=r.upper).toList

theorem Std.Roc.toArray_eq_match_rcc {α : Type u} {r : Roc α} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] : r.toArray = match PRange.succ? r.lower with | none => #[] | some next => (next...=r.upper).toArray

theorem Std.Roc.toList_eq_toList_roo {α : Type u} {r : Roc α} [LE α] [DecidableLE α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLT α] [Rxc.IsAlwaysFinite α] [Rxo.IsAlwaysFinite α] [PRange.InfinitelyUpwardEnumerable α] [PRange.LinearlyUpwardEnumerable α] : r.toList = (r.lower<...PRange.succ r.upper).toList

@[simp]

theorem Std.Roc.toArray_toList {α : Type u} {r : Roc α} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxc.IsAlwaysFinite α] : r.toList.toArray = r.toArray

@[simp]

theorem Std.Roc.toList_toArray {α : Type u} {r : Roc α} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxc.IsAlwaysFinite α] : r.toArray.toList = r.toList

theorem Std.Roc.toList_eq_nil_iff {α : Type u} {r : Roc α} [LE α] [DecidableLE α] [LT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLT α] [Rxc.IsAlwaysFinite α] : r.toList = [] ↔ ¬r.lower < r.upper

theorem Std.Roc.toArray_eq_empty_iff {α : Type u} {r : Roc α} [LE α] [DecidableLE α] [LT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLT α] [Rxc.IsAlwaysFinite α] : r.toArray = #[] ↔ ¬r.lower < r.upper

theorem Std.Roc.mem_toList_iff_mem {α : Type u} {r : Roc α} [LE α] [DecidableLE α] [LT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLT α] [Rxc.IsAlwaysFinite α] {a : α} : a ∈ r.toList ↔ a ∈ r

theorem Std.Roc.mem_toArray_iff_mem {α : Type u} {r : Roc α} [LE α] [DecidableLE α] [LT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLT α] [Rxc.IsAlwaysFinite α] {a : α} : a ∈ r.toArray ↔ a ∈ r

theorem Std.Roc.pairwise_toList_upwardEnumerableLt {α : Type u} {r : Roc α} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] : List.Pairwise (fun (a b : α) => PRange.UpwardEnumerable.LT a b) r.toList

theorem Std.Roc.nodup_toList {α : Type u} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] {a b : α} : (a<...=b).toList.Nodup

theorem Std.Roc.pairwise_toList_ne {α : Type u} {r : Roc α} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] : List.Pairwise (fun (a b : α) => a ≠ b) r.toList

theorem Std.Roc.pairwise_toList_lt {α : Type u} {r : Roc α} [LE α] [DecidableLE α] [LT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLT α] [Rxc.IsAlwaysFinite α] : List.Pairwise (fun (a b : α) => a < b) r.toList

theorem Std.Roc.pairwise_toList_le {α : Type u} {r : Roc α} [LE α] [DecidableLE α] [LT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] : List.Pairwise (fun (a b : α) => a ≤ b) r.toList

theorem Std.Roc.mem_succ_succ_iff {α : Type u} [LE α] [DecidableLE α] [LT α] [PRange.UpwardEnumerable α] [PRange.LinearlyUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLT α] [PRange.InfinitelyUpwardEnumerable α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {lo hi a : α} : a ∈ PRange.succ lo<...=PRange.succ hi ↔ ∃ (a' : α), a = PRange.succ a' ∧ a' ∈ lo<...=hi

theorem Std.Roc.succ_mem_succ_succ_iff {α : Type u} [LE α] [DecidableLE α] [LT α] [PRange.UpwardEnumerable α] [PRange.LinearlyUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLT α] [PRange.InfinitelyUpwardEnumerable α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {lo hi a : α} : PRange.succ a ∈ PRange.succ lo<...=PRange.succ hi ↔ a ∈ lo<...=hi

theorem Std.Roc.toList_succ_succ_eq_map {α : Type u} [LE α] [DecidableLE α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LinearlyUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLT α] [PRange.InfinitelyUpwardEnumerable α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {lo hi : α} : (PRange.succ lo<...=PRange.succ hi).toList = List.map PRange.succ (lo<...=hi).toList

theorem Std.Roc.toArray_succ_succ_eq_map {α : Type u} [LE α] [DecidableLE α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LinearlyUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLT α] [PRange.InfinitelyUpwardEnumerable α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {lo hi : α} : (PRange.succ lo<...=PRange.succ hi).toArray = Array.map PRange.succ (lo<...=hi).toArray

theorem Std.Roc.forIn'_eq_forIn'_toList {α : Type u} {r : Roc α} [LE α] [DecidableLE α] [LT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLT α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} : forIn' r init f = forIn' r.toList init fun (a : α) (ha : a ∈ r.toList) (acc : γ) => f a ⋯ acc

theorem Std.Roc.forIn'_eq_forIn'_toArray {α : Type u} {r : Roc α} [LE α] [DecidableLE α] [LT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLT α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} : forIn' r init f = forIn' r.toArray init fun (a : α) (ha : a ∈ r.toArray) (acc : γ) => f a ⋯ acc

theorem Std.Roc.forIn'_toList_eq_forIn' {α : Type u} {r : Roc α} [LE α] [DecidableLE α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLT α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r.toList → γ → m (ForInStep γ)} : forIn' r.toList init f = forIn' r init fun (a : α) (ha : a ∈ r) (acc : γ) => f a ⋯ acc

theorem Std.Roc.forIn'_toArray_eq_forIn' {α : Type u} {r : Roc α} [LE α] [DecidableLE α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLT α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r.toArray → γ → m (ForInStep γ)} : forIn' r.toArray init f = forIn' r init fun (a : α) (ha : a ∈ r) (acc : γ) => f a ⋯ acc

theorem Std.Roc.mem_of_mem_of_le {α : Type u} [LE α] [LT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLT α] {lo lo' hi a : α} (h : lo ≤ lo') (hmem : a ∈ lo'<...=hi) : a ∈ lo<...=hi

theorem Std.Roc.forIn'_eq_match {α : Type u} {r : Roc α} [LE α] [DecidableLE α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] [LawfulMonad m] {γ : Type u} {init : γ} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} : forIn' r init f = match hs : PRange.succ? r.lower with | none => pure init | some next => if hu : next ≤ r.upper then have hlt := ⋯; do let __do_lift ← f next ⋯ init match __do_lift with | ForInStep.yield c => forIn' (next<...=r.upper) c fun (a : α) (ha : a ∈ next<...=r.upper) (acc : γ) => f a ⋯ acc | ForInStep.done c => pure c else pure init

theorem Std.Roo.toList_eq_match {α : Type u} {r : Roo α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] : r.toList = match PRange.succ? r.lower with | none => [] | some next => if next < r.upper then next :: (next<...r.upper).toList else []

theorem Std.Roo.toArray_eq_match {α : Type u} {r : Roo α} [LE α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] : r.toArray = match PRange.succ? r.lower with | none => #[] | some next => if next < r.upper then #[next] ++ (next<...r.upper).toArray else #[]

theorem Std.Roo.toList_eq_match_rco {α : Type u} {r : Roo α} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] : r.toList = match PRange.succ? r.lower with | none => [] | some next => (next...r.upper).toList

theorem Std.Roo.toArray_eq_match_rco {α : Type u} {r : Roo α} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] : r.toArray = match PRange.succ? r.lower with | none => #[] | some next => (next...r.upper).toArray

@[simp]

theorem Std.Roo.toArray_toList {α : Type u} {r : Roo α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxo.IsAlwaysFinite α] : r.toList.toArray = r.toArray

@[simp]

theorem Std.Roo.toList_toArray {α : Type u} {r : Roo α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxo.IsAlwaysFinite α] : r.toArray.toList = r.toList

theorem Std.Roo.toList_eq_nil_iff {α : Type u} {r : Roo α} [LE α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] : r.toList = [] ↔ ∀ (a : α), PRange.succ? r.lower = some a → ¬a < r.upper

theorem Std.Roo.toArray_eq_empty_iff {α : Type u} {r : Roo α} [LE α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] : r.toArray = #[] ↔ ∀ (a : α), PRange.succ? r.lower = some a → ¬a < r.upper

theorem Std.Roo.mem_toList_iff_mem {α : Type u} {r : Roo α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] {a : α} : a ∈ r.toList ↔ a ∈ r

theorem Std.Roo.mem_toArray_iff_mem {α : Type u} {r : Roo α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] {a : α} : a ∈ r.toArray ↔ a ∈ r

theorem Std.Roo.pairwise_toList_upwardEnumerableLt {α : Type u} {r : Roo α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] : List.Pairwise (fun (a b : α) => PRange.UpwardEnumerable.LT a b) r.toList

theorem Std.Roo.nodup_toList {α : Type u} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] {a b : α} : (a<...b).toList.Nodup

theorem Std.Roo.pairwise_toList_ne {α : Type u} {r : Roo α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] : List.Pairwise (fun (a b : α) => a ≠ b) r.toList

theorem Std.Roo.pairwise_toList_lt {α : Type u} {r : Roo α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] : List.Pairwise (fun (a b : α) => a < b) r.toList

theorem Std.Roo.pairwise_toList_le {α : Type u} {r : Roo α} [LE α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLE α] [Rxo.IsAlwaysFinite α] : List.Pairwise (fun (a b : α) => a ≤ b) r.toList

theorem Std.Roo.mem_succ_succ_iff {α : Type u} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LinearlyUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.InfinitelyUpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {lo hi a : α} : a ∈ PRange.succ lo<...PRange.succ hi ↔ ∃ (a' : α), a = PRange.succ a' ∧ a' ∈ lo<...hi

theorem Std.Roo.succ_mem_succ_succ_iff {α : Type u} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LinearlyUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.InfinitelyUpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {lo hi a : α} : PRange.succ a ∈ PRange.succ lo<...PRange.succ hi ↔ a ∈ lo<...hi

theorem Std.Roo.toList_succ_succ_eq_map {α : Type u} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LinearlyUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.InfinitelyUpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {lo hi : α} : (PRange.succ lo<...PRange.succ hi).toList = List.map PRange.succ (lo<...hi).toList

theorem Std.Roo.toArray_succ_succ_eq_map {α : Type u} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LinearlyUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.InfinitelyUpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {lo hi : α} : (PRange.succ lo<...PRange.succ hi).toArray = Array.map PRange.succ (lo<...hi).toArray

theorem Std.Roo.forIn'_eq_forIn'_toList {α : Type u} {r : Roo α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} : forIn' r init f = forIn' r.toList init fun (a : α) (ha : a ∈ r.toList) (acc : γ) => f a ⋯ acc

theorem Std.Roo.forIn'_eq_forIn'_toArray {α : Type u} {r : Roo α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} : forIn' r init f = forIn' r.toArray init fun (a : α) (ha : a ∈ r.toArray) (acc : γ) => f a ⋯ acc

theorem Std.Roo.forIn'_toList_eq_forIn' {α : Type u} {r : Roo α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r.toList → γ → m (ForInStep γ)} : forIn' r.toList init f = forIn' r init fun (a : α) (ha : a ∈ r) (acc : γ) => f a ⋯ acc

theorem Std.Roo.forIn'_toArray_eq_forIn' {α : Type u} {r : Roo α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r.toArray → γ → m (ForInStep γ)} : forIn' r.toArray init f = forIn' r init fun (a : α) (ha : a ∈ r) (acc : γ) => f a ⋯ acc

theorem Std.Roo.mem_of_mem_of_le {α : Type u} {r : Roo α} [LT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {a b : α} (hrb : PRange.UpwardEnumerable.LE r.lower b) (hmem : a ∈ b<...r.upper) : a ∈ r

theorem Std.Roo.forIn'_eq_match {α : Type u} {r : Roo α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] [LawfulMonad m] {γ : Type u} {init : γ} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} : forIn' r init f = match hs : PRange.succ? r.lower with | none => pure init | some next => if hu : next < r.upper then have hlt := ⋯; have hle := ⋯; do let __do_lift ← f next ⋯ init match __do_lift with | ForInStep.yield c => forIn' (next<...r.upper) c fun (a : α) (ha : a ∈ next<...r.upper) (acc : γ) => f a ⋯ acc | ForInStep.done c => pure c else pure init

theorem Std.Roo.isEmpty_iff_forall_not_mem {α : Type u} {r : Roo α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [Rxo.HasSize α] [Rxo.LawfulHasSize α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] : r.isEmpty = true ↔ ∀ (a : α), ¬a ∈ r

@[simp]

theorem Std.Roi.toArray_toList {α : Type u} {r : Roi α} [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] : r.toList.toArray = r.toArray

@[simp]

theorem Std.Roi.toList_toArray {α : Type u} {r : Roi α} [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] : r.toArray.toList = r.toList

theorem Std.Roi.toList_eq_match {α : Type u} {r : Roi α} [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] : r.toList = match PRange.succ? r.lower with | none => [] | some next => next :: next<...*.toList

theorem Std.Roi.toArray_eq_match {α : Type u} {r : Roi α} [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] : r.toArray = match PRange.succ? r.lower with | none => #[] | some next => #[next] ++ next<...*.toArray

theorem Std.Roi.toArray_eq_match_rci {α : Type u} {r : Roi α} [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] : r.toArray = match PRange.succ? r.lower with | none => #[] | some next => next...*.toArray

theorem Std.Roi.toList_eq_match_rci {α : Type u} {r : Roi α} [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] : r.toList = match PRange.succ? r.lower with | none => [] | some next => next...*.toList

theorem Std.Roi.toList_eq_nil_iff {α : Type u} {r : Roi α} [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] : r.toList = [] ↔ (PRange.succ? r.lower).isNone = true

theorem Std.Roi.toArray_eq_empty_iff {α : Type u} {r : Roi α} [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] : r.toArray = #[] ↔ (PRange.succ? r.lower).isNone = true

theorem Std.Roi.mem_toList_iff_mem {α : Type u} {r : Roi α} [LT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerableLT α] {a : α} : a ∈ r.toList ↔ a ∈ r

theorem Std.Roi.mem_toArray_iff_mem {α : Type u} {r : Roi α} [LT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerableLT α] {a : α} : a ∈ r.toArray ↔ a ∈ r

theorem Std.Roi.pairwise_toList_upwardEnumerableLt {α : Type u} {r : Roi α} [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] : List.Pairwise (fun (a b : α) => PRange.UpwardEnumerable.LT a b) r.toList

theorem Std.Roi.nodup_toList {α : Type u} [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {a : α} : a<...*.toList.Nodup

theorem Std.Roi.pairwise_toList_ne {α : Type u} {r : Roi α} [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] : List.Pairwise (fun (a b : α) => a ≠ b) r.toList

theorem Std.Roi.pairwise_toList_lt {α : Type u} {r : Roi α} [LT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxi.IsAlwaysFinite α] : List.Pairwise (fun (a b : α) => a < b) r.toList

theorem Std.Roi.pairwise_toList_le {α : Type u} {r : Roi α} [LE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxi.IsAlwaysFinite α] : List.Pairwise (fun (a b : α) => a ≤ b) r.toList

theorem Std.Roi.mem_succ_iff {α : Type u} [LT α] [PRange.UpwardEnumerable α] [PRange.LinearlyUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.InfinitelyUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {lo a : α} : a ∈ PRange.succ lo<...* ↔ ∃ (a' : α), a = PRange.succ a' ∧ a' ∈ lo<...*

theorem Std.Roi.succ_mem_succ_succ_iff {α : Type u} [LT α] [PRange.UpwardEnumerable α] [PRange.LinearlyUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.InfinitelyUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {lo a : α} : PRange.succ a ∈ PRange.succ lo<...* ↔ a ∈ lo<...*

theorem Std.Roi.toList_succ_succ_eq_map {α : Type u} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LinearlyUpwardEnumerable α] [PRange.InfinitelyUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] {lo : α} : PRange.succ lo<...*.toList = List.map PRange.succ lo<...*.toList

theorem Std.Roi.toArray_succ_succ_eq_map {α : Type u} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LinearlyUpwardEnumerable α] [PRange.InfinitelyUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] {lo : α} : PRange.succ lo<...*.toArray = Array.map PRange.succ lo<...*.toArray

theorem Std.Roi.forIn'_eq_forIn'_toList {α : Type u} {r : Roi α} [LT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} : forIn' r init f = forIn' r.toList init fun (a : α) (ha : a ∈ r.toList) (acc : γ) => f a ⋯ acc

theorem Std.Roi.forIn'_eq_forIn'_toArray {α : Type u} {r : Roi α} [LT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} : forIn' r init f = forIn' r.toArray init fun (a : α) (ha : a ∈ r.toArray) (acc : γ) => f a ⋯ acc

theorem Std.Roi.forIn'_toList_eq_forIn' {α : Type u} {r : Roi α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r.toList → γ → m (ForInStep γ)} : forIn' r.toList init f = forIn' r init fun (a : α) (ha : a ∈ r) (acc : γ) => f a ⋯ acc

theorem Std.Roi.forIn'_toArray_eq_forIn' {α : Type u} {r : Roi α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r.toArray → γ → m (ForInStep γ)} : forIn' r.toArray init f = forIn' r init fun (a : α) (ha : a ∈ r) (acc : γ) => f a ⋯ acc

theorem Std.Roi.mem_of_mem_of_le {α : Type u} {r : Roi α} [LT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {a b : α} (hrb : PRange.UpwardEnumerable.LE r.lower b) (hmem : a ∈ b<...*) : a ∈ r

theorem Std.Roi.forIn'_eq_match {α : Type u} {r : Roi α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] [LawfulMonad m] {γ : Type u} {init : γ} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} : forIn' r init f = match hs : PRange.succ? r.lower with | none => pure init | some next => have hlt := ⋯; have hle := ⋯; do let __do_lift ← f next hlt init match __do_lift with | ForInStep.yield c => forIn' (next<...*) c fun (a : α) (ha : a ∈ next<...*) (acc : γ) => f a ⋯ acc | ForInStep.done c => pure c

theorem Std.Roi.isEmpty_iff_forall_not_mem {α : Type u} {r : Roi α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [Rxi.HasSize α] [Rxi.LawfulHasSize α] [PRange.LawfulUpwardEnumerableLT α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] : r.isEmpty = true ↔ ∀ (a : α), ¬a ∈ r

@[simp]

theorem Std.Ric.toArray_toList {α : Type u} {r : Ric α} [PRange.Least? α] [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxc.IsAlwaysFinite α] : r.toList.toArray = r.toArray

@[simp]

theorem Std.Ric.toList_toArray {α : Type u} {r : Ric α} [PRange.Least? α] [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxc.IsAlwaysFinite α] : r.toArray.toList = r.toList

theorem Std.Ric.toList_eq_match_rcc {α : Type u} {r : Ric α} [LE α] [DecidableLE α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] : r.toList = match PRange.least? with | none => [] | some least => (least...=r.upper).toList

theorem Std.Ric.toList_eq_toList_rcc {α : Type u} {r : Ric α} [LE α] [DecidableLE α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] : r.toList = (PRange.UpwardEnumerable.least...=r.upper).toList

theorem Std.Ric.toArray_eq_toArray_rcc {α : Type u} {r : Ric α} [LE α] [DecidableLE α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] : r.toArray = (PRange.UpwardEnumerable.least...=r.upper).toArray

theorem Std.Ric.toList_eq_ite_roc {α : Type u} {r : Ric α} [LE α] [DecidableLE α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] : r.toList = have init := PRange.UpwardEnumerable.least; if init ≤ r.upper then init :: (init<...=r.upper).toList else []

@[deprecated Std.Ric.toList_eq_ite_roc (since := "2026-07-21")]

theorem Std.Ric.toList_eq_if_roc {α : Type u} {r : Ric α} [LE α] [DecidableLE α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] : r.toList = have init := PRange.UpwardEnumerable.least; if init ≤ r.upper then init :: (init<...=r.upper).toList else []

theorem Std.Ric.toArray_eq_ite_roc {α : Type u} {r : Ric α} [LE α] [DecidableLE α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] : r.toArray = have init := PRange.UpwardEnumerable.least; if init ≤ r.upper then #[init] ++ (init<...=r.upper).toArray else #[]

@[deprecated Std.Ric.toArray_eq_ite_roc (since := "2026-07-21")]

theorem Std.Ric.toArray_eq_if_roc {α : Type u} {r : Ric α} [LE α] [DecidableLE α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] : r.toArray = have init := PRange.UpwardEnumerable.least; if init ≤ r.upper then #[init] ++ (init<...=r.upper).toArray else #[]

theorem Std.Ric.toList_ne_nil {α : Type u} {r : Ric α} [LE α] [DecidableLE α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] : r.toList ≠ []

theorem Std.Ric.toArray_ne_empty {α : Type u} {r : Ric α} [LE α] [DecidableLE α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] : r.toArray ≠ #[]

theorem Std.Ric.mem_iff_mem_rcc {α : Type u} {r : Ric α} [LE α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] {a : α} : a ∈ r ↔ a ∈ PRange.UpwardEnumerable.least...=r.upper

theorem Std.Ric.mem_toList_iff_mem {α : Type u} {r : Ric α} [LE α] [DecidableLE α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] {a : α} : a ∈ r.toList ↔ a ∈ r

theorem Std.Ric.mem_toArray_iff_mem {α : Type u} {r : Ric α} [LE α] [DecidableLE α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] {a : α} : a ∈ r.toArray ↔ a ∈ r

theorem Std.Ric.pairwise_toList_upwardEnumerableLt {α : Type u} {r : Ric α} [LE α] [DecidableLE α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] : List.Pairwise (fun (a b : α) => PRange.UpwardEnumerable.LT a b) r.toList

theorem Std.Ric.nodup_toList {α : Type u} [LE α] [DecidableLE α] [PRange.Least? α] [PRange.UpwardEnumerable α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] {a : α} : (*...=a).toList.Nodup

theorem Std.Ric.pairwise_toList_ne {α : Type u} {r : Ric α} [LE α] [DecidableLE α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] : List.Pairwise (fun (a b : α) => a ≠ b) r.toList

theorem Std.Ric.pairwise_toList_lt {α : Type u} {r : Ric α} [LE α] [DecidableLE α] [LT α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLT α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerableLeast? α] : List.Pairwise (fun (a b : α) => a < b) r.toList

theorem Std.Ric.pairwise_toList_le {α : Type u} {r : Ric α} [LE α] [DecidableLE α] [LT α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] : List.Pairwise (fun (a b : α) => a ≤ b) r.toList

theorem Std.Ric.mem_succ_iff {α : Type u} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LinearlyUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.InfinitelyUpwardEnumerable α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {hi a : α} : a ∈ *...=PRange.succ hi ↔ a ∈ *...=hi ∨ a = PRange.succ hi

theorem Std.Ric.succ_mem_succ_iff {α : Type u} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LinearlyUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.InfinitelyUpwardEnumerable α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {hi a : α} : PRange.succ a ∈ *...=PRange.succ hi ↔ a ∈ *...=hi

theorem Std.Ric.toList_succ_eq_map {α : Type u} [LE α] [DecidableLE α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LinearlyUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.InfinitelyUpwardEnumerable α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLeast? α] {hi : α} : (*...=PRange.succ hi).toList = PRange.UpwardEnumerable.least :: List.map PRange.succ (*...=hi).toList

theorem Std.Ric.toArray_succ_eq_map {α : Type u} {r : Ric α} [LE α] [DecidableLE α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LinearlyUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.InfinitelyUpwardEnumerable α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLeast? α] {hi : α} : (*...=PRange.succ hi).toArray = #[PRange.UpwardEnumerable.least] ++ Array.map PRange.succ (*...=hi).toArray

theorem Std.Ric.forIn'_eq_forIn'_toList {α : Type u} {r : Ric α} [LE α] [DecidableLE α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} : forIn' r init f = forIn' r.toList init fun (a : α) (ha : a ∈ r.toList) (acc : γ) => f a ⋯ acc

theorem Std.Ric.forIn'_eq_forIn'_toArray {α : Type u} {r : Ric α} [LE α] [DecidableLE α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} : forIn' r init f = forIn' r.toArray init fun (a : α) (ha : a ∈ r.toArray) (acc : γ) => f a ⋯ acc

theorem Std.Ric.forIn'_toList_eq_forIn' {α : Type u} {r : Ric α} [LE α] [DecidableLE α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r.toList → γ → m (ForInStep γ)} : forIn' r.toList init f = forIn' r init fun (a : α) (ha : a ∈ r) (acc : γ) => f a ⋯ acc

theorem Std.Ric.forIn'_toArray_eq_forIn' {α : Type u} {r : Ric α} [LE α] [DecidableLE α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r.toArray → γ → m (ForInStep γ)} : forIn' r.toArray init f = forIn' r init fun (a : α) (ha : a ∈ r) (acc : γ) => f a ⋯ acc

theorem Std.Ric.mem_of_mem_rcc {α : Type u} [LE α] {lo hi a : α} (hmem : a ∈ lo...=hi) : a ∈ *...=hi

theorem Std.Ric.mem_of_mem_roc {α : Type u} [LE α] [LT α] {lo hi a : α} (hmem : a ∈ lo<...=hi) : a ∈ *...=hi

theorem Std.Ric.forIn'_eq_forIn'_rcc {α : Type u} {r : Ric α} [LE α] [DecidableLE α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] [LawfulMonad m] {γ : Type u} {init : γ} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} : forIn' r init f = forIn' (PRange.UpwardEnumerable.least...=r.upper) init fun (a : α) (ha : a ∈ PRange.UpwardEnumerable.least...=r.upper) (acc : γ) => f a ⋯ acc

theorem Std.Ric.forIn'_eq_ite_roc {α : Type u} {r : Ric α} [LE α] [DecidableLE α] [LT α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] [LawfulMonad m] {γ : Type u} {init : γ} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} : forIn' r init f = if hu : PRange.UpwardEnumerable.least ≤ r.upper then do let __do_lift ← f PRange.UpwardEnumerable.least hu init match __do_lift with | ForInStep.yield c => forIn' (PRange.UpwardEnumerable.least<...=r.upper) c fun (a : α) (ha : a ∈ PRange.UpwardEnumerable.least<...=r.upper) (acc : γ) => f a ⋯ acc | ForInStep.done c => pure c else pure init

@[deprecated Std.Ric.forIn'_eq_ite_roc (since := "2026-07-21")]

theorem Std.Ric.forIn'_eq_if_roc {α : Type u} {r : Ric α} [LE α] [DecidableLE α] [LT α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] [LawfulMonad m] {γ : Type u} {init : γ} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} : forIn' r init f = if hu : PRange.UpwardEnumerable.least ≤ r.upper then do let __do_lift ← f PRange.UpwardEnumerable.least hu init match __do_lift with | ForInStep.yield c => forIn' (PRange.UpwardEnumerable.least<...=r.upper) c fun (a : α) (ha : a ∈ PRange.UpwardEnumerable.least<...=r.upper) (acc : γ) => f a ⋯ acc | ForInStep.done c => pure c else pure init

theorem Std.Ric.isEmpty_iff_forall_not_mem {α : Type u} {r : Ric α} [LE α] [PRange.UpwardEnumerable α] [Rxc.HasSize α] [Rxc.LawfulHasSize α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] : r.isEmpty = true ↔ ∀ (a : α), ¬a ∈ r

@[simp]

theorem Std.Rio.toArray_toList {α : Type u} {r : Rio α} [PRange.Least? α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxo.IsAlwaysFinite α] : r.toList.toArray = r.toArray

@[simp]

theorem Std.Rio.toList_toArray {α : Type u} {r : Rio α} [PRange.Least? α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxo.IsAlwaysFinite α] : r.toArray.toList = r.toList

theorem Std.Rio.toList_eq_match_rco {α : Type u} {r : Rio α} [LT α] [DecidableLT α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] : r.toList = match PRange.least? with | none => [] | some least => (least...r.upper).toList

theorem Std.Rio.toArray_eq_match_rco {α : Type u} {r : Rio α} [LT α] [DecidableLT α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] : r.toArray = match PRange.least? with | none => #[] | some least => (least...r.upper).toArray

theorem Std.Rio.toList_eq_toList_rco {α : Type u} {r : Rio α} [LT α] [DecidableLT α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] : r.toList = (PRange.UpwardEnumerable.least...r.upper).toList

theorem Std.Rio.toArray_eq_toArray_rco {α : Type u} {r : Rio α} [LT α] [DecidableLT α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] : r.toArray = (PRange.UpwardEnumerable.least...r.upper).toArray

theorem Std.Rio.toList_eq_ite_roo {α : Type u} {r : Rio α} [LT α] [DecidableLT α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] : r.toList = have init := PRange.UpwardEnumerable.least; if init < r.upper then init :: (init<...r.upper).toList else []

@[deprecated Std.Rio.toList_eq_ite_roo (since := "2026-07-21")]

theorem Std.Rio.toList_eq_if_roo {α : Type u} {r : Rio α} [LT α] [DecidableLT α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] : r.toList = have init := PRange.UpwardEnumerable.least; if init < r.upper then init :: (init<...r.upper).toList else []

theorem Std.Rio.toArray_eq_ite_roo {α : Type u} {r : Rio α} [LT α] [DecidableLT α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] : r.toArray = have init := PRange.UpwardEnumerable.least; if init < r.upper then #[init] ++ (init<...r.upper).toArray else #[]

@[deprecated Std.Rio.toArray_eq_ite_roo (since := "2026-07-21")]

theorem Std.Rio.toArray_eq_if_roo {α : Type u} {r : Rio α} [LT α] [DecidableLT α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] : r.toArray = have init := PRange.UpwardEnumerable.least; if init < r.upper then #[init] ++ (init<...r.upper).toArray else #[]

theorem Std.Rio.toList_eq_nil_iff {α : Type u} {r : Rio α} [LT α] [DecidableLT α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] : r.toList = [] ↔ ¬PRange.UpwardEnumerable.least < r.upper

theorem Std.Rio.toArray_eq_nil_iff {α : Type u} {r : Rio α} [LT α] [DecidableLT α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] : r.toArray = #[] ↔ ¬PRange.UpwardEnumerable.least < r.upper

theorem Std.Rio.mem_iff_mem_rco {α : Type u} {r : Rio α} [LE α] [LT α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] {a : α} : a ∈ r ↔ a ∈ PRange.UpwardEnumerable.least...r.upper

theorem Std.Rio.mem_toList_iff_mem {α : Type u} {r : Rio α} [LT α] [DecidableLT α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] {a : α} : a ∈ r.toList ↔ a ∈ r

theorem Std.Rio.mem_toArray_iff_mem {α : Type u} {r : Rio α} [LT α] [DecidableLT α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] {a : α} : a ∈ r.toArray ↔ a ∈ r

theorem Std.Rio.pairwise_toList_upwardEnumerableLt {α : Type u} {r : Rio α} [LT α] [DecidableLT α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] : List.Pairwise (fun (a b : α) => PRange.UpwardEnumerable.LT a b) r.toList

theorem Std.Rio.nodup_toList {α : Type u} [LT α] [DecidableLT α] [PRange.Least? α] [PRange.UpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] {a : α} : (*...a).toList.Nodup

theorem Std.Rio.pairwise_toList_ne {α : Type u} {r : Rio α} [LT α] [DecidableLT α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] : List.Pairwise (fun (a b : α) => a ≠ b) r.toList

theorem Std.Rio.pairwise_toList_lt {α : Type u} {r : Rio α} [LT α] [DecidableLT α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerableLeast? α] : List.Pairwise (fun (a b : α) => a < b) r.toList

theorem Std.Rio.pairwise_toList_le {α : Type u} {r : Rio α} [LE α] [LT α] [DecidableLT α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] : List.Pairwise (fun (a b : α) => a ≤ b) r.toList

theorem Std.Rio.mem_succ_iff {α : Type u} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LinearlyUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.InfinitelyUpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {hi a : α} : a ∈ *...PRange.succ hi ↔ a ∈ *...hi ∨ a = hi

theorem Std.Rio.succ_mem_succ_iff {α : Type u} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LinearlyUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.InfinitelyUpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {hi a : α} : PRange.succ a ∈ *...PRange.succ hi ↔ a ∈ *...hi

theorem Std.Rio.toList_succ_eq_map {α : Type u} [LT α] [DecidableLT α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LinearlyUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.InfinitelyUpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLeast? α] {hi : α} : (*...PRange.succ hi).toList = PRange.UpwardEnumerable.least :: List.map PRange.succ (*...hi).toList

theorem Std.Rio.toArray_succ_eq_map {α : Type u} {r : Rio α} [LT α] [DecidableLT α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LinearlyUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.InfinitelyUpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLeast? α] {hi : α} : (*...PRange.succ hi).toArray = #[PRange.UpwardEnumerable.least] ++ Array.map PRange.succ (*...hi).toArray

theorem Std.Rio.forIn'_eq_forIn'_toList {α : Type u} {r : Rio α} [LT α] [DecidableLT α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} : forIn' r init f = forIn' r.toList init fun (a : α) (ha : a ∈ r.toList) (acc : γ) => f a ⋯ acc

theorem Std.Rio.forIn'_eq_forIn'_toArray {α : Type u} {r : Rio α} [LT α] [DecidableLT α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} : forIn' r init f = forIn' r.toArray init fun (a : α) (ha : a ∈ r.toArray) (acc : γ) => f a ⋯ acc

theorem Std.Rio.forIn'_toList_eq_forIn' {α : Type u} {r : Rio α} [LT α] [DecidableLT α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r.toList → γ → m (ForInStep γ)} : forIn' r.toList init f = forIn' r init fun (a : α) (ha : a ∈ r) (acc : γ) => f a ⋯ acc

theorem Std.Rio.forIn'_toArray_eq_forIn' {α : Type u} {r : Rio α} [LT α] [DecidableLT α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r.toArray → γ → m (ForInStep γ)} : forIn' r.toArray init f = forIn' r init fun (a : α) (ha : a ∈ r) (acc : γ) => f a ⋯ acc

theorem Std.Rio.mem_of_mem_rco {α : Type u} [LE α] [LT α] {lo hi a : α} (hmem : a ∈ lo...hi) : a ∈ *...hi

theorem Std.Rio.mem_of_mem_roo {α : Type u} [LT α] {lo hi a : α} (hmem : a ∈ lo<...hi) : a ∈ *...hi

theorem Std.Rio.forIn'_eq_ite_roo {α : Type u} {r : Rio α} [LT α] [DecidableLT α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] [LawfulMonad m] {γ : Type u} {init : γ} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} : forIn' r init f = if hu : PRange.UpwardEnumerable.least < r.upper then do let __do_lift ← f PRange.UpwardEnumerable.least hu init match __do_lift with | ForInStep.yield c => forIn' (PRange.UpwardEnumerable.least<...r.upper) c fun (a : α) (ha : a ∈ PRange.UpwardEnumerable.least<...r.upper) (acc : γ) => f a ⋯ acc | ForInStep.done c => pure c else pure init

@[deprecated Std.Rio.forIn'_eq_ite_roo (since := "2026-07-21")]

theorem Std.Rio.forIn'_eq_if_roo {α : Type u} {r : Rio α} [LT α] [DecidableLT α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] [LawfulMonad m] {γ : Type u} {init : γ} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} : forIn' r init f = if hu : PRange.UpwardEnumerable.least < r.upper then do let __do_lift ← f PRange.UpwardEnumerable.least hu init match __do_lift with | ForInStep.yield c => forIn' (PRange.UpwardEnumerable.least<...r.upper) c fun (a : α) (ha : a ∈ PRange.UpwardEnumerable.least<...r.upper) (acc : γ) => f a ⋯ acc | ForInStep.done c => pure c else pure init

theorem Std.Rio.forIn'_eq_forIn'_rco {α : Type u} {r : Rio α} [LE α] [LT α] [DecidableLT α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] [LawfulMonad m] {γ : Type u} {init : γ} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} : forIn' r init f = forIn' (PRange.UpwardEnumerable.least...r.upper) init fun (a : α) (ha : a ∈ PRange.UpwardEnumerable.least...r.upper) (acc : γ) => f a ⋯ acc

theorem Std.Rio.isEmpty_iff_forall_not_mem {α : Type u} {r : Rio α} [LT α] [DecidableLT α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLeast? α] [PRange.LawfulUpwardEnumerable α] : r.isEmpty = true ↔ ∀ (a : α), ¬a ∈ r

@[simp]

theorem Std.Rii.toArray_toList {α : Type u} {r : Rii α} [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] : r.toList.toArray = r.toArray

@[simp]

theorem Std.Rii.toList_toArray {α : Type u} {r : Rii α} [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] : r.toArray.toList = r.toList

theorem Std.Rii.toList_eq_match_rci {α : Type u} {r : Rii α} [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] : r.toList = match PRange.least? with | none => [] | some init => init...*.toList

theorem Std.Rii.toArray_eq_match_rci {α : Type u} {r : Rii α} [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] : r.toArray = match PRange.least? with | none => #[] | some init => init...*.toArray

theorem Std.Rii.toList_eq_match_roi {α : Type u} {r : Rii α} [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] : r.toList = match PRange.least? with | none => [] | some init => init :: init<...*.toList

theorem Std.Rii.toArray_eq_match_roi {α : Type u} {r : Rii α} [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] : r.toArray = match PRange.least? with | none => #[] | some init => #[init] ++ init<...*.toArray

theorem Std.Rii.toList_eq_nil_iff {α : Type u} {r : Rii α} [LT α] [DecidableLT α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] : r.toList = [] ↔ ¬Nonempty α

theorem Std.Rii.toArray_eq_empty_iff {α : Type u} {r : Rii α} [LT α] [DecidableLT α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] : r.toArray = #[] ↔ ¬Nonempty α

theorem Std.Rii.mem_iff_mem_rci {α : Type u} {r : Rii α} [LE α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] {a : α} : a ∈ r ↔ a ∈ PRange.UpwardEnumerable.least...*

theorem Std.Rii.mem_toList {α : Type u} {r : Rii α} [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] {a : α} : a ∈ r.toList

theorem Std.Rii.mem_toArray {α : Type u} {r : Rii α} [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] {a : α} : a ∈ r.toArray

theorem Std.Rii.pairwise_toList_upwardEnumerableLt {α : Type u} {r : Rii α} [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] : List.Pairwise (fun (a b : α) => PRange.UpwardEnumerable.LT a b) r.toList

theorem Std.Rii.nodup_toList {α : Type u} [PRange.Least? α] [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] : *...*.toList.Nodup

theorem Std.Rii.pairwise_toList_ne {α : Type u} {r : Rii α} [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] : List.Pairwise (fun (a b : α) => a ≠ b) r.toList

theorem Std.Rii.pairwise_toList_lt {α : Type u} {r : Rii α} [LT α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerableLeast? α] : List.Pairwise (fun (a b : α) => a < b) r.toList

theorem Std.Rii.pairwise_toList_le {α : Type u} {r : Rii α} [LE α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] : List.Pairwise (fun (a b : α) => a ≤ b) r.toList

theorem Std.Rii.forIn'_eq_forIn'_toList {α : Type u} {r : Rii α} [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} : forIn' r init f = forIn' r.toList init fun (a : α) (x : a ∈ r.toList) (acc : γ) => f a ⋯ acc

theorem Std.Rii.forIn'_eq_forIn'_toArray {α : Type u} {r : Rii α} [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} : forIn' r init f = forIn' r.toArray init fun (a : α) (x : a ∈ r.toArray) (acc : γ) => f a ⋯ acc

theorem Std.Rii.forIn'_toList_eq_forIn' {α : Type u} {r : Rii α} [LT α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r.toList → γ → m (ForInStep γ)} : forIn' r.toList init f = forIn' r init fun (a : α) (x : a ∈ r) (acc : γ) => f a ⋯ acc

theorem Std.Rii.forIn'_toArray_eq_forIn' {α : Type u} {r : Rii α} [LT α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r.toArray → γ → m (ForInStep γ)} : forIn' r.toArray init f = forIn' r init fun (a : α) (x : a ∈ r) (acc : γ) => f a ⋯ acc

theorem Std.Rii.forIn'_eq_match_rci {α : Type u} {r : Rii α} [LE α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] [LawfulMonad m] {γ : Type u} {init : γ} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} : forIn' r init f = match PRange.least? with | none => pure init | some next => forIn' (next...*) init fun (a : α) (x : a ∈ next...*) (acc : γ) => f a ⋯ acc

theorem Std.Rii.forIn'_eq_match_roi {α : Type u} {r : Rii α} {hu : True} [LT α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] [LawfulMonad m] {γ : Type u} {init : γ} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} : forIn' r init f = match PRange.least? with | none => pure init | some next => do let __do_lift ← f next hu init match __do_lift with | ForInStep.yield c => forIn' (next<...*) c fun (a : α) (x : a ∈ next<...*) (acc : γ) => f a ⋯ acc | ForInStep.done c => pure c

theorem Std.Rii.isEmpty_iff {α : Type u} {r : Rii α} [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLeast? α] : r.isEmpty = true ↔ ¬Nonempty α

theorem Std.Rii.isEmpty_iff_forall_not_mem {α : Type u} {r : Rii α} [LT α] [DecidableLT α] [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLeast? α] [PRange.LawfulUpwardEnumerable α] : r.isEmpty = true ↔ ∀ (a : α), ¬a ∈ r

theorem Std.toList_roc_eq_toList_rcc_of_isSome_succ? {α : Type u} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] {lo hi : α} (h : (PRange.succ? lo).isSome = true) : (lo<...=hi).toList = ((PRange.succ? lo).get h...=hi).toList

theorem Std.toList_roo_eq_toList_rco_of_isSome_succ? {α : Type u} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] {lo hi : α} (h : (PRange.succ? lo).isSome = true) : (lo<...hi).toList = ((PRange.succ? lo).get h...hi).toList

theorem Std.toList_roi_eq_toList_rci_of_isSome_succ? {α : Type u} [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] {lo : α} (h : (PRange.succ? lo).isSome = true) : lo<...*.toList = (PRange.succ? lo).get h...*.toList

theorem Std.Rcc.size_eq_ite_roc {α : Type u} {r : Rcc α} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [Rxc.HasSize α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [Rxc.LawfulHasSize α] : r.size = if r.lower ≤ r.upper then (r.lower<...=r.upper).size + 1 else 0

@[deprecated Std.Rcc.size_eq_ite_roc (since := "2026-07-21")]

theorem Std.Rcc.size_eq_if_roc {α : Type u} {r : Rcc α} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [Rxc.HasSize α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [Rxc.LawfulHasSize α] : r.size = if r.lower ≤ r.upper then (r.lower<...=r.upper).size + 1 else 0

theorem Std.Rcc.size_eq_ite_rcc {α : Type u} {r : Rcc α} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [Rxc.HasSize α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [Rxc.LawfulHasSize α] : r.size = if r.lower ≤ r.upper then match PRange.succ? r.lower with | none => 1 | some next => (next...=r.upper).size + 1 else 0

@[deprecated Std.Rcc.size_eq_ite_rcc (since := "2026-07-21")]

theorem Std.Rcc.size_eq_if_rcc {α : Type u} {r : Rcc α} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [Rxc.HasSize α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [Rxc.LawfulHasSize α] : r.size = if r.lower ≤ r.upper then match PRange.succ? r.lower with | none => 1 | some next => (next...=r.upper).size + 1 else 0

@[simp]

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

@[simp]

theorem Std.Rcc.size_toArray {α : Type u} {r : Rcc α} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [Rxc.HasSize α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [Rxc.LawfulHasSize α] : r.toArray.size = r.size

theorem Std.Rcc.getElem?_toList_eq {α : Type u} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] {r : Rcc α} {i : Nat} : r.toList[i]? = Option.filter (fun (x : α) => decide (x ≤ r.upper)) (PRange.succMany? i r.lower)

theorem Std.Rcc.getElem?_toArray_eq {α : Type u} {r : Rcc α} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] {i : Nat} : r.toArray[i]? = Option.filter (fun (x : α) => decide (x ≤ r.upper)) (PRange.succMany? i r.lower)

theorem Std.Rcc.isSome_succMany?_of_lt_length_toList {α : Type u} {r : Rcc α} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] {i : Nat} (h : i < r.toList.length) : (PRange.succMany? i r.lower).isSome = true

theorem Std.Rcc.isSome_succMany?_of_lt_size_toArray {α : Type u} {r : Rcc α} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] {i : Nat} (h : i < r.toArray.size) : (PRange.succMany? i r.lower).isSome = true

theorem Std.Rcc.getElem_toList_eq {α : Type u} {r : Rcc α} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] {i : Nat} {h : i < r.toList.length} : r.toList[i] = (PRange.succMany? i r.lower).get ⋯

theorem Std.Rcc.getElem_toArray_eq {α : Type u} {r : Rcc α} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] {i : Nat} {h : i < r.toArray.size} : r.toArray[i] = (PRange.succMany? i r.lower).get ⋯

theorem Std.Rcc.eq_succMany?_of_toList_eq_append_cons {α : Type u} {r : Rcc α} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] {pref suff : List α} {cur : α} (h : r.toList = pref ++ cur :: suff) : cur = (PRange.succMany? pref.length r.lower).get ⋯

theorem Std.Rcc.eq_succMany?_of_toArray_eq_append_append {α : Type u} {r : Rcc α} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] {pref suff : Array α} {cur : α} (h : r.toArray = pref ++ #[cur] ++ suff) : cur = (PRange.succMany? pref.size r.lower).get ⋯

theorem Std.Roc.size_eq_match_rcc {α : Type u} {r : Roc α} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [Rxc.HasSize α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [Rxc.LawfulHasSize α] : r.size = match PRange.succ? r.lower with | none => 0 | some next => (next...=r.upper).size

theorem Std.Roc.size_eq_match_roc {α : Type u} {r : Roc α} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [Rxc.HasSize α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [Rxc.LawfulHasSize α] : r.size = match PRange.succ? r.lower with | none => 0 | some next => if next ≤ r.upper then (next<...=r.upper).size + 1 else 0

@[simp]

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

@[simp]

theorem Std.Roc.size_toArray {α : Type u} {r : Roc α} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [Rxc.HasSize α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [Rxc.LawfulHasSize α] : r.toArray.size = r.size

theorem Std.Roc.getElem?_toList_eq {α : Type u} {r : Roc α} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] {i : Nat} : r.toList[i]? = Option.filter (fun (x : α) => decide (x ≤ r.upper)) (PRange.succMany? (i + 1) r.lower)

theorem Std.Roc.getElem?_toArray_eq {α : Type u} {r : Roc α} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] {i : Nat} : r.toArray[i]? = Option.filter (fun (x : α) => decide (x ≤ r.upper)) (PRange.succMany? (i + 1) r.lower)

theorem Std.Roc.isSome_succMany?_of_lt_length_toList {α : Type u} {r : Roc α} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] {i : Nat} (h : i < r.toList.length) : (PRange.succMany? (i + 1) r.lower).isSome = true

theorem Std.Roc.isSome_succMany?_of_lt_size_toArray {α : Type u} {r : Roc α} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] {i : Nat} (h : i < r.toArray.size) : (PRange.succMany? (i + 1) r.lower).isSome = true

theorem Std.Roc.getElem_toList_eq {α : Type u} {r : Roc α} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] {i : Nat} {h : i < r.toList.length} : r.toList[i] = (PRange.succMany? (i + 1) r.lower).get ⋯

theorem Std.Roc.getElem_toArray_eq {α : Type u} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] {r : Roc α} {i : Nat} {h : i < r.toArray.size} : r.toArray[i] = (PRange.succMany? (i + 1) r.lower).get ⋯

theorem Std.Roc.eq_succMany?_of_toList_eq_append_cons {α : Type u} {r : Roc α} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] {pref suff : List α} {cur : α} (h : r.toList = pref ++ cur :: suff) : cur = (PRange.succMany? (pref.length + 1) r.lower).get ⋯

theorem Std.Roc.eq_succMany?_of_toArray_eq_append_append {α : Type u} {r : Roc α} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] {pref suff : Array α} {cur : α} (h : r.toArray = pref ++ #[cur] ++ suff) : cur = (PRange.succMany? (pref.size + 1) r.lower).get ⋯

theorem Std.Ric.size_eq_match_rcc {α : Type u} {r : Ric α} [PRange.Least? α] [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [Rxc.HasSize α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [Rxc.LawfulHasSize α] : r.size = match PRange.least? with | none => 0 | some next => (next...=r.upper).size

theorem Std.Ric.size_eq_match_roc {α : Type u} {r : Ric α} [PRange.Least? α] [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [Rxc.HasSize α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [Rxc.LawfulHasSize α] : r.size = match PRange.least? with | none => 0 | some next => if next ≤ r.upper then (next<...=r.upper).size + 1 else 0

@[simp]

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

@[simp]

theorem Std.Ric.size_toArray {α : Type u} {r : Ric α} [PRange.Least? α] [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [Rxc.HasSize α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [Rxc.LawfulHasSize α] : r.toArray.size = r.size

theorem Std.Ric.getElem?_toList_eq {α : Type u} {r : Ric α} [PRange.Least? α] [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] {i : Nat} : r.toList[i]? = Option.filter (fun (x : α) => decide (x ≤ r.upper)) (PRange.succMany? i PRange.UpwardEnumerable.least)

theorem Std.Ric.getElem?_toArray_eq {α : Type u} {r : Ric α} [PRange.Least? α] [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] {i : Nat} : r.toArray[i]? = Option.filter (fun (x : α) => decide (x ≤ r.upper)) (PRange.succMany? i PRange.UpwardEnumerable.least)

theorem Std.Ric.isSome_succMany?_of_lt_length_toList {α : Type u} {r : Ric α} [PRange.Least? α] [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] {i : Nat} (h : i < r.toList.length) : (PRange.succMany? i PRange.UpwardEnumerable.least).isSome = true

theorem Std.Ric.isSome_succMany?_of_lt_size_toArray {α : Type u} {r : Ric α} [PRange.Least? α] [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] {i : Nat} (h : i < r.toArray.size) : (PRange.succMany? i PRange.UpwardEnumerable.least).isSome = true

theorem Std.Ric.getElem_toList_eq {α : Type u} {r : Ric α} [PRange.Least? α] [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] {i : Nat} {h : i < r.toList.length} : r.toList[i] = (PRange.succMany? i PRange.UpwardEnumerable.least).get ⋯

theorem Std.Ric.getElem_toArray_eq {α : Type u} [PRange.Least? α] [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] {r : Ric α} {i : Nat} {h : i < r.toArray.size} : r.toArray[i] = (PRange.succMany? i PRange.UpwardEnumerable.least).get ⋯

theorem Std.Ric.eq_succMany?_of_toList_eq_append_cons {α : Type u} {r : Ric α} [PRange.Least? α] [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] {pref suff : List α} {cur : α} (h : r.toList = pref ++ cur :: suff) : cur = (PRange.succMany? pref.length PRange.UpwardEnumerable.least).get ⋯

theorem Std.Ric.eq_succMany?_of_toArray_eq_append_append {α : Type u} {r : Ric α} [PRange.Least? α] [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] {pref suff : Array α} {cur : α} (h : r.toArray = pref ++ #[cur] ++ suff) : cur = (PRange.succMany? pref.size PRange.UpwardEnumerable.least).get ⋯

theorem Std.Rco.size_eq_ite_roo {α : Type u} {r : Rco α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [Rxo.HasSize α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [Rxo.LawfulHasSize α] : r.size = if r.lower < r.upper then (r.lower<...r.upper).size + 1 else 0

@[deprecated Std.Rco.size_eq_ite_roo (since := "2026-07-21")]

theorem Std.Rco.size_eq_if_roo {α : Type u} {r : Rco α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [Rxo.HasSize α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [Rxo.LawfulHasSize α] : r.size = if r.lower < r.upper then (r.lower<...r.upper).size + 1 else 0

theorem Std.Rco.size_eq_ite_rcc {α : Type u} {r : Rco α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [Rxo.HasSize α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [Rxo.LawfulHasSize α] : r.size = if r.lower < r.upper then match PRange.succ? r.lower with | none => 1 | some next => (next...r.upper).size + 1 else 0

@[deprecated Std.Rco.size_eq_ite_rcc (since := "2026-07-21")]

theorem Std.Rco.size_eq_if_rcc {α : Type u} {r : Rco α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [Rxo.HasSize α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [Rxo.LawfulHasSize α] : r.size = if r.lower < r.upper then match PRange.succ? r.lower with | none => 1 | some next => (next...r.upper).size + 1 else 0

@[simp]

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

@[simp]

theorem Std.Rco.size_toArray {α : Type u} {r : Rco α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [Rxo.HasSize α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [Rxo.LawfulHasSize α] : r.toArray.size = r.size

theorem Std.Rco.getElem?_toList_eq {α : Type u} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] {r : Rco α} {i : Nat} : r.toList[i]? = Option.filter (fun (x : α) => decide (x < r.upper)) (PRange.succMany? i r.lower)

theorem Std.Rco.getElem?_toArray_eq {α : Type u} {r : Rco α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] {i : Nat} : r.toArray[i]? = Option.filter (fun (x : α) => decide (x < r.upper)) (PRange.succMany? i r.lower)

theorem Std.Rco.isSome_succMany?_of_lt_length_toList {α : Type u} {r : Rco α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] {i : Nat} (h : i < r.toList.length) : (PRange.succMany? i r.lower).isSome = true

theorem Std.Rco.isSome_succMany?_of_lt_size_toArray {α : Type u} {r : Rco α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] {i : Nat} (h : i < r.toArray.size) : (PRange.succMany? i r.lower).isSome = true

theorem Std.Rco.getElem_toList_eq {α : Type u} {r : Rco α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] {i : Nat} {h : i < r.toList.length} : r.toList[i] = (PRange.succMany? i r.lower).get ⋯

theorem Std.Rco.getElem_toArray_eq {α : Type u} {r : Rco α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] {i : Nat} {h : i < r.toArray.size} : r.toArray[i] = (PRange.succMany? i r.lower).get ⋯

theorem Std.Rco.eq_succMany?_of_toList_eq_append_cons {α : Type u} {r : Rco α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] {pref suff : List α} {cur : α} (h : r.toList = pref ++ cur :: suff) : cur = (PRange.succMany? pref.length r.lower).get ⋯

theorem Std.Rco.eq_succMany?_of_toArray_eq_append_append {α : Type u} {r : Rco α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] {pref suff : Array α} {cur : α} (h : r.toArray = pref ++ #[cur] ++ suff) : cur = (PRange.succMany? pref.size r.lower).get ⋯

theorem Std.Roo.size_eq_match_rcc {α : Type u} {r : Roo α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [Rxo.HasSize α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [Rxo.LawfulHasSize α] : r.size = match PRange.succ? r.lower with | none => 0 | some next => (next...r.upper).size

theorem Std.Roo.size_eq_match_roc {α : Type u} {r : Roo α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [Rxo.HasSize α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [Rxo.LawfulHasSize α] : r.size = match PRange.succ? r.lower with | none => 0 | some next => if next < r.upper then (next<...r.upper).size + 1 else 0

@[simp]

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

@[simp]

theorem Std.Roo.size_toArray {α : Type u} {r : Roo α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [Rxo.HasSize α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [Rxo.LawfulHasSize α] : r.toArray.size = r.size

theorem Std.Roo.getElem?_toList_eq {α : Type u} {r : Roo α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] {i : Nat} : r.toList[i]? = Option.filter (fun (x : α) => decide (x < r.upper)) (PRange.succMany? (i + 1) r.lower)

theorem Std.Roo.getElem?_toArray_eq {α : Type u} {r : Roo α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] {i : Nat} : r.toArray[i]? = Option.filter (fun (x : α) => decide (x < r.upper)) (PRange.succMany? (i + 1) r.lower)

theorem Std.Roo.isSome_succMany?_of_lt_length_toList {α : Type u} {r : Roo α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] {i : Nat} (h : i < r.toList.length) : (PRange.succMany? (i + 1) r.lower).isSome = true

theorem Std.Roo.isSome_succMany?_of_lt_size_toArray {α : Type u} {r : Roo α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] {i : Nat} (h : i < r.toArray.size) : (PRange.succMany? (i + 1) r.lower).isSome = true

theorem Std.Roo.getElem_toList_eq {α : Type u} {r : Roo α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] {i : Nat} {h : i < r.toList.length} : r.toList[i] = (PRange.succMany? (i + 1) r.lower).get ⋯

theorem Std.Roo.getElem_toArray_eq {α : Type u} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] {r : Roo α} {i : Nat} {h : i < r.toArray.size} : r.toArray[i] = (PRange.succMany? (i + 1) r.lower).get ⋯

theorem Std.Roo.eq_succMany?_of_toList_eq_append_cons {α : Type u} {r : Roo α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] {pref suff : List α} {cur : α} (h : r.toList = pref ++ cur :: suff) : cur = (PRange.succMany? (pref.length + 1) r.lower).get ⋯

theorem Std.Roo.eq_succMany?_of_toArray_eq_append_append {α : Type u} {r : Roo α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] {pref suff : Array α} {cur : α} (h : r.toArray = pref ++ #[cur] ++ suff) : cur = (PRange.succMany? (pref.size + 1) r.lower).get ⋯

theorem Std.Rio.size_eq_match_rcc {α : Type u} {r : Rio α} [PRange.Least? α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [Rxo.HasSize α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [Rxo.LawfulHasSize α] : r.size = match PRange.least? with | none => 0 | some next => (next...r.upper).size

theorem Std.Rio.size_eq_match_roc {α : Type u} {r : Rio α} [PRange.Least? α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [Rxo.HasSize α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [Rxo.LawfulHasSize α] : r.size = match PRange.least? with | none => 0 | some next => if next < r.upper then (next<...r.upper).size + 1 else 0

@[simp]

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

@[simp]

theorem Std.Rio.size_toArray {α : Type u} {r : Rio α} [PRange.Least? α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [Rxo.HasSize α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [Rxo.LawfulHasSize α] : r.toArray.size = r.size

theorem Std.Rio.getElem?_toList_eq {α : Type u} {r : Rio α} [PRange.Least? α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] {i : Nat} : r.toList[i]? = Option.filter (fun (x : α) => decide (x < r.upper)) (PRange.succMany? i PRange.UpwardEnumerable.least)

theorem Std.Rio.getElem?_toArray_eq {α : Type u} {r : Rio α} [PRange.Least? α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] {i : Nat} : r.toArray[i]? = Option.filter (fun (x : α) => decide (x < r.upper)) (PRange.succMany? i PRange.UpwardEnumerable.least)

theorem Std.Rio.isSome_succMany?_of_lt_length_toList {α : Type u} {r : Rio α} [PRange.Least? α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] {i : Nat} (h : i < r.toList.length) : (PRange.succMany? i PRange.UpwardEnumerable.least).isSome = true

theorem Std.Rio.isSome_succMany?_of_lt_size_toArray {α : Type u} {r : Rio α} [PRange.Least? α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] {i : Nat} (h : i < r.toArray.size) : (PRange.succMany? i PRange.UpwardEnumerable.least).isSome = true

theorem Std.Rio.getElem_toList_eq {α : Type u} {r : Rio α} [PRange.Least? α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] {i : Nat} {h : i < r.toList.length} : r.toList[i] = (PRange.succMany? i PRange.UpwardEnumerable.least).get ⋯

theorem Std.Rio.getElem_toArray_eq {α : Type u} [PRange.Least? α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] {r : Rio α} {i : Nat} {h : i < r.toArray.size} : r.toArray[i] = (PRange.succMany? i PRange.UpwardEnumerable.least).get ⋯

theorem Std.Rio.eq_succMany?_of_toList_eq_append_cons {α : Type u} {r : Rio α} [PRange.Least? α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] {pref suff : List α} {cur : α} (h : r.toList = pref ++ cur :: suff) : cur = (PRange.succMany? pref.length PRange.UpwardEnumerable.least).get ⋯

theorem Std.Rio.eq_succMany?_of_toArray_eq_append_append {α : Type u} {r : Rio α} [PRange.Least? α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] {pref suff : Array α} {cur : α} (h : r.toArray = pref ++ #[cur] ++ suff) : cur = (PRange.succMany? pref.size PRange.UpwardEnumerable.least).get ⋯

theorem Std.Rci.size_eq_size_roi {α : Type u} {r : Rci α} [PRange.UpwardEnumerable α] [Rxi.HasSize α] [PRange.LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [Rxi.LawfulHasSize α] : r.size = r.lower<...*.size + 1

theorem Std.Rci.size_eq_match_rci {α : Type u} {r : Rci α} [PRange.UpwardEnumerable α] [Rxi.HasSize α] [PRange.LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [Rxi.LawfulHasSize α] : r.size = match PRange.succ? r.lower with | none => 1 | some next => next...*.size + 1

@[simp]

theorem Std.Rci.length_toList {α : Type u} {r : Rci α} [PRange.UpwardEnumerable α] [Rxi.HasSize α] [PRange.LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [Rxi.LawfulHasSize α] : r.toList.length = r.size

@[simp]

theorem Std.Rci.size_toArray {α : Type u} {r : Rci α} [PRange.UpwardEnumerable α] [Rxi.HasSize α] [PRange.LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [Rxi.LawfulHasSize α] : r.toArray.size = r.size

theorem Std.Rci.getElem?_toList_eq {α : Type u} [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] {r : Rci α} {i : Nat} : r.toList[i]? = PRange.succMany? i r.lower

theorem Std.Rci.getElem?_toArray_eq {α : Type u} {r : Rci α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxi.IsAlwaysFinite α] {i : Nat} : r.toArray[i]? = PRange.succMany? i r.lower

theorem Std.Rci.isSome_succMany?_of_lt_length_toList {α : Type u} {r : Rci α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxi.IsAlwaysFinite α] {i : Nat} (h : i < r.toList.length) : (PRange.succMany? i r.lower).isSome = true

theorem Std.Rci.isSome_succMany?_of_lt_size_toArray {α : Type u} {r : Rci α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxi.IsAlwaysFinite α] {i : Nat} (h : i < r.toArray.size) : (PRange.succMany? i r.lower).isSome = true

theorem Std.Rci.getElem_toList_eq {α : Type u} {r : Rci α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxi.IsAlwaysFinite α] {i : Nat} {h : i < r.toList.length} : r.toList[i] = (PRange.succMany? i r.lower).get ⋯

theorem Std.Rci.getElem_toArray_eq {α : Type u} {r : Rci α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxi.IsAlwaysFinite α] {i : Nat} {h : i < r.toArray.size} : r.toArray[i] = (PRange.succMany? i r.lower).get ⋯

theorem Std.Rci.eq_succMany?_of_toList_eq_append_cons {α : Type u} {r : Rci α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxi.IsAlwaysFinite α] {pref suff : List α} {cur : α} (h : r.toList = pref ++ cur :: suff) : cur = (PRange.succMany? pref.length r.lower).get ⋯

theorem Std.Rci.eq_succMany?_of_toArray_eq_append_append {α : Type u} {r : Rci α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxi.IsAlwaysFinite α] {pref suff : Array α} {cur : α} (h : r.toArray = pref ++ #[cur] ++ suff) : cur = (PRange.succMany? pref.size r.lower).get ⋯

theorem Std.Roi.size_eq_match_rci {α : Type u} {r : Roi α} [PRange.UpwardEnumerable α] [Rxi.HasSize α] [PRange.LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [Rxi.LawfulHasSize α] : r.size = match PRange.succ? r.lower with | none => 0 | some next => next...*.size

theorem Std.Roi.size_eq_match_roi {α : Type u} {r : Roi α} [PRange.UpwardEnumerable α] [Rxi.HasSize α] [PRange.LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [Rxi.LawfulHasSize α] : r.size = match PRange.succ? r.lower with | none => 0 | some next => next<...*.size + 1

@[simp]

theorem Std.Roi.length_toList {α : Type u} {r : Roi α} [PRange.UpwardEnumerable α] [Rxi.HasSize α] [PRange.LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [Rxi.LawfulHasSize α] : r.toList.length = r.size

@[simp]

theorem Std.Roi.size_toArray {α : Type u} {r : Roi α} [PRange.UpwardEnumerable α] [Rxi.HasSize α] [PRange.LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [Rxi.LawfulHasSize α] : r.toArray.size = r.size

theorem Std.Roi.getElem?_toList_eq {α : Type u} {r : Roi α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxi.IsAlwaysFinite α] {i : Nat} : r.toList[i]? = PRange.succMany? (i + 1) r.lower

theorem Std.Roi.getElem?_toArray_eq {α : Type u} {r : Roi α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxi.IsAlwaysFinite α] {i : Nat} : r.toArray[i]? = PRange.succMany? (i + 1) r.lower

theorem Std.Roi.isSome_succMany?_of_lt_length_toList {α : Type u} {r : Roi α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxi.IsAlwaysFinite α] {i : Nat} (h : i < r.toList.length) : (PRange.succMany? (i + 1) r.lower).isSome = true

theorem Std.Roi.isSome_succMany?_of_lt_size_toArray {α : Type u} {r : Roi α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxi.IsAlwaysFinite α] {i : Nat} (h : i < r.toArray.size) : (PRange.succMany? (i + 1) r.lower).isSome = true

theorem Std.Roi.getElem_toList_eq {α : Type u} {r : Roi α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxi.IsAlwaysFinite α] {i : Nat} {h : i < r.toList.length} : r.toList[i] = (PRange.succMany? (i + 1) r.lower).get ⋯

theorem Std.Roi.getElem_toArray_eq {α : Type u} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxi.IsAlwaysFinite α] {r : Roi α} {i : Nat} {h : i < r.toArray.size} : r.toArray[i] = (PRange.succMany? (i + 1) r.lower).get ⋯

theorem Std.Roi.eq_succMany?_of_toList_eq_append_cons {α : Type u} {r : Roi α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxi.IsAlwaysFinite α] {pref suff : List α} {cur : α} (h : r.toList = pref ++ cur :: suff) : cur = (PRange.succMany? (pref.length + 1) r.lower).get ⋯

theorem Std.Roi.eq_succMany?_of_toArray_eq_append_append {α : Type u} {r : Roi α} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Rxi.IsAlwaysFinite α] {pref suff : Array α} {cur : α} (h : r.toArray = pref ++ #[cur] ++ suff) : cur = (PRange.succMany? (pref.size + 1) r.lower).get ⋯

theorem Std.Rii.size_eq_match_rci {α : Type u} {r : Rii α} [PRange.Least? α] [PRange.UpwardEnumerable α] [Rxi.HasSize α] [PRange.LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [Rxi.LawfulHasSize α] : r.size = match PRange.least? with | none => 0 | some next => next...*.size

theorem Std.Rii.size_eq_match_roi {α : Type u} {r : Rii α} [PRange.Least? α] [PRange.UpwardEnumerable α] [Rxi.HasSize α] [PRange.LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [Rxi.LawfulHasSize α] : r.size = match PRange.least? with | none => 0 | some next => next<...*.size + 1

@[simp]

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

@[simp]

theorem Std.Rii.size_toArray {α : Type u} {r : Rii α} [PRange.Least? α] [PRange.UpwardEnumerable α] [Rxi.HasSize α] [PRange.LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [Rxi.LawfulHasSize α] : r.toArray.size = r.size

theorem Std.Rii.getElem?_toList_eq {α : Type u} {r : Rii α} [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] {i : Nat} : r.toList[i]? = PRange.least?.bind (PRange.succMany? i)

theorem Std.Rii.getElem?_toArray_eq {α : Type u} {r : Rii α} [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] {i : Nat} : r.toArray[i]? = PRange.least?.bind (PRange.succMany? i)

theorem Std.Rii.isSome_succMany?_of_lt_length_toList {α : Type u} {r : Rii α} [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] {i : Nat} (h : i < r.toList.length) : (PRange.least?.bind (PRange.succMany? i)).isSome = true

theorem Std.Rii.isSome_succMany?_of_lt_size_toArray {α : Type u} {r : Rii α} [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] {i : Nat} (h : i < r.toArray.size) : (PRange.least?.bind (PRange.succMany? i)).isSome = true

theorem Std.Rii.getElem_toList_eq {α : Type u} {r : Rii α} [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] {i : Nat} {h : i < r.toList.length} : r.toList[i] = (PRange.least?.bind (PRange.succMany? i)).get ⋯

theorem Std.Rii.getElem_toArray_eq {α : Type u} {r : Rii α} [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] {i : Nat} {h : i < r.toArray.size} : r.toArray[i] = (PRange.least?.bind (PRange.succMany? i)).get ⋯

theorem Std.Rii.eq_succMany?_of_toList_eq_append_cons {α : Type u} {r : Rii α} [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] {pref suff : List α} {cur : α} (h : r.toList = pref ++ cur :: suff) : cur = (PRange.least?.bind (PRange.succMany? pref.length)).get ⋯

theorem Std.Rii.eq_succMany?_of_toArray_eq_append_append {α : Type u} {r : Rii α} [PRange.Least? α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] {pref suff : Array α} {cur : α} (h : r.toArray = pref ++ #[cur] ++ suff) : cur = (PRange.least?.bind (PRange.succMany? pref.size)).get ⋯