Commit 2024-03-22 07:07 dddd92df

View on Github →

chore: bump Std (#11576)

Estimated changes

Modified Mathlib/Data/List/Basic.lean

deleted theorem List.dropLast_append_of_ne_nil

deleted theorem List.dropLast_cons_of_ne_nil

deleted theorem List.dropLast_eq_take

deleted theorem List.dropLast_take

deleted theorem List.drop_append

deleted theorem List.drop_drop

deleted theorem List.drop_eq_nil_iff_le

deleted theorem List.drop_length_cons

deleted theorem List.drop_sizeOf_le

deleted theorem List.drop_take

deleted theorem List.get?_drop

deleted theorem List.get?_take

deleted theorem List.get_drop'

deleted theorem List.get_drop

deleted theorem List.get_take'

deleted theorem List.get_take

deleted theorem List.map_drop

deleted theorem List.map_take

deleted theorem List.modifyNthTail_eq_take_drop

deleted theorem List.modifyNth_eq_take_cons_drop

deleted theorem List.modifyNth_eq_take_drop

deleted theorem List.nth_take_of_succ

deleted theorem List.reverse_take

deleted theorem List.set_eq_nil

deleted theorem List.set_eq_take_cons_drop

deleted theorem List.tail_drop

deleted theorem List.take_add

deleted theorem List.take_all_of_le

deleted theorem List.take_append

deleted theorem List.take_append_eq_append_take

deleted theorem List.take_append_of_le_length

deleted theorem List.take_eq_nil_iff

deleted theorem List.take_eq_take

deleted theorem List.take_left'

deleted theorem List.take_left

deleted theorem List.take_replicate

deleted theorem List.take_succ

deleted theorem List.take_take

Modified lake-manifest.json

Modified test/congr.lean