chore(Data/Set/List): nthLe -> get migration (#12398)

Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

Mathlib/Data/Set/List.lean

@@ -22,9 +22,8 @@ variable {α β : Type*} (l : List α)
 namespace Set
 
 theorem range_list_map (f : α → β) : range (map f) = { l | ∀ x ∈ l, x ∈ range f } := by
-  refine'
-    antisymm (range_subset_iff.2 fun l => forall_mem_map_iff.2 fun y _ => mem_range_self _)
-      fun l hl => _
+  refine antisymm (range_subset_iff.2 fun l => forall_mem_map_iff.2 fun y _ => mem_range_self _)
+      fun l hl => ?_
   induction' l with a l ihl; · exact ⟨[], rfl⟩
   rcases ihl fun x hx => hl x <| subset_cons _ _ hx with ⟨l, rfl⟩
   rcases hl a (mem_cons_self _ _) with ⟨a, rfl⟩
@@ -36,14 +35,14 @@ theorem range_list_map_coe (s : Set α) : range (map ((↑) : s → α)) = { l |
 #align set.range_list_map_coe Set.range_list_map_coe
 
 @[simp]
-theorem range_list_nthLe : (range fun k : Fin l.length => l.nthLe k k.2) = { x | x ∈ l } := by
+theorem range_list_get : range l.get = { x | x ∈ l } := by
   ext x
-  rw [mem_setOf_eq, mem_iff_get]
-  exact ⟨fun ⟨⟨n, h₁⟩, h₂⟩ => ⟨⟨n, h₁⟩, h₂⟩, fun ⟨⟨n, h₁⟩, h₂⟩ => ⟨⟨n, h₁⟩, h₂⟩⟩
-#align set.range_list_nth_le Set.range_list_nthLe
+  rw [mem_setOf_eq, mem_iff_get, mem_range]
+#align set.range_list_nth_le Set.range_list_get
+@[deprecated] alias range_list_nthLe := range_list_get -- 2024-04-22
 
 theorem range_list_get? : range l.get? = insert none (some '' { x | x ∈ l }) := by
-  rw [← range_list_nthLe, ← range_comp]
+  rw [← range_list_get, ← range_comp]
   refine' (range_subset_iff.2 fun n => _).antisymm (insert_subset_iff.2 ⟨_, _⟩)
   exacts [(le_or_lt l.length n).imp get?_eq_none.2 (fun hlt => ⟨⟨_, hlt⟩, (get?_eq_get hlt).symm⟩),
     ⟨_, get?_eq_none.2 le_rfl⟩, range_subset_iff.2 fun k => ⟨_, get?_eq_get _⟩]