Commit 2023-03-27 07:56 a0733e9e
View on Github →chore: bump Std (#3113)
Notably incorporates https://github.com/leanprover/std4/pull/98 and https://github.com/leanprover/std4/pull/109.
https://github.com/leanprover/std4/pull/98 moves a number of lemmas from Mathlib to Std, so the bump requires deleting them in Mathlib. I did check on each lemma whether its attributes were kept in the move (and gave attribute markings in Mathlib if they were not present in Std), but a reviewer may wish to re-check.
List.mem_map
changed statement from b ∈ l.map f ↔ ∃ a, a ∈ l ∧ b = f a
to b ∈ l.map f ↔ ∃ a, a ∈ l ∧ f a = b
. Similarly for List.exists_of_mem_map
. This was a deliberate change, so I have simply adjusted proofs (many become simpler, which supports the change). I also deleted List.mem_map'
, List.exists_of_mem_map'
, which were temporary versions in Mathlib while waiting for this change (replacing their uses with the unprimed versions).
Also, the lemma sublist_nil_iff_eq_nil
seems to have been renamed to sublist_nil
during the move, so I added an alias for the old name.
(another issue fixed during review by @digama0) List.Sublist.filter
had an argument change from explicit to implicit. This appears to have been an oversight (cc @JamesGallicchio). I have temporarily introduced List.Sublist.filter'
with the argument explicit, and replaced Mathlib uses of Sublist.filter
with Sublist.filter'
. Later we can fix the argument in Std, and then delete List.Sublist.filter'
.