Commit 2025-02-16 08:40 6e9a2f62

View on Github →

feat(List/InsertIdx): add lemmas (#21448) Also drop a duplicate Trans instance for List.Perm.

Estimated changes

Modified Mathlib/Data/List/InsertIdx.lean

added theorem List.eq_or_mem_of_mem_insertIdx

added theorem List.eraseIdx_map

added theorem List.eraseIdx_pmap

added theorem List.insertIdx_eraseIdx

added theorem List.insertIdx_eraseIdx_getElem

added theorem List.insertIdx_pmap

added theorem List.insertIdx_subset_cons

added theorem List.map_insertIdx

added theorem List.sublist_insertIdx

added theorem List.subset_insertIdx

Modified Mathlib/Data/List/Perm/Basic.lean

added theorem List.getElem_cons_eraseIdx_perm

added theorem List.perm_eraseIdx_of_getElem?_eq

added theorem List.perm_insertIdx_iff

added theorem List.perm_insertIdx_iff_of_le

added theorem List.set_perm_cons_eraseIdx