Commit 2025-08-03 23:41 2b34ec4c

View on Github →

feat: start adding @[grind] annotations for Finset (#27818) Add @[grind =] for all the mem_X theorems for operations X on Finset, and golf some proofs.

Estimated changes

modified theorem Finset.disjUnion_eq_union
modified theorem Finset.erase_cons
modified theorem Finset.erase_insert
modified theorem Finset.erase_inter
modified theorem Finset.erase_inter_comm
modified theorem Finset.erase_sdiff_comm
modified theorem Finset.erase_singleton
modified theorem Finset.erase_ssubset
modified theorem Finset.filter_and
modified theorem Finset.filter_inter
modified theorem Finset.filter_not
modified theorem Finset.filter_or
modified theorem Finset.filter_singleton
modified theorem Finset.filter_union
modified theorem Finset.filter_union_right
modified theorem Finset.insert_erase
modified theorem Finset.inter_erase
modified theorem Finset.inter_filter
modified theorem Finset.range_filter_eq
modified theorem Finset.sdiff_eq_filter
modified theorem Finset.subset_insert_iff
modified theorem Finset.coe_empty
modified theorem Finset.coe_eq_empty
modified theorem Finset.forall_mem_empty_iff
modified theorem Finset.not_ssubset_empty
modified theorem Finset.coe_erase
modified theorem Finset.subset_erase
modified theorem Finset.Finset.filter_filter
modified theorem Finset.coe_map
modified theorem Finset.coe_map_subset_range
modified theorem Finset.image_singleton
modified theorem Finset.coe_eq_singleton
modified theorem Finset.coe_insert
modified theorem Finset.coe_pair
modified theorem Finset.coe_singleton
modified theorem Finset.coe_subset_singleton
modified theorem Finset.insert_comm
modified theorem Finset.insert_idem
modified theorem Finset.insert_subset_iff
modified theorem Finset.insert_subset_insert
modified theorem Finset.singleton_subset_coe
modified theorem Finset.forall_mem_union
modified theorem Finset.inter_assoc
modified theorem Finset.inter_comm
modified theorem Finset.inter_left_comm
modified theorem Finset.inter_right_comm
modified theorem Finset.inter_subset_inter
modified theorem Finset.subset_inter
modified theorem Finset.mem_powersetCard
modified theorem Finset.diag_insert
modified theorem Finset.diag_inter
modified theorem Finset.diag_singleton
modified theorem Finset.diag_union
modified theorem Finset.inter_product
modified theorem Finset.product_inter
modified theorem Finset.product_sdiff_diag
modified theorem Finset.product_union
modified theorem Finset.union_product
modified theorem Finset.cons_sdiff_cons
modified theorem Finset.insert_sdiff_cancel
modified theorem Finset.insert_sdiff_of_mem
modified theorem Finset.inter_sdiff_self
modified theorem Finset.biUnion_mono
modified theorem Finset.biUnion_singleton
modified theorem Finset.biUnion_subset
modified theorem Finset.mem_biUnion
modified theorem Finset.mem_disjiUnion
modified theorem Finset.singleton_biUnion