chore: fix defeq abuse between List.get_mem and List.getElem_mem (#…

…19224)

In all these places the goal state is about `getElem` not `List.get`.

This will reduce the fallout of leanprover/lean4#6095.

Mathlib/Data/List/EditDistance/Bounds.lean

@@ -79,7 +79,7 @@ theorem le_suffixLevenshtein_append_minimum (xs : List α) (ys₁ ys₂) :
 theorem suffixLevenshtein_minimum_le_levenshtein_append (xs ys₁ ys₂) :
     (suffixLevenshtein C xs ys₂).1.minimum ≤ levenshtein C xs (ys₁ ++ ys₂) := by
   cases ys₁ with
-  | nil => exact List.minimum_le_of_mem' (List.get_mem _ _ _)
+  | nil => exact List.minimum_le_of_mem' (List.getElem_mem _)
   | cons y ys₁ =>
       exact (le_suffixLevenshtein_append_minimum _ _ _).trans
         (suffixLevenshtein_minimum_le_levenshtein_cons _ _ _)

Mathlib/Data/List/MinMax.lean

@@ -427,7 +427,7 @@ theorem minimum_of_length_pos_le_of_mem (h : a ∈ l) (w : 0 < l.length) :
 theorem getElem_le_maximum_of_length_pos {i : ℕ} (w : i < l.length) (h := (Nat.zero_lt_of_lt w)) :
     l[i] ≤ l.maximum_of_length_pos h := by
   apply le_maximum_of_length_pos_of_mem
-  exact get_mem l i w
+  exact getElem_mem _
 
 theorem minimum_of_length_pos_le_getElem {i : ℕ} (w : i < l.length) (h := (Nat.zero_lt_of_lt w)) :
     l.minimum_of_length_pos h ≤ l[i] :=

Mathlib/Data/List/Nodup.lean

@@ -122,7 +122,7 @@ theorem not_nodup_of_get_eq_of_ne (xs : List α) (n m : Fin xs.length)
 
 theorem indexOf_getElem [DecidableEq α] {l : List α} (H : Nodup l) (i : Nat) (h : i < l.length) :
     indexOf l[i] l = i :=
-  suffices (⟨indexOf l[i] l, indexOf_lt_length.2 (get_mem _ _ _)⟩ : Fin l.length) = ⟨i, h⟩
+  suffices (⟨indexOf l[i] l, indexOf_lt_length.2 (getElem_mem _)⟩ : Fin l.length) = ⟨i, h⟩
     from Fin.val_eq_of_eq this
   nodup_iff_injective_get.1 H (by simp)
 

Mathlib/Data/List/NodupEquivFin.lean

@@ -127,7 +127,7 @@ theorem sublist_of_orderEmbedding_get?_eq {l l' : List α} (f : ℕ ↪o ℕ)
   rw [← List.take_append_drop (f 0 + 1) l', ← List.singleton_append]
   apply List.Sublist.append _ (IH _ this)
   rw [List.singleton_sublist, ← h, l'.getElem_take' _ (Nat.lt_succ_self _)]
-  apply List.get_mem
+  exact List.getElem_mem _
 
 /-- A `l : List α` is `Sublist l l'` for `l' : List α` iff
 there is `f`, an order-preserving embedding of `ℕ` into `ℕ` such that

Mathlib/Data/List/Permutation.lean

@@ -501,13 +501,13 @@ theorem nodup_permutations (s : List α) (hs : Nodup s) : Nodup s.permutations :
       rcases lt_trichotomy n m with (ht | ht | ht)
       · suffices x ∈ bs by exact h x (hb.subset this) rfl
         rw [← hx', getElem_insertIdx_of_lt _ _ _ _ ht (ht.trans_le hm)]
-        exact get_mem _ _ _
+        exact getElem_mem _
       · simp only [ht] at hm' hn'
         rw [← hm'] at hn'
         exact H (insertIdx_injective _ _ hn')
       · suffices x ∈ as by exact h x (ha.subset this) rfl
         rw [← hx, getElem_insertIdx_of_lt _ _ _ _ ht (ht.trans_le hn)]
-        exact get_mem _ _ _
+        exact getElem_mem _
 
 lemma permutations_take_two (x y : α) (s : List α) :
     (x :: y :: s).permutations.take 2 = [x :: y :: s, y :: x :: s] := by