From eea2d49078cffdda375c888acc6d246666fcd8fc Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 28 Jan 2025 23:23:24 +1100 Subject: [PATCH] chore: lower List/Array/Vector.mem_map simp priority (#6815) This PR lowers the simp priority of `List/Array/Vector.mem_map`, as downstream in Mathlib many lemmas currently need their priority raised to fire before this. --- src/Init/Data/Array/Lemmas.lean | 4 +++- src/Init/Data/List/Lemmas.lean | 4 +++- src/Init/Data/Vector/Lemmas.lean | 4 +++- 3 files changed, 9 insertions(+), 3 deletions(-) diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean index 0fece3ac67..f46bac67c9 100644 --- a/src/Init/Data/Array/Lemmas.lean +++ b/src/Init/Data/Array/Lemmas.lean @@ -1091,7 +1091,9 @@ theorem map_id'' {f : α → α} (h : ∀ x, f x = x) (l : Array α) : map f l = theorem map_singleton (f : α → β) (a : α) : map f #[a] = #[f a] := rfl -@[simp] theorem mem_map {f : α → β} {l : Array α} : b ∈ l.map f ↔ ∃ a, a ∈ l ∧ f a = b := by +-- We use a lower priority here as there are more specific lemmas in downstream libraries +-- which should be able to fire first. +@[simp 500] theorem mem_map {f : α → β} {l : Array α} : b ∈ l.map f ↔ ∃ a, a ∈ l ∧ f a = b := by simp only [mem_def, toList_map, List.mem_map] theorem exists_of_mem_map (h : b ∈ map f l) : ∃ a, a ∈ l ∧ f a = b := mem_map.1 h diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index a07da6dfcc..1f6f84d0ce 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -1046,7 +1046,9 @@ theorem map_id'' {f : α → α} (h : ∀ x, f x = x) (l : List α) : map f l = theorem map_singleton (f : α → β) (a : α) : map f [a] = [f a] := rfl -@[simp] theorem mem_map {f : α → β} : ∀ {l : List α}, b ∈ l.map f ↔ ∃ a, a ∈ l ∧ f a = b +-- We use a lower priority here as there are more specific lemmas in downstream libraries +-- which should be able to fire first. +@[simp 500] theorem mem_map {f : α → β} : ∀ {l : List α}, b ∈ l.map f ↔ ∃ a, a ∈ l ∧ f a = b | [] => by simp | _ :: l => by simp [mem_map (l := l), eq_comm (a := b)] diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean index 07fa54d7ae..53e2a0256a 100644 --- a/src/Init/Data/Vector/Lemmas.lean +++ b/src/Init/Data/Vector/Lemmas.lean @@ -1188,7 +1188,9 @@ theorem map_id'' {f : α → α} (h : ∀ x, f x = x) (l : Vector α n) : map f theorem map_singleton (f : α → β) (a : α) : map f #v[a] = #v[f a] := rfl -@[simp] theorem mem_map {f : α → β} {l : Vector α n} : b ∈ l.map f ↔ ∃ a, a ∈ l ∧ f a = b := by +-- We use a lower priority here as there are more specific lemmas in downstream libraries +-- which should be able to fire first. +@[simp 500] theorem mem_map {f : α → β} {l : Vector α n} : b ∈ l.map f ↔ ∃ a, a ∈ l ∧ f a = b := by cases l simp