instance Subarray.instLawfulSliceSizeSubarrayIteratorSubarrayData {α : Type u_1} : Std.Slice.LawfulSliceSize (Std.Slice.Internal.SubarrayData α)

theorem Subarray.toArray_eq_sliceToArray {α : Type u} {s : Subarray α} : Std.Slice.toArray s = Std.Slice.toArray s

@[simp]

theorem Subarray.forIn_toList {α : Type u} {s : Subarray α} {m : Type v → Type w} [Monad m] [LawfulMonad m] {γ : Type v} {init : γ} {f : α → γ → m (ForInStep γ)} : ForIn.forIn (Std.Slice.toList s) init f = ForIn.forIn s init f

theorem Subarray.forIn_eq_forIn_toList {α : Type u} {s : Subarray α} {m : Type v → Type w} [Monad m] [LawfulMonad m] {γ : Type v} {init : γ} {f : α → γ → m (ForInStep γ)} : ForIn.forIn s init f = ForIn.forIn (Std.Slice.toList s) init f

@[simp]

theorem Subarray.forIn_toArray {α : Type u} {s : Subarray α} {m : Type v → Type w} [Monad m] [LawfulMonad m] {γ : Type v} {init : γ} {f : α → γ → m (ForInStep γ)} : ForIn.forIn (Std.Slice.toArray s) init f = ForIn.forIn s init f

theorem Subarray.sliceFoldlM_eq_foldlM {β : Type u_1} {init : β} {m : Type u_1 → Type u_2} [Monad m] {α : Type u} {s : Subarray α} {f : β → α → m β} : Std.Slice.foldlM f init s = Std.Slice.foldlM f init s

theorem Subarray.sliceFoldl_eq_foldl {β : Type u_1} {init : β} {α : Type u} {s : Subarray α} {f : β → α → β} : Std.Slice.foldl f init s = Std.Slice.foldl f init s

theorem Subarray.foldlM_toList {a✝ : Type u_1} {init : a✝} {m : Type u_1 → Type u_2} [Monad m] {α : Type u} {s : Subarray α} {f : a✝ → α → m a✝} [LawfulMonad m] : List.foldlM f init (Std.Slice.toList s) = Std.Slice.foldlM f init s

theorem Subarray.foldl_toList {α✝ : Type u_1} {init : α✝} {α : Type u} {s : Subarray α} {f : α✝ → α → α✝} : List.foldl f init (Std.Slice.toList s) = Std.Slice.foldl f init s

theorem Array.toSubarray_eq_toSubarray_of_min_eq_min {α : Type u_1} {xs : Array α} {start stop stop' : Nat} (h : min stop xs.size = min stop' xs.size) : xs.toSubarray start stop = xs.toSubarray start stop'

theorem Array.toSubarray_eq_min {α : Type u_1} {xs : Array α} {lo hi : Nat} : xs.toSubarray lo hi = { internalRepresentation := { array := xs, start := min lo (min hi xs.size), stop := min hi xs.size, start_le_stop := ⋯, stop_le_array_size := ⋯ } }

@[simp]

theorem Array.array_toSubarray {α : Type u_1} {xs : Array α} {lo hi : Nat} : (xs.toSubarray lo hi).array = xs

@[simp]

theorem Array.start_toSubarray {α : Type u_1} {xs : Array α} {lo hi : Nat} : (xs.toSubarray lo hi).start = min lo (min hi xs.size)

@[simp]

theorem Array.stop_toSubarray {α : Type u_1} {xs : Array α} {lo hi : Nat} : (xs.toSubarray lo hi).stop = min hi xs.size

theorem Subarray.toList_eq {α : Type u_1} {xs : Subarray α} : Std.Slice.toList xs = (xs.array.extract xs.start xs.stop).toList

theorem Subarray.toList_eq_drop_take {α : Type u_1} {xs : Subarray α} : Std.Slice.toList xs = List.drop xs.start (List.take xs.stop xs.array.toList)

@[simp]

theorem Subarray.size_drop {α : Type u_1} {i : Nat} {xs : Subarray α} : Std.Slice.size (xs.drop i) = Std.Slice.size xs - i

@[simp]

theorem Subarray.size_take {α : Type u_1} {i : Nat} {xs : Subarray α} : Std.Slice.size (xs.take i) = min i (Std.Slice.size xs)

theorem Subarray.sliceSize_eq_size {α : Type u_1} {xs : Subarray α} : Std.Slice.size xs = Std.Slice.size xs

