instance ListSlice.instLawfulSliceSizeTakeListIteratorIdListSliceData {α : Type u_1} : Std.Slice.LawfulSliceSize (Std.Slice.Internal.ListSliceData α)

theorem ListSlice.toList_eq {α : Type u_1} {xs : ListSlice α} : Std.Slice.toList xs = match Std.Slice.Internal.ListSliceData.stop α with | some stop => List.take stop Std.Slice.Internal.ListSliceData.list | none => Std.Slice.Internal.ListSliceData.list

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem List.toList_mkSlice_rci_eq_toList_mkSlice_rco {α : Type u_1} {xs : List α} {lo : Nat} : Std.Slice.toList (Std.Rci.Sliceable.mkSlice xs lo...*) = Std.Slice.toList (Std.Rco.Sliceable.mkSlice xs lo...xs.length)

theorem List.toArray_mkSlice_rci_eq_toArray_mkSlice_rco {α : Type u_1} {xs : List α} {lo : Nat} : Std.Slice.toArray (Std.Rci.Sliceable.mkSlice xs lo...*) = Std.Slice.toArray (Std.Rco.Sliceable.mkSlice xs lo...xs.length)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem List.toList_mkSlice_roi_eq_toList_mkSlice_roo {α : Type u_1} {xs : List α} {lo : Nat} : Std.Slice.toList (Std.Roi.Sliceable.mkSlice xs lo<...*) = Std.Slice.toList (Std.Roo.Sliceable.mkSlice xs lo<...xs.length)

theorem List.toArray_mkSlice_roi_eq_toArray_mkSlice_roo {α : Type u_1} {xs : List α} {lo : Nat} : Std.Slice.toArray (Std.Roi.Sliceable.mkSlice xs lo<...*) = Std.Slice.toArray (Std.Roo.Sliceable.mkSlice xs lo<...xs.length)

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

theorem List.toArray_mkSlice_roi_eq_toArray_mkSlice_rco {α : Type u_1} {xs : List α} {lo : Nat} : Std.Slice.toArray (Std.Roi.Sliceable.mkSlice xs lo<...*) = Std.Slice.toArray (Std.Rco.Sliceable.mkSlice xs (lo + 1)...xs.length)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem List.toList_mkSlice_rii_eq_toList_mkSlice_rco {α : Type u_1} {xs : List α} : Std.Slice.toList (Std.Rii.Sliceable.mkSlice xs *...*) = Std.Slice.toList (Std.Rco.Sliceable.mkSlice xs 0...xs.length)

theorem List.toArray_mkSlice_rii_eq_toArray_mkSlice_rco {α : Type u_1} {xs : List α} : Std.Slice.toArray (Std.Rii.Sliceable.mkSlice xs *...*) = Std.Slice.toArray (Std.Rco.Sliceable.mkSlice xs 0...xs.length)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem ListSlice.toList_mkSlice_rco {α : Type u_1} {xs : ListSlice α} {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 ListSlice.toArray_mkSlice_rco {α : Type u_1} {xs : ListSlice α} {lo hi : Nat} : Std.Slice.toArray (Std.Rco.Sliceable.mkSlice xs lo...hi) = (Std.Slice.toArray xs).extract lo hi

@[simp]

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

@[simp]

theorem ListSlice.toList_mkSlice_rcc {α : Type u_1} {xs : ListSlice α} {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 ListSlice.toArray_mkSlice_rcc {α : Type u_1} {xs : ListSlice α} {lo hi : Nat} : Std.Slice.toArray (Std.Rcc.Sliceable.mkSlice xs lo...=hi) = (Std.Slice.toArray xs).extract lo (hi + 1)

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

theorem ListSlice.toList_mkSlice_roo {α : Type u_1} {xs : ListSlice α} {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 ListSlice.toArray_mkSlice_roo {α : Type u_1} {xs : ListSlice α} {lo hi : Nat} : Std.Slice.toArray (Std.Roo.Sliceable.mkSlice xs lo<...hi) = (Std.Slice.toArray xs).extract (lo + 1) hi

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem ListSlice.toList_mkSlice_roc {α : Type u_1} {xs : ListSlice α} {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 ListSlice.toArray_mkSlice_roc {α : Type u_1} {xs : ListSlice α} {lo hi : Nat} : Std.Slice.toArray (Std.Roc.Sliceable.mkSlice xs lo<...=hi) = (Std.Slice.toArray xs).extract (lo + 1) (hi + 1)

@[simp]

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

theorem ListSlice.toList_mkSlice_roi_eq_toList_mkSlice_roo {α : Type u_1} {xs : ListSlice α} {lo : Nat} : Std.Slice.toList (Std.Roi.Sliceable.mkSlice xs lo<...*) = Std.Slice.toList (Std.Roo.Sliceable.mkSlice xs lo<...Std.Slice.size xs)

theorem ListSlice.toArray_mkSlice_roi_eq_toArray_mkSlice_roo {α : Type u_1} {xs : ListSlice α} {lo : Nat} : Std.Slice.toArray (Std.Roi.Sliceable.mkSlice xs lo<...*) = Std.Slice.toArray (Std.Roo.Sliceable.mkSlice xs lo<...Std.Slice.size xs)

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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