Commit 2023-09-18 01:46 559a3fe0

View on Github →

chore: update to std4#100 (#6743) Std bump patch for https://github.com/leanprover/std4/pull/100

Estimated changes

Modified Mathlib/Data/Finset/Basic.lean

Modified Mathlib/Data/List/Basic.lean

deleted theorem List.drop_append_eq_append_drop

deleted theorem List.drop_append_of_le_length

Modified Mathlib/Data/List/Dedup.lean

added theorem List.dedup_idem

deleted theorem List.dedup_idempotent

Modified Mathlib/Data/List/Nodup.lean

Modified Mathlib/Data/List/Pairwise.lean

deleted theorem List.Pairwise.and

deleted theorem List.Pairwise.and_mem

deleted theorem List.Pairwise.drop

deleted theorem List.Pairwise.filter

deleted theorem List.Pairwise.filter_map

deleted theorem List.Pairwise.forall_of_forall_of_flip

deleted theorem List.Pairwise.iff

deleted theorem List.Pairwise.iff_of_mem

deleted theorem List.Pairwise.imp_mem

deleted theorem List.Pairwise.imp_of_mem

deleted theorem List.Pairwise.imp₂

deleted theorem List.Pairwise.map

deleted theorem List.Pairwise.of_cons

deleted theorem List.Pairwise.of_map

deleted theorem List.Pairwise.tail

deleted theorem List.forall_mem_pwFilter

deleted theorem List.pairwise_and_iff

deleted theorem List.pairwise_append_comm

deleted theorem List.pairwise_bind

deleted theorem List.pairwise_filter

deleted theorem List.pairwise_filterMap

deleted theorem List.pairwise_iff_get

deleted theorem List.pairwise_join

deleted theorem List.pairwise_middle

deleted theorem List.pairwise_of_forall

deleted theorem List.pairwise_of_reflexive_on_dupl_of_forall_ne

deleted theorem List.pairwise_pair

deleted theorem List.pairwise_pwFilter

deleted theorem List.pairwise_replicate

deleted theorem List.pairwise_singleton

deleted theorem List.pwFilter_cons_of_neg

deleted theorem List.pwFilter_cons_of_pos

deleted theorem List.pwFilter_eq_self

deleted theorem List.pwFilter_idempotent

deleted theorem List.pwFilter_map

deleted theorem List.pwFilter_nil

deleted theorem List.pwFilter_sublist

deleted theorem List.pwFilter_subset

deleted theorem List.rel_of_pairwise_cons

Modified Mathlib/Data/List/Perm.lean

Modified Mathlib/Data/Multiset/Dedup.lean

added theorem Multiset.dedup_idem

deleted theorem Multiset.dedup_idempotent

Modified lake-manifest.json