theorem Subarray.getElem_eq_getElem_array {α : Type u_1} {i : Nat} {xs : Subarray α} {h : i < Std.Slice.size xs} : xs[i] = xs.array[xs.start + i]

theorem Subarray.getElem_toList {α : Type u_1} {i : Nat} {xs : Subarray α} {h : i < (Std.Slice.toList xs).length} : (Std.Slice.toList xs)[i] = xs[i]

theorem Subarray.getElem_eq_getElem_toList {α : Type u_1} {i : Nat} {xs : Subarray α} {h : i < Std.Slice.size xs} : xs[i] = (Std.Slice.toList xs)[i]

@[simp]

theorem Subarray.toList_drop {α : Type u_1} {n : Nat} {xs : Subarray α} : Std.Slice.toList (xs.drop n) = List.drop n (Std.Slice.toList xs)

@[simp]

theorem Subarray.toList_take {α : Type u_1} {n : Nat} {xs : Subarray α} : Std.Slice.toList (xs.take n) = List.take n (Std.Slice.toList xs)

@[simp]

theorem Subarray.toArray_toList {α : Type u_1} {xs : Subarray α} : (Std.Slice.toList xs).toArray = Std.Slice.toArray xs

@[simp]

theorem Subarray.toList_toArray {α : Type u_1} {xs : Subarray α} : (Std.Slice.toArray xs).toList = Std.Slice.toList xs

@[simp]

theorem Subarray.length_toList {α : Type u_1} {xs : Subarray α} : (Std.Slice.toList xs).length = Std.Slice.size xs

@[simp]

theorem Subarray.size_toArray {α : Type u_1} {xs : Subarray α} : (Std.Slice.toArray xs).size = Std.Slice.size xs

@[simp]

theorem Array.array_mkSlice_rco {α : Type u_1} {xs : Array α} {lo hi : Nat} : (Std.Rco.Sliceable.mkSlice xs (lo...hi)).array = xs

@[simp]

theorem Array.start_mkSlice_rco {α : Type u_1} {xs : Array α} {lo hi : Nat} : (Std.Rco.Sliceable.mkSlice xs (lo...hi)).start = min lo (min hi xs.size)

@[simp]

theorem Array.stop_mkSlice_rco {α : Type u_1} {xs : Array α} {lo hi : Nat} : (Std.Rco.Sliceable.mkSlice xs (lo...hi)).stop = min hi xs.size

theorem Array.mkSlice_rco_eq_mkSlice_rco_min {α : Type u_1} {xs : Array α} {lo hi : Nat} : Std.Rco.Sliceable.mkSlice xs (lo...hi) = Std.Rco.Sliceable.mkSlice xs (min lo (min hi xs.size)...min hi xs.size)

@[simp]

theorem Array.toList_mkSlice_rco {α : Type u_1} {xs : Array α} {lo hi : Nat} : Std.Slice.toList (Std.Rco.Sliceable.mkSlice xs (lo...hi)) = List.drop lo (List.take hi xs.toList)

@[simp]

theorem Array.toArray_mkSlice_rco {α : Type u_1} {xs : Array α} {lo hi : Nat} : Std.Slice.toArray (Std.Rco.Sliceable.mkSlice xs (lo...hi)) = xs.extract lo hi

@[simp]

theorem Array.size_mkSlice_rco {α : Type u_1} {xs : Array α} {lo hi : Nat} : Std.Slice.size (Std.Rco.Sliceable.mkSlice xs (lo...hi)) = min hi xs.size - lo

@[simp]

theorem Array.mkSlice_rcc_eq_mkSlice_rco {α : Type u_1} {xs : Array α} {lo hi : Nat} : Std.Rcc.Sliceable.mkSlice xs (lo...=hi) = Std.Rco.Sliceable.mkSlice xs (lo...hi + 1)

theorem Array.mkSlice_rcc_eq_mkSlice_rco_min {α : Type u_1} {xs : Array α} {lo hi : Nat} : Std.Rcc.Sliceable.mkSlice xs (lo...=hi) = Std.Rco.Sliceable.mkSlice xs (min lo (min (hi + 1) xs.size)...min (hi + 1) xs.size)

@[simp]

theorem Array.array_mkSlice_rcc {α : Type u_1} {xs : Array α} {lo hi : Nat} : (Std.Rcc.Sliceable.mkSlice xs (lo...=hi)).array = xs

@[simp]

theorem Array.start_mkSlice_rcc {α : Type u_1} {xs : Array α} {lo hi : Nat} : (Std.Rcc.Sliceable.mkSlice xs (lo...=hi)).start = min lo (min (hi + 1) xs.size)

