Commit 2025-10-14 03:26 7893dd08

View on Github →

feat(Data/List/Sigma): grind annotations, some missing API (#30313)

grind annotations for List.keys, List.NodupKeys, and List.lookup, with some shortening of proofs
upstream keys_append, sublist_dlookup, and nodupKeys_middle from https://github.com/leanprover/cslib/pull/68

Estimated changes

Modified Mathlib/Data/List/Sigma.lean

added theorem List.NodupKeys.map₁

added theorem List.NodupKeys.map₂

modified theorem List.dlookup_isSome

added theorem List.keys_append

modified theorem List.map_dlookup_eq_find

added theorem List.map₂_keys

modified theorem List.ne_key

added theorem List.nodupKeys_middle

modified theorem List.notMem_keys

modified theorem List.of_mem_dlookup

added theorem List.sublist_dlookup