feat(List/rotate): migrate to get, new lemmas, golf (#12171)

- Add `List.Nodup.rotate_congr_iff`, `List.cyclicPermutations_ne_nil`,
  `List.head?_cyclicPermutations`, `List.head_cyclicPermutations`,
  `List.cyclicPermutations_injective`, `List.cyclicPermutations_inj`.
- Change `List.nthLe_cyclicPermutations` to
  `List.get_cyclicPermutations`. While the old lemma wasn't deprecated
  during port, the definition `List.nthLe` was,
  so I think that we can drop the lemma without a deprecation period.

Mathlib/Data/List/Rotate.lean

@@ -381,34 +381,26 @@ theorem map_rotate {β : Type*} (f : α → β) (l : List α) (n : ℕ) :
     · simp [hn]
 #align list.map_rotate List.map_rotate
 
-set_option linter.deprecated false in
-theorem Nodup.rotate_eq_self_iff {l : List α} (hl : l.Nodup) {n : ℕ} :
-    l.rotate n = l ↔ n % l.length = 0 ∨ l = [] := by
-  constructor
-  · intro h
-    rcases l.length.zero_le.eq_or_lt with hl' | hl'
-    · simp [← length_eq_zero, ← hl']
-    left
-    rw [nodup_iff_nthLe_inj] at hl
-    refine' hl _ _ (mod_lt _ hl') hl' _
-    rw [← nthLe_rotate' _ n]
-    simp_rw [h, Nat.sub_add_cancel (mod_lt _ hl').le, mod_self]
-  · rintro (h | h)
-    · rw [← rotate_mod, h]
-      exact rotate_zero l
-    · simp [h]
-#align list.nodup.rotate_eq_self_iff List.Nodup.rotate_eq_self_iff
-
-set_option linter.deprecated false in
 theorem Nodup.rotate_congr {l : List α} (hl : l.Nodup) (hn : l ≠ []) (i j : ℕ)
     (h : l.rotate i = l.rotate j) : i % l.length = j % l.length := by
-  have hi : i % l.length < l.length := mod_lt _ (length_pos_of_ne_nil hn)
-  have hj : j % l.length < l.length := mod_lt _ (length_pos_of_ne_nil hn)
-  refine' (nodup_iff_nthLe_inj.mp hl) _ _ hi hj _
-  rw [← nthLe_rotate' l i, ← nthLe_rotate' l j]
-  simp [Nat.sub_add_cancel, hi.le, hj.le, h]
+  rw [← rotate_mod l i, ← rotate_mod l j] at h
+  simpa only [head?_rotate, mod_lt, length_pos_of_ne_nil hn, get?_eq_get, Option.some_inj,
+    hl.get_inj_iff, Fin.ext_iff] using congr_arg head? h
 #align list.nodup.rotate_congr List.Nodup.rotate_congr
 
+theorem Nodup.rotate_congr_iff {l : List α} (hl : l.Nodup) {i j : ℕ} :
+    l.rotate i = l.rotate j ↔ i % l.length = j % l.length ∨ l = [] := by
+  rcases eq_or_ne l [] with rfl | hn
+  · simp
+  · simp only [hn, or_false]
+    refine ⟨hl.rotate_congr hn _ _, fun h ↦ ?_⟩
+    rw [← rotate_mod, h, rotate_mod]
+
+theorem Nodup.rotate_eq_self_iff {l : List α} (hl : l.Nodup) {n : ℕ} :
+    l.rotate n = l ↔ n % l.length = 0 ∨ l = [] := by
+  rw [← zero_mod, ← hl.rotate_congr_iff, rotate_zero]
+#align list.nodup.rotate_eq_self_iff List.Nodup.rotate_eq_self_iff
+
 section IsRotated
 
 variable (l l' : List α)
@@ -548,7 +540,7 @@ theorem IsRotated.map {β : Type*} {l₁ l₂ : List α} (h : l₁ ~r l₂) (f :
 /-- List of all cyclic permutations of `l`.
 The `cyclicPermutations` of a nonempty list `l` will always contain `List.length l` elements.
 This implies that under certain conditions, there are duplicates in `List.cyclicPermutations l`.
-The `n`th entry is equal to `l.rotate n`, proven in `List.nthLe_cyclicPermutations`.
+The `n`th entry is equal to `l.rotate n`, proven in `List.get_cyclicPermutations`.
 The proof that every cyclic permutant of `l` is in the list is `List.mem_cyclicPermutations_iff`.
 
      cyclicPermutations [1, 2, 3, 2, 4] =
@@ -584,109 +576,103 @@ theorem length_cyclicPermutations_of_ne_nil (l : List α) (h : l ≠ []) :
     length (cyclicPermutations l) = length l := by simp [cyclicPermutations_of_ne_nil _ h]
 #align list.length_cyclic_permutations_of_ne_nil List.length_cyclicPermutations_of_ne_nil
 
-set_option linter.deprecated false in
 @[simp]
-theorem nthLe_cyclicPermutations (l : List α) (n : ℕ) (hn : n < length (cyclicPermutations l)) :
-    nthLe (cyclicPermutations l) n hn = l.rotate n := by
-  obtain rfl | h := eq_or_ne l []
-  · simp
-  · rw [length_cyclicPermutations_of_ne_nil _ h] at hn
-    simp [dropLast_eq_take, cyclicPermutations_of_ne_nil _ h, nthLe_take',
-      rotate_eq_drop_append_take hn.le]
-#align list.nth_le_cyclic_permutations List.nthLe_cyclicPermutations
+theorem cyclicPermutations_ne_nil : ∀ l : List α, cyclicPermutations l ≠ []
+  | a::l, h => by simpa using congr_arg length h
 
-set_option linter.deprecated false in
-theorem mem_cyclicPermutations_self (l : List α) : l ∈ cyclicPermutations l := by
-  cases' l with x l
-  · simp
-  · rw [mem_iff_nthLe]
-    refine' ⟨0, by simp, _⟩
-    simp
-#align list.mem_cyclic_permutations_self List.mem_cyclicPermutations_self
+@[simp]
+theorem get_cyclicPermutations (l : List α) (n : Fin (length (cyclicPermutations l))) :
+    (cyclicPermutations l).get n = l.rotate n := by
+  cases l with
+  | nil => simp
+  | cons a l =>
+    simp only [cyclicPermutations_cons, get_dropLast, get_zipWith, get_tails, get_inits]
+    rw [rotate_eq_drop_append_take (by simpa using n.2.le)]
+#align list.nth_le_cyclic_permutations List.get_cyclicPermutations
+
+@[simp]
+theorem head?_cyclicPermutations (l : List α) : (cyclicPermutations l).head? = l := by
+  have h : 0 < length (cyclicPermutations l) := length_pos_of_ne_nil (cyclicPermutations_ne_nil _)
+  simp_rw [← get_zero h, get_cyclicPermutations, rotate_zero]
+
+@[simp]
+theorem head_cyclicPermutations (l : List α) :
+    (cyclicPermutations l).head (cyclicPermutations_ne_nil l) = l := by
+  rw [← Option.some_inj, ← head?_eq_head, head?_cyclicPermutations]
+
+theorem cyclicPermutations_injective : Function.Injective (@cyclicPermutations α) := fun l l' h ↦ by
+  simpa using congr_arg head? h
+
+@[simp]
+theorem cyclicPermutations_inj {l l' : List α} :
+    cyclicPermutations l = cyclicPermutations l' ↔ l = l' :=
+  cyclicPermutations_injective.eq_iff
 
-set_option linter.deprecated false in
 theorem length_mem_cyclicPermutations (l : List α) (h : l' ∈ cyclicPermutations l) :
     length l' = length l := by
-  obtain ⟨k, hk, rfl⟩ := nthLe_of_mem h
+  obtain ⟨k, hk, rfl⟩ := get_of_mem h
   simp
 #align list.length_mem_cyclic_permutations List.length_mem_cyclicPermutations
 
-set_option linter.deprecated false in
+theorem mem_cyclicPermutations_self (l : List α) : l ∈ cyclicPermutations l := by
+  simpa using head_mem (cyclicPermutations_ne_nil l)
+#align list.mem_cyclic_permutations_self List.mem_cyclicPermutations_self
+
 @[simp]
-theorem mem_cyclicPermutations_iff {l l' : List α} : l ∈ cyclicPermutations l' ↔ l ~r l' := by
-  constructor
-  · intro h
-    obtain ⟨k, hk, rfl⟩ := nthLe_of_mem h
-    simp
-  · intro h
-    obtain ⟨k, rfl⟩ := h.symm
-    rw [mem_iff_nthLe]
-    simp only [exists_prop, nthLe_cyclicPermutations]
-    cases' l' with x l
+theorem cyclicPermutations_rotate (l : List α) (k : ℕ) :
+    (l.rotate k).cyclicPermutations = l.cyclicPermutations.rotate k := by
+  have : (l.rotate k).cyclicPermutations.length = length (l.cyclicPermutations.rotate k) := by
+    cases l
     · simp
-    · refine' ⟨k % length (x :: l), _, rotate_mod _ _⟩
-      simpa using Nat.mod_lt _ (zero_lt_succ _)
+    · rw [length_cyclicPermutations_of_ne_nil] <;> simp
+  refine' ext_get this fun n hn hn' => _
+  rw [get_rotate, get_cyclicPermutations, rotate_rotate, ← rotate_mod, Nat.add_comm]
+  cases l <;> simp
+#align list.cyclic_permutations_rotate List.cyclicPermutations_rotate
+
+@[simp]
+theorem mem_cyclicPermutations_iff : l ∈ cyclicPermutations l' ↔ l ~r l' := by
+  constructor
+  · simp_rw [mem_iff_get, get_cyclicPermutations]
+    rintro ⟨k, rfl⟩
+    exact .forall _ _
+  · rintro ⟨k, rfl⟩
+    rw [cyclicPermutations_rotate, mem_rotate]
+    apply mem_cyclicPermutations_self
 #align list.mem_cyclic_permutations_iff List.mem_cyclicPermutations_iff
 
 @[simp]
-theorem cyclicPermutations_eq_nil_iff {l : List α} : cyclicPermutations l = [[]] ↔ l = [] := by
-  refine' ⟨fun h => _, fun h => by simp [h]⟩
-  rw [eq_comm, ← isRotated_nil_iff', ← mem_cyclicPermutations_iff, h, mem_singleton]
+theorem cyclicPermutations_eq_nil_iff {l : List α} : cyclicPermutations l = [[]] ↔ l = [] :=
+  cyclicPermutations_injective.eq_iff' rfl
 #align list.cyclic_permutations_eq_nil_iff List.cyclicPermutations_eq_nil_iff
 
 @[simp]
 theorem cyclicPermutations_eq_singleton_iff {l : List α} {x : α} :
-    cyclicPermutations l = [[x]] ↔ l = [x] := by
-  refine' ⟨fun h => _, fun h => by simp [cyclicPermutations, h, dropLast_eq_take]⟩
-  rw [eq_comm, ← isRotated_singleton_iff', ← mem_cyclicPermutations_iff, h, mem_singleton]
+    cyclicPermutations l = [[x]] ↔ l = [x] :=
+  cyclicPermutations_injective.eq_iff' rfl
 #align list.cyclic_permutations_eq_singleton_iff List.cyclicPermutations_eq_singleton_iff
 
-set_option linter.deprecated false in
 /-- If a `l : List α` is `Nodup l`, then all of its cyclic permutants are distinct. -/
-theorem Nodup.cyclicPermutations {l : List α} (hn : Nodup l) : Nodup (cyclicPermutations l) := by
-  cases' l with x l
-  · simp
-  rw [nodup_iff_nthLe_inj]
-  intro i j hi hj h
-  simp only [length_cyclicPermutations_cons] at hi hj
-  rw [← mod_eq_of_lt hi, ← mod_eq_of_lt hj]
-  apply hn.rotate_congr
+protected theorem Nodup.cyclicPermutations {l : List α} (hn : Nodup l) :
+    Nodup (cyclicPermutations l) := by
+  rcases eq_or_ne l [] with rfl | hl
   · simp
-  · simpa using h
+  · rw [nodup_iff_injective_get]
+    rintro ⟨i, hi⟩ ⟨j, hj⟩ h
+    simp only [length_cyclicPermutations_of_ne_nil l hl] at hi hj
+    simpa [hn.rotate_congr_iff, mod_eq_of_lt, *] using h
 #align list.nodup.cyclic_permutations List.Nodup.cyclicPermutations
 
-set_option linter.deprecated false in
-@[simp]
-theorem cyclicPermutations_rotate (l : List α) (k : ℕ) :
-    (l.rotate k).cyclicPermutations = l.cyclicPermutations.rotate k := by
-  have : (l.rotate k).cyclicPermutations.length = length (l.cyclicPermutations.rotate k) := by
-    cases l
-    · simp
-    · rw [length_cyclicPermutations_of_ne_nil] <;> simp
-  refine' ext_nthLe this fun n hn hn' => _
-  rw [nthLe_rotate, nthLe_cyclicPermutations, rotate_rotate, ← rotate_mod, Nat.add_comm]
-  cases l <;> simp
-#align list.cyclic_permutations_rotate List.cyclicPermutations_rotate
-
-theorem IsRotated.cyclicPermutations {l l' : List α} (h : l ~r l') :
+protected theorem IsRotated.cyclicPermutations {l l' : List α} (h : l ~r l') :
     l.cyclicPermutations ~r l'.cyclicPermutations := by
   obtain ⟨k, rfl⟩ := h
   exact ⟨k, by simp⟩
 #align list.is_rotated.cyclic_permutations List.IsRotated.cyclicPermutations
 
-set_option linter.deprecated false in
 @[simp]
 theorem isRotated_cyclicPermutations_iff {l l' : List α} :
     l.cyclicPermutations ~r l'.cyclicPermutations ↔ l ~r l' := by
-  by_cases hl : l = []
-  · simp [hl, eq_comm]
-  have hl' : l.cyclicPermutations.length = l.length := length_cyclicPermutations_of_ne_nil _ hl
-  refine' ⟨fun h => _, IsRotated.cyclicPermutations⟩
-  obtain ⟨k, hk⟩ := h
-  refine' ⟨k % l.length, _⟩
-  have hk' : k % l.length < l.length := mod_lt _ (length_pos_of_ne_nil hl)
-  rw [← nthLe_cyclicPermutations _ _ (hk'.trans_le hl'.ge), ← nthLe_rotate' _ k]
-  simp [hk, hl', Nat.sub_add_cancel hk'.le]
+  simp only [IsRotated, ← cyclicPermutations_rotate, cyclicPermutations_inj]
 #align list.is_rotated_cyclic_permutations_iff List.isRotated_cyclicPermutations_iff
 
 section Decidable