Commit 2025-09-22 12:37 11bbf0d6

View on Github →

feat: grind annotations for Finset.sdiff (#29427) Note that grind often will not instantiate equational lemmas that are not fully applied, so we need to split some theorems into versions for simp and versions for grind. Moves:

  • sup_eq_union -> sup_eq_union'
  • inf_eq_inter -> inf_eq_inter'

Estimated changes

added theorem Finset.nontrivial_def
added theorem Finset.inf_eq_inter'
modified theorem Finset.inf_eq_inter
added theorem Finset.sup_eq_union'
modified theorem Finset.sup_eq_union
modified theorem Finset.sdiff_ssubset
modified theorem Finset.sdiff_subset_sdiff