feat: port Data.List.Sublists (#1494)

Co-authored-by: qawbecrdtey <qawbecrdtey@kaist.ac.kr>
Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>

Mathlib.lean

@@ -280,6 +280,7 @@ import Mathlib.Data.List.Range
 import Mathlib.Data.List.Rdrop
 import Mathlib.Data.List.Sections
 import Mathlib.Data.List.Sigma
+import Mathlib.Data.List.Sublists
 import Mathlib.Data.List.TFAE
 import Mathlib.Data.List.Zip
 import Mathlib.Data.Multiset.Basic

Mathlib/Data/List/Defs.lean

@@ -215,14 +215,6 @@ end mapIdxM
 #align list.sublists List.sublists
 #align list.forall₂ List.Forall₂
 
-/-- Definition of a `sublists` function with an explicit list construction function
-    Used in `Data.Lists.Sublists`: TODO: move there when ported.
--/
-def sublistsAux₁ : List α → (List α → List β) → List β
-  | [], _ => []
-  | a :: l, f => f [a] ++ sublistsAux₁ l fun ys => f ys ++ f (a :: ys)
-#align list.sublists_aux₁ List.sublistsAux₁
-
 /-- `l.all₂ p` is equivalent to `∀ a ∈ l, p a`, but unfolds directly to a conjunction, i.e.
 `list.all₂ p [0, 1, 2] = p 0 ∧ p 1 ∧ p 2`. -/
 @[simp]

Mathlib/Data/List/Range.lean

@@ -359,6 +359,10 @@ theorem get_finRange {n : ℕ} {i : ℕ} (h) :
     (finRange n).get ⟨i, h⟩ = ⟨i, length_finRange n ▸ h⟩ := by
   simp only [finRange, get_range, get_pmap]
 
+--Porting note: new theorem
+theorem finRange_map_get (l : List α) : (finRange l.length).map l.get = l :=
+  List.ext_get (by simp) (by simp)
+
 set_option linter.deprecated false in
 @[simp]
 theorem nthLe_finRange {n : ℕ} {i : ℕ} (h) :