Commit 2025-12-08 16:53 7c4f93d3

View on Github →

chore(Data/Finset/Basic): use more dot notation in Data.Finset.Basic (#31838)

Estimated changes

Modified Mathlib/Data/Finset/Basic.lean

modified theorem Finset.attach_empty

modified theorem Finset.choose_mem

modified theorem Finset.choose_property

modified theorem Finset.choose_spec

modified theorem Finset.erase_eq_iff_eq_insert

modified theorem Finset.erase_injOn'

modified theorem Finset.erase_insert

modified theorem Finset.erase_insert_subset

modified theorem Finset.filter_erase

modified theorem Finset.filter_inter

modified theorem Finset.insert_erase

modified theorem Finset.insert_erase_subset

modified theorem Finset.inter_filter

modified theorem Finset.sdiff_eq_filter

modified theorem Finset.sdiff_singleton_eq_erase

modified theorem Finset.subset_insert_iff

modified theorem Multiset.toFinset_add

modified theorem Multiset.toFinset_inter