Commit 2024-03-24 06:28 9682f6b2

View on Github →

chore: make List.mem_split an alias of List.append_of_mem (#11060) List.mem_split duplicates List.append_of_mem from Std: https://github.com/leanprover/std4/blob/a756b7d643ae5dcd7bf314e99f8e493e5d81b9ed/Std/Data/List/Lemmas.lean#L94-L96 This PR makes it an alias.

Estimated changes

Modified Archive/MiuLanguage/DecisionSuf.lean

Modified Mathlib/Data/List/Basic.lean

deleted theorem List.mem_split

Modified Mathlib/Data/List/BigOperators/Lemmas.lean

Modified Mathlib/Data/List/Perm.lean

Modified Mathlib/Data/List/Sort.lean

Modified Mathlib/Data/Multiset/Basic.lean