@[simp]

theorem Array.stop_mkSlice_rcc {α : Type u_1} {xs : Array α} {lo hi : Nat} : (Std.Rcc.Sliceable.mkSlice xs (lo...=hi)).stop = min (hi + 1) xs.size

@[simp]

theorem Array.toList_mkSlice_rcc {α : Type u_1} {xs : Array α} {lo hi : Nat} : Std.Slice.toList (Std.Rcc.Sliceable.mkSlice xs (lo...=hi)) = List.drop lo (List.take (hi + 1) xs.toList)

@[simp]

theorem Array.toArray_mkSlice_rcc {α : Type u_1} {xs : Array α} {lo hi : Nat} : Std.Slice.toArray (Std.Rcc.Sliceable.mkSlice xs (lo...=hi)) = xs.extract lo (hi + 1)

@[simp]

theorem Array.size_mkSlice_rcc {α : Type u_1} {xs : Array α} {lo hi : Nat} : Std.Slice.size (Std.Rcc.Sliceable.mkSlice xs (lo...=hi)) = min (hi + 1) xs.size - lo

@[simp]

theorem Array.array_mkSlice_rci {α : Type u_1} {xs : Array α} {lo : Nat} : (Std.Rci.Sliceable.mkSlice xs (lo...*)).array = xs

@[simp]

theorem Array.start_mkSlice_rci {α : Type u_1} {xs : Array α} {lo : Nat} : (Std.Rci.Sliceable.mkSlice xs (lo...*)).start = min lo xs.size

@[simp]

theorem Array.stop_mkSlice_rci {α : Type u_1} {xs : Array α} {lo : Nat} : (Std.Rci.Sliceable.mkSlice xs (lo...*)).stop = xs.size

theorem Array.mkSlice_rci_eq_mkSlice_rco {α : Type u_1} {xs : Array α} {lo : Nat} : Std.Rci.Sliceable.mkSlice xs (lo...*) = Std.Rco.Sliceable.mkSlice xs (lo...xs.size)

theorem Array.mkSlice_rci_eq_mkSlice_rco_min {α : Type u_1} {xs : Array α} {lo : Nat} : Std.Rci.Sliceable.mkSlice xs (lo...*) = Std.Rco.Sliceable.mkSlice xs (min lo xs.size...xs.size)

@[simp]

theorem Array.toList_mkSlice_rci {α : Type u_1} {xs : Array α} {lo : Nat} : Std.Slice.toList (Std.Rci.Sliceable.mkSlice xs (lo...*)) = List.drop lo xs.toList

@[simp]

theorem Array.toArray_mkSlice_rci {α : Type u_1} {xs : Array α} {lo : Nat} : Std.Slice.toArray (Std.Rci.Sliceable.mkSlice xs (lo...*)) = xs.extract lo

@[simp]

theorem Array.size_mkSlice_rci {α : Type u_1} {xs : Array α} {lo : Nat} : Std.Slice.size (Std.Rci.Sliceable.mkSlice xs (lo...*)) = xs.size - lo

@[simp]

theorem Array.array_mkSlice_roo {α : Type u_1} {xs : Array α} {lo hi : Nat} : (Std.Roo.Sliceable.mkSlice xs (lo<...hi)).array = xs

@[simp]

theorem Array.start_mkSlice_roo {α : Type u_1} {xs : Array α} {lo hi : Nat} : (Std.Roo.Sliceable.mkSlice xs (lo<...hi)).start = min (lo + 1) (min hi xs.size)

@[simp]

theorem Array.stop_mkSlice_roo {α : Type u_1} {xs : Array α} {lo hi : Nat} : (Std.Roo.Sliceable.mkSlice xs (lo<...hi)).stop = min hi xs.size

theorem Array.mkSlice_roo_eq_mkSlice_rco {α : Type u_1} {xs : Array α} {lo hi : Nat} : Std.Roo.Sliceable.mkSlice xs (lo<...hi) = Std.Rco.Sliceable.mkSlice xs (lo + 1...hi)

theorem Array.mkSlice_roo_eq_mkSlice_roo_min {α : Type u_1} {xs : Array α} {lo hi : Nat} : Std.Roo.Sliceable.mkSlice xs (lo<...hi) = Std.Rco.Sliceable.mkSlice xs (min (lo + 1) (min hi xs.size)...min hi xs.size)

@[simp]

theorem Array.toList_mkSlice_roo {α : Type u_1} {xs : Array α} {lo hi : Nat} : Std.Slice.toList (Std.Roo.Sliceable.mkSlice xs (lo<...hi)) = List.drop (lo + 1) (List.take hi xs.toList)

