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'.

Estimated changes

deleted theorem List.Sublist.diff_right
deleted theorem List.Sublist.eq_of_length
deleted theorem List.Sublist.erase
deleted theorem List.Sublist.filter
deleted theorem List.Sublist.filterMap
deleted theorem List.cons_diff
deleted theorem List.cons_diff_of_mem
deleted theorem List.cons_diff_of_not_mem
deleted theorem List.diff_append
deleted theorem List.diff_cons
deleted theorem List.diff_cons_right
deleted theorem List.diff_eq_foldl
deleted theorem List.diff_erase
deleted theorem List.diff_nil
deleted theorem List.diff_sublist
deleted theorem List.diff_subset
deleted theorem List.eq_replicate
deleted theorem List.filterMap_append
deleted theorem List.filterMap_cons
deleted theorem List.filterMap_cons_none
deleted theorem List.filterMap_cons_some
deleted theorem List.filterMap_eq_filter
deleted theorem List.filterMap_eq_map
deleted theorem List.filterMap_filter
deleted theorem List.filterMap_filterMap
deleted theorem List.filterMap_join
deleted theorem List.filterMap_map
deleted theorem List.filterMap_nil
deleted theorem List.filterMap_some
deleted theorem List.filter_append
deleted theorem List.filter_congr'
deleted theorem List.filter_cons_of_neg
deleted theorem List.filter_cons_of_pos
deleted theorem List.filter_eq_nil
deleted theorem List.filter_eq_self
deleted theorem List.filter_filter
deleted theorem List.filter_filterMap
deleted theorem List.filter_nil
deleted theorem List.filter_sublist
deleted theorem List.find?_cons_of_neg
deleted theorem List.find?_cons_of_pos
deleted theorem List.find?_eq_none
deleted theorem List.find?_some
deleted theorem List.length_filterMap_le
deleted theorem List.length_filter_le
deleted theorem List.map_filter
deleted theorem List.map_filterMap
deleted theorem List.map_filterMap_of_inv
deleted theorem List.mem_diff_of_mem
deleted theorem List.mem_filterMap
deleted theorem List.mem_map'
deleted theorem List.mem_of_ne_of_mem
deleted theorem List.ne_of_not_mem_cons
deleted theorem List.nil_diff
deleted theorem List.not_mem_append
deleted theorem List.singleton_sublist