Commit 2025-08-01 01:40 ca2c27d7

View on Github →

feat: start using grind in Set API (#27670) This PR starts adding grind annotations to theorems about Set, and simplifying proofs. Neither effort is exhaustive in any of the files I touch here; it's just a start.

Estimated changes

modified theorem Set.EqOn.image_eq
modified theorem Set.EqOn.image_eq_self
modified theorem Set.EqOn.inter_preimage_eq
modified theorem Set.image_comp_eq
modified theorem Set.image_congr'
modified theorem Set.image_empty
modified theorem Set.image_mono
modified theorem Set.image_pair
modified theorem Set.image_preimage_eq_iff
modified theorem Set.image_singleton
modified theorem Set.image_subset
modified theorem Set.image_union
modified theorem Set.image_univ
modified theorem Set.range_comp_subset_range
modified theorem Set.insert_comm
modified theorem Set.insert_eq_of_mem
modified theorem Set.insert_eq_self
modified theorem Set.insert_idem
modified theorem Set.insert_inter_distrib
modified theorem Set.insert_inter_of_mem
modified theorem Set.insert_inter_of_notMem
modified theorem Set.insert_ne_self
modified theorem Set.insert_subset
modified theorem Set.insert_subset_iff
modified theorem Set.insert_subset_insert
modified theorem Set.insert_union
modified theorem Set.insert_union_distrib
modified theorem Set.inter_insert_of_mem
modified theorem Set.inter_insert_of_notMem
modified theorem Set.ne_insert_of_notMem
modified theorem Set.pair_subset_iff
modified theorem Set.powerset_singleton
modified theorem Set.ssubset_iff_insert
modified theorem Set.ssubset_insert
modified theorem Set.subset_pair_iff
modified theorem Set.subset_singleton_iff_eq
modified theorem Set.union_insert
modified theorem Set.mem_compl_iff
modified theorem Set.mem_diagonal_iff
modified theorem Set.mem_diff
modified theorem Set.mem_image2
modified theorem Set.mem_pi
modified theorem Set.mem_range
modified theorem Set.mem_setOf_eq
modified theorem Set.mem_univ
modified theorem Set.empty_pi
modified theorem Set.mk_preimage_prod_left
modified theorem Set.mk_preimage_prod_right
modified theorem Set.pi_congr
modified theorem Set.pi_eq_empty
modified theorem Set.pi_inter_compl
modified theorem Set.pi_inter_distrib
modified theorem Set.preimage_swap_prod
modified theorem Set.prod_diff_prod
modified theorem Set.singleton_pi
modified theorem Set.empty_sigma
modified theorem Set.insert_sigma
modified theorem Set.mem_sigma_iff
modified theorem Set.mk_preimage_sigma
modified theorem Set.range_sigmaMk
modified theorem Set.sigma_empty
modified theorem Set.sigma_union
modified theorem Set.sigma_univ
modified theorem Set.singleton_sigma
modified theorem Set.union_sigma
modified theorem Set.univ_sigma_univ