@[simp]

theorem Array.toArray_mkSlice_roo {α : Type u_1} {xs : Array α} {lo hi : Nat} : Std.Slice.toArray (Std.Roo.Sliceable.mkSlice xs (lo<...hi)) = xs.extract (lo + 1) hi

@[simp]

theorem Array.size_mkSlice_roo {α : Type u_1} {xs : Array α} {lo hi : Nat} : Std.Slice.size (Std.Roo.Sliceable.mkSlice xs (lo<...hi)) = min hi xs.size - (lo + 1)

@[simp]

theorem Array.array_mkSlice_roc {α : Type u_1} {xs : Array α} {lo hi : Nat} : (Std.Roc.Sliceable.mkSlice xs (lo<...=hi)).array = xs

@[simp]

theorem Array.start_mkSlice_roc {α : Type u_1} {xs : Array α} {lo hi : Nat} : (Std.Roc.Sliceable.mkSlice xs (lo<...=hi)).start = min (lo + 1) (min (hi + 1) xs.size)

@[simp]

theorem Array.stop_mkSlice_roc {α : Type u_1} {xs : Array α} {lo hi : Nat} : (Std.Roc.Sliceable.mkSlice xs (lo<...=hi)).stop = min (hi + 1) xs.size

theorem Array.mkSlice_roc_eq_mkSlice_roo {α : Type u_1} {xs : Array α} {lo hi : Nat} : Std.Roc.Sliceable.mkSlice xs (lo<...=hi) = Std.Roo.Sliceable.mkSlice xs (lo<...hi + 1)

theorem Array.mkSlice_roc_eq_mkSlice_rco {α : Type u_1} {xs : Array α} {lo hi : Nat} : Std.Roc.Sliceable.mkSlice xs (lo<...=hi) = Std.Rco.Sliceable.mkSlice xs (lo + 1...hi + 1)

theorem Array.mkSlice_roc_eq_mkSlice_roo_min {α : Type u_1} {xs : Array α} {lo hi : Nat} : Std.Roc.Sliceable.mkSlice xs (lo<...=hi) = Std.Rco.Sliceable.mkSlice xs (min (lo + 1) (min (hi + 1) xs.size)...min (hi + 1) xs.size)

@[simp]

theorem Array.toList_mkSlice_roc {α : Type u_1} {xs : Array α} {lo hi : Nat} : Std.Slice.toList (Std.Roc.Sliceable.mkSlice xs (lo<...=hi)) = List.drop (lo + 1) (List.take (hi + 1) xs.toList)

@[simp]

theorem Array.toArray_mkSlice_roc {α : Type u_1} {xs : Array α} {lo hi : Nat} : Std.Slice.toArray (Std.Roc.Sliceable.mkSlice xs (lo<...=hi)) = xs.extract (lo + 1) (hi + 1)

@[simp]

theorem Array.size_mkSlice_roc {α : Type u_1} {xs : Array α} {lo hi : Nat} : Std.Slice.size (Std.Roc.Sliceable.mkSlice xs (lo<...=hi)) = min (hi + 1) xs.size - (lo + 1)

@[simp]

theorem Array.array_mkSlice_roi {α : Type u_1} {xs : Array α} {lo : Nat} : (Std.Roi.Sliceable.mkSlice xs (lo<...*)).array = xs

@[simp]

theorem Array.start_mkSlice_roi {α : Type u_1} {xs : Array α} {lo : Nat} : (Std.Roi.Sliceable.mkSlice xs (lo<...*)).start = min (lo + 1) xs.size

@[simp]

theorem Array.stop_mkSlice_roi {α : Type u_1} {xs : Array α} {lo : Nat} : (Std.Roi.Sliceable.mkSlice xs (lo<...*)).stop = xs.size

theorem Array.mkSlice_roi_eq_mkSlice_rci {α : Type u_1} {xs : Array α} {lo : Nat} : Std.Roi.Sliceable.mkSlice xs (lo<...*) = Std.Rci.Sliceable.mkSlice xs (lo + 1...*)

theorem Array.mkSlice_roi_eq_mkSlice_roo {α : Type u_1} {xs : Array α} {lo : Nat} : Std.Roi.Sliceable.mkSlice xs (lo<...*) = Std.Roo.Sliceable.mkSlice xs (lo<...xs.size)

theorem Array.mkSlice_roi_eq_mkSlice_rco {α : Type u_1} {xs : Array α} {lo : Nat} : Std.Roi.Sliceable.mkSlice xs (lo<...*) = Std.Rco.Sliceable.mkSlice xs (lo + 1...xs.size)

