Commit 2026-10-31 04:12 c1cc962a

View on Github →

feat: use max/min for union/inter in Set, Finset, ZFSet, Class (#42316) This lets us write ∪/∩ for sets while the underlying constant is max/min. This is a follow-up to #32983, which made the same change for ⊆, ⊂, ⊇ and ⊃. The implementation for ∪/∩ is analogous. The first commit contains the implementation change, and all other commits are just adaptations. Note that there are now two different special delaborators for max/min, because we already had the delaborator that chooses between max/min and ⊔/⊓. It is important that the one for ∪/∩ is tried first. There is no priority mechanism for delaborators: they are always executed newest to oldest. So, this PR adds a (redundant) import to ensure that this order is respected.

  • I modified the delaborator for ⊔/⊓ so that it doesn't fire if LinearOrder isn't imported. Due to the extra redundant import, that is now a more common situation and I think in that situation it's better to print max a b instead of a ⊔ b.
  • It is now not anymore possible to write simp [(· ∪ ·)] due to elaboration issues. The same also already applied to simp [(· ⊆ ·)].
  • Many simp calls had to be fixed because the simp set for max/min contains more lemmas than what we had for union/inter. For example, compl_inf and inf_of_le_left/inf_of_le_right now also apply to intersections.
  • In particular inf_of_le_left/inf_of_le_right are quite slow simp lemmas, which means that this PR gives a bit of slowdown.
  • A grind call had to be fixed because it timed out. Originally, that grind call was already doing too much stuff, but it didn't quite reach its limits.
  • Many @[simp] and some @[gcongr] tags could be removed because they are now subsumed by more general tags.
  • I removed @[mfld_simp] from inter_subset_left, as it seemed a bit weird to have it there and not on its dual or its mirror lemma.

Estimated changes

modified theorem SimpleGraph.lineGraph_bot
modified theorem Finset.disjoint_union_left
modified theorem Finset.disjoint_union_right
modified theorem Finset.inter_univ
modified theorem Finset.univ_inter
modified theorem Finset.inf_eq_inter'
modified theorem Finset.inter_assoc
modified theorem Finset.inter_comm
modified theorem Finset.inter_eq_left
modified theorem Finset.inter_eq_right
modified theorem Finset.inter_left_comm
modified theorem Finset.inter_right_comm
modified theorem Finset.inter_self
modified theorem Finset.inter_subset_inter
modified theorem Finset.inter_subset_left
modified theorem Finset.inter_subset_right
modified theorem Finset.inter_union_self
modified theorem Finset.left_eq_union
modified theorem Finset.right_eq_union
modified theorem Finset.subset_inter
modified theorem Finset.subset_union_left
modified theorem Finset.subset_union_right
modified theorem Finset.sup_eq_union'
modified theorem Finset.union_eq_left
modified theorem Finset.union_eq_right
modified theorem Finset.union_left_comm
modified theorem Finset.union_right_comm
modified theorem Finset.union_self
modified theorem Finset.union_subset_union
modified theorem Finset.empty_inter
modified theorem Finset.empty_union
modified theorem Finset.inter_empty
modified theorem Finset.union_empty
modified theorem Finset.inter_sdiff_self
modified theorem Finset.sdiff_subset_sdiff
modified theorem Set.empty_inter
modified theorem Set.inter_assoc
modified theorem Set.inter_comm
modified theorem Set.inter_empty
modified theorem Set.inter_eq_left
modified theorem Set.inter_eq_right
modified theorem Set.inter_left_comm
modified theorem Set.inter_right_comm
modified theorem Set.inter_self
modified theorem Set.inter_subset_inter
modified theorem Set.inter_subset_inter_left
modified theorem Set.inter_subset_left
modified theorem Set.inter_subset_right
modified theorem Set.left_eq_inter
modified theorem Set.right_eq_inter
modified theorem Set.subset_inter
modified theorem Set.subset_inter_iff
modified theorem Set.subset_union_left
modified theorem Set.subset_union_right
modified theorem Set.union_inter_cancel_left
modified theorem Set.union_subset
modified theorem Set.union_subset_iff
modified theorem Set.union_subset_union
modified theorem Set.union_subset_union_left
modified theorem Set.inter_singleton_of_mem
modified theorem Set.singleton_inter_of_mem
modified theorem Equiv.Perm.support_mul_le
modified theorem Equiv.Perm.support_prod_le
modified theorem Set.compl_union_self
modified theorem Set.sdiff_union_inter
added structure Top'
deleted structure Top