Commit 2024-11-19 17:43 22fb3a45

View on Github →

chore: make Finset.subset_union_left simp (#19249) ... and around. The corresponding Set lemmas already are simp From GrowthInGroups

Estimated changes

Modified Mathlib/Data/Finset/Lattice/Basic.lean

modified theorem Finset.inter_subset_left

modified theorem Finset.inter_subset_right

modified theorem Finset.subset_union_left

modified theorem Finset.subset_union_right