chore(Order/JordanHolder): List.nthLe → List.get (#12208)

Mathlib/Order/JordanHolder.lean

@@ -262,11 +262,8 @@ theorem mem_toList {s : CompositionSeries X} {x : X} : x ∈ s.toList ↔ x ∈
 def ofList (l : List X) (hl : l ≠ []) (hc : List.Chain' IsMaximal l) : CompositionSeries X
     where
   length := l.length - 1
-  series i :=
-    l.nthLe i
-      (by
-        conv_rhs => rw [← tsub_add_cancel_of_le (Nat.succ_le_of_lt (List.length_pos_of_ne_nil hl))]
-        exact i.2)
+  series i := l.get <| i.cast <|
+    tsub_add_cancel_of_le (Nat.succ_le_of_lt (List.length_pos_of_ne_nil hl))
   step' := fun ⟨i, hi⟩ => List.chain'_iff_get.1 hc i hi
 #align composition_series.of_list CompositionSeries.ofList
 
@@ -280,8 +277,7 @@ theorem ofList_toList (s : CompositionSeries X) :
   refine' ext_fun _ _
   · rw [length_ofList, length_toList, Nat.add_one_sub_one]
   · rintro ⟨i, hi⟩
-    -- Porting note: Was `dsimp [ofList, toList]; rw [List.nthLe_ofFn']`.
-    simp [ofList, toList, -List.ofFn_succ]
+    simp [ofList, toList]
 #align composition_series.of_list_to_list CompositionSeries.ofList_toList
 
 @[simp]