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 xs.internalRepresentation.stop with | some stop => List.take stop xs.internalRepresentation.list | none => xs.internalRepresentation.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

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

@[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

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

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)

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)

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)

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)

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

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

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.size_mkSlice_rco {α : Type u_1} {xs : ListSlice α} {lo hi : Nat} : Std.Slice.size (Std.Rco.Sliceable.mkSlice xs (lo...hi)) = min hi (Std.Slice.size xs) - lo

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.size_mkSlice_rcc {α : Type u_1} {xs : ListSlice α} {lo hi : Nat} : Std.Slice.size (Std.Rcc.Sliceable.mkSlice xs (lo...=hi)) = min (hi + 1) (Std.Slice.size xs) - lo

@[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

@[simp]

theorem ListSlice.size_mkSlice_rci {α : Type u_1} {xs : ListSlice α} {lo : Nat} : Std.Slice.size (Std.Rci.Sliceable.mkSlice xs (lo...*)) = Std.Slice.size xs - 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))

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.size_mkSlice_roo {α : Type u_1} {xs : ListSlice α} {lo hi : Nat} : Std.Slice.size (Std.Roo.Sliceable.mkSlice xs (lo<...hi)) = min hi (Std.Slice.size xs) - (lo + 1)

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)

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)

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.size_mkSlice_roc {α : Type u_1} {xs : ListSlice α} {lo hi : Nat} : Std.Slice.size (Std.Roc.Sliceable.mkSlice xs (lo<...=hi)) = min (hi + 1) (Std.Slice.size xs) - (lo + 1)

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.size_mkSlice_roi {α : Type u_1} {xs : ListSlice α} {lo : Nat} : Std.Slice.size (Std.Roi.Sliceable.mkSlice xs (lo<...*)) = Std.Slice.size xs - (lo + 1)

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.size_mkSlice_rio {α : Type u_1} {xs : ListSlice α} {hi : Nat} : Std.Slice.size (Std.Rio.Sliceable.mkSlice xs *...hi) = min hi (Std.Slice.size xs)

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

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.size_mkSlice_ric {α : Type u_1} {xs : ListSlice α} {hi : Nat} : Std.Slice.size (Std.Ric.Sliceable.mkSlice xs *...=hi) = min (hi + 1) (Std.Slice.size xs)

@[simp]

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