theorem Array.mkSlice_roi_eq_mkSlice_roo_min {α : Type u_1} {xs : Array α} {lo : Nat} : Std.Roi.Sliceable.mkSlice xs (lo<...*) = Std.Rco.Sliceable.mkSlice xs (min (lo + 1) xs.size...xs.size)

@[simp]

theorem Array.toList_mkSlice_roi {α : Type u_1} {xs : Array α} {lo : Nat} : Std.Slice.toList (Std.Roi.Sliceable.mkSlice xs (lo<...*)) = List.drop (lo + 1) xs.toList

@[simp]

theorem Array.toArray_mkSlice_roi {α : Type u_1} {xs : Array α} {lo : Nat} : Std.Slice.toArray (Std.Roi.Sliceable.mkSlice xs (lo<...*)) = xs.drop (lo + 1)

@[simp]

theorem Array.size_mkSlice_roi {α : Type u_1} {xs : Array α} {lo : Nat} : Std.Slice.size (Std.Roi.Sliceable.mkSlice xs (lo<...*)) = xs.size - (lo + 1)

@[simp]

theorem Array.array_mkSlice_rio {α : Type u_1} {xs : Array α} {hi : Nat} : (Std.Rio.Sliceable.mkSlice xs *...hi).array = xs

@[simp]

theorem Array.start_mkSlice_rio {α : Type u_1} {xs : Array α} {hi : Nat} : (Std.Rio.Sliceable.mkSlice xs *...hi).start = 0

@[simp]

theorem Array.stop_mkSlice_rio {α : Type u_1} {xs : Array α} {hi : Nat} : (Std.Rio.Sliceable.mkSlice xs *...hi).stop = min hi xs.size

theorem Array.mkSlice_rio_eq_mkSlice_rco {α : Type u_1} {xs : Array α} {hi : Nat} : Std.Rio.Sliceable.mkSlice xs *...hi = Std.Rco.Sliceable.mkSlice xs (0...hi)

theorem Array.mkSlice_rio_eq_mkSlice_rio_min {α : Type u_1} {xs : Array α} {hi : Nat} : Std.Rio.Sliceable.mkSlice xs *...hi = Std.Rio.Sliceable.mkSlice xs *...min hi xs.size

@[simp]

theorem Array.toList_mkSlice_rio {α : Type u_1} {xs : Array α} {hi : Nat} : Std.Slice.toList (Std.Rio.Sliceable.mkSlice xs *...hi) = List.take hi xs.toList

@[simp]

theorem Array.toArray_mkSlice_rio {α : Type u_1} {xs : Array α} {hi : Nat} : Std.Slice.toArray (Std.Rio.Sliceable.mkSlice xs *...hi) = xs.extract 0 hi

@[simp]

theorem Array.size_mkSlice_rio {α : Type u_1} {xs : Array α} {hi : Nat} : Std.Slice.size (Std.Rio.Sliceable.mkSlice xs *...hi) = min hi xs.size

@[simp]

theorem Array.array_mkSlice_ric {α : Type u_1} {xs : Array α} {hi : Nat} : (Std.Ric.Sliceable.mkSlice xs *...=hi).array = xs

@[simp]

theorem Array.start_mkSlice_ric {α : Type u_1} {xs : Array α} {hi : Nat} : (Std.Ric.Sliceable.mkSlice xs *...=hi).start = 0

@[simp]

theorem Array.stop_mkSlice_ric {α : Type u_1} {xs : Array α} {hi : Nat} : (Std.Ric.Sliceable.mkSlice xs *...=hi).stop = min (hi + 1) xs.size

theorem Array.mkSlice_ric_eq_mkSlice_rio {α : Type u_1} {xs : Array α} {hi : Nat} : Std.Ric.Sliceable.mkSlice xs *...=hi = Std.Rio.Sliceable.mkSlice xs *...hi + 1

theorem Array.mkSlice_ric_eq_mkSlice_rco {α : Type u_1} {xs : Array α} {hi : Nat} : Std.Ric.Sliceable.mkSlice xs *...=hi = Std.Rco.Sliceable.mkSlice xs (0...hi + 1)

theorem Array.mkSlice_ric_eq_mkSlice_rio_min {α : Type u_1} {xs : Array α} {hi : Nat} : Std.Ric.Sliceable.mkSlice xs *...=hi = Std.Rio.Sliceable.mkSlice xs *...min (hi + 1) xs.size

