chore: deprecate redundant lemma List.get?_injective (#12630)

Deprecates `List.get?_injective`, which is a duplicate of `List.gen?_inj` in `Std`: https://github.com/leanprover/std4/blob/80cf5a1f2d8ed48753e8ff783bf0f7b6872bb007/Std/Data/List/Lemmas.lean#L773-L788

Mathlib/Data/List/Basic.lean

@@ -1243,21 +1243,8 @@ theorem mem_iff_nthLe {a} {l : List α} : a ∈ l ↔ ∃ n h, nthLe l n h = a :
 #align list.mem_iff_nth List.mem_iff_get?
 #align list.nth_zero List.get?_zero
 
--- Porting note: couldn't synthesize _ in cases h x _ rfl anymore, needed to be given explicitly
-theorem get?_injective {α : Type u} {xs : List α} {i j : ℕ} (h₀ : i < xs.length) (h₁ : Nodup xs)
-    (h₂ : xs.get? i = xs.get? j) : i = j := by
-  induction xs generalizing i j with
-  | nil => cases h₀
-  | cons x xs tail_ih =>
-    cases i <;> cases j
-    case zero.zero => rfl
-    case succ.succ =>
-      congr; cases h₁
-      apply tail_ih <;> solve_by_elim [lt_of_succ_lt_succ]
-    all_goals (dsimp at h₂; cases' h₁ with _ _ h h')
-    · cases (h x (mem_iff_get?.mpr ⟨_, h₂.symm⟩) rfl)
-    · cases (h x (mem_iff_get?.mpr ⟨_, h₂⟩) rfl)
-#align list.nth_injective List.get?_injective
+@[deprecated] alias get?_injective := get?_inj -- 2024-05-03
+#align list.nth_injective List.get?_inj
 
 #align list.nth_map List.get?_map
 

Mathlib/Testing/SlimCheck/Functions.lean

@@ -391,7 +391,7 @@ theorem applyId_injective [DecidableEq α] {xs ys : List α} (h₀ : List.Nodup
     have h₂ := h₁.length_eq
     rw [List.applyId_zip_eq h₀ h₂ _ _ _ hx] at h
     rw [← hx, ← hy]; congr
-    apply List.get?_injective _ (h₁.nodup_iff.1 h₀)
+    apply List.get?_inj _ (h₁.nodup_iff.1 h₀)
     · symm; rw [h]
       rw [← List.applyId_zip_eq] <;> assumption
     · rw [← h₁.length_eq]