chore(*): drop porting notes about List.nthLe → List.get (#12203)

Mathlib/Algebra/BigOperators/Fin.lean

@@ -494,7 +494,6 @@ theorem prod_ofFn {n : ℕ} {f : Fin n → α} : (ofFn f).prod = ∏ i, f i := b
 
 end CommMonoid
 
--- Porting note: Statement had deprecated `L.nthLe i i.is_lt` instead of `L.get i`.
 @[to_additive]
 theorem alternatingProd_eq_finset_prod {G : Type*} [CommGroup G] :
     ∀ (L : List G), alternatingProd L = ∏ i : Fin L.length, L.get i ^ (-1 : ℤ) ^ (i : ℕ)

Mathlib/Combinatorics/Young/YoungDiagram.lean

@@ -413,7 +413,6 @@ def rowLens (μ : YoungDiagram) : List ℕ :=
   (List.range <| μ.colLen 0).map μ.rowLen
 #align young_diagram.row_lens YoungDiagram.rowLens
 
--- Porting note: use `List.get` instead of `List.nthLe` because it has been deprecated
 @[simp]
 theorem get_rowLens {μ : YoungDiagram} {i} :
     μ.rowLens.get i = μ.rowLen i := by simp only [rowLens, List.get_range, List.get_map]
@@ -459,7 +458,6 @@ protected def cellsOfRowLens : List ℕ → Finset (ℕ × ℕ)
         (Embedding.prodMap ⟨_, Nat.succ_injective⟩ (Embedding.refl ℕ))
 #align young_diagram.cells_of_row_lens YoungDiagram.cellsOfRowLens
 
--- Porting note: use `List.get` instead of `List.nthLe` because it has been deprecated
 protected theorem mem_cellsOfRowLens {w : List ℕ} {c : ℕ × ℕ} :
     c ∈ YoungDiagram.cellsOfRowLens w ↔ ∃ h : c.fst < w.length, c.snd < w.get ⟨c.fst, h⟩  := by
   induction' w with w_hd w_tl w_ih generalizing c <;> rw [YoungDiagram.cellsOfRowLens]
@@ -470,10 +468,8 @@ protected theorem mem_cellsOfRowLens {w : List ℕ} {c : ℕ × ℕ} :
     · simp [w_ih, -Finset.singleton_product, Nat.succ_lt_succ_iff]
 #align young_diagram.mem_cells_of_row_lens YoungDiagram.mem_cellsOfRowLens
 
--- Porting note: use `List.get` instead of `List.nthLe` because it has been deprecated
 /-- Young diagram from a sorted list -/
-def ofRowLens (w : List ℕ) (hw : w.Sorted (· ≥ ·)) : YoungDiagram
-    where
+def ofRowLens (w : List ℕ) (hw : w.Sorted (· ≥ ·)) : YoungDiagram where
   cells := YoungDiagram.cellsOfRowLens w
   isLowerSet := by
     rintro ⟨i2, j2⟩ ⟨i1, j1⟩ ⟨hi : i1 ≤ i2, hj : j1 ≤ j2⟩ hcell
@@ -489,7 +485,6 @@ def ofRowLens (w : List ℕ) (hw : w.Sorted (· ≥ ·)) : YoungDiagram
         · exact List.pairwise_iff_get.mp hw _ _ h
 #align young_diagram.of_row_lens YoungDiagram.ofRowLens
 
--- Porting note: use `List.get` instead of `List.nthLe` because it has been deprecated
 theorem mem_ofRowLens {w : List ℕ} {hw : w.Sorted (· ≥ ·)} {c : ℕ × ℕ} :
     c ∈ ofRowLens w hw ↔ ∃ h : c.fst < w.length, c.snd < w.get ⟨c.fst, h⟩ :=
   YoungDiagram.mem_cellsOfRowLens
@@ -503,7 +498,6 @@ theorem rowLens_length_ofRowLens {w : List ℕ} {hw : w.Sorted (· ≥ ·)} (hpo
   exact ⟨not_false, fun n hn => ⟨hn, hpos _ (List.get_mem _ _ hn)⟩⟩
 #align young_diagram.row_lens_length_of_row_lens YoungDiagram.rowLens_length_ofRowLens
 
--- Porting note: use `List.get` instead of `List.nthLe` because it has been deprecated
 /-- The length of the `i`th row in `ofRowLens w hw` is the `i`th entry of `w` -/
 theorem rowLen_ofRowLens {w : List ℕ} {hw : w.Sorted (· ≥ ·)} (i : Fin w.length) :
     (ofRowLens w hw).rowLen i = w.get i := by
@@ -520,7 +514,6 @@ theorem ofRowLens_to_rowLens_eq_self {μ : YoungDiagram} : ofRowLens _ (rowLens_
 /-- The right_inv direction of the equivalence -/
 theorem rowLens_ofRowLens_eq_self {w : List ℕ} {hw : w.Sorted (· ≥ ·)} (hpos : ∀ x ∈ w, 0 < x) :
     (ofRowLens w hw).rowLens = w :=
-  -- Porting note: golf by `List.get`
   List.ext_get (rowLens_length_ofRowLens hpos) fun i _ h₂ =>
     get_rowLens.trans <| rowLen_ofRowLens ⟨i, h₂⟩
 #align young_diagram.row_lens_of_row_lens_eq_self YoungDiagram.rowLens_ofRowLens_eq_self

Mathlib/Data/List/Indexes.lean

@@ -203,12 +203,11 @@ theorem nthLe_mapIdx {α β} (l : List α) (f : ℕ → α → β) (i : ℕ) (h
   simp [mapIdx_eq_enum_map, enum_eq_zip_range]
 #align list.nth_le_map_with_index List.nthLe_mapIdx
 
--- Porting note: Changed the type to use `List.get` instead of deprecated `List.nthLe`.
 theorem mapIdx_eq_ofFn {α β} (l : List α) (f : ℕ → α → β) :
     l.mapIdx f = ofFn fun i : Fin l.length ↦ f (i : ℕ) (l.get i) := by
-  induction' l with hd tl IH generalizing f
-  · rfl
-  · simp [IH]
+  induction l generalizing f with
+  | nil => rfl
+  | cons _ _ IH => simp [IH]
 #align list.map_with_index_eq_of_fn List.mapIdx_eq_ofFn
 
 end MapIdx

Mathlib/LinearAlgebra/Matrix/Transvection.lean

@@ -373,8 +373,7 @@ theorem listTransvecCol_mul_last_row_drop (i : Sum (Fin r) Unit) {k : ℕ} (hk :
   refine' Nat.decreasingInduction' _ hk _
   · intro n hn _ IH
     have hn' : n < (listTransvecCol M).length := by simpa [listTransvecCol] using hn
-    -- Porting note: after changing from `nthLe` to `get`, we need to provide all arguments
-    rw [← @List.cons_get_drop_succ _ _ ⟨n, hn'⟩]
+    rw [List.drop_eq_get_cons hn']
     simpa [listTransvecCol, Matrix.mul_assoc]
   · simp only [listTransvecCol, List.length_ofFn, le_refl, List.drop_eq_nil_of_le, List.prod_nil,
       Matrix.one_mul]
@@ -402,8 +401,7 @@ theorem listTransvecCol_mul_last_col (hM : M (inr unit) (inr unit) ≠ 0) (i : F
   · intro n hn hk IH
     have hn' : n < (listTransvecCol M).length := by simpa [listTransvecCol] using hn
     let n' : Fin r := ⟨n, hn⟩
-    -- Porting note: after changing from `nthLe` to `get`, we need to provide all arguments
-    rw [← @List.cons_get_drop_succ _ _ ⟨n, hn'⟩]
+    rw [List.drop_eq_get_cons hn']
     have A :
       (listTransvecCol M).get ⟨n, hn'⟩ =
         transvection (inl n') (inr unit) (-M (inl n') (inr unit) / M (inr unit) (inr unit)) :=

Mathlib/Order/JordanHolder.lean

@@ -227,10 +227,8 @@ theorem toList_injective : Function.Injective (@CompositionSeries.toList X _ _)
     Nat.succ_injective
       ((List.length_ofFn s₁).symm.trans <| (congr_arg List.length h).trans <| List.length_ofFn s₂)
   apply ext_fun h₁
-  -- Porting note: `List.nthLe_ofFn` has been deprecated but `List.get_ofFn` has a
-  --               different type, so we do golf here.
-  exact congr_fun <|
-          List.ofFn_injective <| h.trans <| List.ofFn_congr (congr_arg Nat.succ h₁).symm _
+  exact congr_fun <| List.ofFn_injective <| h.trans <|
+    List.ofFn_congr (congr_arg Nat.succ h₁).symm _
 #align composition_series.to_list_injective CompositionSeries.toList_injective
 
 theorem chain'_toList (s : CompositionSeries X) : List.Chain' IsMaximal s.toList :=