@[simp]

theorem Array.toList_mkSlice_ric {α : Type u_1} {xs : Array α} {hi : Nat} : Std.Slice.toList (Std.Ric.Sliceable.mkSlice xs *...=hi) = List.take (hi + 1) xs.toList

@[simp]

theorem Array.toArray_mkSlice_ric {α : Type u_1} {xs : Array α} {hi : Nat} : Std.Slice.toArray (Std.Ric.Sliceable.mkSlice xs *...=hi) = xs.extract 0 (hi + 1)

@[simp]

theorem Array.size_mkSlice_ric {α : Type u_1} {xs : Array α} {hi : Nat} : Std.Slice.size (Std.Ric.Sliceable.mkSlice xs *...=hi) = min (hi + 1) xs.size

theorem Array.mkSlice_rii_eq_mkSlice_rci {α : Type u_1} {xs : Array α} : Std.Rii.Sliceable.mkSlice xs *...* = Std.Rci.Sliceable.mkSlice xs (0...*)

theorem Array.mkSlice_rii_eq_mkSlice_rio {α : Type u_1} {xs : Array α} : Std.Rii.Sliceable.mkSlice xs *...* = Std.Rio.Sliceable.mkSlice xs *...xs.size

theorem Array.mkSlice_rii_eq_mkSlice_rco {α : Type u_1} {xs : Array α} : Std.Rii.Sliceable.mkSlice xs *...* = Std.Rco.Sliceable.mkSlice xs (0...xs.size)

theorem Array.mkSlice_rii_eq_mkSlice_rio_min {α : Type u_1} {xs : Array α} : Std.Rii.Sliceable.mkSlice xs *...* = Std.Rio.Sliceable.mkSlice xs *...xs.size

@[simp]

theorem Array.toList_mkSlice_rii {α : Type u_1} {xs : Array α} : Std.Slice.toList (Std.Rii.Sliceable.mkSlice xs *...*) = xs.toList

@[simp]

theorem Array.toArray_mkSlice_rii {α : Type u_1} {xs : Array α} : Std.Slice.toArray (Std.Rii.Sliceable.mkSlice xs *...*) = xs

@[simp]

theorem Array.size_mkSlice_rii {α : Type u_1} {xs : Array α} : Std.Slice.size (Std.Rii.Sliceable.mkSlice xs *...*) = xs.size

@[simp]

theorem Array.array_mkSlice_rii {α : Type u_1} {xs : Array α} : (Std.Rii.Sliceable.mkSlice xs *...*).array = xs

@[simp]

theorem Array.start_mkSlice_rii {α : Type u_1} {xs : Array α} : (Std.Rii.Sliceable.mkSlice xs *...*).start = 0

@[simp]

theorem Array.stop_mkSlice_rii {α : Type u_1} {xs : Array α} : (Std.Rii.Sliceable.mkSlice xs *...*).stop = xs.size

@[simp]

theorem Subarray.toList_mkSlice_rco {α : Type u_1} {xs : Subarray α} {lo hi : Nat} : Std.Slice.toList (Std.Rco.Sliceable.mkSlice xs (lo...hi)) = List.drop lo (List.take hi (Std.Slice.toList xs))

@[simp]

theorem Subarray.toArray_mkSlice_rco {α : Type u_1} {xs : Subarray α} {lo hi : Nat} : Std.Slice.toArray (Std.Rco.Sliceable.mkSlice xs (lo...hi)) = (Std.Slice.toArray xs).extract lo hi

@[simp]

theorem Subarray.size_mkSlice_rco {α : Type u_1} {xs : Subarray α} {lo hi : Nat} : Std.Slice.size (Std.Rco.Sliceable.mkSlice xs (lo...hi)) = min hi (Std.Slice.size xs) - lo

theorem Subarray.mkSlice_rcc_eq_mkSlice_rco {α : Type u_1} {xs : Subarray α} {lo hi : Nat} : Std.Rcc.Sliceable.mkSlice xs (lo...=hi) = Std.Rco.Sliceable.mkSlice xs (lo...hi + 1)

@[simp]

theorem Subarray.toList_mkSlice_rcc {α : Type u_1} {xs : Subarray α} {lo hi : Nat} : Std.Slice.toList (Std.Rcc.Sliceable.mkSlice xs (lo...=hi)) = List.drop lo (List.take (hi + 1) (Std.Slice.toList xs))

@[simp]

theorem Subarray.toArray_mkSlice_rcc {α : Type u_1} {xs : Subarray α} {lo hi : Nat} : Std.Slice.toArray (Std.Rcc.Sliceable.mkSlice xs (lo...=hi)) = (Std.Slice.toArray xs).extract lo (hi + 1)

