Commit 2025-11-24 11:02 19bdc16c

View on Github →

chore(Data/List): reduce imports (#31643)

  • Use Nat-specific lemmas instead of generic ones to avoid extra imports.
  • Drop an unneeded assumption in List.idxOf_inj.
  • Use [BEq α] [LawfulBEq α] instead of [DecidableEq α] to sync with core.

Estimated changes

modified theorem List.erase_getElem
modified theorem List.getElem?_idxOf
modified theorem List.getElem_idxOf
modified theorem List.idxOf_cons_ne
modified theorem List.idxOf_get
modified theorem List.idxOf_inj
modified theorem List.map_diff
modified theorem List.map_erase
modified theorem List.map_foldl_erase
modified theorem List.count_map_of_injective
modified theorem List.inter_reverse
modified theorem List.Nodup.diff
modified theorem List.Nodup.erase_get
modified theorem List.Nodup.erase_getElem
modified theorem List.Nodup.inter
modified theorem List.Nodup.mem_diff_iff
modified theorem List.Nodup.union
modified theorem List.count_eq_one_of_mem
modified theorem List.getElem_bijective_iff
modified theorem List.get_bijective_iff
modified theorem List.get_idxOf
modified theorem List.idxOf_getElem
modified theorem List.nodup_iff_count_eq_one
modified theorem List.nodup_iff_count_le_one