Commit 2024-06-06 10:53 711e6be2

View on Github →

chore: Make more arguments to inter_subset_left implicit (#13445) There are a few commonplace lemmas whose explicit arguments are (almost) always inferred in practice. This means that one needs to put brackets around and feeds them underscores very often. This is annoying. Remove the explicit arguments to the six most commonplace (series of) lemmas that are like that:

  • inter_subset_left
  • inter_subset_right
  • subset_union_left
  • subset_union_right
  • Set.diff_subset/Finset.sdiff_subset
  • Function.Injective.InjOn

Estimated changes

modified theorem Finset.inter_subset_left
modified theorem Finset.inter_subset_right
modified theorem Finset.sdiff_subset
modified theorem Finset.subset_union_left
modified theorem Finset.subset_union_right
modified theorem Finset.image_mul_right
modified theorem Finset.preimage_inv
modified theorem Finset.preimage_map
modified theorem List.inter_subset_left
modified theorem List.inter_subset_right
modified theorem Set.diff_subset
modified theorem Set.inter_subset_left
modified theorem Set.inter_subset_right
modified theorem Set.subset_union_left
modified theorem Set.subset_union_right
modified theorem Equiv.bijOn_image
modified theorem Set.injOn_id
modified theorem Set.injOn_of_injective
modified theorem LowerSet.erase_le
modified theorem LowerSet.sdiff_le_left
modified theorem UpperSet.le_erase
modified theorem UpperSet.le_sdiff_left