@[simp]

theorem Subarray.size_mkSlice_rcc {α : Type u_1} {xs : Subarray α} {lo hi : Nat} : Std.Slice.size (Std.Rcc.Sliceable.mkSlice xs (lo...=hi)) = min (hi + 1) (Std.Slice.size xs) - lo

theorem Subarray.mkSlice_rci_eq_mkSlice_rco {α : Type u_1} {xs : Subarray α} {lo : Nat} : Std.Rci.Sliceable.mkSlice xs (lo...*) = Std.Rco.Sliceable.mkSlice xs (lo...Std.Slice.size xs)

@[simp]

theorem Subarray.toList_mkSlice_rci {α : Type u_1} {xs : Subarray α} {lo : Nat} : Std.Slice.toList (Std.Rci.Sliceable.mkSlice xs (lo...*)) = List.drop lo (Std.Slice.toList xs)

@[simp]

theorem Subarray.toArray_mkSlice_rci {α : Type u_1} {xs : Subarray α} {lo : Nat} : Std.Slice.toArray (Std.Rci.Sliceable.mkSlice xs (lo...*)) = (Std.Slice.toArray xs).extract lo

@[simp]

theorem Subarray.size_mkSlice_rci {α : Type u_1} {xs : Subarray α} {lo : Nat} : Std.Slice.size (Std.Rci.Sliceable.mkSlice xs (lo...*)) = Std.Slice.size xs - lo

theorem Subarray.mkSlice_roc_eq_mkSlice_roo {α : Type u_1} {xs : Subarray α} {lo hi : Nat} : Std.Roc.Sliceable.mkSlice xs (lo<...=hi) = Std.Roo.Sliceable.mkSlice xs (lo<...hi + 1)

theorem Subarray.mkSlice_roo_eq_mkSlice_rco {α : Type u_1} {xs : Subarray α} {lo hi : Nat} : Std.Roo.Sliceable.mkSlice xs (lo<...hi) = Std.Rco.Sliceable.mkSlice xs (lo + 1...hi)

theorem Subarray.mkSlice_roc_eq_mkSlice_rco {α : Type u_1} {xs : Subarray α} {lo hi : Nat} : Std.Roc.Sliceable.mkSlice xs (lo<...=hi) = Std.Rco.Sliceable.mkSlice xs (lo + 1...hi + 1)

@[simp]

theorem Subarray.toList_mkSlice_roo {α : Type u_1} {xs : Subarray α} {lo hi : Nat} : Std.Slice.toList (Std.Roo.Sliceable.mkSlice xs (lo<...hi)) = List.drop (lo + 1) (List.take hi (Std.Slice.toList xs))

@[simp]

theorem Subarray.toArray_mkSlice_roo {α : Type u_1} {xs : Subarray α} {lo hi : Nat} : Std.Slice.toArray (Std.Roo.Sliceable.mkSlice xs (lo<...hi)) = (Std.Slice.toArray xs).extract (lo + 1) hi

@[simp]

theorem Subarray.size_mkSlice_roo {α : Type u_1} {xs : Subarray α} {lo hi : Nat} : Std.Slice.size (Std.Roo.Sliceable.mkSlice xs (lo<...hi)) = min hi (Std.Slice.size xs) - (lo + 1)

theorem Subarray.mkSlice_roc_eq_mkSlice_rcc {α : Type u_1} {xs : Subarray α} {lo hi : Nat} : Std.Roc.Sliceable.mkSlice xs (lo<...=hi) = Std.Rcc.Sliceable.mkSlice xs (lo + 1...=hi)

@[simp]

theorem Subarray.toList_mkSlice_roc {α : Type u_1} {xs : Subarray α} {lo hi : Nat} : Std.Slice.toList (Std.Roc.Sliceable.mkSlice xs (lo<...=hi)) = List.drop (lo + 1) (List.take (hi + 1) (Std.Slice.toList xs))

@[simp]

theorem Subarray.toArray_mkSlice_roc {α : Type u_1} {xs : Subarray α} {lo hi : Nat} : Std.Slice.toArray (Std.Roc.Sliceable.mkSlice xs (lo<...=hi)) = (Std.Slice.toArray xs).extract (lo + 1) (hi + 1)

@[simp]

theorem Subarray.size_mkSlice_roc {α : Type u_1} {xs : Subarray α} {lo hi : Nat} : Std.Slice.size (Std.Roc.Sliceable.mkSlice xs (lo<...=hi)) = min (hi + 1) (Std.Slice.size xs) - (lo + 1)

