Commit 2025-09-24 12:05 365203ec

View on Github →

feat: grind golf in Mathlib.Data.List (#29492) Much of this comes from locations identified by the new linter.tacticAnalysis.terminalToGrind, and then cleaning up in flagged files.

Estimated changes

modified theorem List.eq_cons_of_length_one
modified theorem List.idxOf_append_of_mem
modified theorem List.bagInter_sublist_left
added theorem List.cons_bagInteger
modified theorem List.count_bagInter
added theorem List.inter_cons
modified theorem List.mem_bagInter
added theorem List.lookmap_cons