Commit 2024-05-06 00:00 b8ee9e38

chore: deprecate redundant lemma List.find?_mem (#12677) Deprecates List.find?_mem, which duplicates List.mem_of_find?_eq_some from Std: https://github.com/leanprover/std4/blob/80cf5a1f2d8ed48753e8ff783bf0f7b6872bb007/Std/Data/List/Lemmas.lean#L1755-L1759 The lemmas only differ in the ordering of the implicit arguments l and a.

List.find?_mem.{u} {α : Type u} {p : α → Bool} {l : List α} {a : α} (H : List.find? p l = some a) : a ∈ l
List.mem_of_find?_eq_some.{u_1} : ∀ {α : Type u_1} {p : α → Bool} {a : α} {l : List α}, List.find? p l = some a → a ∈ l