theorem Subarray.mkSlice_roi_eq_mkSlice_rci {α : Type u_1} {xs : Subarray α} {lo : Nat} : Std.Roi.Sliceable.mkSlice xs (lo<...*) = Std.Rci.Sliceable.mkSlice xs (lo + 1...*)

theorem Subarray.mkSlice_roi_eq_mkSlice_rco {α : Type u_1} {xs : Subarray α} {lo : Nat} : Std.Roi.Sliceable.mkSlice xs (lo<...*) = Std.Rco.Sliceable.mkSlice xs (lo + 1...Std.Slice.size xs)

@[simp]

theorem Subarray.toList_mkSlice_roi {α : Type u_1} {xs : Subarray α} {lo : Nat} : Std.Slice.toList (Std.Roi.Sliceable.mkSlice xs (lo<...*)) = List.drop (lo + 1) (Std.Slice.toList xs)

@[simp]

theorem Subarray.toArray_mkSlice_roi {α : Type u_1} {xs : Subarray α} {lo : Nat} : Std.Slice.toArray (Std.Roi.Sliceable.mkSlice xs (lo<...*)) = (Std.Slice.toArray xs).extract (lo + 1)

@[simp]

theorem Subarray.size_mkSlice_roi {α : Type u_1} {xs : Subarray α} {lo : Nat} : Std.Slice.size (Std.Roi.Sliceable.mkSlice xs (lo<...*)) = Std.Slice.size xs - (lo + 1)

theorem Subarray.mkSlice_ric_eq_mkSlice_rio {α : Type u_1} {xs : Subarray α} {hi : Nat} : Std.Ric.Sliceable.mkSlice xs *...=hi = Std.Rio.Sliceable.mkSlice xs *...hi + 1

theorem Subarray.mkSlice_rio_eq_mkSlice_rco {α : Type u_1} {xs : Subarray α} {hi : Nat} : Std.Rio.Sliceable.mkSlice xs *...hi = Std.Rco.Sliceable.mkSlice xs (0...hi)

theorem Subarray.mkSlice_ric_eq_mkSlice_rco {α : Type u_1} {xs : Subarray α} {hi : Nat} : Std.Ric.Sliceable.mkSlice xs *...=hi = Std.Rco.Sliceable.mkSlice xs (0...hi + 1)

@[simp]

theorem Subarray.toList_mkSlice_rio {α : Type u_1} {xs : Subarray α} {hi : Nat} : Std.Slice.toList (Std.Rio.Sliceable.mkSlice xs *...hi) = List.take hi (Std.Slice.toList xs)

@[simp]

theorem Subarray.toArray_mkSlice_rio {α : Type u_1} {xs : Subarray α} {hi : Nat} : Std.Slice.toArray (Std.Rio.Sliceable.mkSlice xs *...hi) = (Std.Slice.toArray xs).extract 0 hi

@[simp]

theorem Subarray.size_mkSlice_rio {α : Type u_1} {xs : Subarray α} {hi : Nat} : Std.Slice.size (Std.Rio.Sliceable.mkSlice xs *...hi) = min hi (Std.Slice.size xs)

theorem Subarray.mkSlice_ric_eq_mkSlice_rcc {α : Type u_1} {xs : Subarray α} {hi : Nat} : Std.Ric.Sliceable.mkSlice xs *...=hi = Std.Rcc.Sliceable.mkSlice xs (0...=hi)

@[simp]

theorem Subarray.toList_mkSlice_ric {α : Type u_1} {xs : Subarray α} {hi : Nat} : Std.Slice.toList (Std.Ric.Sliceable.mkSlice xs *...=hi) = List.take (hi + 1) (Std.Slice.toList xs)

@[simp]

theorem Subarray.toArray_mkSlice_ric {α : Type u_1} {xs : Subarray α} {hi : Nat} : Std.Slice.toArray (Std.Ric.Sliceable.mkSlice xs *...=hi) = (Std.Slice.toArray xs).extract 0 (hi + 1)

@[simp]

theorem Subarray.size_mkSlice_ric {α : Type u_1} {xs : Subarray α} {hi : Nat} : Std.Slice.size (Std.Ric.Sliceable.mkSlice xs *...=hi) = min (hi + 1) (Std.Slice.size xs)

@[simp]

theorem Subarray.mkSlice_rii {α : Type u_1} {xs : Subarray α} : Std.Rii.Sliceable.mkSlice xs *...* = xs