From 1e0407b45cb2322dbd2b41abf386130b7691b793 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Mon, 18 Nov 2024 21:30:22 +0000 Subject: [PATCH] chore: fix defeq abuse between `List.get_mem` and `List.getElem_mem` This will reduce the fallout of leanprover/lean4#6095. --- Mathlib/Data/List/EditDistance/Bounds.lean | 2 +- Mathlib/Data/List/MinMax.lean | 2 +- Mathlib/Data/List/Nodup.lean | 2 +- Mathlib/Data/List/NodupEquivFin.lean | 2 +- Mathlib/Data/List/Permutation.lean | 4 ++-- 5 files changed, 6 insertions(+), 6 deletions(-) diff --git a/Mathlib/Data/List/EditDistance/Bounds.lean b/Mathlib/Data/List/EditDistance/Bounds.lean index 7a20e9e681c9a..df199af6ccfa1 100644 --- a/Mathlib/Data/List/EditDistance/Bounds.lean +++ b/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 _ _ _) diff --git a/Mathlib/Data/List/MinMax.lean b/Mathlib/Data/List/MinMax.lean index 6b18d25cf4107..0237438fa2eda 100644 --- a/Mathlib/Data/List/MinMax.lean +++ b/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] := diff --git a/Mathlib/Data/List/Nodup.lean b/Mathlib/Data/List/Nodup.lean index f6b34a9b86b77..1368f8f1890a3 100644 --- a/Mathlib/Data/List/Nodup.lean +++ b/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) diff --git a/Mathlib/Data/List/NodupEquivFin.lean b/Mathlib/Data/List/NodupEquivFin.lean index 0dcf11280caae..65a48a57e4574 100644 --- a/Mathlib/Data/List/NodupEquivFin.lean +++ b/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 diff --git a/Mathlib/Data/List/Permutation.lean b/Mathlib/Data/List/Permutation.lean index d90a8bbe313e9..2ce7b4ce525f3 100644 --- a/Mathlib/Data/List/Permutation.lean +++ b/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